## Stream: maths

### Topic: GCD

#### Patrick Massot (Sep 01 2018 at 08:38):

@Johannes Hölzl could you summarize the current state of GCD stuff? How many versions do we now have? What are the logical dependencies and future plans?

#### Johannes Hölzl (Sep 01 2018 at 09:26):

We have nat.gcd, int.gcd and gcd_domain.gcd (similar for lcm). The future plan is to add a gcd_domain for polynomials

#### Johannes Hölzl (Sep 01 2018 at 09:31):

There is some more stuff coming from Mason–Stothers. Especially UFDs, formal derivatives, etc

#### Patrick Massot (Sep 01 2018 at 09:33):

Are those three things completely independant?

#### Mario Carneiro (Sep 01 2018 at 14:43):

Now that gcd_domain and normalization_domain are merged, I would like to see a proof that every integral domain has a normalization. @Kevin Buzzard You mentioned something about prime ideals when I asked about this, can you elaborate?

Here's my analysis: The units of $R$ act freely on $R-\{0\}$ by left multiplication. If we quotient by the orbit relation, we obtain a monoid $M$. The goal is to prove the existence of a monoid homomorphism from $M$ to the unit group of $R$. Is there an abstract nonsense reason this should be true?

#### Mario Carneiro (Sep 01 2018 at 15:18):

Never mind, that proof doesn't make any sense. We want to define a subset $N\subseteq R-\{0\}$ of normalized elements which is a submonoid of $R$, and such that $N$ contains one element for every associate equivalence class.

#### Kevin Buzzard (Sep 01 2018 at 15:29):

What I said about prime ideals was just for Z[sqrt(2)]. My understanding is that a normalization domain boils down to a choice of your set $N$ above. My observation was that, for integral domains, one way of thinking about such a choice is to ask for a canonical generator for each principal ideal, because in an integral domain the ideals $(a)$ and $(b)$ are equal if and only if $a$ is a unit times $b$.

#### Kevin Buzzard (Sep 01 2018 at 15:31):

Now in a principal ideal domain, or more generally in a Dedekind domain, every non-zero ideal is uniquely a product of prime ideals. So I was noting that in a PID all you have to do is to make the choice for each prime ideal (i.e. each prime element) and then you can extend. In retrospect what I was saying about prime ideals can be simplified to the statement that in a UFD to make this $N$ choice it suffices to choose what is going on for the prime elements.

#### Mario Carneiro (Sep 01 2018 at 15:35):

Let's try Zorn's lemma. Call a subnormalization a submonoid $N'$ where no two elements are associate. Obviously the union of a chain of subnormalizations is a subnormalization, so it suffices to show that if $N$ is not a normalization, then there is a proper extension of it. If we pick any element $x\notin N$ and extend to the submonoid closure $N'$, we must show that $N'$ still has no associates. Each such element has the form $x^ny$ where $y\in N$, so we reduce to the case $y\sim x^n z$ where $y,z\in N$.

#### Mario Carneiro (Sep 01 2018 at 15:49):

Possible ways to refine this sketch include adding additional constraints on subnormalizations, and choosing $x$ more carefully. In a PID, then if $x' \notin R^*N$, it has a prime factorization and there must be some prime $p$ in the factorization which is not in $N$ (otherwise $x'\in R^*N$), and we can take $N'$ to be the submonoid generated by $N,p$. Unique factorization ensures that if $y\sim p^n z$ then $n=0$ and $y=z$.

#### Kenny Lau (Sep 01 2018 at 15:50):

Does normalization mean something different here? To me, the normalization of an integral domain A is the integral closure of A in its fraction field K

#### Mario Carneiro (Sep 01 2018 at 15:50):

yes, that's a different sense

#### Johannes Hölzl (Sep 01 2018 at 16:18):

11:33 Are those three things completely independant?

mostly: I want to use UFDs to construct a GCD domain on polynomials. formal derivatives over polynomials are independent of this.

#### Johannes Hölzl (Sep 01 2018 at 16:24):

My next step is to introduce the quotient over associated elements and unique factorization domains: https://github.com/johoelzl/mathlib/tree/ufd
I guess one could classically construct from this the normalisation?

#### Kevin Buzzard (Sep 01 2018 at 16:27):

Does normalization mean something different here? To me, the normalization of an integral domain A is the integral closure of A in its fraction field K

