English
If the q_i are pairwise coprime, the supremum of torsionBy q_i equals the torsionBy of the product ∏ q_i.
Русский
Если q_i попарно взаимно просты, то sup_torsionBy по q_i равно torsionBy по произведению ∏ q_i.
LaTeX
$$$\bigvee_i \mathrm{torsionBy}\,R\,M\,(q_i) = \mathrm{torsionBy}\,R\,M\,(\prod_i q_i)$$$
Lean4
theorem iSup_torsionBy_eq_torsionBy_prod (hq : (S : Set ι).Pairwise <| (IsCoprime on q)) :
⨆ i ∈ S, torsionBy R M (q i) = torsionBy R M (∏ i ∈ S, q i) :=
by
rw [← torsionBySet_span_singleton_eq, Ideal.submodule_span_eq, ← Ideal.finset_inf_span_singleton _ _ hq,
Finset.inf_eq_iInf, ← iSup_torsionBySet_ideal_eq_torsionBySet_iInf]
· congr
ext : 1
congr
ext : 1
exact (torsionBySet_span_singleton_eq _).symm
exact fun i hi j hj ij => (Ideal.sup_eq_top_iff_isCoprime _ _).mpr (hq hi hj ij)
