Stream: new members
Kevin Buzzard (Jan 29 2019 at 07:30):
Localisation is there but I don't know if anyone specifically put the field of fractions there. What does one want? Just the statement that if you localise an integral domain at 0 then you get a field?
GCD of an ideal -- does that always exist? I'd not heard of it before.
Aditya Agarwal (Jan 29 2019 at 08:30):
It doesn't always have to exist. But that was the definition of the GCD we used in Algebra 1, and what is used in the proof of the Gauss Lemma I'm trying to write in lean.
Wikipedia also seems to use that definition. https://en.wikipedia.org/wiki/GCD_domain
Aditya Agarwal (Jan 29 2019 at 08:32):
I would prefer working with the GCD being defined in terms of ideals because it lets me ignore multiplication by units. However, working with the ordinary defintion doesn't create any insurmountable issue.
Kevin Buzzard (Jan 29 2019 at 08:53):
That link is only about GCD's of finite sets of elements, not arbitrary ideals. I vaguely remember some talk here about GCD domains a few months back.
Aditya Agarwal (Jan 29 2019 at 09:35):
Whoops, yeah. I totally forgot the infintie case exists.
Aditya Agarwal (Jan 29 2019 at 09:37):
There is https://github.com/leanprover/mathlib/blob/master/src/algebra/gcd_domain.lean , but it seems to use the normal definition of GCD.
Kevin Buzzard (Jan 29 2019 at 09:48):
My memory was that the CS people at some stage wanted to choose a generator of every ideal or something. They think about stuff in really weird asymmetric ways.
Kevin Buzzard (Jan 29 2019 at 09:50):
There was some discussion about whether it was possible to choose a generator of every principal ideal in a way compatible with multiplication, and it works great for some rings (eg choose the monic generator for poly rings and the non negative generator for the integers) but it can't be done in general
Last updated: May 13 2021 at 21:12 UTC