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} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} : TensorPower R n M →ₗ[R] TensorAlgebra R M

The canonical embedding from a tensor power to the tensor algebra

Equations

• TensorPower.toTensorAlgebra = PiTensorProduct.lift (TensorAlgebra.tprod R M n)

@[simp]

theorem TensorPower.toTensorAlgebra_tprod {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) : toTensorAlgebra ((PiTensorProduct.tprod R) x) = (TensorAlgebra.tprod R M n) x

@[simp]

theorem TensorPower.toTensorAlgebra_gOne {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : toTensorAlgebra GradedMonoid.GOne.one = 1

@[simp]

theorem TensorPower.toTensorAlgebra_gMul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {i j : ℕ} (a : TensorPower R i M) (b : TensorPower R j M) : toTensorAlgebra (GradedMonoid.GMul.mul a b) = toTensorAlgebra a * toTensorAlgebra b

@[simp]

theorem TensorPower.toTensorAlgebra_galgebra_toFun {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (r : R) : toTensorAlgebra (DirectSum.GAlgebra.toFun r) = (algebraMap R (TensorAlgebra R M)) r

noncomputable def TensorAlgebra.ofDirectSum {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : (DirectSum ℕ fun (n : ℕ) => TensorPower R n M) →ₐ[R] TensorAlgebra R M

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

Equations

• TensorAlgebra.ofDirectSum = DirectSum.toAlgebra R (fun (n : ℕ) => TensorPower R n M) (fun (x : ℕ) => TensorPower.toTensorAlgebra) ⋯ ⋯

@[simp]

theorem TensorAlgebra.ofDirectSum_of_tprod {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) : ofDirectSum ((DirectSum.of (fun (n : ℕ) => TensorPower R n M) n) ((PiTensorProduct.tprod R) x)) = (tprod R M n) x

noncomputable def TensorAlgebra.toDirectSum {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : TensorAlgebra 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

• TensorAlgebra.toDirectSum = (TensorAlgebra.lift R) (DirectSum.lof R ℕ (fun (n : ℕ) => TensorPower R n M) 1 ∘ₗ ↑(PiTensorProduct.subsingletonEquiv 0).symm)

@[simp]

theorem TensorAlgebra.toDirectSum_ι {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (x : M) : toDirectSum ((ι R) x) = (DirectSum.of (fun (n : ℕ) => TensorPower R n M) 1) ((PiTensorProduct.tprod R) fun (x_1 : Fin 1) => x)

theorem TensorAlgebra.ofDirectSum_comp_toDirectSum {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : ofDirectSum.comp toDirectSum = AlgHom.id R (TensorAlgebra R M)

@[simp]

theorem TensorAlgebra.ofDirectSum_toDirectSum {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (x : TensorAlgebra R M) : ofDirectSum (toDirectSum x) = x

@[simp]

theorem TensorAlgebra.mk_reindex_cast {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n m : ℕ} (h : n = m) (x : TensorPower R n M) : GradedMonoid.mk m ((PiTensorProduct.reindex R (fun (x : Fin n) => M) (Equiv.cast ⋯)) x) = GradedMonoid.mk n x

@[simp]

theorem TensorAlgebra.mk_reindex_fin_cast {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n m : ℕ} (h : n = m) (x : TensorPower R n M) : GradedMonoid.mk m ((PiTensorProduct.reindex R (fun (x : Fin n) => M) (finCongr h)) x) = GradedMonoid.mk n x

theorem TensorPower.list_prod_gradedMonoid_mk_single {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (x : Fin n → M) : (List.map (fun (a : Fin n) => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun (x_1 : Fin 1) => x a)) (List.finRange n)).prod = GradedMonoid.mk n ((PiTensorProduct.tprod R) x)

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} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (x : Fin n → M) : toDirectSum ((tprod R M n) x) = (DirectSum.of (fun (i : ℕ) => TensorPower R i M) n) ((PiTensorProduct.tprod R) x)

theorem TensorAlgebra.toDirectSum_comp_ofDirectSum {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : toDirectSum.comp ofDirectSum = AlgHom.id R (DirectSum ℕ fun (n : ℕ) => TensorPower R n M)

@[simp]

theorem TensorAlgebra.toDirectSum_ofDirectSum {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (x : DirectSum ℕ fun (n : ℕ) => TensorPower R n M) : toDirectSum (ofDirectSum x) = x

noncomputable def TensorAlgebra.equivDirectSum {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : TensorAlgebra 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 ⋯ ⋯

@[simp]

theorem TensorAlgebra.equivDirectSum_symm_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : DirectSum ℕ fun (n : ℕ) => TensorPower R n M) : equivDirectSum.symm a = ofDirectSum a

@[simp]

theorem TensorAlgebra.equivDirectSum_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : TensorAlgebra R M) : equivDirectSum a = toDirectSum a