decomposeAlgEquiv — Mathlib

English

There is an algebra isomorphism between A and the direct sum of its graded pieces, realized via a decomposeAlgEquiv.

Русский

Существует алгеброизоморфизм между A и прямой суммой его градуированных частей, реализованный через decomposeAlgEquiv.

LaTeX

$$$\mathrm{decomposeAlgEquiv} : A \cong_A (\bigoplus_i 𝒜 i).$$$

Lean4

/-- If `A` is graded by `ι` with degree `i` component `𝒜 i`, then it is isomorphic as
an algebra to a direct sum of components. -/
-- We have to write the `@[simps]` lemmas by hand to see through the
-- `AlgEquiv.symm (decomposeAddEquiv 𝒜).symm`.

def decomposeAlgEquiv : A ≃ₐ[R] ⨁ i, 𝒜 i :=
  AlgEquiv.symm
    { (decomposeAddEquiv 𝒜).symm with
      map_mul' := map_mul (coeAlgHom 𝒜)
      commutes' := (coeAlgHom 𝒜).commutes }

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