English
There is a convenient way to build a decomposition from a linear map decompose such that the left and right inverse relations hold with the canonical embedding maps.
Русский
Существуют условия для построения разложения из линейного отображения, чтобы выполнялись левый и правый обратные связи по каноническим вложениям.
LaTeX
$$$\exists (\text{decompose} : M \to \bigoplus_i \mathcal{M}_i)\; (h_{\text{left}} : (DirectSum.coeLinearMap \mathcal{M}) \circ_{\ell} \text{decompose} = \mathrm{id})\; (h_{\text{right}} : \text{decompose} \circ_{\ell} DirectSum.coeLinearMap \mathcal{M} = \mathrm{id})\; \Rightarrow\; \text{Decomposition } \mathcal{M}$$
Lean4
/-- A convenience method to construct a decomposition from an `LinearMap`, such that the proofs
of left and right inverse can be constructed via `ext`. -/
abbrev ofLinearMap (decompose : M →ₗ[R] ⨁ i, ℳ i) (h_left_inv : DirectSum.coeLinearMap ℳ ∘ₗ decompose = .id)
(h_right_inv : decompose ∘ₗ DirectSum.coeLinearMap ℳ = .id) : Decomposition ℳ
where
decompose' := decompose
left_inv := DFunLike.congr_fun h_left_inv
right_inv := DFunLike.congr_fun h_right_inv
