# Documentation

Mathlib.LinearAlgebra.TensorPower

# Tensor power of a semimodule over a commutative semiring #

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

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

## Main definitions: #

• TensorPower.gsemiring: the tensor powers form a graded semiring.
• TensorPower.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 GradedMonoid should be preferred.

@[reducible]
def TensorPower (R : Type u_1) (n : ) (M : Type u_2) [] [] [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.

Instances For
Instances For
theorem PiTensorProduct.gradedMonoid_eq_of_reindex_cast {R : Type u_1} {M : Type u_2} [] [] [Module R M] {ιι : Type u_3} {ι : ιιType u_4} {a : GradedMonoid fun ii => ⨂[R] (x : ι ii), M} {b : GradedMonoid fun ii => ⨂[R] (x : ι ii), M} (h : a.fst = b.fst) :
↑(PiTensorProduct.reindex R M (Equiv.cast (_ : ι a.fst = ι b.fst))) a.snd = b.snda = b

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

instance TensorPower.gOne {R : Type u_1} {M : Type u_2} [] [] [Module R M] :

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

theorem TensorPower.gOne_def {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
def TensorPower.mulEquiv {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } {m : } :

A variant of PiTensorProduct.tmulEquiv with the result indexed by Fin (n + m).

Instances For
instance TensorPower.gMul {R : Type u_1} {M : Type u_2} [] [] [Module R M] :

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

theorem TensorPower.gMul_def {R : Type u_1} {M : Type u_2} [] [] [Module R M] {i : } {j : } (a : TensorPower R i M) (b : TensorPower R j M) :
= TensorPower.mulEquiv (a ⊗ₜ[R] b)
theorem TensorPower.gMul_eq_coe_linearMap {R : Type u_1} {M : Type u_2} [] [] [Module R M] {i : } {j : } (a : TensorPower R i M) (b : TensorPower R j M) :
= ↑(↑(LinearMap.compr₂ (TensorProduct.mk R (TensorPower R i M) (TensorPower R j M)) TensorPower.mulEquiv) a) b
def TensorPower.cast (R : Type u_1) (M : Type u_2) [] [] [Module R M] {i : } {j : } (h : i = j) :

Cast between "equal" tensor powers.

Instances For
theorem TensorPower.cast_tprod (R : Type u_1) (M : Type u_2) [] [] [Module R M] {i : } {j : } (h : i = j) (a : Fin iM) :
↑() (↑() a) = ↑() (a Fin.cast (_ : j = i))
@[simp]
theorem TensorPower.cast_refl (R : Type u_1) (M : Type u_2) [] [] [Module R M] {i : } (h : i = i) :
@[simp]
theorem TensorPower.cast_symm (R : Type u_1) (M : Type u_2) [] [] [Module R M] {i : } {j : } (h : i = j) :
@[simp]
theorem TensorPower.cast_trans (R : Type u_1) (M : Type u_2) [] [] [Module R M] {i : } {j : } {k : } (h : i = j) (h' : j = k) :
@[simp]
theorem TensorPower.cast_cast {R : Type u_1} {M : Type u_2} [] [] [Module R M] {i : } {j : } {k : } (h : i = j) (h' : j = k) (a : TensorPower R i M) :
↑(TensorPower.cast R M h') (↑() a) = ↑(TensorPower.cast R M (_ : i = k)) a
theorem TensorPower.gradedMonoid_eq_of_cast {R : Type u_1} {M : Type u_2} [] [] [Module R M] {a : GradedMonoid fun n => ⨂[R] (x : Fin n), M} {b : GradedMonoid fun n => ⨂[R] (x : Fin n), M} (h : a.fst = b.fst) (h2 : ↑() a.snd = b.snd) :
a = b
theorem TensorPower.cast_eq_cast {R : Type u_1} {M : Type u_2} [] [] [Module R M] {i : } {j : } (h : i = j) :
↑() = cast (_ : TensorPower R i M = TensorPower R j M)
theorem TensorPower.tprod_mul_tprod (R : Type u_1) {M : Type u_2} [] [] [Module R M] {na : } {nb : } (a : Fin naM) (b : Fin nbM) :
GradedMonoid.GMul.mul (↑() a) (↑() b) = ↑() ()
theorem TensorPower.one_mul {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } (a : TensorPower R n M) :
↑(TensorPower.cast R M (_ : 0 + n = n)) (GradedMonoid.GMul.mul GradedMonoid.GOne.one a) = a
theorem TensorPower.mul_one {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } (a : TensorPower R n M) :
↑(TensorPower.cast R M (_ : n + 0 = n)) (GradedMonoid.GMul.mul a GradedMonoid.GOne.one) = a
theorem TensorPower.mul_assoc {R : Type u_1} {M : Type u_2} [] [] [Module R M] {na : } {nb : } {nc : } (a : TensorPower R na M) (b : TensorPower R nb M) (c : TensorPower R nc M) :
↑(TensorPower.cast R M (_ : na + nb + nc = na + (nb + nc))) () =
instance TensorPower.gmonoid {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
def TensorPower.algebraMap₀ {R : Type u_1} {M : Type u_2} [] [] [Module R M] :

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

Instances For
theorem TensorPower.algebraMap₀_eq_smul_one {R : Type u_1} {M : Type u_2} [] [] [Module R M] (r : R) :
theorem TensorPower.algebraMap₀_one {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
theorem TensorPower.algebraMap₀_mul {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } (r : R) (a : TensorPower R n M) :
↑(TensorPower.cast R M (_ : 0 + n = n)) (GradedMonoid.GMul.mul (TensorPower.algebraMap₀ r) a) = r a
theorem TensorPower.mul_algebraMap₀ {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } (r : R) (a : TensorPower R n M) :
↑(TensorPower.cast R M (_ : n + 0 = n)) (GradedMonoid.GMul.mul a (TensorPower.algebraMap₀ r)) = r a
theorem TensorPower.algebraMap₀_mul_algebraMap₀ {R : Type u_1} {M : Type u_2} [] [] [Module R M] (r : R) (s : R) :
↑(TensorPower.cast R M (_ : 0 + 0 = 0)) (GradedMonoid.GMul.mul (TensorPower.algebraMap₀ r) (TensorPower.algebraMap₀ s)) = TensorPower.algebraMap₀ (r * s)
instance TensorPower.gsemiring {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
instance TensorPower.galgebra {R : Type u_1} {M : Type u_2} [] [] [Module R M] :

The tensor powers form a graded algebra.

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

theorem TensorPower.galgebra_toFun_def {R : Type u_1} {M : Type u_2} [] [] [Module R M] (r : R) :
DirectSum.GAlgebra.toFun r = TensorPower.algebraMap₀ r