English
If the family q_i is pairwise coprime and M is annihilated by the product ∏_{i∈S} q_i, then M is the internal direct sum of its q_i-torsion submodules.
Русский
Если семейство q_i попарно взаимно простые и M аннигилируется произведением ∏_{i∈S} q_i, то M является внутренней прямой суммой своих q_i-торсионных подмодулей.
LaTeX
$$$(S:\\text{Set}~\\iota).\\,\\text{Pairwise}~(\\text{IsCoprime on } q)\\;\\land\\;\\operatorname{IsTorsionBy}\\, R\\, M\\left(\\prod_{i\\in S} q_i\\right) \\Rightarrow \\DirectSum.IsInternal\\; (\\lambda i: S \\;\\Rightarrow\\; \\operatorname{torsionBy} R M (q\,i)).$$$
Lean4
/-- If the `q i` are pairwise coprime, a `∏ i, q i`-torsion module is the internal direct sum of
its `q i`-torsion submodules. -/
theorem torsionBy_isInternal {q : ι → R} (hq : (S : Set ι).Pairwise <| (IsCoprime on q))
(hM : Module.IsTorsionBy R M <| ∏ i ∈ S, q i) : DirectSum.IsInternal fun i : S => torsionBy R M <| q i :=
by
rw [← Module.isTorsionBySet_span_singleton_iff, Ideal.submodule_span_eq, ← Ideal.finset_inf_span_singleton _ _ hq,
Finset.inf_eq_iInf] at hM
convert torsionBySet_isInternal (fun i hi j hj ij => (Ideal.sup_eq_top_iff_isCoprime (q i) _).mpr <| hq hi hj ij) hM
exact (torsionBySet_span_singleton_eq _ (R := R) (M := M)).symm
