feat(RingTheory/IsLasker): strength primary decomposition to a minima…

…l one (#18296)

Each primary ideal in the decomposition is necessary, and has an indepedent radical.

Mathlib/Data/Finset/Lattice.lean

@@ -732,6 +732,10 @@ theorem le_sup' {b : β} (h : b ∈ s) : f b ≤ s.sup' ⟨b, h⟩ f :=
 theorem le_sup'_of_le {a : α} {b : β} (hb : b ∈ s) (h : a ≤ f b) : a ≤ s.sup' ⟨b, hb⟩ f :=
   h.trans <| le_sup' _ hb
 
+lemma sup'_eq_of_forall {a : α} (h : ∀ b ∈ s, f b = a) : s.sup' H f = a :=
+  le_antisymm (sup'_le _ _ (fun _ hb ↦ (h _ hb).le))
+    (le_sup'_of_le _ H.choose_spec (h _ H.choose_spec).ge)
+
 @[simp]
 theorem sup'_const (a : α) : s.sup' H (fun _ => a) = a := by
   apply le_antisymm
@@ -900,6 +904,9 @@ theorem inf'_le {b : β} (h : b ∈ s) : s.inf' ⟨b, h⟩ f ≤ f b :=
 theorem inf'_le_of_le {a : α} {b : β} (hb : b ∈ s) (h : f b ≤ a) :
     s.inf' ⟨b, hb⟩ f ≤ a := (inf'_le _ hb).trans h
 
+lemma inf'_eq_of_forall {a : α} (h : ∀ b ∈ s, f b = a) : s.inf' H f = a :=
+  sup'_eq_of_forall (α := αᵒᵈ) H f h
+
 @[simp]
 theorem inf'_const (a : α) : (s.inf' H fun _ => a) = a :=
   sup'_const (α := αᵒᵈ) H a

Mathlib/RingTheory/Ideal/IsPrimary.lean

@@ -60,4 +60,25 @@ theorem isPrimary_inf {I J : Ideal R} (hi : I.IsPrimary) (hj : J.IsPrimary)
     · rw [hij] at hyi
       exact Or.inr hyi⟩
 
+open Finset in
+lemma isPrimary_finset_inf {ι} {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_emptyc_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)]
+
 end Ideal

Mathlib/RingTheory/Ideal/Operations.lean

@@ -811,6 +811,22 @@ variable {I J} in
 theorem IsRadical.inf (hI : IsRadical I) (hJ : IsRadical J) : IsRadical (I ⊓ J) := by
   rw [IsRadical, radical_inf]; exact inf_le_inf hI hJ
 
