Ideals in a Dedekind domain form a `gcd_monoid`

Stream: new members

[Paul Lezeau]

I'm currently trying to write down statements of the form: if $R$ is a Dedekind domain and $I, J$ are ideals in $R$, then $\gcd I \ J = I \sqcup J$. This should make sense to Lean because it has already been show that ideal R is a unique_factorization_monoid and that any unique_factorization_monoid is a gcd_monoid. When I tried to write it out, I got a failed to synthesize type class instance error.

import ring_theory.ideal.operations
import ring_theory.ideal.basic
import ring_theory.dedekind_domain

lemma gcd_eq_sup {R : Type} [integral_domain R] [is_dedekind_domain R] (I : ideal R) (J : ideal R):
gcd I J = I ⊔ J := sorry

How do I remind Lean that ideal R is a gcd_monoid ?

[Anne Baanen]

The problem you are encountering is that docs#unique_factorization_monoid.to_gcd_monoid needs two extra assumptions:

import ring_theory.ideal.operations
import ring_theory.ideal.basic
import ring_theory.dedekind_domain

variables {R : Type} [integral_domain R] [is_dedekind_domain R]

example : gcd_monoid (ideal R) := unique_factorization_monoid.to_gcd_monoid (ideal R)
/-
failed to synthesize type class instance for
R : Type,
_inst_1 : integral_domain R,
_inst_2 : is_dedekind_domain R
⊢ decidable_eq (associates (ideal R))

failed to synthesize type class instance for
R : Type,
_inst_1 : integral_domain R,
_inst_2 : is_dedekind_domain R
⊢ decidable_eq (ideal R)
-/

[Anne Baanen]

So let's say we don't care about computability and throw in an open_locale classical:

import ring_theory.ideal.operations
import ring_theory.ideal.basic
import ring_theory.dedekind_domain

variables {R : Type} [integral_domain R] [is_dedekind_domain R]

open_locale classical

noncomputable example : gcd_monoid (ideal R) := unique_factorization_monoid.to_gcd_monoid (ideal R)

lemma gcd_eq_sup [decidable_eq (ideal R)] [decidable_eq (associates (ideal R))] (I : ideal R) (J : ideal R) :
  gcd I J = I ⊔ J := sorry -- Still no `gcd_monoid` instance!

[Anne Baanen]

The second issue here is that unique_factorization_monoid.to_gcd_monoid is not actually an instance, so the typeclass system won't pick it up. Two ways to fix it: either promote to_gcd_monoid to an instance, or what would be a neater solution: provide your own instance for ideal R where gcd is defined as sup.

[Anne Baanen]

That is, a better way to formalize gcd I J = I \sup J is to fill out these sorrys:

import ring_theory.ideal.operations
import ring_theory.ideal.basic
import ring_theory.dedekind_domain

variables {R : Type} [integral_domain R] [is_dedekind_domain R]

open_locale classical

noncomputable instance : gcd_monoid (ideal R) :=
gcd_monoid_of_gcd (⊔) sorry sorry sorry sorry

[Johan Commelin]

Does it make sense to have a gcd_monoid.copy that allows one to use unique_factorization_monoid.to_gcd_monoid for the proofy part, but replace the gcd function by something propeq?

[Anne Baanen]

copy is a good idea for structures in general. But I think the hypotheses for docs#gcd_monoid_of_gcd are basically exactly what you would need to show something equals gcd, right? Do you have a suggestion as to what kind of work you would save?

[Johan Commelin]

The only proof obligation with the copy approach would be to show that I ⊔ J is propeq to whatever unique_factorization_monoid.to_gcd_monoid thinks is the gcd of two ideals.

[Anne Baanen]

Aha, in this case that would be something like I ⊔ J = (factors I ⊓ factors J).prod.

[Anne Baanen]

I guess that would work fine, as long as there would be a convenient way to derive that equality from the characteristic predicates of gcd, i.e. I <= I ⊔ J, J <= I ⊔ J, I ⊔ J ≤ K ↔ I ≤ K ∨ J ≤ K and normalize (I ⊔ J) = I ⊔ J.

[Anne Baanen]

Or would we just write in the docstring for gcd_monoid.copy something like "if you want to show this through the characteristic predicate, check out docs#gcd_monoid_of_gcd".

[Johan Commelin]

yup, exactly

[Paul Lezeau]

Thanks for the answers !
How exactly should I use gcd_monoid.copy ? I've never come across copybefore :-)

[Kevin Buzzard]

I can't actually find gcd_monoid.copy but I have come across copy before and the idea is that if you have some instance of a structure but one of the fields is definitionally a bit convoluted, and you would like to get a new instance of the structure which is "the same" instance but with the bad field redefined in a more convenient way, then various copy functions enable you to do this in a pretty painless manner: you give the new field, a proof that it's equal to the old field, and then let the copy function build the new instance.

[Paul Lezeau]

Ok, that makes sense, thanks a lot !

[Scott Morrison]

I think the suggestion above is that someone (Paul? :-) should add a gcd_monoid.copy.

[Johan Commelin]

See docs#complete_lattice.copy for an example of such a copy constructor.

[Paul Lezeau]

Scott Morrison said:

I think the suggestion above is that someone (Paul? :-) should add a gcd_monoid.copy.

Yup, I'll get to work on that soonish ;-)