Zulip Chat Archive

Stream: maths

Topic: GCD


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Johannes Hölzl (Sep 01 2018 at 09:31):

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

view this post on Zulip Patrick Massot (Sep 01 2018 at 09:33):

Are those three things completely independant?

view this post on Zulip 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 RR act freely on R{0}R-\{0\} by left multiplication. If we quotient by the orbit relation, we obtain a monoid MM. The goal is to prove the existence of a monoid homomorphism from MM to the unit group of RR. Is there an abstract nonsense reason this should be true?

view this post on Zulip Mario Carneiro (Sep 01 2018 at 15:18):

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

view this post on Zulip 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 NN 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)(a) and (b)(b) are equal if and only if aa is a unit times bb.

view this post on Zulip 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 NN choice it suffices to choose what is going on for the prime elements.

view this post on Zulip Mario Carneiro (Sep 01 2018 at 15:35):

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

view this post on Zulip Mario Carneiro (Sep 01 2018 at 15:49):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 01 2018 at 15:50):

yes, that's a different sense

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Sep 01 2018 at 16:37):

why norm_unit u = u⁻¹?

view this post on Zulip Mario Carneiro (Sep 01 2018 at 16:38):

That just means that every unit is normalized to 1

view this post on Zulip Mario Carneiro (Sep 01 2018 at 16:39):

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

view this post on Zulip Kenny Lau (Sep 01 2018 at 16:39):

oh ok

view this post on Zulip Kenny Lau (Sep 01 2018 at 16:39):

then why don't we...

view this post on Zulip Mario Carneiro (Sep 01 2018 at 16:40):

why don't we what?

view this post on Zulip Kenny Lau (Sep 01 2018 at 16:44):

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

view this post on Zulip Mario Carneiro (Sep 01 2018 at 16:49):

because you want the evidence that the map is a unit

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 01 2018 at 17:35):

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

view this post on Zulip 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 :-)

view this post on Zulip Mario Carneiro (Sep 01 2018 at 17:37):

I'm open to alternate terminology

view this post on Zulip Mario Carneiro (Sep 01 2018 at 17:38):

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

view this post on Zulip Kevin Buzzard (Sep 01 2018 at 17:39):

Yes.

view this post on Zulip Mario Carneiro (Sep 01 2018 at 17:39):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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=Z[(4)1/2]=Z[2i]R=\mathbb{Z}[{(-4)}^{1/2}]=\mathbb{Z}[2i] then 2i2i and 22 are not associates, but their squares are, and I think this kills it.


Last updated: May 19 2021 at 02:10 UTC