Tensor power of a semimodule over a commutative semirings #

We define the nth tensor power of M as the n-ary tensor product indexed by fin n of M, ⨂[R] (i : fin n), M. This is a special case of pi_tensor_product.

This file introduces the notation ⨂[R]^n M for tensor_power R n M, which in turn is an abbreviation for ⨂[R] i : fin n, M.

Main definitions: #

TODO #

Show direct_sum.galgebra R (λ i, ⨂[R]^i M) and algebra R (⨁ n : ℕ, ⨂[R]^n M).

Implementation notes #

In this file we use ₜ1 and ₜ* as local notation for the graded multiplicative structure on tensor powers. Elsewhere, using 1 and * on graded_monoid should be preferred.

source

@[protected, reducible]

def tensor_power (R : Type u_1) (n : ℕ) (M : Type u_2) [comm_semiring R] [add_comm_monoid M] [module R M] :

Type (max u_1 u_2)

Homogenous tensor powers $M^{\otimes n}$. ⨂[R]^n M is a shorthand for ⨂[R] (i : fin n), M.

Equations

tensor_power R n M = pi_tensor_product R (λ (i : fin n), M)

source

@[protected, instance]

def tensor_power.ghas_one {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] :

graded_monoid.ghas_one (λ (i : ℕ), tensor_power R i M)

As a graded monoid, ⨂[R]^i M has a 1 : ⨂[R]^0 M.

Equations

tensor_power.ghas_one = {one := ⇑(pi_tensor_product.tprod R) fin.elim0}

source

theorem tensor_power.ghas_one_def {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] :

graded_monoid.ghas_one.one = ⇑(pi_tensor_product.tprod R) fin.elim0

source

def tensor_power.mul_equiv {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] {n m : ℕ} :

tensor_product R (tensor_power R n M) (tensor_power R m M) ≃ₗ[R] tensor_power R (n + m) M

A variant of pi_tensor_prod.tmul_equiv with the result indexed by fin (n + m).

Equations

tensor_power.mul_equiv = (pi_tensor_product.tmul_equiv R M).trans (pi_tensor_product.reindex R M fin_sum_fin_equiv)

source

@[protected, instance]

def tensor_power.ghas_mul {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] :

graded_monoid.ghas_mul (λ (i : ℕ), tensor_power R i M)

As a graded monoid, ⨂[R]^i M has a (*) : ⨂[R]^i M → ⨂[R]^j M → ⨂[R]^(i + j) M.

Equations

tensor_power.ghas_mul = {mul := λ (i j : ℕ) (a : tensor_power R i M) (b : tensor_power R j M), ⇑tensor_power.mul_equiv (a ⊗ₜ[R] b)}

source

theorem tensor_power.ghas_mul_def {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) :

graded_monoid.ghas_mul.mul a b = ⇑tensor_power.mul_equiv (a ⊗ₜ[R] b)