English
The explicit formula for f in terms of the complement data holds.
Русский
Раскрытая формула f через данные дополнения выполняется.
LaTeX
$$$f = (p.prodEquivOfIsCompl(ker f)\ h.isCompl).toLinearMap \circ (\mathrm{id} \;\times\; 0) \circ (p.prodEquivOfIsCompl(ker f)\ h.isCompl)^{-1}$$$
Lean4
theorem eq_conj_prod_map' {f : E →ₗ[R] E} (h : IsProj p f) :
f =
(p.prodEquivOfIsCompl (ker f) h.isCompl).toLinearMap ∘ₗ
prodMap id 0 ∘ₗ (p.prodEquivOfIsCompl (ker f) h.isCompl).symm.toLinearMap :=
by
rw [← LinearMap.comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm]
ext x
·
simp only [coe_prodEquivOfIsCompl, comp_apply, coe_inl, coprod_apply, coe_subtype, map_zero, add_zero,
h.map_id x x.2, prodMap_apply, id_apply]
·
simp only [coe_prodEquivOfIsCompl, comp_apply, coe_inr, coprod_apply, map_zero, coe_subtype, zero_add, map_coe_ker,
prodMap_apply, zero_apply, add_zero]
