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)
Homogenous 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
Instances For
Homogenous 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}
[CommSemiring R]
[AddCommMonoid M]
[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.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)
Instances For
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)
Instances For
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 : 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}
[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 = let __src := TensorPower.gMul; let __src_1 := TensorPower.gOne; 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
Instances For
theorem
TensorPower.algebraMap₀_eq_smul_one
{R : Type u_1}
{M : Type u_2}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(r : R)
:
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 : 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 = let __src := TensorPower.gmonoid; 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