English
Let p be a fixed submodule of E. The complements q of p (i.e., submodules with E = p ⊕ q) are in bijection with linear maps f: E → p that restrict to the identity on p, i.e. f|_p = id_p.
Русский
Пусть p — фиксированное подсообщество E. Непересечения q с p (то есть q такое, что E = p ⊕ q) образуют биекцию c нестандартной формы с линейными отображениями f: E → p, удовлетворяющими f|_p = id_p, то есть ∀ x ∈ p, f x = x.
LaTeX
$$$\{ q \mid \IsCompl(p,q) \} \simeq \{ f : E \to_{R} p \mid \forall x \in p,\ f(x)=x \}.$$$
Lean4
/-- Equivalence between submodules `q` such that `IsCompl p q` and linear maps `f : E →ₗ[R] p`
such that `∀ x : p, f x = x`. -/
def isComplEquivProj : { q // IsCompl p q } ≃ { f : E →ₗ[R] p // ∀ x : p, f x = x }
where
toFun q := ⟨linearProjOfIsCompl p q q.2, linearProjOfIsCompl_apply_left q.2⟩
invFun f := ⟨ker (f : E →ₗ[R] p), isCompl_of_proj f.2⟩
left_inv := fun ⟨q, hq⟩ => by simp only [linearProjOfIsCompl_ker]
right_inv := fun ⟨f, hf⟩ => Subtype.eq <| f.linearProjOfIsCompl_of_proj hf
