English
If a submodule p is closed complemented, there exists a q and a continuous linear equivalence e: M ≃ L (p × q) with coordinate projections on p and q and a simple expression for e.symm.
Русский
Если p — замкнутое дополняющееся подпольное подпространство, существует q и непрерывное линейное эквивалентное отображение $M \simeq p \times q$ с заданными координатами.
LaTeX
$$$\exists q\;\exists e : M \simeL[R] (p \times q), \; (\forall x : p, e x = (x, 0)) \land (\forall y : q, e y = (0, y)) \land (\forall x, e^{-1} x = x.1 + x.2)$$$
Lean4
/-- If `p` is a closed complemented submodule,
then there exists a submodule `q` and a continuous linear equivalence `M ≃L[R] (p × q)` such that
`e (x : p) = (x, 0)`, `e (y : q) = (0, y)`, and `e.symm x = x.1 + x.2`.
In fact, the properties of `e` imply the properties of `e.symm` and vice versa,
but we provide both for convenience. -/
theorem exists_submodule_equiv_prod [IsTopologicalAddGroup M] {p : Submodule R M} (hp : p.ClosedComplemented) :
∃ (q : Submodule R M) (e : M ≃L[R] (p × q)),
(∀ x : p, e x = (x, 0)) ∧ (∀ y : q, e y = (0, y)) ∧ (∀ x, e.symm x = x.1 + x.2) :=
let ⟨f, hf⟩ := hp
⟨LinearMap.ker f, .equivOfRightInverse _ p.subtypeL hf, fun _ ↦ by ext <;> simp [hf], fun _ ↦ by ext <;> simp, fun _ ↦
rfl⟩
