English
Under pairwise coprimality, the iSup of torsionBy for q_i coincides with the torsionBy of the product ∏ q_i.
Русский
При попарной взаимной простоте q_i, iSup по torsionBy совпадает с torsionBy по произведению ∏ q_i.
LaTeX
$$$\text{iSup}_{i} \mathrm{torsionBy}\,R\,M\,(q_i) = \mathrm{torsionBy}\,R\,M\,(\prod_i q_i)$$$
Lean4
/-- If the `p i` are pairwise coprime, a `⨅ i, p i`-torsion module is the internal direct sum of
its `p i`-torsion submodules. -/
theorem torsionBySet_isInternal {p : ι → Ideal R} (hp : (S : Set ι).Pairwise fun i j => p i ⊔ p j = ⊤)
(hM : Module.IsTorsionBySet R M (⨅ i ∈ S, p i : Ideal R)) :
DirectSum.IsInternal fun i : S => torsionBySet R M <| p i :=
DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
(iSupIndep_iff_supIndep.mpr <| supIndep_torsionBySet_ideal hp)
(by
apply (iSup_subtype'' ↑S fun i => torsionBySet R M <| p i).trans
apply
(iSup_torsionBySet_ideal_eq_torsionBySet_iInf hp).trans <|
(Module.isTorsionBySet_iff_torsionBySet_eq_top _).mp hM)
