GCD for ideals, fractional field

Stream: new members

[Kevin Buzzard]

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]

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]

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]

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]

Whoops, yeah. I totally forgot the infintie case exists.

[Aditya Agarwal]

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]

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]

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