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) [CommSemiring R] [AddCommMonoid M] [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

• TensorPower R n M = PiTensorProduct R fun (x : Fin n) => M

def TensorProduct.«term⨂[_]^_» : Lean.ParserDescr

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.

theorem PiTensorProduct.gradedMonoid_eq_of_reindex_cast {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ιι : Type u_3} {ι : ιι → Type u_4} {a 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.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.

noncomputable instance TensorPower.gOne {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [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 := (PiTensorProduct.tprod R) Fin.elim0 }

theorem TensorPower.gOne_def {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : GradedMonoid.GOne.one = (PiTensorProduct.tprod R) Fin.elim0

noncomputable def TensorPower.mulEquiv {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n m : ℕ} : TensorProduct R (TensorPower R n M) (TensorPower R m M) ≃ₗ[R] TensorPower R (n + m) M

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

Equations

• TensorPower.mulEquiv = (PiTensorProduct.tmulEquiv R M).trans (PiTensorProduct.reindex R (fun (x : Fin n ⊕ Fin m) => M) finSumFinEquiv)

noncomputable instance TensorPower.gMul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] {i j : ℕ} (a : TensorPower R i M) (b : TensorPower R j M) : GradedMonoid.GMul.mul a b = TensorPower.mulEquiv (a ⊗ₜ[R] b)

theorem TensorPower.gMul_eq_coe_linearMap {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {i j : ℕ} (a : TensorPower R i M) (b : TensorPower R j M) : GradedMonoid.GMul.mul a b = (((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) [CommSemiring R] [AddCommMonoid M] [Module R M] {i j : ℕ} (h : i = j) : TensorPower R i M ≃ₗ[R] TensorPower R j M

Cast between "equal" tensor powers.

Equations

• TensorPower.cast R M h = PiTensorProduct.reindex R (fun (x : Fin i) => M) (finCongr h)

theorem TensorPower.cast_tprod (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] {i j : ℕ} (h : i = j) (a : Fin i → M) : (TensorPower.cast R M h) ((PiTensorProduct.tprod R) a) = (PiTensorProduct.tprod R) (a ∘ Fin.cast ⋯)

@[simp]

theorem TensorPower.cast_refl (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] {i : ℕ} (h : i = i) : TensorPower.cast R M h = LinearEquiv.refl R (TensorPower R i M)

@[simp]

theorem TensorPower.cast_symm (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] {i j : ℕ} (h : i = j) : (TensorPower.cast R M h).symm = TensorPower.cast R M ⋯

@[simp]

theorem TensorPower.cast_trans (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] {i j k : ℕ} (h : i = j) (h' : j = k) : TensorPower.cast R M h ≪≫ₗ TensorPower.cast R M h' = TensorPower.cast R M ⋯

@[simp]

theorem TensorPower.cast_cast {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] {a 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} [CommSemiring R] [AddCommMonoid M] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] {na nb : ℕ} (a : Fin na → M) (b : Fin nb → M) : GradedMonoid.GMul.mul ((PiTensorProduct.tprod R) a) ((PiTensorProduct.tprod R) b) = (PiTensorProduct.tprod R) (Fin.append a b)

theorem TensorPower.one_mul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (a : TensorPower R n M) : (TensorPower.cast R M ⋯) (GradedMonoid.GMul.mul GradedMonoid.GOne.one a) = a

theorem TensorPower.mul_one {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (a : TensorPower R n M) : (TensorPower.cast R M ⋯) (GradedMonoid.GMul.mul a GradedMonoid.GOne.one) = a

theorem TensorPower.mul_assoc {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [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 ⋯) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)

noncomputable instance TensorPower.gmonoid {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : GradedMonoid.GMonoid fun (i : ℕ) => TensorPower R i M

Equations

• TensorPower.gmonoid = GradedMonoid.GMonoid.mk ⋯ ⋯ ⋯ GradedMonoid.GMonoid.gnpowRec ⋯ ⋯

noncomputable def TensorPower.algebraMap₀ {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : R ≃ₗ[R] TensorPower R 0 M

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

Equations

• TensorPower.algebraMap₀ = (PiTensorProduct.isEmptyEquiv (Fin 0)).symm

theorem TensorPower.algebraMap₀_eq_smul_one {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (r : R) : TensorPower.algebraMap₀ r = r • GradedMonoid.GOne.one

theorem TensorPower.algebraMap₀_one {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : TensorPower.algebraMap₀ 1 = GradedMonoid.GOne.one

theorem TensorPower.algebraMap₀_mul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [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} [CommSemiring R] [AddCommMonoid M] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] (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} [CommSemiring R] [AddCommMonoid M] [Module R M] : DirectSum.GSemiring fun (i : ℕ) => TensorPower R i 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} [CommSemiring R] [AddCommMonoid M] [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} [CommSemiring R] [AddCommMonoid M] [Module R M] (r : R) : DirectSum.GAlgebra.toFun r = TensorPower.algebraMap₀ r