gcd_domain

Stream: new members

[Paul van Wamelen]

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]

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

[Kevin Buzzard]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Kevin Buzzard]

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]

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\}$.

[Reid Barton]

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

[Kevin Buzzard]

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]

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]

But this statement isn't true.

[Kevin Buzzard]

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

[Paul van Wamelen]

OK, up to units! :)

[Kevin Buzzard]

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

[Paul van Wamelen]

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

[Kevin Buzzard]

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]

unique_factorization_domain.lean should contain everything you need.

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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 $a_i$ divides the product of the $b_i$ then the multiset of $a_i$ is a subset of the multiset of $b_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]

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

[Kevin Buzzard]

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]

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]

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]

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