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 R is a Dedekind domain and I,J I, J are ideals in R R , then gcdI J=IJ\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".

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