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