+/-- `Ideal.radical` as an `InfTopHom`, bundling in that it distributes over `inf`. -/
+def radicalInfTopHom : InfTopHom (Ideal R) (Ideal R) where
+  toFun := radical
+  map_inf' := radical_inf
+  map_top' := radical_top _
+
+@[simp]
+lemma radicalInfTopHom_apply (I : Ideal R) : radicalInfTopHom I = radical I := rfl
+
+open Finset in
+lemma radical_finset_inf {ι} {s : Finset ι} {f : ι → Ideal R} {i : ι} (hi : i ∈ s)
+    (hs : ∀ ⦃y⦄, y ∈ s → (f y).radical = (f i).radical) :
+    (s.inf f).radical = (f i).radical := by
+  rw [← radicalInfTopHom_apply, map_finset_inf, ← Finset.inf'_eq_inf ⟨_, hi⟩]
+  exact Finset.inf'_eq_of_forall _ _ hs
+
 /-- The reverse inclusion does not hold for e.g. `I := fun n : ℕ ↦ Ideal.span {(2 ^ n : ℤ)}`. -/
 theorem radical_iInf_le {ι} (I : ι → Ideal R) : radical (⨅ i, I i) ≤ ⨅ i, radical (I i) :=
   le_iInf fun _ ↦ radical_mono (iInf_le _ _)

Mathlib/RingTheory/Lasker.lean

@@ -15,13 +15,16 @@ import Mathlib.RingTheory.Noetherian
 
 - `IsLasker`: A ring `R` satisfies `IsLasker R` when any `I : Ideal R` can be decomposed into
   finitely many primary ideals.
+- `IsLasker.minimal`: Any `I : Ideal R` in a ring `R` satisifying `IsLasker R` can be
+  decomposed into primary ideals, such that the decomposition is minimal:
+  each primary ideal is necessary, and each primary ideal has an indepedent radical.
 - `Ideal.isLasker`: Every Noetherian commutative ring is a Lasker ring.
 
 ## Implementation details
 
 There is a generalization for submodules that needs to be implemented.
-Also, one needs to prove that the decomposition can be made minimal,
-and that minimal decompositions are equivalent.
+Also, one needs to prove that the radicals of minimal decompositions are independent of the
+  precise decomposition.
 
 -/
 
@@ -34,6 +37,78 @@ finitely many primary ideals.-/
 def IsLasker : Prop :=
   ∀ I : Ideal R, ∃ s : Finset (Ideal R), s.inf id = I ∧ ∀ ⦃J⦄, J ∈ s → J.IsPrimary
 
+variable {R}
+
+namespace Ideal
+
+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
+  induction s using Finset.strongInductionOn
+  rename_i _ s IH
+  by_cases H : ∀ J ∈ s, ¬ (s.erase J).inf id ≤ J
+  · exact ⟨s, le_rfl, hs, H⟩
+  push_neg at H
+  obtain ⟨J, hJ, hJ'⟩ := H
+  refine (IH (s.erase J) (Finset.erase_ssubset hJ) ?_).imp
+    fun t ↦ And.imp_left (fun ht ↦ ht.trans (Finset.erase_subset _ _))
+  rw [← Finset.insert_erase hJ] at hs
+  simp [← hs, hJ']
+
+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
+  classical
+  refine ⟨(s.image (fun J ↦ s.filter (fun I ↦ I.radical = J.radical))).image fun t ↦ t.inf id,
+    ?_, ?_, ?_⟩
+  · rw [← hs]
+    refine le_antisymm ?_ ?_ <;> intro x hx
+    · simp only [Finset.inf_image, CompTriple.comp_eq, Submodule.mem_finset_inf,
+      Function.comp_apply, Finset.mem_filter, id_eq, and_imp] at hx ⊢
+      intro J hJ
+      exact hx J hJ J hJ rfl
+    · simp only [Submodule.mem_finset_inf, id_eq, Finset.inf_image, CompTriple.comp_eq,
+      Function.comp_apply, Finset.mem_filter, and_imp] at hx ⊢
+      intro J _ K hK _
+      exact hx K hK
+  · 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)
+    · simp [hJ]
+    · simp only [Finset.mem_filter, id_eq, and_imp]
+      intro y hy
+      simp [hs' hy]
+  · intro I hI J hJ hIJ
+    simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, exists_exists_and_eq_and] at hI hJ
+    obtain ⟨I', hI', hI⟩ := hI
+    obtain ⟨J', hJ', hJ⟩ := hJ
+    simp only [Function.onFun, ne_eq]
+    contrapose! hIJ
+    suffices I'.radical = J'.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)) ∧
+      (∀ ⦃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'⟩
+
+lemma IsLasker.minimal [DecidableEq (Ideal R)] (h : IsLasker R) (I : Ideal R) :
+    ∃ t : Finset (Ideal R), t.inf id = I ∧ (∀ ⦃J⦄, J ∈ t → J.IsPrimary) ∧
+      ((t : Set (Ideal R)).Pairwise ((· ≠ ·) on radical)) ∧
+      (∀ ⦃J⦄, J ∈ t → ¬ (t.erase J).inf id ≤ J) := by
+  obtain ⟨s, hs, hs'⟩ := h I
+  exact exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition hs hs'
+
+end Ideal
+
 end IsLasker
 
 namespace Ideal
@@ -80,15 +155,11 @@ lemma _root_.InfIrred.isPrimary {I : Ideal R} (h : InfIrred I) : I.IsPrimary :=
     refine Or.inr ⟨n, ?_⟩
     simpa using mem_sup_right (mem_span_singleton_self _)
 
-lemma exists_isPrimary_decomposition (I : Ideal R) :
-    ∃ s : Finset (Ideal R), s.inf id = I ∧ ∀ ⦃J⦄, J ∈ s → J.IsPrimary :=
-  (exists_infIrred_decomposition I).imp fun _ h ↦ h.imp_right fun h' _ ht ↦ (h' ht).isPrimary
-
-variable (R)
-
+variable (R) in
 /-- The Lasker--Noether theorem: every ideal in a Noetherian ring admits a decomposition into
   primary ideals. -/
-lemma isLasker : IsLasker R := exists_isPrimary_decomposition
+lemma isLasker : IsLasker R := fun I ↦
+  (exists_infIrred_decomposition I).imp fun _ h ↦ h.imp_right fun h' _ ht ↦ (h' ht).isPrimary
 
 end Noetherian