English
If a family of ideals p_i is pairwise compatible, then the corresponding torsion submodules form a SupIndep family.
Русский
Если семейство идеалов p_i совместимо, то соответствующие торионы образуют супиндеп-семью.
LaTeX
$$$S.SupIndep\, (i \mapsto \mathrm{torsionBySet}\,R\,M\,(p_i))$ under pairwise condition$$
Lean4
theorem supIndep_torsionBySet_ideal (hp : (S : Set ι).Pairwise fun i j => p i ⊔ p j = ⊤) :
S.SupIndep fun i => torsionBySet R M <| p i := fun T hT i hi hiT =>
by
rw [disjoint_iff, Finset.sup_eq_iSup,
iSup_torsionBySet_ideal_eq_torsionBySet_iInf fun i hi j hj ij => hp (hT hi) (hT hj) ij]
have := GaloisConnection.u_inf (b₁ := OrderDual.toDual (p i)) (b₂ := OrderDual.toDual (⨅ i ∈ T, p i)) (torsion_gc R M)
dsimp at this ⊢
rw [← this, Ideal.sup_iInf_eq_top, top_coe, torsionBySet_univ]
intro j hj; apply hp hi (hT hj); rintro rfl; exact hiT hj
