refactor(RingTheory/Lasker): generalize from Ideal to Submodule

Mathlib/RingTheory/Ideal/IsPrimary.lean

@@ -67,39 +67,21 @@ theorem isPrimary_of_isMaximal_radical {I : Ideal R} (hi : IsMaximal (radical I)
       rw [add_le_iff, span_singleton_le_iff_mem, ← hm.isPrime.radical_le_iff] at hy
       exact Or.inr (hi.eq_of_le hm.ne_top hy.1 ▸ hy.2)
 
-theorem isPrimary_inf {I J : Ideal R} (hi : I.IsPrimary) (hj : J.IsPrimary)
+theorem IsPrimary.inf {I J : Ideal R} (hi : I.IsPrimary) (hj : J.IsPrimary)
     (hij : radical I = radical J) : (I ⊓ J).IsPrimary :=
-  isPrimary_iff.mpr
-  ⟨ne_of_lt <| lt_of_le_of_lt inf_le_left (lt_top_iff_ne_top.2 hi.1),
-   fun {x y} ⟨hxyi, hxyj⟩ => by
-    rw [radical_inf, hij, inf_idem]
-    rcases (isPrimary_iff.mp hi).2 hxyi with hxi | hyi
-    · rcases (isPrimary_iff.mp hj).2 hxyj with hxj | hyj
-      · exact Or.inl ⟨hxi, hxj⟩
-      · exact Or.inr hyj
-    · rw [hij] at hyi
-      exact Or.inr hyi⟩
-
-open Finset in
-lemma isPrimary_finset_inf {ι} {s : Finset ι} {f : ι → Ideal R} {i : ι} (hi : i ∈ s)
+  Submodule.IsPrimary.inf hi hj (by simpa)
+
+@[deprecated (since := "2025-01-19")]
+alias isPrimary_inf := IsPrimary.inf
+
+lemma isPrimary_finsetInf {ι} {s : Finset ι} {f : ι → Ideal R} {i : ι} (hi : i ∈ s)
     (hs : ∀ ⦃y⦄, y ∈ s → (f y).IsPrimary)
     (hs' : ∀ ⦃y⦄, y ∈ s → (f y).radical = (f i).radical) :
-    IsPrimary (s.inf f) := by
-  classical
-  induction s using Finset.induction_on generalizing i with
-  | empty => simp at hi
-  | insert a s ha IH =>
-    rcases s.eq_empty_or_nonempty with rfl | ⟨y, hy⟩
-    · simp only [insert_empty_eq, mem_singleton] at hi
-      simpa [hi] using hs
-    simp only [inf_insert]
-    have H : ∀ ⦃x : ι⦄, x ∈ s → (f x).radical = (f y).radical := by
-      intro x hx
-      rw [hs' (mem_insert_of_mem hx), hs' (mem_insert_of_mem hy)]
-    refine isPrimary_inf (hs (by simp)) (IH hy ?_ H) ?_
-    · intro x hx
-      exact hs (by simp [hx])
-    · rw [radical_finset_inf hy H, hs' (mem_insert_self _ _), hs' (mem_insert_of_mem hy)]
+    IsPrimary (s.inf f) :=
+  Submodule.isPrimary_finsetInf hi hs (by simpa)
+
+@[deprecated (since := "2026-01-19")]
+alias isPrimary_finset_inf := isPrimary_finsetInf
 
 lemma IsPrimary.comap {I : Ideal S} (hI : I.IsPrimary) (φ : R →+* S) : (I.comap φ).IsPrimary := by
   rw [isPrimary_iff] at hI ⊢

Mathlib/RingTheory/IsPrimary.lean

@@ -6,6 +6,7 @@ Authors: Yakov Pechersky
 module
 
 public import Mathlib.LinearAlgebra.Quotient.Basic
+public import Mathlib.RingTheory.Ideal.Colon
 public import Mathlib.RingTheory.Ideal.Operations
 
 /-!
@@ -49,10 +50,43 @@ variable {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M]
 protected def IsPrimary (S : Submodule R M) : Prop :=
   S ≠ ⊤ ∧ ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n : ℕ, (r ^ n • ⊤ : Submodule R M) ≤ S
 
-variable {S : Submodule R M}
+variable {S T : Submodule R M}
 
 lemma IsPrimary.ne_top (h : S.IsPrimary) : S ≠ ⊤ := h.left
 
+lemma IsPrimary.mem_or_mem (h : S.IsPrimary) {r : R} {m : M} (hrm : r • m ∈ S) :
+    m ∈ S ∨ r ∈ (S.colon ⊤).radical :=
+  h.right hrm
+
+protected lemma IsPrimary.inf (hS : S.IsPrimary) (hT : T.IsPrimary)
+    (h : (S.colon Set.univ).radical = (T.colon Set.univ).radical) :
+    (S ⊓ T).IsPrimary := by
+  obtain ⟨_, hS⟩ := hS
+  obtain ⟨_, hT⟩ := hT
+  refine ⟨by grind, fun ⟨hS', hT'⟩ ↦ ?_⟩
+  simp_rw [← mem_colon_iff_le, ← Ideal.mem_radical_iff, inf_colon, Ideal.radical_inf,
+    top_coe, h, inf_idem, mem_inf, and_or_right] at hS hT ⊢
+  exact ⟨hS hS', hT hT'⟩
+
+open Finset in
+lemma isPrimary_finsetInf {ι : Type*} {s : Finset ι} {f : ι → Submodule R M} {i : ι} (hi : i ∈ s)
+    (hs : ∀ ⦃y⦄, y ∈ s → (f y).IsPrimary)
+    (hs' : ∀ ⦃y⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) :
+    (s.inf f).IsPrimary := by
+  classical
+  induction s using Finset.induction_on generalizing i with
+  | empty => simp at hi
+  | insert a s ha IH =>
+    rcases s.eq_empty_or_nonempty with rfl | ⟨y, hy⟩
+    · simp only [insert_empty_eq, mem_singleton] at hi
+      simpa [hi] using hs
+    simp only [inf_insert]
+    have H ⦃x⦄ (hx : x ∈ s) : ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical := by
+      rw [hs' (mem_insert_of_mem hx), hs' (mem_insert_of_mem hy)]
+    refine IsPrimary.inf (hs (by simp)) (IH hy (fun x hx ↦ hs (by simp [hx])) H) ?_
+    rw [colon_finsetInf, Ideal.radical_finset_inf hy H,
+      hs' (mem_insert_self _ _), hs' (mem_insert_of_mem hy)]
+
 end CommSemiring
 
 section CommRing

Mathlib/RingTheory/Lasker.lean

@@ -24,8 +24,7 @@ public import Mathlib.RingTheory.Noetherian.Defs
 
 ## Implementation details
 
-There is a generalization for submodules that needs to be implemented.
-Also, one needs to prove that the radicals of minimal decompositions are independent of the
+One needs to prove that the radicals of minimal decompositions are independent of the
   precise decomposition.
 
 -/
@@ -34,20 +33,23 @@ Also, one needs to prove that the radicals of minimal decompositions are indepen
 
 section IsLasker
 
-variable (R : Type*) [CommSemiring R]
+open Ideal
+
+variable (R M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M]
 
 /-- A ring `R` satisfies `IsLasker R` when any `I : Ideal R` can be decomposed into
 finitely many primary ideals. -/
 def IsLasker : Prop :=
-  ∀ I : Ideal R, ∃ s : Finset (Ideal R), s.inf id = I ∧ ∀ ⦃J⦄, J ∈ s → J.IsPrimary
+  ∀ I : Submodule R M, ∃ s : Finset (Submodule R M), s.inf id = I ∧ ∀ ⦃J⦄, J ∈ s → J.IsPrimary
 
-variable {R}
+variable {R M}
 
-namespace Ideal
+namespace Submodule
 
-lemma decomposition_erase_inf [DecidableEq (Ideal R)] {I : Ideal R}
-    {s : Finset (Ideal R)} (hs : s.inf id = I) :
-    ∃ t : Finset (Ideal R), t ⊆ s ∧ t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → ¬ (t.erase J).inf id ≤ J) := by
+lemma decomposition_erase_inf [DecidableEq (Submodule R M)] {I : Submodule R M}
+    {s : Finset (Submodule R M)} (hs : s.inf id = I) :
+    ∃ t : Finset (Submodule R M), t ⊆ s ∧ t.inf id = I ∧
+      ∀ ⦃J⦄, J ∈ t → ¬ (t.erase J).inf id ≤ J := by
   induction s using Finset.eraseInduction with
   | H s IH =>
     by_cases! H : ∀ J ∈ s, ¬ (s.erase J).inf id ≤ J
@@ -60,19 +62,19 @@ lemma decomposition_erase_inf [DecidableEq (Ideal R)] {I : Ideal R}
 
 open scoped Function -- required for scoped `on` notation
 
-lemma isPrimary_decomposition_pairwise_ne_radical {I : Ideal R}
-    {s : Finset (Ideal R)} (hs : s.inf id = I) (hs' : ∀ ⦃J⦄, J ∈ s → J.IsPrimary) :
-    ∃ t : Finset (Ideal R), t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧
-      (t : Set (Ideal R)).Pairwise ((· ≠ ·) on radical) := by
+lemma isPrimary_decomposition_pairwise_ne_radical {I : Submodule R M}
+    {s : Finset (Submodule R M)} (hs : s.inf id = I) (hs' : ∀ ⦃J⦄, J ∈ s → J.IsPrimary) :
+    ∃ t : Finset (Submodule R M), t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧
+      (t : Set (Submodule R M)).Pairwise ((· ≠ ·) on fun J ↦ (J.colon Set.univ).radical) := by
   classical
-  refine ⟨(s.image (fun J ↦ {I ∈ s | I.radical = J.radical})).image fun t ↦ t.inf id,
-    ?_, ?_, ?_⟩
+  refine ⟨(s.image fun J ↦ {I ∈ s | (I.colon .univ).radical = (J.colon .univ).radical}).image
+    fun t ↦ t.inf id, ?_, ?_, ?_⟩
   · ext
     grind [Finset.inf_image, Submodule.mem_finsetInf]
   · simp only [Finset.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp,
     forall_apply_eq_imp_iff₂]
     intro J hJ
-    refine isPrimary_finset_inf (i := J) ?_ ?_ (by simp)
+    refine isPrimary_finsetInf (i := J) ?_ ?_ (by simp)
     · simp [hJ]
     · simp only [Finset.mem_filter, id_eq, and_imp]
       intro y hy
@@ -83,94 +85,110 @@ lemma isPrimary_decomposition_pairwise_ne_radical {I : Ideal R}
     obtain ⟨J', hJ', hJ⟩ := hJ
     simp only [Function.onFun, ne_eq]
     contrapose! hIJ
-    suffices I'.radical = J'.radical by
+    suffices (I'.colon Set.univ).radical = (J'.colon Set.univ).radical by
       rw [← hI, ← hJ, this]
-    · rw [← hI, radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ
-      rw [hIJ, ← hJ, radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq]
-
-lemma exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition [DecidableEq (Ideal R)]
-    {I : Ideal R} {s : Finset (Ideal R)} (hs : s.inf id = I) (hs' : ∀ ⦃J⦄, J ∈ s → J.IsPrimary) :
-    ∃ t : Finset (Ideal R), t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧
-      ((t : Set (Ideal R)).Pairwise ((· ≠ ·) on radical)) ∧
+    · rw [← hI, colon_finsetInf,
+        radical_finset_inf (i := I') (by simp [hI']) (by simp), id_eq] at hIJ
+      rw [hIJ, ← hJ, colon_finsetInf,
+        radical_finset_inf (i := J') (by simp [hJ']) (by simp), id_eq]
+
+lemma exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition
+    [DecidableEq (Submodule R M)] {I : Submodule R M} {s : Finset (Submodule R M)}
+    (hs : s.inf id = I) (hs' : ∀ ⦃J⦄, J ∈ s → J.IsPrimary) :
+    ∃ t : Finset (Submodule R M), t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧
+      ((t : Set (Submodule R M)).Pairwise ((· ≠ ·) on fun J ↦ (J.colon Set.univ).radical)) ∧
       (∀ ⦃J⦄, J ∈ t → ¬ (t.erase J).inf id ≤ J) := by
   obtain ⟨t, ht, ht', ht''⟩ := isPrimary_decomposition_pairwise_ne_radical hs hs'
   obtain ⟨u, hut, hu, hu'⟩ := decomposition_erase_inf ht
   exact ⟨u, hu, fun _ hi ↦ ht' (hut hi), ht''.mono hut, hu'⟩
 
-/-- A `Finset` of ideals is a maximal primary decomposition of `I` if the ideals intersect to `I`,
-are primary, have pairwise distinct radicals, and removing any ideal changes the intersection. -/
-structure IsMinimalPrimaryDecomposition [DecidableEq (Ideal R)]
-    (I : Ideal R) (t : Finset (Ideal R)) : Prop where
+/-- A `Finset` of submodules is a minimal primary decomposition of `I` if the submodules intersect
+to `I`, are primary, have pairwise distinct radicals of colons, and removing any submodule changes
+the intersection. -/
+structure IsMinimalPrimaryDecomposition [DecidableEq (Submodule R M)]
+    (I : Submodule R M) (t : Finset (Submodule R M)) where
   inf_eq : t.inf id = I
   primary : ∀ ⦃J⦄, J ∈ t → J.IsPrimary
-  distinct : (t : Set (Ideal R)).Pairwise ((· ≠ ·) on radical)
+  distinct : (t : Set (Submodule R M)).Pairwise ((· ≠ ·) on fun J ↦ (J.colon Set.univ).radical)
   minimal : ∀ ⦃J⦄, J ∈ t → ¬ (t.erase J).inf id ≤ J
 
-lemma IsLasker.exists_isMinimalPrimaryDecomposition [DecidableEq (Ideal R)]
-    (h : IsLasker R) (I : Ideal R) :
-    ∃ t : Finset (Ideal R), I.IsMinimalPrimaryDecomposition t := by
-  obtain ⟨s, hs₁, hs₂⟩ := h I
-  obtain ⟨t, h₁, h₂, h₃, h₄⟩ :=
-    exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition hs₁ hs₂
-  exact ⟨t, h₁, h₂, h₃, h₄⟩
+lemma IsLasker.exists_isMinimalPrimaryDecomposition [DecidableEq (Submodule R M)]
+    (h : IsLasker R M) (I : Submodule R M) :
+    ∃ t : Finset (Submodule R M), I.IsMinimalPrimaryDecomposition t := by
+  obtain ⟨s, hs1, hs2⟩ := h I
+  obtain ⟨t, h1, h2, h3, h4⟩ :=
+    exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition hs1 hs2
+  exact ⟨t, h1, h2, h3, h4⟩
+
+end Submodule
+
+@[deprecated (since := "2026-01-19")]
+alias Ideal.decomposition_erase_inf := Submodule.decomposition_erase_inf
+
+@[deprecated (since := "2026-01-19")]
+alias Ideal.isPrimary_decomposition_pairwise_ne_radical :=
+  Submodule.isPrimary_decomposition_pairwise_ne_radical
 
-@[deprecated (since := "2026-01-09")]
-alias IsLasker.minimal := IsLasker.exists_isMinimalPrimaryDecomposition
+@[deprecated (since := "2026-01-19")]
+alias Ideal.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition :=
+  Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition
 
-end Ideal
+@[deprecated (since := "2026-01-19")]
+alias Ideal.IsMinimalPrimaryDecomposition := Submodule.IsMinimalPrimaryDecomposition
+
+@[deprecated (since := "2026-01-19")]
+alias Ideal.IsLasker.exists_isMinimalPrimaryDecomposition :=
+  Submodule.IsLasker.exists_isMinimalPrimaryDecomposition
+
+@[deprecated (since := "2026-01-19")]
+alias Ideal.IsLasker.minimal := Submodule.IsLasker.exists_isMinimalPrimaryDecomposition
 
 end IsLasker
 
-namespace Ideal
+namespace Submodule
 
 section Noetherian
 
-variable {R : Type*} [CommRing R] [IsNoetherianRing R]
+open Pointwise
 
-lemma _root_.InfIrred.isPrimary {I : Ideal R} (h : InfIrred I) : I.IsPrimary := by
-  rw [Ideal.isPrimary_iff]
+variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherian R M]
+
+lemma _root_.InfIrred.isPrimary {I : Submodule R M} (h : InfIrred I) : I.IsPrimary := by
+  rw [Submodule.IsPrimary]
   refine ⟨h.ne_top, fun {a b} hab ↦ ?_⟩
-  let f : ℕ → Ideal R := fun n ↦ (I.colon (span {b ^ n}))
+  let f : ℕ → Submodule R M := fun n ↦
+  { carrier := {x | a ^ n • x ∈ I}
+    add_mem' hx hy := by simp [I.add_mem hx hy]
+    zero_mem' := by simp
+    smul_mem' x y h := by simp [smul_comm _ x, I.smul_mem x h] }
   have hf : Monotone f := by
-    intro n m hnm
-    simp_rw [f]
-    exact (Submodule.colon_mono le_rfl (Ideal.span_singleton_le_span_singleton.mpr
-      (pow_dvd_pow b hnm)))
+    intro n m hnm x hx
+    simpa [hnm, smul_smul, ← pow_add] using I.smul_mem (a ^ (m - n)) hx
   obtain ⟨n, hn⟩ := monotone_stabilizes_iff_noetherian.mpr ‹_› ⟨f, hf⟩
   rcases h with ⟨-, h⟩
-  specialize @h (I.colon (span {b ^ n})) (I + (span {b ^ n})) ?_
-  · refine le_antisymm (fun r ↦ ?_) (le_inf (fun _ ↦ ?_) ?_)
-    · simp only [Submodule.add_eq_sup, sup_comm I, mem_inf, mem_colon_span_singleton,
-        mem_span_singleton_sup, and_imp, forall_exists_index]
-      rintro hrb t s hs rfl
-      refine add_mem ?_ hs
-      have := hn (n + n) (by simp)
-      simp only [OrderHom.coe_mk, f] at this
-      rw [add_mul, mul_assoc, ← pow_add] at hrb
-      rwa [← mem_colon_span_singleton, this, mem_colon_span_singleton,
-           ← Ideal.add_mem_iff_left _ (Ideal.mul_mem_right _ _ hs)]
-    · simpa only [mem_colon_span_singleton] using mul_mem_right _ _
-    · simp
-  rcases h with (h | h)
-  · replace h : I = I.colon (span {b}) := by
-      rcases eq_or_ne n 0 with rfl | hn'
-      · simpa [f, ← Ideal.colon_span (R := R) (S := {1})] using hn 1 zero_le_one
-      refine le_antisymm ?_ (h.le.trans' (Submodule.colon_mono le_rfl ?_))
-      · intro
-        simpa only [mem_colon_span_singleton] using mul_mem_right _ _
-      · exact span_singleton_le_span_singleton.mpr (dvd_pow_self b hn')
-    rw [← mem_colon_span_singleton, ← h] at hab
-    exact Or.inl hab
-  · rw [← h]
-    refine Or.inr ⟨n, ?_⟩
-    simpa using mem_sup_right (mem_span_singleton_self _)
-
-variable (R) in
-/-- The Lasker--Noether theorem: every ideal in a Noetherian ring admits a decomposition into
-  primary ideals. -/
-lemma isLasker : IsLasker R := fun I ↦
+  specialize @h (f n) (I + a ^ n • ⊤) ?_
+  · refine le_antisymm (fun r ⟨h1, h2⟩ ↦ ?_) (le_inf (fun x ↦ I.smul_mem (a ^ n)) (by simp))
+    simp only [add_eq_sup, SetLike.mem_coe, mem_sup, mem_smul_pointwise_iff_exists] at h2
+    obtain ⟨x, hx, -, ⟨y, -, rfl⟩, rfl⟩ := h2
+    have h : (a ^ n • y ∈ I) = (a ^ (n + n) • y ∈ I) := congr_arg (y ∈ ·) (hn (n + n) le_add_self)
+    rw [pow_add, mul_smul] at h
+    rwa [I.add_mem_iff_right hx, h, ← I.add_mem_iff_right (I.smul_mem (a ^ n) hx), ← smul_add]
+  rw [add_eq_sup, sup_eq_left] at h
+  refine h.imp (fun h ↦ ?_) (fun h ↦ ⟨n, h⟩)
+  replace hn : f n = f (n + 1) := hn (n + 1) n.le_succ
+  rw [← h, hn]
+  rw [← h] at hab
+  simpa [f, pow_succ, mul_smul] using hab
+
+variable (R M) in
+/-- The Lasker--Noether theorem: every submodule in a Noetherian module admits a decomposition into
+  primary submodules. -/
+lemma isLasker : IsLasker R M := fun I ↦
   (exists_infIrred_decomposition I).imp fun _ h ↦ h.imp_right fun h' _ ht ↦ (h' ht).isPrimary
 
 end Noetherian
 
-end Ideal
+end Submodule
+
+@[deprecated (since := "2026-01-19")]
+alias Ideal.isLasker := Submodule.isLasker

docs/1000.yaml

@@ -67,7 +67,7 @@ Q164262:
 
 Q172298:
   title: Lasker–Noether theorem
-  decl: Ideal.isPrimary_decomposition_pairwise_ne_radical
+  decl: Submodule.isPrimary_decomposition_pairwise_ne_radical
 
 Q174955:
   title: Mihăilescu's theorem