feat(ring_theory): Dedekind domains have invertible fractional ideals (…

…#8396)

This PR proves the other side of the equivalence `is_dedekind_domain → is_dedekind_domain_inv`, and uses this to provide a `comm_group_with_zero (fractional_ideal A⁰ K)` instance.

Co-Authored-By: Ashvni ashvni.n@gmail.com
Co-Authored-By: Filippo A. E. Nuccio filippo.nuccio@univ-st-etienne.fr



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/ring_theory/dedekind_domain.lean

@@ -86,6 +86,9 @@ class is_dedekind_domain : Prop :=
 (dimension_le_one : dimension_le_one A)
 (is_integrally_closed : integral_closure A (fraction_ring A) = ⊥)
 
+-- See library note [lower instance priority]
+attribute [instance, priority 100] is_dedekind_domain.is_noetherian_ring
+
 /-- An integral domain is a Dedekind domain iff and only if it is not a field, is
 Noetherian, has dimension ≤ 1, and is integrally closed in a given fraction field.
 In particular, this definition does not depend on the choice of this fraction field. -/
@@ -111,8 +114,6 @@ structure is_dedekind_domain_dvr : Prop :=
 
 section inverse
 
-open_locale classical
-
 variables {R₁ : Type*} [integral_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K]
 variables {I J : fractional_ideal R₁⁰ K}
 
@@ -130,6 +131,26 @@ lemma coe_inv_of_nonzero {J : fractional_ideal R₁⁰ K} (h : J ≠ 0) :
   (↑J⁻¹ : submodule R₁ K) = is_localization.coe_submodule K ⊤ / J :=
 by { rwa inv_nonzero _, refl, assumption }
 
+variables {K}
+
+lemma mem_inv_iff (hI : I ≠ 0) {x : K} :
+  x ∈ I⁻¹ ↔ ∀ y ∈ I, x * y ∈ (1 : fractional_ideal R₁⁰ K) :=
+fractional_ideal.mem_div_iff_of_nonzero hI
+
+lemma inv_anti_mono (hI : I ≠ 0) (hJ : J ≠ 0) (hIJ : I ≤ J) :
+  J⁻¹ ≤ I⁻¹ :=
+λ x, by { simp only [mem_inv_iff hI, mem_inv_iff hJ], exact λ h y hy, h y (hIJ hy) }
+
+lemma le_self_mul_inv {I : fractional_ideal R₁⁰ K} (hI : I ≤ (1 : fractional_ideal R₁⁰ K)) :
+  I ≤ I * I⁻¹ :=
+fractional_ideal.le_self_mul_one_div hI
+
+variables (K)
+
+lemma coe_ideal_le_self_mul_inv (I : ideal R₁) :
+  (I : fractional_ideal R₁⁰ K) ≤ I * I⁻¹ :=
+le_self_mul_inv fractional_ideal.coe_ideal_le_one
+
 /-- `I⁻¹` is the inverse of `I` if `I` has an inverse. -/
 theorem right_inverse_eq (I J : fractional_ideal R₁⁰ K) (h : I * J = 1) :
   J = I⁻¹ :=
@@ -165,8 +186,6 @@ variables {K' : Type*} [field K'] [algebra R₁ K'] [is_fraction_ring R₁ K']
   (I⁻¹).map (h : K →ₐ[R₁] K') = (I.map h)⁻¹ :=
 by rw [inv_eq, fractional_ideal.map_div, fractional_ideal.map_one, inv_eq]
 
-open_locale classical
-
 open submodule submodule.is_principal
 
 @[simp] lemma span_singleton_inv (x : K) :
@@ -224,6 +243,9 @@ begin
     ((generator (I : submodule R₁ K))⁻¹)) hI).symm
 end
 
+@[simp] lemma fractional_ideal.one_inv : (1⁻¹ : fractional_ideal R₁⁰ K) = 1 :=
+fractional_ideal.div_one
+
 /--
 A Dedekind domain is an integral domain such that every fractional ideal has an inverse.
 
@@ -352,4 +374,222 @@ theorem is_dedekind_domain : is_dedekind_domain A :=
 
 end is_dedekind_domain_inv
 
