# Zulip Chat Archive

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

s:

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

#### Johan Commelin (Aug 26 2021 at 12:24):

yup, exactly

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

Thanks for the answers !

How exactly should I use `gcd_monoid.copy`

? I've never come across `copy`

before :-)

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