# 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, inline]
noncomputable abbrev TensorPower (R : Type u_1) (n : ) (M : Type u_2) [] [] [Module R M] :
Type (max u_2 u_1)

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

Equations
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
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 : ιι) => PiTensorProduct R fun (x : ι ii) => M} {b : GradedMonoid fun (ii : ιι) => PiTensorProduct R fun (x : ι ii) => M} (h : a.fst = b.fst) :
(PiTensorProduct.reindex R (fun (x : ι a.fst) => M) (Equiv.cast )) 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.

noncomputable instance TensorPower.gOne {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
GradedMonoid.GOne fun (i : ) => TensorPower R i M

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

Equations
• TensorPower.gOne = { one := Fin.elim0 }
theorem TensorPower.gOne_def {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
noncomputable 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).

Equations
Instances For
noncomputable instance TensorPower.gMul {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
GradedMonoid.GMul fun (i : ) => TensorPower R i M

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

Equations
• One or more equations did not get rendered due to their size.
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) :
= (((TensorProduct.mk R (TensorPower R i M) (TensorPower R j M)).compr₂ TensorPower.mulEquiv) a) b
noncomputable def TensorPower.cast (R : Type u_1) (M : Type u_2) [] [] [Module R M] {i : } {j : } (h : i = j) :

Cast between "equal" tensor powers.

Equations
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) :
(TensorPower.cast R M h) ( a) = (a )
@[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) :
(TensorPower.cast R M h).symm =
@[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) :
≪≫ₗ TensorPower.cast R M h' =
@[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') ((TensorPower.cast R M h) a) = (TensorPower.cast R M ) a
theorem TensorPower.gradedMonoid_eq_of_cast {R : Type u_1} {M : Type u_2} [] [] [Module R M] {a : GradedMonoid fun (n : ) => PiTensorProduct R fun (x : Fin n) => M} {b : GradedMonoid fun (n : ) => PiTensorProduct R fun (x : Fin n) => M} (h : a.fst = b.fst) (h2 : (TensorPower.cast R M h) 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) :
(TensorPower.cast R M h) = cast
theorem TensorPower.tprod_mul_tprod (R : Type u_1) {M : Type u_2} [] [] [Module R M] {na : } {nb : } (a : Fin naM) (b : Fin nbM) :
theorem TensorPower.one_mul {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } (a : TensorPower R n M) :
theorem TensorPower.mul_one {R : Type u_1} {M : Type u_2} [] [] [Module R M] {n : } (a : TensorPower R n M) :
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 ) =
noncomputable instance TensorPower.gmonoid {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
Equations
noncomputable 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.

Equations
• TensorPower.algebraMap₀ = .symm
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 ) (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 ) (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 ) (GradedMonoid.GMul.mul (TensorPower.algebraMap₀ r) (TensorPower.algebraMap₀ s)) = TensorPower.algebraMap₀ (r * s)
noncomputable instance TensorPower.gsemiring {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
Equations
• TensorPower.gsemiring = DirectSum.GSemiring.mk GradedMonoid.GMonoid.gnpow (fun (n : ) => TensorPower.algebraMap₀ n)
noncomputable instance TensorPower.galgebra {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
DirectSum.GAlgebra R fun (i : ) => TensorPower R i M

The tensor powers form a graded algebra.

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

Equations
• TensorPower.galgebra = { toFun := (↑TensorPower.algebraMap₀).toAddMonoidHom, map_one := , map_mul := , commutes := , smul_def := }
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