# mathlibdocumentation

linear_algebra.tensor_power

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

• tensor_power.ghas_one
• tensor_power.ghas_mul

## 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.

@[protected, reducible]
def tensor_power (R : Type u_1) (n : ) (M : Type u_2) [ 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
• n M = (λ (i : fin n), M)
@[protected, instance]
def tensor_power.ghas_one {R : Type u_1} {M : Type u_2} [ M] :
graded_monoid.ghas_one (λ (i : ), i M)

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

Equations
theorem tensor_power.ghas_one_def {R : Type u_1} {M : Type u_2} [ M] :
def tensor_power.mul_equiv {R : Type u_1} {M : Type u_2} [ M] {n m : } :
n M) m M) ≃ₗ[R] (n + m) M

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

Equations
@[protected, instance]
def tensor_power.ghas_mul {R : Type u_1} {M : Type u_2} [ M] :
graded_monoid.ghas_mul (λ (i : ), i M)

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

Equations
theorem tensor_power.ghas_mul_def {R : Type u_1} {M : Type u_2} [ M] {i j : } (a : i M) (b : j M) :