toDirectSum — Mathlib

English

There is a canonical map from TensorAlgebra R M to the direct sum of tensor powers.

Русский

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

LaTeX

$$$ toDirectSum : TensorAlgebra R M \rightarrow_A ⨁ n, ⨂[R]^n M $$$

Lean4

/-- The canonical map from the tensor algebra to a direct sum of tensor powers. -/
def toDirectSum : TensorAlgebra R M →ₐ[R] ⨁ n, ⨂[R]^n M :=
  TensorAlgebra.lift R <|
    DirectSum.lof R ℕ (fun n => ⨂[R]^n M) _ ∘ₗ
      (LinearEquiv.symm <| PiTensorProduct.subsingletonEquiv (0 : Fin 1) : M ≃ₗ[R] _).toLinearMap

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