# Zulip Chat Archive

## Stream: general

### Topic: Typeclass issue

#### Paul Lezeau (Sep 06 2021 at 15:49):

I'm currently working on some stuff to do with ideals in Dedekind Domains, but am running into issues.

For instance, when the following compiles when I put it in a separate file, but when I add it at the bottom of `ring_theory/dedekind_domain`

(minus the two import lines, and deleting `{R : Type}`

since `R`

has already been defined), I get some `failed to synthesize type class instance`

errors. Does anyone know why ?

```
import data.multiset.basic
import ring_theory.dedekind_domain
namespace ideal_factorization
open_locale classical
noncomputable theory
open unique_factorization_monoid
variables {α : Type} [comm_cancel_monoid_with_zero α] [unique (units α)] [nontrivial α]
{R : Type} [integral_domain R] [is_dedekind_domain R](I : ideal R) (J : ideal R)
lemma eq_of_associated' {x y : α} (h : associated x y) : x = y :=
by { obtain ⟨u, hu⟩ := h, rw [units_eq_one u, units.coe_one, mul_one] at hu, exact hu }
lemma prod_factors_eq_ideal' {I : ideal R} (hI : I ≠ 0) : (factors I).prod = I :=
eq_of_associated (factors_prod hI)
end ideal_factorization
```

#### Yaël Dillies (Sep 06 2021 at 15:52):

This has probably to do with `α`

already being defined and having typeclasses in `ring_theory.dedekind_domain. So you think you're talking about whatever thing you want on your `

α` but end up talking about the file's `

α`, which has less instances.

#### Kevin Buzzard (Sep 06 2021 at 16:07):

What's the exact text of the *first* error you get?

#### Paul Lezeau (Sep 06 2021 at 16:12):

So the precise text is

```
failed to synthesize type class instance for
R : Type u_1,
_inst_1 : comm_ring R,
_inst_4 : integral_domain R,
_inst_5 : is_dedekind_domain R,
I : ideal R,
hI : I ≠ 0
⊢ unique (units (ideal R))
```

#### Yaël Dillies (Sep 06 2021 at 16:15):

And what's the output of `#where`

right before the incriminated lemma?

#### Paul Lezeau (Sep 06 2021 at 16:17):

```
namespace ideal_factorization
open algebra unique_factorization_monoid ring submodule submodule.is_principal ideal fractional_ideal
variables {α : Type} (R : Type u_1) (A : Type u_2) (K : Type u_3) (J I : ideal R) [comm_ring R]
[integral_domain A] [field K] [comm_cancel_monoid_with_zero α] [unique (units α)]
[nontrivial α] [integral_domain R] [is_dedekind_domain R]
end ideal_factorization
```

#### Kevin Buzzard (Sep 06 2021 at 16:21):

~~When I post your stuff into that file, the ~~ Sorry, I missed your comment about deleting R*first* error I get is a complaint about R already being defined, so I think Yael's explanation is correct. I cannot reproduce your error, and furthermore the code you posted above does not compile, so there is some confusion here.

#### Kevin Buzzard (Sep 06 2021 at 16:24):

I still cannot reproduce your error. Can you fix up the code so that it works independently, and also post precisely what you are posting on the end of the dedekind_domain file?

#### Paul Lezeau (Sep 06 2021 at 16:47):

Here's the full code I'd I'm trying to add at the end of `dedekind_domain`

, including the imports (the code compiles fine when I leave it in a separate file).

