mathlib3 documentation

linear_algebra.tensor_algebra.to_tensor_power

Tensor algebras as direct sums of tensor powers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
def tensor_power.to_tensor_algebra {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] {n : ℕ} :
tensor_power R n M →ₗ[R] tensor_algebra R M

The canonical embedding from a tensor power to the tensor algebra

Equations
source
@[simp]
theorem tensor_power.to_tensor_algebra_tprod {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] {n : ℕ} (x : fin n → M) :
⇑tensor_power.to_tensor_algebra (⇑(pi_tensor_product.tprod R) x) = ⇑(tensor_algebra.tprod R M n) x
source
@[simp]
theorem tensor_power.to_tensor_algebra_ghas_one {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] :
⇑tensor_power.to_tensor_algebra graded_monoid.ghas_one.one = 1
source
@[simp]
theorem tensor_power.to_tensor_algebra_ghas_mul {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] {i j : ℕ} (a : tensor_power R i M) (b : tensor_power R j M) :
⇑tensor_power.to_tensor_algebra (graded_monoid.ghas_mul.mul a b) = ⇑tensor_power.to_tensor_algebra a * ⇑tensor_power.to_tensor_algebra b
source
@[simp]
theorem tensor_power.to_tensor_algebra_galgebra_to_fun {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (r : R) :
⇑tensor_power.to_tensor_algebra (⇑direct_sum.galgebra.to_fun r) = ⇑(algebra_map R (tensor_algebra R M)) r
source
def tensor_algebra.of_direct_sum {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] :
direct_sum ℕ (λ (n : ℕ), tensor_power R n M) →ₐ[R] tensor_algebra R M

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

Equations
source
@[simp]
theorem tensor_algebra.of_direct_sum_of_tprod {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] {n : ℕ} (x : fin n → M) :
⇑tensor_algebra.of_direct_sum (⇑(direct_sum.of (λ {n : ℕ}, pi_tensor_product R (λ (i : fin n), M)) n) (⇑(pi_tensor_product.tprod R) x)) = ⇑(tensor_algebra.tprod R M n) x
source
def tensor_algebra.to_direct_sum {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] :
tensor_algebra R M →ₐ[R] direct_sum ℕ (λ (n : ℕ), tensor_power R n M)

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

Equations
source
@[simp]
theorem tensor_algebra.to_direct_sum_ι {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (x : M) :
⇑tensor_algebra.to_direct_sum (⇑(tensor_algebra.ι R) x) = ⇑(direct_sum.of (λ (n : ℕ), tensor_power R n M) 1) (⇑(pi_tensor_product.tprod R) (λ (_x : fin 1), x))
source
theorem tensor_algebra.of_direct_sum_comp_to_direct_sum {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] :
tensor_algebra.of_direct_sum.comp tensor_algebra.to_direct_sum = alg_hom.id R (tensor_algebra R M)
source
@[simp]
theorem tensor_algebra.of_direct_sum_to_direct_sum {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (x : tensor_algebra R M) :
⇑tensor_algebra.of_direct_sum (⇑tensor_algebra.to_direct_sum x) = x
source
@[simp]
theorem tensor_algebra.mk_reindex_cast {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] {n m : ℕ} (h : n = m) (x : tensor_power R n M) :
graded_monoid.mk m (⇑(pi_tensor_product.reindex R M (equiv.cast _)) x) = graded_monoid.mk n x
source
@[simp]
theorem tensor_algebra.mk_reindex_fin_cast {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] {n m : ℕ} (h : n = m) (x : tensor_power R n M) :
graded_monoid.mk m (⇑(pi_tensor_product.reindex R M (fin.cast h).to_equiv) x) = graded_monoid.mk n x
source
theorem tensor_power.list_prod_graded_monoid_mk_single {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (n : ℕ) (x : fin n → M) :
(list.map (λ (a : fin n), graded_monoid.mk 1 (⇑(pi_tensor_product.tprod R) (λ (i : fin 1), x a))) (list.fin_range n)).prod = graded_monoid.mk n (⇑(pi_tensor_product.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 tensor_algebra.to_direct_sum_tensor_power_tprod {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] {n : ℕ} (x : fin n → M) :
⇑tensor_algebra.to_direct_sum (⇑(tensor_algebra.tprod R M n) x) = ⇑(direct_sum.of (λ {n : ℕ}, pi_tensor_product R (λ (i : fin n), M)) n) (⇑(pi_tensor_product.tprod R) x)
source
theorem tensor_algebra.to_direct_sum_comp_of_direct_sum {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] :
tensor_algebra.to_direct_sum.comp tensor_algebra.of_direct_sum = alg_hom.id R (direct_sum ℕ (λ (n : ℕ), tensor_power R n M))
source
@[simp]
theorem tensor_algebra.to_direct_sum_of_direct_sum {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (x : direct_sum ℕ (λ (n : ℕ), tensor_power R n M)) :
⇑tensor_algebra.to_direct_sum (⇑tensor_algebra.of_direct_sum x) = x
source
@[simp]
theorem tensor_algebra.equiv_direct_sum_symm_apply {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (ᾰ : direct_sum ℕ (λ (n : ℕ), tensor_power R n M)) :
⇑(tensor_algebra.equiv_direct_sum.symm) ᾰ = ⇑tensor_algebra.of_direct_sum ᾰ
source
def tensor_algebra.equiv_direct_sum {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] :
tensor_algebra R M ≃ₐ[R] direct_sum ℕ (λ (n : ℕ), tensor_power R n M)

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

Equations
source
@[simp]
theorem tensor_algebra.equiv_direct_sum_apply {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] (ᾰ : tensor_algebra R M) :
⇑tensor_algebra.equiv_direct_sum ᾰ = ⇑tensor_algebra.to_direct_sum ᾰ