feat(ring_theory/fractional_ideal): move inv to dedekind_domain (#5053)

Remove all instances of `inv` and I^{-1}. The notation (1 / I) is the one used for the old I^{-1}.



Co-authored-by: faenuccio <65080144+faenuccio@users.noreply.github.com>
Co-authored-by: Filippo A. E. Nuccio <65080144+faenuccio@users.noreply.github.com>

src/ring_theory/dedekind_domain.lean

@@ -18,10 +18,10 @@ giving three equivalent definitions (TODO: and shows that they are equivalent).
  - `is_dedekind_domain` defines a Dedekind domain as a commutative ring that is not a field,
    Noetherian, integrally closed in its field of fractions and has Krull dimension exactly one.
    `is_dedekind_domain_iff` shows that this does not depend on the choice of field of fractions.
- - `is_dedekind_domain_dvr` alternatively defines a Dedekind domain as an integral domain that is not a field,
-   Noetherian, and the localization at every nonzero prime ideal is a discrete valuation ring.
- - `is_dedekind_domain_inv` alternatively defines a Dedekind domain as an integral domain that is not a field,
-   and every nonzero fractional ideal is invertible.
+ - `is_dedekind_domain_dvr` alternatively defines a Dedekind domain as an integral domain that
+   is not a field, Noetherian, and the localization at every nonzero prime ideal is a DVR.
+ - `is_dedekind_domain_inv` alternatively defines a Dedekind domain as an integral domain that
+   is not a field, and every nonzero fractional ideal is invertible.
  - `is_dedekind_domain_inv_iff` shows that this does note depend on the choice of field of fractions.
 
 ## Implementation notes
@@ -81,8 +81,8 @@ class is_dedekind_domain : Prop :=
 (dimension_le_one : dimension_le_one A)
 (is_integrally_closed : integral_closure A (fraction_ring A) = ⊥)
 
-/-- 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.
+/-- 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. -/
 lemma is_dedekind_domain_iff (f : fraction_map A K) :
   is_dedekind_domain A ↔
@@ -96,8 +96,8 @@ lemma is_dedekind_domain_iff (f : fraction_map A K) :
          hi, algebra.map_bot]⟩⟩
 
 /--
-A Dedekind domain is an integral domain that is not a field, is Noetherian, and the localization at
-every nonzero prime is a discrete valuation ring.
+A Dedekind domain is an integral domain that is not a field, is Noetherian, and the
+localization at every nonzero prime is a discrete valuation ring.
 
 This is equivalent to `is_dedekind_domain`.
 TODO: prove the equivalence.
@@ -108,33 +108,144 @@ structure is_dedekind_domain_dvr : Prop :=
 (is_dvr_at_nonzero_prime : ∀ P ≠ (⊥ : ideal A), P.is_prime →
   discrete_valuation_ring (localization.at_prime P))
 
