English
If we have two submodules A_i and A_j with i ≠ j, and the indexing set reduces to {i, j}, then A_i and A_j are complementary: their sum is direct and they intersect trivially.
Русский
Если индексы i и j различны и разложение индексировано только двумя элементами, тогда A_i и A_j дополняют друг друга: сумма образует прямую сумму, пересечение тривиально.
LaTeX
$$$\IsCompl(A_i, A_j)$ under the stated conditions.$$
Lean4
/-- When indexed by only two distinct elements, `DirectSum.IsInternal` implies
the two submodules are complementary. Over a `Ring R`, this is true as an iff, as
`DirectSum.isInternal_submodule_iff_isCompl`. -/
theorem isCompl {A : ι → Submodule R M} {i j : ι} (hij : i ≠ j) (h : (Set.univ : Set ι) = { i, j })
(hi : IsInternal A) : IsCompl (A i) (A j) :=
⟨hi.submodule_iSupIndep.pairwiseDisjoint hij,
codisjoint_iff.mpr <|
Eq.symm <|
hi.submodule_iSup_eq_top.symm.trans <| by
rw [← sSup_pair, iSup, ← Set.image_univ, h, Set.image_insert_eq, Set.image_singleton]⟩
