English
There exists a canonical way to extract a decomposition from a LinearMap, yielding a DirectSum.Decomposition structure for the given ℳ when left and right inverse conditions hold.
Русский
Существует канонический способ извлечения разложения из линейного отображения, образуя структуру DirectSum.Decomposition для ℳ при выполнении условий левого и правого обратного отображения.
LaTeX
$$$\exists decompose' : M \to \bigoplus_i \mathcal{M}_i,\ leftInv,\ rightInv \\text{such that } decompose' \circ DirectSum.coeLinearMap \mathcal{M} = id,\ (DirectSum.coeLinearMap \mathcal{M}) \circ decompose' = id$$$
Lean4
/-- The decomposition of `(1 : R)` where `1 = e₁ + e₂ + ⋯ + eₙ` which is induced by
the decomposition of the semiring `R = V1 ⊕ V2 ⊕ ⋯ ⊕ Vn`. -/
def idempotent (i : I) : R :=
decompose V 1 i