+variables [algebra A K] [is_fraction_ring A K]
+
+/-- Specialization of `exists_prime_spectrum_prod_le_and_ne_bot_of_domain` to Dedekind domains:
+Let `I : ideal A` be a nonzero ideal, where `A` is a Dedekind domain that is not a field.
+Then `exists_prime_spectrum_prod_le_and_ne_bot_of_domain` states we can find a product of prime
+ideals that is contained within `I`. This lemma extends that result by making the product minimal:
+let `M` be a maximal ideal that contains `I`, then the product including `M` is contained within `I`
+and the product excluding `M` is not contained within `I`. -/
+lemma exists_multiset_prod_cons_le_and_prod_not_le [is_dedekind_domain A]
+  (hNF : ¬ is_field A) {I M : ideal A} (hI0 : I ≠ ⊥) (hIM : I ≤ M) [hM : M.is_maximal] :
+  ∃ (Z : multiset (prime_spectrum A)),
+    (M ::ₘ (Z.map prime_spectrum.as_ideal)).prod ≤ I ∧
+    ¬ (multiset.prod (Z.map prime_spectrum.as_ideal) ≤ I) :=
+begin
+  -- Let `Z` be a minimal set of prime ideals such that their product is contained in `J`.
+  obtain ⟨Z₀, hZ₀⟩ := exists_prime_spectrum_prod_le_and_ne_bot_of_domain hNF hI0,
+  obtain ⟨Z, ⟨hZI, hprodZ⟩, h_eraseZ⟩ := multiset.well_founded_lt.has_min
+    (λ Z, (Z.map prime_spectrum.as_ideal).prod ≤ I ∧ (Z.map prime_spectrum.as_ideal).prod ≠ ⊥)
+    ⟨Z₀, hZ₀⟩,
+  have hZM : multiset.prod (Z.map prime_spectrum.as_ideal) ≤ M := le_trans hZI hIM,
+  have hZ0 : Z ≠ 0, { rintro rfl, simpa [hM.ne_top] using hZM },
+  obtain ⟨_, hPZ', hPM⟩ := (hM.is_prime.multiset_prod_le (mt multiset.map_eq_zero.mp hZ0)).mp hZM,
+  -- Then in fact there is a `P ∈ Z` with `P ≤ M`.
+  obtain ⟨P, hPZ, rfl⟩ := multiset.mem_map.mp hPZ',
+  letI := classical.dec_eq (ideal A),
+  have := multiset.map_erase prime_spectrum.as_ideal subtype.coe_injective P Z,
+  obtain ⟨hP0, hZP0⟩ : P.as_ideal ≠ ⊥ ∧ ((Z.erase P).map prime_spectrum.as_ideal).prod ≠ ⊥,
+  { rwa [ne.def, ← multiset.cons_erase hPZ', multiset.prod_cons, ideal.mul_eq_bot,
+         not_or_distrib, ← this] at hprodZ },
+  -- By maximality of `P` and `M`, we have that `P ≤ M` implies `P = M`.
+  have hPM' := (is_dedekind_domain.dimension_le_one _ hP0 P.is_prime).eq_of_le hM.ne_top hPM,
+  tactic.unfreeze_local_instances,
+  subst hPM',
+
+  -- By minimality of `Z`, erasing `P` from `Z` is exactly what we need.
+  refine ⟨Z.erase P, _, _⟩,
+  { convert hZI,
+    rw [this, multiset.cons_erase hPZ'] },
+  { refine λ h, h_eraseZ (Z.erase P) ⟨h, _⟩ (multiset.erase_lt.mpr hPZ),
+    exact hZP0 }
+end
+
+namespace fractional_ideal
+
+lemma exists_not_mem_one_of_ne_bot [is_dedekind_domain A]
+  (hNF : ¬ is_field A) {I : ideal A} (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) :
+  ∃ x : K, x ∈ (I⁻¹ : fractional_ideal A⁰ K) ∧ x ∉ (1 : fractional_ideal A⁰ K) :=
+begin
+  -- WLOG, let `I` be maximal.
+  suffices : ∀ {M : ideal A} (hM : M.is_maximal),
+    ∃ x : K, x ∈ (M⁻¹ : fractional_ideal A⁰ K) ∧ x ∉ (1 : fractional_ideal A⁰ K),
+  { obtain ⟨M, hM, hIM⟩ : ∃ (M : ideal A), is_maximal M ∧ I ≤ M := ideal.exists_le_maximal I hI1,
+    resetI,
+    have hM0 := (M.bot_lt_of_maximal hNF).ne',
+    obtain ⟨x, hxM, hx1⟩ := this hM,
+    refine ⟨x, inv_anti_mono _ _ ((coe_ideal_le_coe_ideal _).mpr hIM) hxM, hx1⟩;
+      apply fractional_ideal.coe_ideal_ne_zero; assumption },
+
+  -- Let `a` be a nonzero element of `M` and `J` the ideal generated by `a`.
+  intros M hM,
+  resetI,
+  obtain ⟨⟨a, haM⟩, ha0⟩ := submodule.nonzero_mem_of_bot_lt (M.bot_lt_of_maximal hNF),
+  replace ha0 : a ≠ 0 := subtype.coe_injective.ne ha0,
+  let J : ideal A := ideal.span {a},
+  have hJ0 : J ≠ ⊥ := mt ideal.span_singleton_eq_bot.mp ha0,
+  have hJM : J ≤ M := ideal.span_le.mpr (set.singleton_subset_iff.mpr haM),
+  have hM0 : ⊥ < M := M.bot_lt_of_maximal hNF,
+
+  -- Then we can find a product of prime (hence maximal) ideals contained in `J`,
+  -- such that removing element `M` from the product is not contained in `J`.
+  obtain ⟨Z, hle, hnle⟩ := exists_multiset_prod_cons_le_and_prod_not_le hNF hJ0 hJM,
+  -- Choose an element `b` of the product that is not in `J`.
+  obtain ⟨b, hbZ, hbJ⟩ := set_like.not_le_iff_exists.mp hnle,
+  have hnz_fa : algebra_map A K a ≠ 0 :=
+    mt ((ring_hom.injective_iff _).mp (is_fraction_ring.injective A K) a) ha0,
+  have hb0 : algebra_map A K b ≠ 0 :=
+    mt ((ring_hom.injective_iff _).mp (is_fraction_ring.injective A K) b)
+      (λ h, hbJ $ h.symm ▸ J.zero_mem),
+  -- Then `b a⁻¹ : K` is in `M⁻¹` but not in `1`.
+  refine ⟨algebra_map A K b * (algebra_map A K a)⁻¹, (mem_inv_iff _).mpr _, _⟩,
+  { exact (fractional_ideal.coe_to_fractional_ideal_ne_zero (le_refl _)).mpr hM0.ne' },
+  { rintro y₀ hy₀,
+    obtain ⟨y, h_Iy, rfl⟩ := (fractional_ideal.mem_coe_ideal _).mp hy₀,
+    rw [mul_comm, ← mul_assoc, ← ring_hom.map_mul],
+    have h_yb : y * b ∈ J,
+    { apply hle,
+      rw multiset.prod_cons,
+      exact submodule.smul_mem_smul h_Iy hbZ },
+    rw ideal.mem_span_singleton' at h_yb,
+    rcases h_yb with ⟨c, hc⟩,
+    rw [← hc, ring_hom.map_mul, mul_assoc, mul_inv_cancel hnz_fa, mul_one],
+    apply fractional_ideal.coe_mem_one },
+  { refine mt (fractional_ideal.mem_one_iff _).mp _,
+    rintros ⟨x', h₂_abs⟩,
+    rw [← div_eq_mul_inv, eq_div_iff_mul_eq hnz_fa, ← ring_hom.map_mul] at h₂_abs,
+    have := ideal.mem_span_singleton'.mpr ⟨x', is_fraction_ring.injective A K h₂_abs⟩,
+    contradiction },
+end
+
+lemma one_mem_inv_coe_ideal {I : ideal A} (hI : I ≠ ⊥) :
+  (1 : K) ∈ (I : fractional_ideal A⁰ K)⁻¹ :=
+begin
+  rw mem_inv_iff (fractional_ideal.coe_ideal_ne_zero hI),
+  intros y hy,
+  rw one_mul,
+  exact coe_ideal_le_one hy,
+  assumption
+end
+
+lemma mul_inv_cancel_of_le_one [h : is_dedekind_domain A]
+  {I : ideal A} (hI0 : I ≠ ⊥) (hI : ((I * I⁻¹)⁻¹ : fractional_ideal A⁰ K) ≤ 1) :
+  (I * I⁻¹ : fractional_ideal A⁰ K) = 1 :=
+begin
+  -- Handle a few trivial cases.
+  by_cases hI1 : I = ⊤,
+  { rw [hI1, coe_ideal_top, one_mul, fractional_ideal.one_inv] },
+  by_cases hNF : is_field A,
+  { letI := hNF.to_field A, rcases hI1 (I.eq_bot_or_top.resolve_left hI0) },
+  -- We'll show a contradiction with `exists_not_mem_one_of_ne_bot`:
+  -- `J⁻¹ = (I * I⁻¹)⁻¹` cannot have an element `x ∉ 1`, so it must equal `1`.
+  by_contradiction h_abs,
+  obtain ⟨J, hJ⟩ : ∃ (J : ideal A), (J : fractional_ideal A⁰ K) = I * I⁻¹ :=
+    le_one_iff_exists_coe_ideal.mp mul_one_div_le_one,
+  by_cases hJ0 : J = ⊥,
+  { subst hJ0,
+    apply hI0,
+    rw [eq_bot_iff, ← coe_ideal_le_coe_ideal K, hJ],
+    exact coe_ideal_le_self_mul_inv K I,
+    apply_instance },
+  have hJ1 : J ≠ ⊤,
+  { rintro rfl,
+    rw [← hJ, coe_ideal_top] at h_abs,
+    exact h_abs rfl },
+  obtain ⟨x, hx, hx1⟩ : ∃ (x : K),
+    x ∈ (J : fractional_ideal A⁰ K)⁻¹ ∧ x ∉ (1 : fractional_ideal A⁰ K) :=
+    exists_not_mem_one_of_ne_bot hNF hJ0 hJ1,
+  rw hJ at hx,
+  exact hx1 (hI hx)
+end
+
+/-- Nonzero integral ideals in a Dedekind domain are invertible.
+
+We will use this to show that nonzero fractional ideals are invertible,
+and finally conclude that fractional ideals in a Dedekind domain form a group with zero.
+-/
+lemma coe_ideal_mul_inv [h : is_dedekind_domain A] (I : ideal A) (hI0 : I ≠ ⊥) :
+  (I * I⁻¹ : fractional_ideal A⁰ K) = 1 :=
+begin
+  -- We'll show `1 ≤ J⁻¹ = (I * I⁻¹)⁻¹ ≤ 1`.
+  apply mul_inv_cancel_of_le_one hI0,
+  by_cases hJ0 : (I * I⁻¹ : fractional_ideal A⁰ K) = 0,
+  { rw [hJ0, inv_zero'], exact fractional_ideal.zero_le _ },
+  intros x hx,
+  -- In particular, we'll show all `x ∈ J⁻¹` are integral.
+  suffices : x ∈ integral_closure A K,
+  { rwa [((is_dedekind_domain_iff _ _).mp h).2.2, algebra.mem_bot, set.mem_range,
+         ← fractional_ideal.mem_one_iff] at this;
+      assumption },
+  -- For that, we'll find a subalgebra that is f.g. as a module and contains `x`.
+  -- `A` is a noetherian ring, so we just need to find a subalgebra between `{x}` and `I⁻¹`.
+  rw mem_integral_closure_iff_mem_fg,
+  have x_mul_mem : ∀ b ∈ (I⁻¹ : fractional_ideal A⁰ K), x * b ∈ (I⁻¹ : fractional_ideal A⁰ K),
+  { intros b hb,
+    rw mem_inv_iff at ⊢ hx,
+    swap, { exact fractional_ideal.coe_ideal_ne_zero hI0 },
+    swap, { exact hJ0 },
+    simp only [mul_assoc, mul_comm b] at ⊢ hx,
+    intros y hy,
+    exact hx _ (fractional_ideal.mul_mem_mul hy hb) },
+  -- It turns out the subalgebra consisting of all `p(x)` for `p : polynomial A` works.
+  refine ⟨alg_hom.range (polynomial.aeval x : polynomial A →ₐ[A] K),
+          is_noetherian_submodule.mp (fractional_ideal.is_noetherian I⁻¹) _ (λ y hy, _),
+          ⟨polynomial.X, polynomial.aeval_X x⟩⟩,
+  obtain ⟨p, rfl⟩ := (alg_hom.mem_range _).mp hy,
+  rw polynomial.aeval_eq_sum_range,
+  refine submodule.sum_mem _ (λ i hi, submodule.smul_mem _ _ _),
+  clear hi,
+  induction i with i ih,
+  { rw pow_zero, exact one_mem_inv_coe_ideal hI0 },
+  { show x ^ i.succ ∈ (I⁻¹ : fractional_ideal A⁰ K),
+    rw pow_succ, exact x_mul_mem _ ih },
+end
+
+/-- Nonzero fractional ideals in a Dedekind domain are units. -/
+theorem mul_inv_cancel [is_dedekind_domain A]
+  {I : fractional_ideal A⁰ K} (hne : I ≠ 0) : I * I⁻¹ = 1 :=
+begin
+  obtain ⟨a, J, ha, hJ⟩ :
+    ∃ (a : A) (aI : ideal A), a ≠ 0 ∧ I = span_singleton A⁰ (algebra_map _ _ a)⁻¹ * aI :=
+    exists_eq_span_singleton_mul I,
+  suffices h₂ : I * (span_singleton A⁰ (algebra_map _ _ a) * J⁻¹) = 1,
+  { rw mul_inv_cancel_iff,
+    exact ⟨span_singleton A⁰ (algebra_map _ _ a) * J⁻¹, h₂⟩ },
+  subst hJ,
+  rw [mul_assoc, mul_left_comm (J : fractional_ideal A⁰ K), coe_ideal_mul_inv, mul_one,
+      fractional_ideal.span_singleton_mul_span_singleton, inv_mul_cancel,
+      fractional_ideal.span_singleton_one],
+  { exact mt ((algebra_map A K).injective_iff.mp (is_fraction_ring.injective A K) _) ha },
+  { exact fractional_ideal.coe_ideal_ne_zero_iff.mp (right_ne_zero_of_mul hne) }
+end
+
+end fractional_ideal
+
+/-- `is_dedekind_domain` and `is_dedekind_domain_inv` are equivalent ways
+to express that an integral domain is a Dedekind domain. -/
+theorem is_dedekind_domain_iff_is_dedekind_domain_inv :
+  is_dedekind_domain A ↔ is_dedekind_domain_inv A :=
+⟨λ h I hI, by exactI fractional_ideal.mul_inv_cancel hI, λ h, h.is_dedekind_domain⟩
+
+noncomputable instance fractional_ideal.comm_group_with_zero
+  [is_dedekind_domain A] : comm_group_with_zero (fractional_ideal A⁰ K) :=
+{ inv := λ I, I⁻¹,
+  inv_zero := inv_zero' _,
+  exists_pair_ne := ⟨0, 1, (coe_to_fractional_ideal_injective (le_refl _)).ne
+    (by simpa using @zero_ne_one (ideal A) _ _)⟩,
+  mul_inv_cancel := λ I, fractional_ideal.mul_inv_cancel,
+  .. fractional_ideal.comm_semiring }
+
 end inverse

src/ring_theory/fractional_ideal.lean

@@ -944,6 +944,33 @@ by rw [map_div, map_one]
 
 end quotient
 
+section field
+
+variables {R₁ K L : Type*} [integral_domain R₁] [field K] [field L]
+variables [algebra R₁ K] [is_fraction_ring R₁ K] [algebra K L] [is_fraction_ring K L]
+
+lemma eq_zero_or_one (I : fractional_ideal K⁰ L) : I = 0 ∨ I = 1 :=
+begin
+  rw or_iff_not_imp_left,
+  intro hI,
+  simp_rw [@set_like.ext_iff _ _ _ I 1, fractional_ideal.mem_one_iff],
+  intro x,
+  split,
+  { intro x_mem,
+    obtain ⟨n, d, rfl⟩ := is_localization.mk'_surjective K⁰ x,
+    refine ⟨n / d, _⟩,
+    rw [ring_hom.map_div, is_fraction_ring.mk'_eq_div] },
+  { rintro ⟨x, rfl⟩,
+    obtain ⟨y, y_ne, y_mem⟩ := fractional_ideal.exists_ne_zero_mem_is_integer hI,
+    rw [← div_mul_cancel x y_ne, ring_hom.map_mul, ← algebra.smul_def],
+    exact submodule.smul_mem I _ y_mem }
+end
+
+lemma eq_zero_or_one_of_is_field (hF : is_field R₁) (I : fractional_ideal R₁⁰ K) : I = 0 ∨ I = 1 :=
+by { letI : field R₁ := hF.to_field R₁, exact eq_zero_or_one I }
+
+end field
+
 section principal_ideal_ring
 
 variables {R₁ : Type*} [integral_domain R₁] {K : Type*} [field K]