# Tensor algebras as direct sums of tensor powers #

In this file we show that TensorAlgebra R M is isomorphic to a direct sum of tensor powers, as TensorAlgebra.equivDirectSum.

noncomputable def TensorPower.toTensorAlgebra {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } :

The canonical embedding from a tensor power to the tensor algebra

Equations
• TensorPower.toTensorAlgebra = PiTensorProduct.lift ()
Instances For
@[simp]
theorem TensorPower.toTensorAlgebra_tprod {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } (x : Fin nM) :
TensorPower.toTensorAlgebra () = () x
@[simp]
theorem TensorPower.toTensorAlgebra_gOne {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
@[simp]
theorem TensorPower.toTensorAlgebra_gMul {R : Type u_1} {M : Type u_2} [] [] [Module R M] {i : } {j : } (a : TensorPower R i M) (b : TensorPower R j M) :
TensorPower.toTensorAlgebra () = TensorPower.toTensorAlgebra a * TensorPower.toTensorAlgebra b
@[simp]
theorem TensorPower.toTensorAlgebra_galgebra_toFun {R : Type u_1} {M : Type u_2} [] [] [Module R M] (r : R) :
TensorPower.toTensorAlgebra (DirectSum.GAlgebra.toFun r) = (algebraMap R ()) r
noncomputable def TensorAlgebra.ofDirectSum {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
(DirectSum fun (n : ) => TensorPower R n M) →ₐ[R]

The canonical map from a direct sum of tensor powers to the tensor algebra.

Equations
Instances For
@[simp]
theorem TensorAlgebra.ofDirectSum_of_tprod {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } (x : Fin nM) :
TensorAlgebra.ofDirectSum ((DirectSum.of (fun (n : ) => TensorPower R n M) n) ()) = () x
noncomputable def TensorAlgebra.toDirectSum {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
→ₐ[R] DirectSum fun (n : ) => TensorPower R n M

The canonical map from the tensor algebra to a direct sum of tensor powers.

Equations
Instances For
@[simp]
theorem TensorAlgebra.toDirectSum_ι {R : Type u_1} {M : Type u_2} [] [] [Module R M] (x : M) :
TensorAlgebra.toDirectSum (() x) = (DirectSum.of (fun (n : ) => TensorPower R n M) 1) ( fun (x_1 : Fin 1) => x)
theorem TensorAlgebra.ofDirectSum_comp_toDirectSum {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
TensorAlgebra.ofDirectSum.comp TensorAlgebra.toDirectSum = AlgHom.id R ()
@[simp]
theorem TensorAlgebra.ofDirectSum_toDirectSum {R : Type u_1} {M : Type u_2} [] [] [Module R M] (x : ) :
TensorAlgebra.ofDirectSum (TensorAlgebra.toDirectSum x) = x
@[simp]
theorem TensorAlgebra.mk_reindex_cast {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } {m : } (h : n = m) (x : TensorPower R n M) :
GradedMonoid.mk m ((PiTensorProduct.reindex R (fun (x : Fin n) => M) ()) x) =
@[simp]
theorem TensorAlgebra.mk_reindex_fin_cast {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } {m : } (h : n = m) (x : TensorPower R n M) :
GradedMonoid.mk m ((PiTensorProduct.reindex R (fun (x : Fin n) => M) ()) x) =
theorem TensorPower.list_prod_gradedMonoid_mk_single {R : Type u_1} {M : Type u_2} [] [] [Module R M] (n : ) (x : Fin nM) :
(List.map (fun (a : Fin n) => GradedMonoid.mk 1 ( fun (x_1 : Fin 1) => x a)) ()).prod = GradedMonoid.mk n ()

The product of tensor products made of a single vector is the same as a single product of all the vectors.

theorem TensorAlgebra.toDirectSum_tensorPower_tprod {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } (x : Fin nM) :
TensorAlgebra.toDirectSum (() x) = (DirectSum.of (fun (i : ) => TensorPower R i M) n) ()
theorem TensorAlgebra.toDirectSum_comp_ofDirectSum {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
TensorAlgebra.toDirectSum.comp TensorAlgebra.ofDirectSum = AlgHom.id R (DirectSum fun (n : ) => TensorPower R n M)
@[simp]
theorem TensorAlgebra.toDirectSum_ofDirectSum {R : Type u_1} {M : Type u_2} [] [] [Module R M] (x : DirectSum fun (n : ) => TensorPower R n M) :
TensorAlgebra.toDirectSum (TensorAlgebra.ofDirectSum x) = x
noncomputable def TensorAlgebra.equivDirectSum {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
≃ₐ[R] DirectSum fun (n : ) => TensorPower R n M

The tensor algebra is isomorphic to a direct sum of tensor powers.

Equations
• TensorAlgebra.equivDirectSum = AlgEquiv.ofAlgHom TensorAlgebra.toDirectSum TensorAlgebra.ofDirectSum
Instances For
@[simp]
theorem TensorAlgebra.equivDirectSum_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : ) :
TensorAlgebra.equivDirectSum a = TensorAlgebra.toDirectSum a
@[simp]
theorem TensorAlgebra.equivDirectSum_symm_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (a : DirectSum fun (n : ) => TensorPower R n M) :
TensorAlgebra.equivDirectSum.symm a = TensorAlgebra.ofDirectSum a