decomposeLinearEquiv — Mathlib

English

If M is graded by ι with degree components ℳ_i, then M is linearly isomorphic to the direct sum ⨁_i ℳ_i via a canonical decomposition isomorphism.

Русский

Если M имеет градацию по ι с компонентами ℳ_i, то существует линейное изоморфизм M ≅ ⨁_i ℳ_i, связывающий M с прямой суммой компонентов.

LaTeX

$$$M \cong_{R} \bigoplus_i \mathcal{M}_i$$

Lean4

/-- If `M` is graded by `ι` with degree `i` component `ℳ i`, then it is isomorphic as
a module to a direct sum of components. -/
def decomposeLinearEquiv : M ≃ₗ[R] ⨁ i, ℳ i :=
  LinearEquiv.symm { (decomposeAddEquiv ℳ).symm with map_smul' := map_smul (DirectSum.coeLinearMap ℳ) }

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