decomposeAlgEquiv_symm_apply — Mathlib

English

Let A be a graded algebra with components 𝒜(i). The inverse of the decomposition isomorphism decomposeAlgEquiv 𝒜 coincides with the inverse of the direct-sum decomposition decompose 𝒜 on every element a of the direct sum ⨁ᵢ 𝒜(i).

Русский

Пусть A — градуированная алгебра с компонентами 𝒜(i). Обратное отображение изоморфизма разложения decomposeAlgEquiv 𝒜 совпадает с обратным отображением разложения DirectSum decompose 𝒜 на любом элементе прямой суммы ⊕ᵢ 𝒜(i).

LaTeX

$$$\\\\forall a \\,\\in \\,\\\\bigoplus_i 𝒜(i): (decomposeAlgEquiv 𝒜)^{-1}(a) = (decompose 𝒜)^{-1}(a).$$$

Lean4

@[simp]
theorem decomposeAlgEquiv_symm_apply (a : ⨁ i, 𝒜 i) : (decomposeAlgEquiv 𝒜).symm a = (decompose 𝒜).symm a :=
  rfl

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