feat(RingTheory): regular local ring is domain

Mathlib.lean

@@ -6673,6 +6673,7 @@ public import Mathlib.RingTheory.Regular.Depth
 public import Mathlib.RingTheory.Regular.Flat
 public import Mathlib.RingTheory.Regular.IsSMulRegular
 public import Mathlib.RingTheory.Regular.RegularSequence
+public import Mathlib.RingTheory.RegularLocalRing.Basic
 public import Mathlib.RingTheory.RegularLocalRing.Defs
 public import Mathlib.RingTheory.RingHom.Bijective
 public import Mathlib.RingTheory.RingHom.EssFiniteType

Mathlib/Algebra/Module/SpanRank.lean

@@ -266,6 +266,18 @@ lemma spanFinrank_singleton {m : M} (hm : m ≠ 0) : (span R {m}).spanFinrank =
   · by_contra!
     simp [Submodule.spanFinrank_eq_zero_iff_eq_bot (fg_span_singleton m), hm] at this
 
+lemma spanFinrank_eq_one_iff (p : Submodule R M) : p.spanFinrank = 1 ↔ p.IsPrincipal ∧ p ≠ ⊥ := by
+  refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨prin, ne⟩ ↦ ?_⟩
+  · have fg : p.FG := by
+      contrapose h
+      simp [Submodule.spanFinrank_of_not_fg h]
+    obtain ⟨a, ha⟩ : ∃ a, p.generators = {a} := by simpa [← fg.generators_ncard] using h
+    exact ⟨a, ha ▸ (p.span_generators).symm⟩
+  · aesop
+  · rcases prin with ⟨a, rfl⟩
+    apply Submodule.spanFinrank_singleton
+    aesop
+
 end Defs
 
 end Submodule

Mathlib/RingTheory/Filtration.lean

@@ -447,6 +447,14 @@ theorem Ideal.isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing {R} [CommRing R]
     rintro (_ | n) <;> simp [H.pow_succ_eq]
   · rintro (rfl | rfl) <;> simp [IsIdempotentElem]
 
+variable (R) in
+lemma IsLocalRing.maximalIdeal_sq_lt_maximalIdeal [IsLocalRing R] [IsNoetherianRing R] :
+    maximalIdeal R ^ 2 < maximalIdeal R ↔ ¬ IsField R := by
+  trans ¬ IsIdempotentElem (maximalIdeal R)
+  · simp [IsIdempotentElem, ← pow_two, lt_iff_le_and_ne, Ideal.pow_le_self]
+  · simp [Ideal.isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing, Ideal.IsPrime.ne_top,
+      isField_iff_maximalIdeal_eq]
+
 open IsLocalRing in
 theorem Ideal.iInf_pow_smul_eq_bot_of_isTorsionFree [IsDomain R]
     [IsNoetherianRing R] [Module.IsTorsionFree R M]

Mathlib/RingTheory/Ideal/AssociatedPrime/Localization.lean

@@ -131,10 +131,11 @@ variable (R M) in
 lemma minimalPrimes_annihilator_subset_associatedPrimes [IsNoetherianRing R] [Module.Finite R M] :
     (Module.annihilator R M).minimalPrimes ⊆ associatedPrimes R M := by
   intro p hp
-  have prime := hp.1.1
+  have prime := Ideal.minimalPrimes_isPrime hp
   let Rₚ := Localization.AtPrime p
   have : Nontrivial (LocalizedModule p.primeCompl M) := by
-    simpa [← Module.mem_support_iff (p := ⟨p, prime⟩), Module.support_eq_zeroLocus] using hp.1.2
+    simpa [← Module.mem_support_iff (p := ⟨p, prime⟩), Module.support_eq_zeroLocus] using
+      Ideal.le_minimalPrimes hp
   rcases associatedPrimes.nonempty Rₚ (LocalizedModule p.primeCompl M) with ⟨q, hq⟩
   have q_prime : q.IsPrime := IsAssociatedPrime.isPrime hq
   simp only [← preimage_comap_associatedPrimes_eq_associatedPrimes_of_isLocalizedModule p.primeCompl

Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean

@@ -83,7 +83,7 @@ lemma Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing
     ← (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q)).map_rel_iff]
   refine Submodule.le_of_le_smul_of_le_jacobson_bot (I := I) (IsNoetherian.noetherian _) ?_ ?_
   · rw [IsLocalRing.jacobson_eq_maximalIdeal]
