Tensor power of a semimodule over a commutative semirings #
We define the n
th 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 pi_tensor_product
.
This file introduces the notation ⨂[R]^n M
for tensor_power R n M
, which in turn is an
abbreviation for ⨂[R] i : fin n, M
.
Main definitions: #
TODO #
Show direct_sum.galgebra R (λ i, ⨂[R]^i M)
and algebra R (⨁ n : ℕ, ⨂[R]^n M)
.
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 graded_monoid
should be preferred.
Homogenous tensor powers $M^{\otimes n}$. ⨂[R]^n M
is a shorthand for
⨂[R] (i : fin n), M
.
Equations
- tensor_power R n M = pi_tensor_product R (λ (i : fin n), M)
As a graded monoid, ⨂[R]^i M
has a 1 : ⨂[R]^0 M
.
Equations
A variant of pi_tensor_prod.tmul_equiv
with the result indexed by fin (n + m)
.
Equations
As a graded monoid, ⨂[R]^i M
has a (*) : ⨂[R]^i M → ⨂[R]^j M → ⨂[R]^(i + j) M
.
Equations
- tensor_power.ghas_mul = {mul := λ (i j : ℕ) (a : tensor_power R i M) (b : tensor_power R j M), ⇑tensor_power.mul_equiv (a ⊗ₜ[R] b)}