GCD

Stream: maths

[Patrick Massot]

@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]

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]

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

[Patrick Massot]

Are those three things completely independant?

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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]

yes, that's a different sense

[Johannes Hölzl]

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]

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]

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]

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]

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]

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]

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]

why norm_unit u = u⁻¹?

[Mario Carneiro]

That just means that every unit is normalized to 1

[Mario Carneiro]

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

[Kenny Lau]

oh ok

[Kenny Lau]

then why don't we...

[Mario Carneiro]

why don't we what?

[Kenny Lau]

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

[Mario Carneiro]

because you want the evidence that the map is a unit

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

I'm open to alternate terminology

[Mario Carneiro]

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

[Kevin Buzzard]

Yes.

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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.