feat(Torsion/PrimaryComponent): direct sum of primaryComponent on primes is the whole module (leanprover-community#37466)

Let `M(P)` be the `primaryComponent` for `P : HeightOneSpectrum A`, we have  $$M \cong \bigoplus_{P} M(P).$$

This is implemented as `DirectSum.IsInternal`.

Co-authored-by: María Inés de Frutos Fernández <[mariaines.dff@gmail.com](mailto:mariaines.dff@gmail.com)>
Co-authored-by: Xavier Genereux <xaviergenereux@hotmail.com>

Author: xgenereux

Mathlib/Algebra/Module/Torsion/PrimaryComponent.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Module.Torsion.Basic
 public import Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
+public import Mathlib.RingTheory.DedekindDomain.Factorization
 
 /-!
 # I-Primary Components of modules
@@ -15,7 +16,7 @@ Let `A` be a commutative ring and `I`, an ideal of `A`.
 Given an `A`-Module `M` it's `I`-primary component is defined as
   $$M(I) := \bigcup_{i : \mathbb{N}} \text{torsionBySet A  M }  I ^ i.$$
 
-For `P : HeightOneSpectrum A`, the main result of this file (TODO) is that
+For `P : HeightOneSpectrum A`, the main result of this file is that
   $$M \cong \bigoplus_{P} M(P).$$
 
 ## Main definitions
@@ -28,6 +29,8 @@ For `P : HeightOneSpectrum A`, the main result of this file (TODO) is that
 
 variable {A M M₁ M₂ : Type*} [CommRing A]
 
+open IsDedekindDomain Submodule Module HeightOneSpectrum Set Function
+
 namespace Ideal
 
 variable (I : Ideal A)
@@ -127,6 +130,64 @@ theorem primaryComponent_sup (N₁ N₂ : Submodule A M) (hD : Disjoint N₁ N
       aesop
     · use y, hymem, z, hzmem
 
+section IsDedekindDomain
+
+variable [IsDedekindDomain A]
+
+open scoped nonZeroDivisors
+
+theorem iSup_primaryComponent_eq_top (h : IsTorsion A M) :
+    ⨆ P : HeightOneSpectrum A, primaryComponent M (P : Ideal A) = ⊤ := by
+  rw [eq_top_iff']
+  intro x
+  obtain ⟨⟨a : A, ha : a ∈ A⁰⟩, hmem : a • x = 0⟩ := h (x := x)
+  replace hmem : x ∈ torsionBySet A M (span {a}) := by
+    simp_all [← torsionBySet_eq_torsionBySet_span {a}]
+  have ha0 : span {a} ≠ ⊥ := by simpa using nonZeroDivisors.ne_zero ha
+  rw [← iInf_maxPowDividing_eq ha0] at hmem
+  let : Fintype (mulSupport fun v : HeightOneSpectrum A => v.maxPowDividing (span {a})) :=
+    Finite.fintype (hasFiniteMulSupport ha0)
+  let S := (mulSupport fun v : HeightOneSpectrum A => v.maxPowDividing (span {a})).toFinset
+  have : (⨅ i : HeightOneSpectrum A, i.maxPowDividing (span {a})) =
+      (⨅ i ∈ S, i.maxPowDividing (span {a})) := by
+    ext x
+    constructor
+    · aesop
+    · simp only [mem_iInf]
+      intro h i
+      by_cases htop : i.maxPowDividing (span {a}) = ⊤ <;> simp_all [S]
+  have hPairwise : (S : Set (HeightOneSpectrum _)).Pairwise
+      fun i j ↦ i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤ :=
+    fun r hr s hs hrs ↦ (isCoprime_pow_of_ne _ _ hrs _ _).sup_eq
+  rw [this, ← iSup_torsionBySet_ideal_eq_torsionBySet_iInf hPairwise] at hmem
+  revert x
+  rw [← SetLike.le_def]
+  refine iSup_mono (fun P x hxmem ↦ ?_)
+  by_cases hPS : P ∈ S
+  · simp_all only [mem_nonZeroDivisors_iff_ne_zero, ne_eq, mem_toFinset, mem_mulSupport,
+      one_eq_top, primaryComponent_mem, mem_torsionBySet_iff, SetLike.coe_sort_coe,
+      Subtype.forall, iSup_pos, S]
+    exact ⟨(Associates.mk P.asIdeal).count (Associates.mk (span {a})).factors, fun _ b ↦ hxmem _ b⟩
+  · simp_all
+
+variable (A M) in
+theorem iSupIndep_primaryComponent :
+    iSupIndep fun P : HeightOneSpectrum A => primaryComponent M (P : Ideal A) := by
+  rw [iSupIndep_iff_finset_sum_eq_zero_imp_eq_zero]
+  intro s p hmem hsum
+  simp only [primaryComponent_mem] at hmem
+  choose! f hmem using hmem
+  let m := s.sup f
+  have hSupIndep : iSupIndep fun i : HeightOneSpectrum A ↦ torsionBySet A M ↑(i.asIdeal ^ m) := by
+    rw [iSupIndep_iff_supIndep]
+    exact fun _ ↦ supIndep_torsionBySet_ideal
+      fun _ _ _ _ hPQ ↦ (isCoprime_pow_of_ne _ _ hPQ _ _).sup_eq
+  rw [iSupIndep_iff_finset_sum_eq_zero_imp_eq_zero] at hSupIndep
+  apply hSupIndep _ _ ?_ hsum
+  exact fun P hP ↦ torsionBySet_le_torsionBySet_pow _ _ (Finset.le_sup hP) _ (hmem P hP)
+
+end IsDedekindDomain
+
 end AddCommGroup
 
 end CommRing