-    exacts [hp.1.2, bot_ne_top]
+    exacts [Ideal.le_minimalPrimes hp, bot_ne_top]
   · replace hn := congr(Ideal.comap (Ideal.Quotient.mk I) $(hn _ n.le_succ))
     simp only [qs, OrderHom.coe_mk, ← RingHom.ker_eq_comap_bot, Ideal.mk_ker,
       Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective] at hn
@@ -106,7 +106,7 @@ lemma Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing
   has height at most 1. -/
 lemma Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes
     (I : Ideal R) [I.IsPrincipal] (p : Ideal R) (hp : p ∈ I.minimalPrimes) : p.height ≤ 1 := by
-  have := hp.1.1
+  have := Ideal.minimalPrimes_isPrime hp
   let f := algebraMap R (Localization.AtPrime p)
   have := Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing (I.map f) ?_
   · rwa [← IsLocalization.height_comap p.primeCompl,
@@ -117,14 +117,15 @@ lemma Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes
 theorem Ideal.map_height_le_one_of_mem_minimalPrimes {I p : Ideal R} {x : R}
     (hp : p ∈ (I ⊔ span {x}).minimalPrimes) : (p.map (Ideal.Quotient.mk I)).height ≤ 1 :=
   let f := Ideal.Quotient.mk I
-  have : p.IsPrime := hp.1.1
-  have hfp : RingHom.ker f ≤ p := I.mk_ker.trans_le (le_sup_left.trans hp.1.2)
+  have : p.IsPrime := Ideal.minimalPrimes_isPrime hp
+  have hfp : RingHom.ker f ≤ p := I.mk_ker.trans_le (le_sup_left.trans (Ideal.le_minimalPrimes hp))
   height_le_one_of_isPrincipal_of_mem_minimalPrimes ((span {x}).map f) (p.map f)
-    ⟨⟨map_isPrime_of_surjective Quotient.mk_surjective hfp, map_mono (le_sup_right.trans hp.1.2)⟩,
-      fun _ ⟨hr, hxr⟩ hrp ↦ map_le_iff_le_comap.mpr <| hp.2 ⟨hr.comap f, sup_le_iff.mpr
-        ⟨I.mk_ker.symm.trans_le <| ker_le_comap (Ideal.Quotient.mk I), le_comap_of_map_le hxr⟩⟩ <|
-          (comap_mono hrp).trans <| Eq.le <|
-            (p.comap_map_of_surjective _ Quotient.mk_surjective).trans <| sup_eq_left.mpr hfp⟩
+    ⟨⟨map_isPrime_of_surjective Quotient.mk_surjective hfp,
+      map_mono (le_sup_right.trans (Ideal.le_minimalPrimes hp))⟩,
+        fun _ ⟨hr, hxr⟩ hrp ↦ map_le_iff_le_comap.mpr <| hp.2 ⟨hr.comap f, sup_le_iff.mpr
+          ⟨I.mk_ker.symm.trans_le <| ker_le_comap (Ideal.Quotient.mk I), le_comap_of_map_le hxr⟩⟩ <|
+            (comap_mono hrp).trans <| Eq.le <|
+              (p.comap_map_of_surjective _ Quotient.mk_surjective).trans <| sup_eq_left.mpr hfp⟩
 
 /-- If `q < p` are prime ideals such that `p` is minimal over `span (s ∪ {x})` and
 `t` is a set contained in `q` such that `s ⊆ √span (t ∪ {x})`, then `q` is minimal over `span t`.
@@ -145,14 +146,14 @@ theorem Ideal.mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert {q p : Ide
         sup_eq_left.mpr hI'q, sup_eq_left.mpr hI'p] using comap_mono (f := f) e
     have : (q.map f).IsPrime := map_isPrime_of_surjective hf (by rwa [mk_ker])
     have : (p.map f).FiniteHeight := ⟨Or.inr (h.trans_lt (WithTop.coe_lt_top 1)).ne⟩
-    rw [height_eq_primeHeight] at h
-    have := (primeHeight_strict_mono h_lt).trans_le h
-    rw [ENat.lt_one_iff_eq_zero, primeHeight_eq_zero_iff] at this
+    have := (height_strict_mono_of_isPrime_of_isPrime h_lt).trans_le h
+    rw [ENat.lt_one_iff_eq_zero, height_eq_zero_iff] at this
     have := minimal_primes_comap_of_surjective hf this
     rwa [comap_map_of_surjective f hf, ← RingHom.ker_eq_comap_bot,
       mk_ker, sup_eq_left.mpr hI'q] at this
   refine height_le_one_of_isPrincipal_of_mem_minimalPrimes ((span {x}).map f) (p.map f) ⟨⟨this,
-    map_mono <| span_le.mpr <| Set.singleton_subset_iff.mpr <| hp.1.2 <| subset_span <| .inl rfl⟩,
+    map_mono <| span_le.mpr <| Set.singleton_subset_iff.mpr <| (Ideal.le_minimalPrimes hp) <|
+      subset_span <| .inl rfl⟩,
     fun r ⟨hr, hxr⟩ hrp ↦ map_le_iff_le_comap.mpr (hp.2 ⟨hr.comap f, ?_⟩ ?_)⟩
   · rw [span_le, Set.insert_subset_iff]
     have := map_le_iff_le_comap.mp hxr (subset_span rfl)
@@ -176,11 +177,10 @@ nonrec lemma Ideal.height_le_spanRank_toENat_of_mem_minimal_primes
   induction hn : s.card using Nat.strong_induction_on generalizing R with
   | h n H =>
     replace hn : s.card ≤ n := hn.le
-    have := hp.1.1
+    have := Ideal.minimalPrimes_isPrime hp
     cases n with
     | zero =>
-      rw [ENat.coe_zero, nonpos_iff_eq_zero, height_eq_primeHeight p,
-        primeHeight_eq_zero_iff, minimalPrimes]
+      rw [ENat.coe_zero, nonpos_iff_eq_zero, height_eq_zero_iff, minimalPrimes]
       simp_all
     | succ n =>
       wlog hR : ∃ (_ : IsLocalRing R), p = maximalIdeal R
@@ -204,7 +204,7 @@ nonrec lemma Ideal.height_le_spanRank_toENat_of_mem_minimal_primes
           ⟨le_sup_left, x, mem_sup_right (mem_span_singleton_self _), hxq⟩).trans_le hJ)
           ((le_maximalIdeal hJ'.ne_top).lt_of_not_ge h)
       have h : (s' : Set R) ⊆ (q ⊔ span {x}).radical := by
-        have := hp.1.2.trans this
+        have := (Ideal.le_minimalPrimes hp).trans this
         rw [span_le, Finset.coe_insert, Set.insert_subset_iff] at this
         exact this.2
       obtain ⟨t, ht, hspan⟩ := exists_subset_radical_span_sup_of_subset_radical_sup _ _ _ h
@@ -239,7 +239,7 @@ lemma Ideal.height_le_spanRank_toENat (I : Ideal R) (hI : I ≠ ⊤) :
   obtain ⟨J, hJ⟩ := nonempty_minimalPrimes hI
   refine (iInf₂_le J hJ).trans ?_
   convert (I.height_le_spanRank_toENat_of_mem_minimal_primes J hJ)
-  exact Eq.symm (@height_eq_primeHeight _ _ J hJ.1.1)
+  exact Eq.symm (@height_eq_primeHeight _ _ J (Ideal.minimalPrimes_isPrime hJ))
 
 lemma Ideal.height_le_spanFinrank (I : Ideal R) (hI : I ≠ ⊤) :
     I.height ≤ I.spanFinrank := by
@@ -318,7 +318,8 @@ lemma Ideal.height_le_height_add_spanFinrank_of_le {I p : Ideal R} [p.IsPrime] (
   let p' := p.map (algebraMap R (R ⧸ I))
   have : p'.IsPrime := isPrime_map_quotientMk_of_isPrime hrp
   obtain ⟨s, hps, hs⟩ := exists_finset_card_eq_height_of_isNoetherianRing p'
-  have hsp' : (s : Set (R ⧸ I)) ⊆ (p' : Set _) := fun _ hx ↦ hps.1.2 (subset_span hx)
+  have hsp' : (s : Set (R ⧸ I)) ⊆ (p' : Set _) :=
+    fun _ hx ↦ (Ideal.le_minimalPrimes hps) (subset_span hx)
   have : Set.SurjOn (Ideal.Quotient.mk I) p s := by
     refine Set.SurjOn.mono subset_rfl hsp' fun x hx ↦ ?_
     obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
@@ -415,7 +416,7 @@ lemma Ideal.height_le_height_add_of_liesOver [IsNoetherianRing S] (p : Ideal R)
   let P' := P.map (Ideal.Quotient.mk <| p.map (algebraMap R S))
   obtain ⟨s', hP', heq'⟩ := P'.exists_finset_card_eq_height_of_isNoetherianRing
   have hsP'sub : (s' : Set <| S ⧸ (Ideal.map (algebraMap R S) p)) ⊆ (P' : Set <| S ⧸ _) :=
-    fun x hx ↦ hP'.1.2 (Ideal.subset_span hx)
+    fun x hx ↦ (Ideal.le_minimalPrimes hP') (Ideal.subset_span hx)
   have : Set.SurjOn (Ideal.Quotient.mk (p.map (algebraMap R S))) P s' := by
     refine Set.SurjOn.mono subset_rfl hsP'sub fun x hx ↦ ?_
     obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective x

Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean

@@ -54,6 +54,12 @@ variable {I J}
 theorem Ideal.minimalPrimes_isPrime {p : Ideal R} (h : p ∈ I.minimalPrimes) : p.IsPrime :=
   h.1.1
 
+theorem Ideal.le_minimalPrimes {p : Ideal R} (h : p ∈ I.minimalPrimes) : I ≤ p :=
+  h.1.2
+
+theorem minimalPrimes_isPrime {p : Ideal R} (h : p ∈ minimalPrimes R) : p.IsPrime :=
+  h.1.1
+
 theorem Ideal.exists_minimalPrimes_le [J.IsPrime] (e : I ≤ J) : ∃ p ∈ I.minimalPrimes, p ≤ J := by
   set S := { p : (Ideal R)ᵒᵈ | Ideal.IsPrime p ∧ I ≤ OrderDual.ofDual p }
   suffices h : ∃ m, OrderDual.toDual J ≤ m ∧ Maximal (· ∈ S) m by
@@ -117,17 +123,17 @@ theorem Ideal.minimalPrimes_eq_subsingleton (hI : I.IsPrimary) : I.minimalPrimes
   ext J
   constructor
   · exact fun H =>
-      let e := H.1.1.radical_le_iff.mpr H.1.2
+      let e := (Ideal.minimalPrimes_isPrime H).radical_le_iff.mpr (Ideal.le_minimalPrimes H)
       (H.2 ⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩ e).antisymm e
   · rintro (rfl : J = I.radical)
     exact ⟨⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩, fun _ H _ => H.1.radical_le_iff.mpr H.2⟩
 
 theorem Ideal.minimalPrimes_eq_subsingleton_self [I.IsPrime] : I.minimalPrimes = {I} := by
   ext J
-  constructor
-  · exact fun H => (H.2 ⟨inferInstance, rfl.le⟩ H.1.2).antisymm H.1.2
-  · rintro (rfl : J = I)
-    exact ⟨⟨inferInstance, rfl.le⟩, fun _ h _ => h.2⟩
+  refine ⟨fun H => (H.2 ⟨inferInstance, rfl.le⟩ (Ideal.le_minimalPrimes H)).antisymm
+    (Ideal.le_minimalPrimes H), ?_⟩
+  rintro (rfl : J = I)
+  exact ⟨⟨inferInstance, rfl.le⟩, fun _ h _ => h.2⟩
 
 variable (R) in
 theorem IsDomain.minimalPrimes_eq_singleton_bot [IsDomain R] :
@@ -144,7 +150,7 @@ theorem Ideal.minimalPrimes_top : (⊤ : Ideal R).minimalPrimes = ∅ := by
   ext p
   simp only [Set.notMem_empty, iff_false]
   intro h
-  exact h.1.1.ne_top (top_le_iff.mp h.1.2)
+  exact (Ideal.minimalPrimes_isPrime h).ne_top (top_le_iff.mp (Ideal.le_minimalPrimes h))
 
 theorem Ideal.minimalPrimes_eq_empty_iff (I : Ideal R) :
     I.minimalPrimes = ∅ ↔ I = ⊤ := by
@@ -163,7 +169,8 @@ lemma Ideal.mem_minimalPrimes_sup {R : Type*} [CommRing R] {p I J : Ideal R} [p.
     p ∈ (I ⊔ J).minimalPrimes := by
   refine ⟨⟨‹_›, ?_⟩, fun q ⟨_, hq⟩ hqp ↦ ?_⟩
   · rw [sup_le_iff]
-    exact ⟨hle, by simpa [hle] using Ideal.comap_mono (f := Ideal.Quotient.mk I) h.1.2⟩
+    refine ⟨hle, ?_⟩
+    simpa [hle] using Ideal.comap_mono (f := Ideal.Quotient.mk I) (Ideal.le_minimalPrimes h)
   · rw [sup_le_iff] at hq
     have h2 : p.map (Quotient.mk I) ≤ q.map (Quotient.mk I) :=
       h.2 ⟨isPrime_map_quotientMk_of_isPrime hq.1, map_mono hq.2⟩ (map_mono hqp)
@@ -183,7 +190,7 @@ lemma Ideal.map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes
   refine ⟨⟨inferInstance, sup_le_iff.mpr ?_⟩, fun q ⟨_, hleq⟩ hqle ↦ ?_⟩
   · refine ⟨?_, hJP⟩
     rw [Ideal.map_le_iff_le_comap, ← Ideal.under_def, ← Ideal.over_def P p]
-    exact hI.1.2
+    exact Ideal.le_minimalPrimes hI
   · simp only [sup_le_iff] at hleq
     have h1 : p.map (algebraMap R S) ≤ q := by
       rw [Ideal.map_le_iff_le_comap]

Mathlib/RingTheory/Ideal/MinimalPrime/Colon.lean

@@ -48,7 +48,8 @@ theorem exists_eq_colon_of_mem_minimalPrimes [IsNoetherianRing R]
     refine ⟨n, hn0, ((h.toFinset.erase I).inf id) ^ n, hn, ?_⟩
     have (K : Ideal R) (hKI : K ≤ I) (hK : K ∈ ann.minimalPrimes) : K = I :=
       le_antisymm hKI (hI.2 hK.1 hKI)
-    simpa [hI.1.1.pow_le_iff hn0, hI.1.1.inf_le', imp_not_comm, not_imp_not]
+    simpa [(Ideal.minimalPrimes_isPrime hI).pow_le_iff hn0,
+      (Ideal.minimalPrimes_isPrime hI).inf_le', imp_not_comm, not_imp_not]
   obtain ⟨hn0, J, hJ, hJI⟩ := Nat.find_spec key
   -- let `n` be minimal such that there exists an ideal `J` with `I ^ n * J ≤ ann` and `¬ J ≠ I`
   set n := Nat.find key
@@ -74,9 +75,7 @@ theorem exists_eq_colon_of_mem_minimalPrimes [IsNoetherianRing R]
   -- let `z` be the product of these finitely many `f y`'s
   let z := ∏ y ∈ s, f y
   -- then `z ∉ I`
-  have hz : z ∉ I := by
-    simp only [z, hI.1.1.prod_mem_iff, not_exists, not_and_or]
-    exact fun i ↦ Or.inr (h i)
+  have hz : z ∉ I := by simp [z, (Ideal.minimalPrimes_isPrime hI).prod_mem_iff, h]
   -- and `K ≤ colon N {z • x}`
   have hz' : K ≤ colon N {z • x} := by
     rw [← (map_injective_of_injective K.subtype_injective).eq_iff, map_subtype_top] at hs
@@ -92,11 +91,12 @@ theorem exists_eq_colon_of_mem_minimalPrimes [IsNoetherianRing R]
     simpa only [ann, mem_colon_singleton, mul_comm, mul_smul] using hz' hi
   -- but now `K = I ^ (n - 1) * J` contradicts the minimality of `n`
   have hK : I ^ (n - 1) * (J * Ideal.span {z}) ≤ ann ∧ ¬ J * Ideal.span {z} ≤ I := by
-    rw [← mul_assoc, hI.1.1.mul_le, not_or, Ideal.span_singleton_le_iff_mem]
+    rw [← mul_assoc, (Ideal.minimalPrimes_isPrime hI).mul_le, not_or,
+      Ideal.span_singleton_le_iff_mem]
     exact ⟨hz', hJI, hz⟩
   by_cases hn' : n - 1 = 0
   · simp [K, show n = 1 by grind] at hz'
-    exact (hK.2 (hz'.trans hI.1.2)).elim
+    exact (hK.2 (hz'.trans (Ideal.le_minimalPrimes hI))).elim
   · grind [Nat.find_min' key ⟨hn', J * Ideal.span {z}, hK⟩]
 
 end Submodule