decompose — Mathlib

English

If M is decomposed into components ℳ_i, then M is canonically isomorphic to the direct sum ∨ i ℳ_i.

Русский

Если M раскладывается в компоненты ℳ_i, то M канонически изоморфна прямой сумме ∑_i ℳ_i.

LaTeX

$$$M \cong+ \bigoplus_i \mathcal{M}_i$$$

Lean4

/-- If `M` is graded by `ι` with degree `i` component `ℳ i`, then it is isomorphic as
to a direct sum of components. This is the canonical spelling of the `decompose'` field. -/
def decompose : M ≃ ⨁ i, ℳ i where
  toFun := Decomposition.decompose'
  invFun := DirectSum.coeAddMonoidHom ℳ
  left_inv := Decomposition.left_inv
  right_inv := Decomposition.right_inv

Похожие утверждения