Zulip Chat Archive

Stream: new members

Topic: gcd_domain

Paul van Wamelen (Apr 18 2020 at 16:26):

I want to use the gcd in a general unique factorization domain and prove e.g. what the prime factorization of gcd a b looks like in terms of the the prime factorizations of a and b. So (but I'm probably misunderstanding something) I don't think I can "just ask for a gcd_domain". I want both a gcd_domain and a unique_factorization_doamin, but I can't variables [unique_factorization_domain α] without integral_domain...

Kevin Buzzard (Apr 18 2020 at 16:52):

But there is no gcd in a general UFD. It's only defined up to units.

Kevin Buzzard (Apr 18 2020 at 16:54):

The whole purpose of normalisation domains is to give a fixed notion of a gcd.

Reid Barton (Apr 18 2020 at 16:55):

So I guess the first question is, in math, do you want to treat a general UFD?

Reid Barton (Apr 18 2020 at 16:56):

If so then I think you can't use one of these funny normalization_domain/gcd_domains.

Reid Barton (Apr 18 2020 at 16:58):

Then the second question will be how to say what you want to say using mathlib's classes.

Kevin Buzzard (Apr 18 2020 at 17:01):

Hmm, I think that on a general UFD you can give a structure of a normalization domain. You put the equivalence relation "our ratio is a unit" on all the irreducible elements of the UFD and then randomly choose an element in each equivalence class, and then extend multiplicatively.

Kevin Buzzard (Apr 18 2020 at 17:03):

Although you'll have to be careful not to make it too random, because normalization domain int is already an instance in mathlib, where they chose the positive element of each equivalence class {p,p}\{p,-p\}.

Reid Barton (Apr 18 2020 at 17:04):

Oh I see, I forgot you had these irreducibles to work with.

Kevin Buzzard (Apr 18 2020 at 17:06):

I'm not sure this construction is in mathlib though (I don't know this part of the library, I'm just browsing through it). The def unique_factorization_domain.to_gcd_domain assumes a normalization domain.

Paul van Wamelen (Apr 18 2020 at 17:08):

Ultimately what I wanted to prove was that in the gaussian_ints, if the product of 2 relatively prime elements is a k'th power then each element is a k'th power. I was thinking it would be possible to do the normalization in gaussian_ints like Kevin describes.

Kevin Buzzard (Apr 18 2020 at 17:08):

But this statement isn't true.

Kevin Buzzard (Apr 18 2020 at 17:09):

9i9i and 4i-4i are not squares, but their product is.

Paul van Wamelen (Apr 18 2020 at 17:10):

OK, up to units! :)

Kevin Buzzard (Apr 18 2020 at 17:10):

If you only care up to units then hopefully you don't need any of that normalisation domain nonsense.

Paul van Wamelen (Apr 18 2020 at 17:12):

I thought all the "normalization domain nonsense" was exactly there to make it easy to state things "up to units"!

Kevin Buzzard (Apr 18 2020 at 17:13):

On the contrary, my impression is that it's exactly there because the computer scientists thought it was a good idea, and no self-respecting mathematician would touch it.

Kevin Buzzard (Apr 18 2020 at 17:13):

unique_factorization_domain.lean should contain everything you need.

Kevin Buzzard (Apr 18 2020 at 17:14):

associates R is the type of equivalence classes R/R×R/R^\times

Kevin Buzzard (Apr 18 2020 at 17:15):

and there is a predicate irreducible on them, and factor_set is the type of (finite) multisets of elements of associates R plus a random extra term corresponding to the factors of 0

Kevin Buzzard (Apr 18 2020 at 17:16):

and factors' r is the multiset of prime factors of r if r0r\not=0 (multiset just means set but you're allowed repeated elements)

Kevin Buzzard (Apr 18 2020 at 17:18):

If you think about how you want to formalise things, then you want a factorization of a non-zero thing to be exactly a collection of primes-up-to-units (with repeats allowed) whose product is the thing, and this is exactly what factors and factors' are giving you, and all the lemmas you want are proved about these things.

Reid Barton (Apr 18 2020 at 17:19):

It sure would be easier if we didn't have all these crazy negative and imaginary numbers

Kevin Buzzard (Apr 18 2020 at 17:21):

I think that's what the computer scientists are thinking. You also have to learn to see through the computer science lattice notation, e.g. theorem prod_le {a b : factor_set α} : a.prod ≤ b.prod ↔ a ≤ b means that if the product of the aia_i divides the product of the bib_i then the multiset of aia_i is a subset of the multiset of bib_i, and lemma sup_mul_inf (a b : associates α) : (a ⊔ b) * (a ⊓ b) = a * b means that gcd(a,b)*lcm(a,b)=a*b, where equality is up to units (a and b are not elements of R, they're elements of associates R)

Paul van Wamelen (Apr 18 2020 at 17:22):

OK, thanks Kevin! I'll give all of this another think.

Kevin Buzzard (Apr 18 2020 at 17:22):

If you only want to work up to units then associates R is the type you're looking for, and there are a ton of lemmas about it.

Paul van Wamelen (Apr 18 2020 at 17:25):

Yep, have been staring at this for a while now... I was thinking using to_gcd_domain would get me a bit more functionality, but I can certainly survive without it.

Kevin Buzzard (Apr 18 2020 at 17:26):

The only thing it will give you is a non-canonical but fixed splitting of the map R -> associates R, but given that the statement you want is only true up to units I'm not sure you're buying much with it.

Chris Hughes (Apr 20 2020 at 01:10):

gcd_domain really needs to be refactored at some point I think, to unlink it from normalization_domain.

Last updated: Dec 20 2023 at 11:08 UTC