equivDirectSum — Mathlib

English

There exists an algebra isomorphism between the tensor algebra T_R(M) and the direct sum ⨁_n M^{⊗ n} over n, given by the pair of canonical maps toDirectSum and ofDirectSum with the obvious inverses.

Русский

Существуют алгебраическое изоморфизм между тензорной алгеброй T_R(M) и прямой суммой ⨁_n M^{⊗ n} по всем n, задаваемый каноническими отображениями toDirectSum и ofDirectSum с очевидными обратными.

LaTeX

$$$T_R(M) \\simeq_A_R \\bigoplus_{n \\ge 0} M^{\\otimes n}_R.$$$

Lean4

/-- The tensor algebra is isomorphic to a direct sum of tensor powers. -/
@[simps!]
def equivDirectSum : TensorAlgebra R M ≃ₐ[R] ⨁ n, ⨂[R]^n M :=
  AlgEquiv.ofAlgHom toDirectSum ofDirectSum toDirectSum_comp_ofDirectSum ofDirectSum_comp_toDirectSum

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