Euclidean domain and GCD domain

Stream: general

[AHan]

While trying to understand the definition of euclidean_domain and gcd_domain in Lean,
since in abstract algebra, ED is contained in GCD domain,
I've been wondering if it's possible to prove that euclidean_domain is an instance of gcd_domain in Lean?

To prove that euclidean_domain is an instance of gcd_domain, we must prove that gcd is unique up to multiplication by units in euclidean_domain. To prove this, we need to first define fields such as norm_unit for euclidean_domain. And I can figure out a way to define the norm_unit such that I can prove that gcd is unique up to multiplication by units.

Am I missing something?

[Kenny Lau]

in Lean you need a euclidean domain and a normalization domain to form a GCD domain, I believe

[Mario Carneiro]

I don't think it's possible. I recall discussing this with @Kevin Buzzard - not every domain is a normalization_domain; even using choice, you can't necessarily define a coherent normalization across the whole ring

[AHan]

So is this contradict to the relation of ED and GCD domain in abstract algebra ?

[Mario Carneiro]

I think gcd_domain should actually be renamed, or it should lose its dependence on normalization_domain, because this constraint is not in the maths definition of the term, and indeed there are lots of examples of GCD domains that have no natural normalization

[Mario Carneiro]

int is a normalization domain but I think it is an exception in this regard

[AHan]

If both euclidean_domain and gcd_domain are not depend on normalization_domain,
then is gcd still unique up to something?

[Mario Carneiro]

if gcd_domain does not depend on normalization_domain, then gcd will not be a function, it will be an assertion that a gcd exists

[Mario Carneiro]

lean's gcd_domain is more like "a domain where you can say gcd a b and mean something"

[Mario Carneiro]

but the maths definition is more abstract than that

[Mario Carneiro]

One way to say it is "associates A is a lattice"

[Chris Hughes]

That has computational content

[Mario Carneiro]

I'm not sure whether to give it content

[Mario Carneiro]

I think we probably want those operations on associates, so that's one option

[Mario Carneiro]

it can also be written gcd : A -> A -> associates A

[Mario Carneiro]

But I think that gcd_domain was written for the more CSy goal of just unifying int.gcd and nat.gcd. I think this is a bad idea, I think we want these operations regardless and gcd_domain is not really generalizing these