## Stream: new members

### Topic: Ideals in a Dedekind domain form a gcd_monoid

#### Paul Lezeau (Aug 26 2021 at 10:48):

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 (Aug 26 2021 at 11:59):

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 (Aug 26 2021 at 12:01):

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 (Aug 26 2021 at 12:03):

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 (Aug 26 2021 at 12:06):

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 (Aug 26 2021 at 12:09):

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 (Aug 26 2021 at 12:12):

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 (Aug 26 2021 at 12:14):

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 (Aug 26 2021 at 12:18):

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

#### Anne Baanen (Aug 26 2021 at 12:20):

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 (Aug 26 2021 at 12:22):

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".

yup, exactly

#### Paul Lezeau (Aug 26 2021 at 13:17):

How exactly should I use gcd_monoid.copy ? I've never come across copybefore :-)

#### Kevin Buzzard (Aug 26 2021 at 14:49):

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 (Aug 26 2021 at 16:01):

Ok, that makes sense, thanks a lot !

#### Scott Morrison (Aug 27 2021 at 01:01):

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

#### Johan Commelin (Aug 27 2021 at 05:10):

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

#### Paul Lezeau (Aug 27 2021 at 07:32):

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 ;-)

Last updated: Dec 20 2023 at 11:08 UTC