+section inverse
+
+open_locale classical
+
+variables {R₁ : Type*} [integral_domain R₁] {g : fraction_map R₁ K}
+variables {I J : fractional_ideal g}
+
+noncomputable instance : has_inv (fractional_ideal g) := ⟨λ I, 1 / I⟩
+
+lemma inv_eq : I⁻¹ = 1 / I := rfl
+
+lemma inv_zero' : (0 : fractional_ideal g)⁻¹ = 0 := fractional_ideal.div_zero
+
+lemma inv_nonzero {J : fractional_ideal g} (h : J ≠ 0) :
+J⁻¹ = ⟨(1 : fractional_ideal g) / J, fractional_ideal.fractional_div_of_nonzero h⟩ :=
+fractional_ideal.div_nonzero _
+
+lemma coe_inv_of_nonzero {J : fractional_ideal g} (h : J ≠ 0) :
+  (↑J⁻¹ : submodule R₁ g.codomain) = g.coe_submodule 1 / J :=
+by { rwa inv_nonzero _, refl, assumption}
+
+/-- `I⁻¹` is the inverse of `I` if `I` has an inverse. -/
+theorem right_inverse_eq (I J : fractional_ideal g) (h : I * J = 1) :
+  J = I⁻¹ :=
+begin
+  have hI : I ≠ 0 := fractional_ideal.ne_zero_of_mul_eq_one I J h,
+  suffices h' : I * (1 / I) = 1,
+  { exact (congr_arg units.inv $
+      @units.ext _ _ (units.mk_of_mul_eq_one _ _ h) (units.mk_of_mul_eq_one _ _ h') rfl) },
+  apply le_antisymm,
+  { apply fractional_ideal.mul_le.mpr _,
+    intros x hx y hy,
+    rw mul_comm,
+    exact (fractional_ideal.mem_div_iff_of_nonzero hI).mp hy x hx },
+  rw ← h,
+  apply fractional_ideal.mul_left_mono I,
+  apply (fractional_ideal.le_div_iff_of_nonzero hI).mpr _,
+  intros y hy x hx,
+  rw mul_comm,
+  exact fractional_ideal.mul_mem_mul hx hy
+end
+
+theorem mul_inv_cancel_iff {I : fractional_ideal g} :
+  I * I⁻¹ = 1 ↔ ∃ J, I * J = 1 :=
+⟨λ h, ⟨I⁻¹, h⟩, λ ⟨J, hJ⟩, by rwa [← @right_inverse_eq _ _ _ _ _ I J hJ]⟩
+
+variables {K' : Type*} [field K'] {g' : fraction_map R₁ K'}
+
+@[simp] lemma map_inv (I : fractional_ideal g) (h : g.codomain ≃ₐ[R₁] g'.codomain) :
+  (I⁻¹).map (h : g.codomain →ₐ[R₁] g'.codomain) = (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 : g.codomain) :
+  (fractional_ideal.span_singleton x)⁻¹ = fractional_ideal.span_singleton (x⁻¹) :=
+fractional_ideal.one_div_span_singleton x
+
+lemma mul_generator_self_inv (I : fractional_ideal g)
+  [submodule.is_principal (I : submodule R₁ g.codomain)] (h : I ≠ 0) :
+  I * fractional_ideal.span_singleton (generator (I : submodule R₁ g.codomain))⁻¹ = 1 :=
+begin
+  -- Rewrite only the `I` that appears alone.
+  conv_lhs { congr, rw fractional_ideal.eq_span_singleton_of_principal I },
+  rw [fractional_ideal.span_singleton_mul_span_singleton, mul_inv_cancel,
+    fractional_ideal.span_singleton_one],
+  intro generator_I_eq_zero,
+  apply h,
+  rw [fractional_ideal.eq_span_singleton_of_principal I, generator_I_eq_zero,
+    fractional_ideal.span_singleton_zero]
+end
+
+lemma invertible_of_principal (I : fractional_ideal g)
+  [submodule.is_principal (I : submodule R₁ g.codomain)] (h : I ≠ 0) :
+  I * I⁻¹ = 1 :=
+(fractional_ideal.mul_div_self_cancel_iff).mpr
+  ⟨fractional_ideal.span_singleton (generator (I : submodule R₁ g.codomain))⁻¹,
+    @mul_generator_self_inv _ _ _ _ _ I _ h⟩
+
+lemma invertible_iff_generator_nonzero (I : fractional_ideal g)
+  [submodule.is_principal (I : submodule R₁ g.codomain)] :
+  I * I⁻¹ = 1 ↔ generator (I : submodule R₁ g.codomain) ≠ 0 :=
+begin
+  split,
+  { intros hI hg,
+    apply fractional_ideal.ne_zero_of_mul_eq_one _ _ hI,
+    rw [fractional_ideal.eq_span_singleton_of_principal I, hg,
+        fractional_ideal.span_singleton_zero] },
+  { intro hg,
+    apply invertible_of_principal,
+    rw [fractional_ideal.eq_span_singleton_of_principal I],
+    intro hI,
+    have := fractional_ideal.mem_span_singleton_self (generator (I : submodule R₁ g.codomain)),
+    rw [hI, fractional_ideal.mem_zero_iff] at this,
+    contradiction }
+end
+
+lemma is_principal_inv (I : fractional_ideal g)
+  [submodule.is_principal (I : submodule R₁ g.codomain)] (h : I ≠ 0) :
+  submodule.is_principal (I⁻¹).1 :=
+begin
+  rw [fractional_ideal.val_eq_coe, fractional_ideal.is_principal_iff],
+  use (generator (I : submodule R₁ g.codomain))⁻¹,
+  have hI : I  * fractional_ideal.span_singleton ((generator (I : submodule R₁ g.codomain))⁻¹)  = 1,
+  apply @mul_generator_self_inv _ _ _ _ _ I _ h,
+  apply (@right_inverse_eq _ _ _ _ _ I (fractional_ideal.span_singleton
+    ( (generator (I : submodule R₁ g.codomain))⁻¹)) hI).symm,
+end
+
 /--
-A Dedekind domain is an integral domain that is not a field such that every fractional ideal has an inverse.
+A Dedekind domain is an integral domain that is not a field such that every fractional ideal
+has an inverse.
 
 This is equivalent to `is_dedekind_domain`.
 TODO: prove the equivalence.
 -/
 structure is_dedekind_domain_inv : Prop :=
 (not_is_field : ¬ is_field A)
-(mul_inv_cancel : ∀ I ≠ (⊥ : fractional_ideal (fraction_ring.of A)), I * I⁻¹ = 1)
-
-section
+(mul_inv_cancel : ∀ I ≠ (⊥ : fractional_ideal (fraction_ring.of A)), I * (1 / I) = 1)
 
 open ring.fractional_ideal
 
 lemma is_dedekind_domain_inv_iff (f : fraction_map A K) :
   is_dedekind_domain_inv A ↔
     (¬ is_field A) ∧ (∀ I ≠ (⊥ : fractional_ideal f), I * I⁻¹ = 1) :=
 begin
+  set h : (fraction_ring.of A).codomain ≃ₐ[A] f.codomain := fraction_ring.alg_equiv_of_quotient f,
   split; rintros ⟨hf, hi⟩; use hf; intros I hI,
-  { have := hi (map (fraction_ring.alg_equiv_of_quotient f).symm.to_alg_hom I) (map_ne_zero _ hI),
-    erw [← map_inv, ← fractional_ideal.map_mul] at this,
-    convert congr_arg (map (fraction_ring.alg_equiv_of_quotient f).to_alg_hom) this;
-      simp only [alg_equiv.to_alg_hom_eq_coe, map_symm_map, map_one] },
-  { have := hi (map (fraction_ring.alg_equiv_of_quotient f).to_alg_hom I) (map_ne_zero _ hI),
-    erw [← map_inv, ← fractional_ideal.map_mul] at this,
-    convert congr_arg (map (fraction_ring.alg_equiv_of_quotient f).symm.to_alg_hom) this;
-      simp only [alg_equiv.to_alg_hom_eq_coe, map_map_symm, map_one] }
+  { have := hi (map ↑h.symm I) (map_ne_zero _ hI),
+    convert congr_arg (map (h : (fraction_ring.of A).codomain →ₐ[A] f.codomain)) this;
+      simp only [map_symm_map, map_one, fractional_ideal.map_mul, fractional_ideal.map_div,
+                 inv_eq] },
+  { have := hi (map ↑h I) (map_ne_zero _ hI),
+    convert congr_arg (map (h.symm : f.codomain →ₐ[A] (fraction_ring.of A).codomain)) this;
+      simp only [map_map_symm, map_one, fractional_ideal.map_mul, fractional_ideal.map_div,
+                 inv_eq] },
 end
 
-end
+end inverse

src/ring_theory/fractional_ideal.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Anne Baanen
+Authors: Anne Baanen, Filippo A. E. Nuccio
 -/
 import ring_theory.localization
 import ring_theory.noetherian
@@ -31,7 +31,8 @@ Let `K` be the localization of `R` at `R \ {0}` and `g` the natural ring hom fro
 ## Main statements
 
   * `mul_left_mono` and `mul_right_mono` state that ideal multiplication is monotone
-  * `right_inverse_eq` states that `1 / I` is the inverse of `I` if one exists
+  * `prod_one_self_div_eq` states that `1 / I` is the inverse of `I` if one exists
+  * `is_noetherian` states that very fractional ideal of a noetherian integral domain is noetherian
 
 ## Implementation notes
 
@@ -719,10 +720,6 @@ noncomputable instance fractional_ideal_has_div :
 
 variables {I J : fractional_ideal g} [ J ≠ 0 ]
 
-noncomputable instance : has_inv (fractional_ideal g) := ⟨λ I, 1 / I⟩
-
-lemma inv_eq {I : fractional_ideal g} : I⁻¹ = 1 / I := rfl
-
 @[simp] lemma div_zero {I : fractional_ideal g} :
   I / 0 = 0 :=
 dif_pos rfl
@@ -731,12 +728,6 @@ lemma div_nonzero {I J : fractional_ideal g} (h : J ≠ 0) :
   (I / J) = ⟨I.1 / J.1, fractional_div_of_nonzero h⟩ :=
 dif_neg h
 
-lemma inv_zero : (0 : fractional_ideal g)⁻¹ = 0 := div_zero
-
-lemma inv_nonzero {I : fractional_ideal g} (h : I ≠ 0) :
-  I⁻¹ = ⟨(1 : fractional_ideal g) / I, fractional_div_of_nonzero h⟩ :=
-div_nonzero h
-
 @[simp] lemma coe_div {I J : fractional_ideal g} (hJ : J ≠ 0) :
   (↑(I / J) : submodule R₁ g.codomain) = ↑I / (↑J : submodule R₁ g.codomain) :=
 begin
@@ -780,10 +771,6 @@ begin
   refl,
 end
 
-lemma coe_inv_of_nonzero {I : fractional_ideal g} (h : I ≠ 0) :
-  (↑I⁻¹ : submodule R₁ g.codomain) = g.coe_submodule 1 / I :=
-by { rw inv_nonzero h, refl }
-
 @[simp] lemma div_one {I : fractional_ideal g} : I / 1 = I :=
 begin
   rw [div_nonzero (@one_ne_zero (fractional_ideal g) _ _)],
@@ -802,9 +789,9 @@ end
 lemma ne_zero_of_mul_eq_one (I J : fractional_ideal g) (h : I * J = 1) : I ≠ 0 :=
 λ hI, @zero_ne_one (fractional_ideal g) _ _ (by { convert h, simp [hI], })
 
-/-- `I⁻¹` is the inverse of `I` if `I` has an inverse. -/
-theorem right_inverse_eq (I J : fractional_ideal g) (h : I * J = 1) :
-  J = I⁻¹ :=
+
+theorem eq_one_div_of_mul_eq_one (I J : fractional_ideal g) (h : I * J = 1) :
+  J = 1 / I :=
 begin
   have hI : I ≠ 0 := ne_zero_of_mul_eq_one I J h,
   suffices h' : I * (1 / I) = 1,
@@ -820,12 +807,12 @@ begin
   apply (le_div_iff_of_nonzero hI).mpr _,
   intros y hy x hx,
   rw mul_comm,
-  exact mul_mem_mul hx hy
+  exact mul_mem_mul hx hy,
 end
 
-theorem mul_inv_cancel_iff {I : fractional_ideal g} :
-  I * I⁻¹ = 1 ↔ ∃ J, I * J = 1 :=
-⟨λ h, ⟨I⁻¹, h⟩, λ ⟨J, hJ⟩, by rwa [←right_inverse_eq I J hJ]⟩
+theorem mul_div_self_cancel_iff {I : fractional_ideal g} :
+  I * (1 / I) = 1 ↔ ∃ J, I * J = 1 :=
+⟨λ h, ⟨(1 / I), h⟩, λ ⟨J, hJ⟩, by rwa [← eq_one_div_of_mul_eq_one I J hJ]⟩
 
 variables {K' : Type*} [field K'] {g' : fraction_map R₁ K'}
 
@@ -838,9 +825,9 @@ begin
     simp [div_nonzero H, div_nonzero (map_ne_zero _ H), submodule.map_div] }
 end
 
-@[simp] lemma map_inv (I : fractional_ideal g) (h : g.codomain ≃ₐ[R₁] g'.codomain) :
-  (I⁻¹).map (h : g.codomain →ₐ[R₁] g'.codomain) = (I.map h)⁻¹ :=
-by rw [inv_eq, map_div, map_one, inv_eq]
+@[simp] lemma map_one_div (I : fractional_ideal g) (h : g.codomain ≃ₐ[R₁] g'.codomain) :
+  (1 / I).map (h : g.codomain →ₐ[R₁] g'.codomain) = 1 / I.map h :=
+by rw [map_div, map_one]
 
 end quotient
 
@@ -968,57 +955,11 @@ begin
     exact mul_mem_mul (mem_span_singleton.mpr ⟨1, one_smul _ _⟩) hy' }
 end
 
-lemma mul_generator_self_inv (I : fractional_ideal g)
-  [submodule.is_principal (I : submodule R₁ g.codomain)] (h : I ≠ 0) :
-  I * span_singleton (generator (I : submodule R₁ g.codomain))⁻¹ = 1 :=
-begin
-  -- Rewrite only the `I` that appears alone.
-  conv_lhs { congr, rw eq_span_singleton_of_principal I },
-  rw [span_singleton_mul_span_singleton, mul_inv_cancel, span_singleton_one],
-  intro generator_I_eq_zero,
-  apply h,
-  rw [eq_span_singleton_of_principal I, generator_I_eq_zero, span_singleton_zero]
-end
-
 lemma one_div_span_singleton (x : g.codomain) :
   1 / span_singleton x = span_singleton (x⁻¹) :=
-if h : x = 0 then by simp [h] else (right_inverse_eq _ _ (by simp [h])).symm
-
-@[simp]
-lemma span_singleton_inv (x : g.codomain) :
-  (span_singleton x)⁻¹ = span_singleton (x⁻¹) :=
-one_div_span_singleton x
-
-lemma invertible_of_principal (I : fractional_ideal g)
-  [submodule.is_principal (I : submodule R₁ g.codomain)] (h : I ≠ 0) :
-  I * I⁻¹ = 1 :=
-mul_inv_cancel_iff.mpr
-  ⟨span_singleton (generator (I : submodule R₁ g.codomain))⁻¹, mul_generator_self_inv I h⟩
-
-lemma invertible_iff_generator_nonzero (I : fractional_ideal g)
-  [submodule.is_principal (I : submodule R₁ g.codomain)] :
-  I * I⁻¹ = 1 ↔ generator (I : submodule R₁ g.codomain) ≠ 0 :=
-begin
-  split,
-  { intros hI hg,
-    apply ne_zero_of_mul_eq_one _ _ hI,
-    rw [eq_span_singleton_of_principal I, hg, span_singleton_zero] },
-  { intro hg,
-    apply invertible_of_principal,
-    rw [eq_span_singleton_of_principal I],
-    intro hI,
-    have := mem_span_singleton_self (generator (I : submodule R₁ g.codomain)),
-    rw [hI, mem_zero_iff] at this,
-    contradiction }
-end
+if h : x = 0 then by simp [h] else (eq_one_div_of_mul_eq_one _ _ (by simp [h])).symm
 
-lemma is_principal_inv (I : fractional_ideal g)
-  [submodule.is_principal (I : submodule R₁ g.codomain)] (h : I ≠ 0) :
-  submodule.is_principal (I⁻¹).1 :=
-I⁻¹.is_principal_iff.mpr ⟨_, (right_inverse_eq _ _ (mul_generator_self_inv I h)).symm⟩
-
-@[simp]
-lemma div_span_singleton (J : fractional_ideal g) (d : g.codomain) :
+@[simp] lemma div_span_singleton (J : fractional_ideal g) (d : g.codomain) :
   J / span_singleton d = span_singleton (d⁻¹) * J :=
 begin
   rw ← one_div_span_singleton,
@@ -1096,7 +1037,7 @@ begin
   exact fg_map (is_noetherian.noetherian J),
 end
 
-lemma is_noetherian_span_singleton_to_map_inv_mul (x : R₁) {I : fractional_ideal g}
+lemma is_noetherian_span_singleton_inv_to_map_mul (x : R₁) {I : fractional_ideal g}
   (hI : is_noetherian R₁ I) :
   is_noetherian R₁ (span_singleton (g.to_map x)⁻¹ * I : fractional_ideal g) :=
 begin
@@ -1119,10 +1060,10 @@ begin
 end
 
 /-- Every fractional ideal of a noetherian integral domain is noetherian. -/
-lemma is_noetherian [is_noetherian_ring R₁] (I : fractional_ideal g) : is_noetherian R₁ I :=
+theorem is_noetherian [is_noetherian_ring R₁] (I : fractional_ideal g) : is_noetherian R₁ I :=
 begin
   obtain ⟨d, J, h_nzd, rfl⟩ := exists_eq_span_singleton_mul I,
-  apply is_noetherian_span_singleton_to_map_inv_mul,
+  apply is_noetherian_span_singleton_inv_to_map_mul,
   apply is_noetherian_coe_to_fractional_ideal,
 end