English
Let A be a family of submodules A: ι → Submodule R M. If i and j are the only indices (i ≠ j) and the universe of indices is {i, j}, then the internality of the family A is equivalent to the complementarity of A_i and A_j; that is, IsInternal A iff IsCompl (A_i) (A_j).
Русский
Пусть A : ι → Submodule R M - семьёй подпространств. Пусть существует i ≠ j такие, что Set.univ = {i, j}. Тогда внутренняя свойство A эквивалентно тому, что подпространства A_i и A_j являются комплементами: IsInternal A ⇔ IsCompl (A_i) (A_j).
LaTeX
$$$\forall A:\, ι \to Submodule R M\; \forall i j : ι,\; i \neq j \;\to\; (Set.univ : Set ι) = \{ i, j \} \;\to\; IsInternal A \leftrightarrow IsCompl (A i) (A j)$$$
Lean4
/-- If a collection of submodules has just two indices, `i` and `j`, then
`DirectSum.IsInternal` is equivalent to `isCompl`. -/
theorem isInternal_submodule_iff_isCompl (A : ι → Submodule R M) {i j : ι} (hij : i ≠ j)
(h : (Set.univ : Set ι) = { i, j }) : IsInternal A ↔ IsCompl (A i) (A j) :=
by
have : ∀ k, k = i ∨ k = j := fun k ↦ by simpa using Set.ext_iff.mp h k
rw [isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, iSup, ← Set.image_univ, h, Set.image_insert_eq,
Set.image_singleton, sSup_pair, iSupIndep_pair hij this]
exact ⟨fun ⟨hd, ht⟩ ↦ ⟨hd, codisjoint_iff.mpr ht⟩, fun ⟨hd, ht⟩ ↦ ⟨hd, ht.eq_top⟩⟩
