# mathlib3documentation

linear_algebra.tensor_power

# Tensor power of a semimodule over a commutative semirings #

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

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.gsemiring: the tensor powers form a graded semiring.
• tensor_power.galgebra: the tensor powers form a graded algebra.

## 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)
@[ext]
theorem pi_tensor_product.graded_monoid_eq_of_reindex_cast {R : Type u_1} {M : Type u_2} [ M] {ιι : Type u_3} {ι : ιι Type u_4} {a b : graded_monoid (λ (ii : ιι), (λ (i : ι ii), M))} (h : a.fst = b.fst) :
(equiv.cast _)) a.snd = b.snd a = b

Two dependent pairs of tensor products are equal if their index is equal and the contents are equal after a canonical reindexing.

@[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) :
theorem tensor_power.ghas_mul_eq_coe_linear_map {R : Type u_1} {M : Type u_2} [ M] {i j : } (a : i M) (b : j M) :
def tensor_power.cast (R : Type u_1) (M : Type u_2) [ M] {i j : } (h : i = j) :
i M ≃ₗ[R] j M

Cast between "equal" tensor powers.

Equations
• h =
theorem tensor_power.cast_tprod (R : Type u_1) (M : Type u_2) [ M] {i j : } (h : i = j) (a : fin i M) :
h) a) = (a (fin.cast _))
@[simp]
theorem tensor_power.cast_refl (R : Type u_1) (M : Type u_2) [ M] {i : } (h : i = i) :
h = i M)
@[simp]
theorem tensor_power.cast_symm (R : Type u_1) (M : Type u_2) [ M] {i j : } (h : i = j) :
h).symm = _
@[simp]
theorem tensor_power.cast_trans (R : Type u_1) (M : Type u_2) [ M] {i j k : } (h : i = j) (h' : j = k) :
h).trans h') = _
@[simp]
theorem tensor_power.cast_cast {R : Type u_1} {M : Type u_2} [ M] {i j k : } (h : i = j) (h' : j = k) (a : i M) :
h') ( h) a) = _) a
@[ext]
theorem tensor_power.graded_monoid_eq_of_cast {R : Type u_1} {M : Type u_2} [ M] {a b : graded_monoid (λ (n : ), (λ (i : fin n), M))} (h : a.fst = b.fst) (h2 : h) a.snd = b.snd) :
a = b
theorem tensor_power.cast_eq_cast {R : Type u_1} {M : Type u_2} [ M] {i j : } (h : i = j) :
h) = cast _
theorem tensor_power.tprod_mul_tprod (R : Type u_1) {M : Type u_2} [ M] {na nb : } (a : fin na M) (b : fin nb M) :
= b)
theorem tensor_power.one_mul {R : Type u_1} {M : Type u_2} [ M] {n : } (a : n M) :
theorem tensor_power.mul_one {R : Type u_1} {M : Type u_2} [ M] {n : } (a : n M) :
theorem tensor_power.mul_assoc {R : Type u_1} {M : Type u_2} [ M] {na nb nc : } (a : na M) (b : nb M) (c : nc M) :
@[protected, instance]
def tensor_power.gmonoid {R : Type u_1} {M : Type u_2} [ M] :
graded_monoid.gmonoid (λ (i : ), i M)
Equations
def tensor_power.algebra_map₀ {R : Type u_1} {M : Type u_2} [ M] :
R ≃ₗ[R] 0 M

The canonical map from R to ⨂[R]^0 M corresponding to the algebra_map of the tensor algebra.

Equations
theorem tensor_power.algebra_map₀_eq_smul_one {R : Type u_1} {M : Type u_2} [ M] (r : R) :
theorem tensor_power.algebra_map₀_one {R : Type u_1} {M : Type u_2} [ M] :
theorem tensor_power.algebra_map₀_mul {R : Type u_1} {M : Type u_2} [ M] {n : } (r : R) (a : n M) :
= r a
theorem tensor_power.mul_algebra_map₀ {R : Type u_1} {M : Type u_2} [ M] {n : } (r : R) (a : n M) :
= r a
theorem tensor_power.algebra_map₀_mul_algebra_map₀ {R : Type u_1} {M : Type u_2} [ M] (r s : R) :
@[protected, instance]
def tensor_power.gsemiring {R : Type u_1} {M : Type u_2} [ M] :
direct_sum.gsemiring (λ (i : ), i M)
Equations
@[protected, instance]
def tensor_power.galgebra {R : Type u_1} {M : Type u_2} [ M] :
(λ (i : ), i M)

The tensor powers form a graded algebra.

Note that this instance implies algebra R (⨁ n : ℕ, ⨂[R]^n M) via direct_sum.algebra.

Equations
theorem tensor_power.galgebra_to_fun_def {R : Type u_1} {M : Type u_2} [ M] (r : R) :