# Zulip Chat Archive

## Stream: maths

### Topic: group of fractions

#### Kevin Buzzard (Jul 17 2019 at 18:11):

Do we have the "group of fractions" associated to a cancellative monoid? I only need the abelian case.

#### Patrick Massot (Jul 17 2019 at 18:12):

Look at what Lean is doing to us...

#### Kevin Buzzard (Jul 17 2019 at 18:12):

It's ten times worse Patrick. I need the group-with-zero attached to a Massot monoid.

#### Kevin Buzzard (Jul 17 2019 at 18:13):

I was thinking that if we had group of fractions then I could at least look at how the professionals did it before I started.

#### Kevin Buzzard (Jul 17 2019 at 18:15):

I had to make a call between using "monoid with zero such that if you remove 0 you get a group" and Massot monoid ("monoid with zero such that if you remove zero you get a cancellative monoid"), I chose the latter (because it's the right generality) and now I want to extend a faithful valuation on an integral domain to its field of fractions I need to invert some non-invertible non-zero elments of the Massot monoid.

#### Patrick Massot (Jul 17 2019 at 18:15):

Meanwhile I'm writing hundreds of lines about filter bases

#### Kevin Buzzard (Jul 17 2019 at 18:16):

Who would have guessed two years ago?

#### Johan Commelin (Jul 17 2019 at 18:37):

I guess the first half of `ring_theory/localization.lean`

can be rewritten to not use `+`

and `-`

.

#### Kevin Buzzard (Jul 17 2019 at 18:37):

Actually, I guess that I can do group of fractions and then use it. It's at times like this which I am allowed to use `with_zero`

; instead of making the object and then using it, I make the object, define an instance of `Massot_monoid`

on it and then I'm done. So this will end up being a bunch more `for_mathlib`

files if it's not there already. First I need group of fractions of a cancellative monoid (just with `*`

as group law but I guess `to_additive`

can be used), then a totally ordered version, and then a version with zero.

#### Johan Commelin (Jul 17 2019 at 18:37):

If we also immediately introduce a characteristic predicate, we have two wins.

#### Patrick Massot (Jul 17 2019 at 18:46):

I spent way too much time constructing the product of two filters basis. It's clear indication I should leave my office and go hunting for food.

#### Kevin Buzzard (Jul 17 2019 at 18:51):

ha, the joys of no family. When you've finished foraging you can go back to your office :D (although someone has to feed the cat, right?)

Last updated: May 09 2021 at 11:09 UTC