# 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 domain`

s 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_domain`

s.

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

#### 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_int`

s, 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_int`

s 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):

$9i$ and $-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^\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 $r\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 $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 (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