English
The construction that, given an injection i: F → E and a complement subspace q of E with E decomposed as range(i) ⊕ q, yields a linear projection from E onto the range of i along q.
Русский
Конструкция проекции: дано включение i: F → E и дополнение q к E так, что E разлагается как range(i) ⊕ q; существует линейная проекция из E на range(i) вдоль q.
LaTeX
$$$\text{Given } i:F\to E\text{ with }\operatorname{Im}(i)=\operatorname{range}(i),\text{ and } h:IsCompl(\operatorname{range}(i),q)=E,\; \text{define } \mathrm{linearProjOfIsCompl}(q,i,\cdot,\cdot):E\to F\text{ as }(\mathrm{LinearEquiv.ofInjective}\; i)
^{-1} \circ (\operatorname{range}(i))\text{ projection along }q.$$$
Lean4
/-- Projection to the image of an injection along a complement.
This has an advantage over `Submodule.linearProjOfIsCompl` in that it allows the user better
definitional control over the type. -/
def linearProjOfIsCompl {F : Type*} [AddCommGroup F] [Module R F] (i : F →ₗ[R] E) (hi : Function.Injective i)
(h : IsCompl (LinearMap.range i) q) : E →ₗ[R] F :=
(LinearEquiv.ofInjective i hi).symm ∘ₗ (LinearMap.range i).linearProjOfIsCompl q h