Yes that's the standard use in maths. I've never heard of this use before -- the key examples are "normalising" a non-zero poly by making it monic and "normalising" a non-zero integer by taking its absolute value. I don't really know why these CS people want it but it would not surprise me if there were a good reason.

#### Kevin Buzzard (Sep 01 2018 at 16:29):

Oh -- I wrote my comment before I saw Johannes'. So perhaps the issue is that the usual definition of unique factorization domain kind of stinks, you are saying something is equal up to units and re-ordering, which is sort of a mess in Lean. Mario asked me to give an example of how UFD's were used in mathematics, and I couldn't give an example which wasn't of the form "we can solve this Diophantine equation using this trick". But since then we have a couple.

#### Kevin Buzzard (Sep 01 2018 at 16:30):

One is that Johannes pointed out that Mason-Stothers uses it, and the other one is Brian Conrad's observation which he made to me in email, saying that in the theory of smooth schemes one uses a lot that (a) regular local rings are UFD's and (b) in a UFD, all height one primes are principal. So Kenny if you fancy learning some abstract ring theory you can learn the proofs of these two things and then you might have some opinions about how the notion of a UFD should be formalised in Lean.

#### Mario Carneiro (Sep 01 2018 at 16:32):

I didn't write the definition of normalization domain, but it's pretty natural once you decide you want a function gcd : R -> R -> R, and given the definition I want to know if it relates in any obvious way to standard ring theoretic definitions

#### Mario Carneiro (Sep 01 2018 at 16:35):

I guess another option is to quotient by associates; then you could have a function into that quotient which doesn't have this non-functorial normalization structure overlaid

#### Kenny Lau (Sep 01 2018 at 16:37):

why norm_unit u = u⁻¹?

#### Mario Carneiro (Sep 01 2018 at 16:38):

That just means that every unit is normalized to 1

#### Mario Carneiro (Sep 01 2018 at 16:39):

The actual normalization function is normalize x = x * norm_unit x

oh ok

#### Kenny Lau (Sep 01 2018 at 16:39):

then why don't we...

#### Mario Carneiro (Sep 01 2018 at 16:40):

why don't we what?

#### Kenny Lau (Sep 01 2018 at 16:44):

why don't we define the normalization to send the element to its normalization?

#### Mario Carneiro (Sep 01 2018 at 16:49):

because you want the evidence that the map is a unit

#### Mario Carneiro (Sep 01 2018 at 17:34):

Maybe the folks at MSE will know whether it is true: https://math.stackexchange.com/q/2901858/50776

#### Kevin Buzzard (Sep 01 2018 at 17:35):

Oh, I hadn't realised there was a maths question.

#### Kevin Buzzard (Sep 01 2018 at 17:36):

Heh, when I read the thing about integral domains and normalizations I incorrectly thought (as did Kenny) that you were talking about the integral closure :-)

#### Mario Carneiro (Sep 01 2018 at 17:37):

I'm open to alternate terminology

#### Mario Carneiro (Sep 01 2018 at 17:38):

is this the normalization you are talking about? https://en.wikipedia.org/wiki/Normal_scheme

Yes.

#### Mario Carneiro (Sep 01 2018 at 17:39):

Would "orientation" be more or less confusing than "normalization"?

#### Kevin Buzzard (Sep 01 2018 at 17:40):

heh, that means something else in maths too of course, but not in algebra (as far as I know), so the two clashing uses of "normalisation of an integral domain" would be replaced by something which would confuse a geometer (who wants to orient certain kinds of manifolds) but which would be safer in general I guess.

#### Mario Carneiro (Sep 01 2018 at 17:56):

actually I rather like the "orientation" terminology, since it makes the question of whether there are non-orientable integral domains sound more interesting

#### Mario Carneiro (Sep 01 2018 at 17:57):

(plus there is an obvious analogy to orientable manifolds, at least in the case where the unit group has two elements)

#### Kevin Buzzard (Sep 01 2018 at 19:06):

OK so there are problems if the ID is not normal (;-)) i.e. integrally closed. If $R=\mathbb{Z}[{(-4)}^{1/2}]=\mathbb{Z}[2i]$ then $2i$ and $2$ are not associates, but their squares are, and I think this kills it.

Last updated: May 19 2021 at 02:10 UTC