ofDirectSum — Mathlib

English

There is a canonical algebra homomorphism from the direct sum of tensor powers to the tensor algebra.

Русский

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

LaTeX

$$$ ofDirectSum : (\bigoplus_n \otimes_R^n M) \rightarrow_A R (TensorAlgebra R M) $$$

Lean4

/-- The canonical map from a direct sum of tensor powers to the tensor algebra. -/
def ofDirectSum : (⨁ n, ⨂[R]^n M) →ₐ[R] TensorAlgebra R M :=
  DirectSum.toAlgebra _ _ (fun _ => TensorPower.toTensorAlgebra) TensorPower.toTensorAlgebra_gOne
    (fun {_ _} => TensorPower.toTensorAlgebra_gMul)

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