mathlib documentation

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

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

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

Equations
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 : } :

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} [comm_semiring R] [add_comm_monoid M] [module R M] :

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

Equations