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.

source

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

Instances For

source

@[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) :

↑TensorPower.toTensorAlgebra (↑(PiTensorProduct.tprod R) x) = ↑(TensorAlgebra.tprod R M n) x

source

@[simp]

theorem TensorPower.toTensorAlgebra_gOne {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :

↑TensorPower.toTensorAlgebra GradedMonoid.GOne.one = 1

source

@[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) :

↑TensorPower.toTensorAlgebra (GradedMonoid.GMul.mul a b) = ↑TensorPower.toTensorAlgebra a * ↑TensorPower.toTensorAlgebra b

source

@[simp]

theorem TensorPower.toTensorAlgebra_galgebra_toFun {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (r : R) :

↑TensorPower.toTensorAlgebra (↑DirectSum.GAlgebra.toFun r) = ↑(algebraMap R (TensorAlgebra R M)) r

source

def TensorAlgebra.ofDirectSum {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 map from a direct sum of tensor powers to the tensor algebra.

Instances For

source

@[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) :

↑TensorAlgebra.ofDirectSum (↑(DirectSum.of (fun n => TensorPower R n M) n) (↑(PiTensorProduct.tprod R) x)) = ↑(TensorAlgebra.tprod R M n) x

source

def TensorAlgebra.toDirectSum {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :

TensorAlgebra R M →ₐ[R] ⨁ (n : ℕ), TensorPower R n M

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

Instances For

source

@[simp]

theorem TensorAlgebra.toDirectSum_ι {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (x : M) :

↑TensorAlgebra.toDirectSum (↑(TensorAlgebra.ι R) x) = ↑(DirectSum.of (fun n => TensorPower R n M) 1) (⨂ₜ[R] (x : Fin 1), x)

source

theorem TensorAlgebra.ofDirectSum_comp_toDirectSum {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :

AlgHom.comp TensorAlgebra.ofDirectSum TensorAlgebra.toDirectSum = AlgHom.id R (TensorAlgebra R M)

source

@[simp]

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

↑TensorAlgebra.ofDirectSum (↑TensorAlgebra.toDirectSum x) = x

source

@[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 M (Equiv.cast (_ : Fin n = Fin m))) x) = GradedMonoid.mk n x

source

@[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 M (Fin.castIso h).toEquiv) x) = GradedMonoid.mk n x

source

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.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x : Fin 1), x a)) (List.finRange n)) = 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.

source

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) :

↑TensorAlgebra.toDirectSum (↑(TensorAlgebra.tprod R M n) x) = ↑(DirectSum.of (fun i => TensorPower R i M) n) (↑(PiTensorProduct.tprod R) x)

source

theorem TensorAlgebra.toDirectSum_comp_ofDirectSum {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :

AlgHom.comp TensorAlgebra.toDirectSum TensorAlgebra.ofDirectSum = AlgHom.id R (⨁ (n : ℕ), TensorPower R n M)

source

@[simp]

theorem TensorAlgebra.toDirectSum_ofDirectSum {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (x : ⨁ (n : ℕ), TensorPower R n M) :

↑TensorAlgebra.toDirectSum (↑TensorAlgebra.ofDirectSum x) = x

source

@[simp]

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

↑TensorAlgebra.equivDirectSum a = ↑TensorAlgebra.toDirectSum a

source

@[simp]

theorem TensorAlgebra.equivDirectSum_symm_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (a : ⨁ (n : ℕ), TensorPower R n M) :

↑(AlgEquiv.symm TensorAlgebra.equivDirectSum) a = ↑TensorAlgebra.ofDirectSum a

source

def TensorAlgebra.equivDirectSum {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] :

TensorAlgebra R M ≃ₐ[R] ⨁ (n : ℕ), TensorPower R n M

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

Instances For