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: Dec 20 2023 at 11:08 UTC