Typeclass issue

Stream: general

[Paul Lezeau]

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

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]

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

[Paul Lezeau]

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]

And what's the output of #where right before the incriminated lemma?

[Paul Lezeau]

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]

When I post your stuff into that file, the 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. Sorry, I missed your comment about deleting R

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

I just changed R to T everywhere in my code, and that seems to have done the trick !

[Paul Lezeau]

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