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)
[CommSemiring R]
[AddCommMonoid M]
[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
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 => ⨂[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.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.
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.
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'
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).
Instances For
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.
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 = ↑(↑(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)
[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.
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 (_ : j = i))
@[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)
:
LinearEquiv.symm (TensorPower.cast R M h) = TensorPower.cast R M (_ : j = i)
@[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)
:
LinearEquiv.trans (TensorPower.cast R M h) (TensorPower.cast R M h') = TensorPower.cast R M (_ : i = k)
@[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 (_ : i = k)) 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 => ⨂[R] (x : Fin n), M}
{b : GradedMonoid fun n => ⨂[R] (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 (_ : TensorPower R i M = TensorPower R j M)
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 (_ : 0 + n = n)) (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 (_ : n + 0 = n)) (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 (_ : na + nb + nc = na + (nb + nc))) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
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
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.
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 (_ : 0 + n = n)) (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 (_ : 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}
[CommSemiring R]
[AddCommMonoid M]
[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}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
:
DirectSum.GSemiring fun i => TensorPower R i M
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.
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