```
import data.multiset.basic
import ring_theory.dedekind_domain
import ring_theory.ideal.basic
import ring_theory.ideal.operations
namespace ideal_factorization
open_locale classical
noncomputable theory
open unique_factorization_monoid multiset ideal
variables {R : Type*} [integral_domain R] [is_dedekind_domain R] (I : ideal R) (J : ideal R)
lemma eq_of_associated {I J : ideal R} (H : associated I J) : I = J :=
by { obtain ⟨u, hu⟩ := H, rw [units_eq_one u, units.coe_one, mul_one] at hu, exact hu}
lemma prod_factors_eq_ideal {I : ideal R} (hI : I ≠ 0) : (unique_factorization_monoid.factors I).prod = I :=
eq_of_associated (unique_factorization_monoid.factors_prod hI)
lemma associated_equiv_eq : (associated : (ideal R) → ideal R → Prop) = eq :=
begin
ext a b,
split,
{ exact eq_of_associated },
{ intro hab, rw hab },
end
lemma factors_prod_factors_eq_factors {α : multiset (ideal R)} (h₁ : (0 : ideal R) ∉ α) (h₂ : ∀ p ∈ α, prime p):
factors α.prod = α :=
begin
suffices : (factors α.prod).prod = α.prod,
{ have H₁ : associated (factors α.prod).prod α.prod,
rw this,
have H := prime_factors_unique (prime_of_factor) h₂ H₁,
rw [associated_equiv_eq, multiset.rel_eq] at H,
exact H },
{ exact eq_of_associated (factors_prod (prod_ne_zero h₁)) },
end
lemma ne_zero_of_ne_zero_le {I J : ideal R} (h : I ≤ J) (hI : I ≠ 0) : J ≠ 0 :=
begin
rw [zero_eq_bot, ← bot_lt_iff_ne_bot] at hI,
rw [zero_eq_bot, ← bot_lt_iff_ne_bot],
exact lt_of_lt_of_le hI h,
end
lemma count_le_of_ideal_le {I J : ideal R} (h : I ≤ J) (hI : I ≠ 0) (K : ideal R) :
count K (factors J) ≤ count K (factors I) :=
begin
rw [← dvd_iff_le, dvd_iff_factors_le_factors ] at h,
exact le_iff_count.1 h K,
exact ne_zero_of_ne_zero_le (le_of_dvd h) hI,
exact hI,
end
lemma zero_not_mem_inf_factors (I J : ideal R) : (0 : ideal R) ∉ factors I ⊓ factors J :=
begin
by_contra hcontra,
rw [multiset.inf_eq_inter, mem_inter] at hcontra,
exact false_of_ne (prime.ne_zero (prime_of_factor (0 : ideal R) hcontra.left)),
end
-- This is the result I'm hoping to PR
lemma sup_eq_prod_inf_factors (hI : I ≠ 0) (hJ : J ≠ 0): I ⊔ J = (factors I ⊓ factors J).prod :=
begin
have H : factors (factors I ⊓ factors J).prod = factors I ⊓ factors J,
{ apply factors_prod_factors_eq_factors (zero_not_mem_inf_factors I J),
intros p hp,
rw [multiset.inf_eq_inter, mem_inter] at hp,
exact prime_of_factor p hp.left },
apply le_antisymm,
{ rw [sup_le_iff, ← dvd_iff_le, ← dvd_iff_le],
split,
{ rw [dvd_iff_factors_le_factors (prod_ne_zero (zero_not_mem_inf_factors I J)) hI, H],
exact inf_le_left },
{ rw [dvd_iff_factors_le_factors (prod_ne_zero (zero_not_mem_inf_factors I J)) hJ, H],
exact inf_le_right } },
rw [← dvd_iff_le, dvd_iff_factors_le_factors, factors_prod_factors_eq_factors, le_iff_count],
intro a,
rw [multiset.inf_eq_inter, multiset.count_inter],
exact le_min (count_le_of_ideal_le le_sup_left hI a) (count_le_of_ideal_le le_sup_right hJ a),
exact zero_not_mem_inf_factors I J,
{ intros p hp,
rw [multiset.inf_eq_inter, mem_inter] at hp,
exact prime_of_factor p hp.left },
{ exact ne_zero_of_ne_zero_le le_sup_left hI },
exact prod_ne_zero (zero_not_mem_inf_factors I J),
end
end ideal_factorization
```

#### Paul Lezeau (Sep 06 2021 at 16:48):

(Some of the results here probably should go in other files of course :-) )

#### Kevin Buzzard (Sep 06 2021 at 16:56):

If all you remove is the imports then, as is already noted, you'll get an error about variable R already being declared. I was trying to establish exactly what you are doing about this error because whatever I tried didn't give me the error you're seeing.

#### Kevin Buzzard (Sep 06 2021 at 16:58):

In that file, the convention is that R is a `comm_ring`

and A is an integral domain, so you are mixing conventions and this might be what is causing your problems, however because you are still not showing me how to reproduce your problems I am still not able to help.

#### Kevin Buzzard (Sep 06 2021 at 17:18):

Oh! I just noticed that in your output to `#where`

you have `[comm_ring R] [integral_domain R]`

so that's probably your problem. Why not use a different variable name eg A?

#### Paul Lezeau (Sep 06 2021 at 17:19):

I just changed `R`

to `T`

everywhere in my code, and that seems to have done the trick !

#### Paul Lezeau (Sep 06 2021 at 17:23):

Thanks a lot for the help, this error was driving me nuts ;-)

Last updated: Aug 03 2023 at 10:10 UTC