toTensor — Mathlib

English

There is a canonical algebra homomorphism from FreeAlgebra R M to TensorAlgebra R M, sending FreeAlgebra.ι_R x to TensorAlgebra.ι_R x.

Русский

Существует канонический алгебра-гомоморфизм из FreeAlgebra_R M в TensorAlgebra_R M, отправляющий FreeAlgebra.ι_R x в TensorAlgebra.ι_R x.

LaTeX

$$$\\text{toTensor} : \\mathrm{FreeAlgebra}_R M \\to_A \\mathrm{TensorAlgebra}_R M,\\quad \\text{toTensor}(\\mathrm{FreeAlgebra.ι}_R x) = \\mathrm{TensorAlgebra.ι}_R x$$$

Lean4

/-- The canonical image of the `FreeAlgebra` in the `TensorAlgebra`, which maps
`FreeAlgebra.ι R x` to `TensorAlgebra.ι R x`. -/
def toTensor : FreeAlgebra R M →ₐ[R] TensorAlgebra R M :=
  FreeAlgebra.lift R (TensorAlgebra.ι R)

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