Tensor power of a semimodule over a commutative semirings #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 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: #
tensor_power.gsemiring: the tensor powers form a graded semiring.tensor_power.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 graded_monoid should be preferred.
@[protected, reducible]
def
tensor_power
(R : Type u_1)
(n : ℕ)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid 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.
Equations
- tensor_power R n M = pi_tensor_product R (λ (i : fin n), M)
@[ext]
theorem
pi_tensor_product.graded_monoid_eq_of_reindex_cast
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{ιι : Type u_3}
{ι : ιι → Type u_4}
{a b : graded_monoid (λ (ii : ιι), pi_tensor_product R (λ (i : ι ii), M))}
(h : a.fst = b.fst) :
⇑(pi_tensor_product.reindex R 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.
@[protected, instance]
def
tensor_power.ghas_one
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
graded_monoid.ghas_one (λ (i : ℕ), tensor_power R i M)
As a graded monoid, ⨂[R]^i M has a 1 : ⨂[R]^0 M.
Equations
theorem
tensor_power.ghas_one_def
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
def
tensor_power.mul_equiv
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{n m : ℕ} :
tensor_product R (tensor_power R n M) (tensor_power R m M) ≃ₗ[R] tensor_power R (n + m) M
A variant of pi_tensor_prod.tmul_equiv with the result indexed by fin (n + m).
Equations
@[protected, instance]
def
tensor_power.ghas_mul
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
graded_monoid.ghas_mul (λ (i : ℕ), tensor_power R i M)
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_product.mk R (tensor_power R i M) (tensor_power R j M)).compr₂ ↑tensor_power.mul_equiv) a) b}
theorem
tensor_power.ghas_mul_def
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{i j : ℕ}
(a : tensor_power R i M)
(b : tensor_power R j M) :
graded_monoid.ghas_mul.mul a b = ⇑tensor_power.mul_equiv (a ⊗ₜ[R] b)
theorem
tensor_power.ghas_mul_eq_coe_linear_map
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{i j : ℕ}
(a : tensor_power R i M)
(b : tensor_power R j M) :
graded_monoid.ghas_mul.mul a b = ⇑(⇑((tensor_product.mk R (tensor_power R i M) (tensor_power R j M)).compr₂ ↑tensor_power.mul_equiv) a) b
def
tensor_power.cast
(R : Type u_1)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{i j : ℕ}
(h : i = j) :
tensor_power R i M ≃ₗ[R] tensor_power R j M
Cast between "equal" tensor powers.
Equations
- tensor_power.cast R M h = pi_tensor_product.reindex R M (fin.cast h).to_equiv
theorem
tensor_power.cast_tprod
(R : Type u_1)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{i j : ℕ}
(h : i = j)
(a : fin i → M) :
⇑(tensor_power.cast R M h) (⇑(pi_tensor_product.tprod R) a) = ⇑(pi_tensor_product.tprod R) (a ∘ ⇑(fin.cast _))
@[simp]
theorem
tensor_power.cast_refl
(R : Type u_1)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{i : ℕ}
(h : i = i) :
tensor_power.cast R M h = linear_equiv.refl R (tensor_power R i M)
@[simp]
theorem
tensor_power.cast_symm
(R : Type u_1)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{i j : ℕ}
(h : i = j) :
(tensor_power.cast R M h).symm = tensor_power.cast R M _
@[simp]
theorem
tensor_power.cast_trans
(R : Type u_1)
(M : Type u_2)
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{i j k : ℕ}
(h : i = j)
(h' : j = k) :
(tensor_power.cast R M h).trans (tensor_power.cast R M h') = tensor_power.cast R M _
@[simp]
theorem
tensor_power.cast_cast
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{i j k : ℕ}
(h : i = j)
(h' : j = k)
(a : tensor_power R i M) :
⇑(tensor_power.cast R M h') (⇑(tensor_power.cast R M h) a) = ⇑(tensor_power.cast R M _) a
@[ext]
theorem
tensor_power.graded_monoid_eq_of_cast
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{a b : graded_monoid (λ (n : ℕ), pi_tensor_product R (λ (i : fin n), M))}
(h : a.fst = b.fst)
(h2 : ⇑(tensor_power.cast R M h) a.snd = b.snd) :
a = b
theorem
tensor_power.cast_eq_cast
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{i j : ℕ}
(h : i = j) :
⇑(tensor_power.cast R M h) = cast _
theorem
tensor_power.tprod_mul_tprod
(R : Type u_1)
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{na nb : ℕ}
(a : fin na → M)
(b : fin nb → M) :
graded_monoid.ghas_mul.mul (⇑(pi_tensor_product.tprod R) a) (⇑(pi_tensor_product.tprod R) b) = ⇑(pi_tensor_product.tprod R) (fin.append a b)
theorem
tensor_power.one_mul
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{n : ℕ}
(a : tensor_power R n M) :
theorem
tensor_power.mul_one
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{n : ℕ}
(a : tensor_power R n M) :
theorem
tensor_power.mul_assoc
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{na nb nc : ℕ}
(a : tensor_power R na M)
(b : tensor_power R nb M)
(c : tensor_power R nc M) :
⇑(tensor_power.cast R M _) (graded_monoid.ghas_mul.mul (graded_monoid.ghas_mul.mul a b) c) = graded_monoid.ghas_mul.mul a (graded_monoid.ghas_mul.mul b c)
@[protected, instance]
def
tensor_power.gmonoid
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
graded_monoid.gmonoid (λ (i : ℕ), tensor_power R i M)
Equations
- tensor_power.gmonoid = {mul := graded_monoid.ghas_mul.mul tensor_power.ghas_mul, one := graded_monoid.ghas_one.one tensor_power.ghas_one, one_mul := _, mul_one := _, mul_assoc := _, gnpow := graded_monoid.gmonoid.gnpow_rec {one := graded_monoid.ghas_one.one tensor_power.ghas_one}, gnpow_zero' := _, gnpow_succ' := _}
def
tensor_power.algebra_map₀
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
R ≃ₗ[R] tensor_power R 0 M
The canonical map from R to ⨂[R]^0 M corresponding to the algebra_map of the tensor
algebra.
Equations
theorem
tensor_power.algebra_map₀_eq_smul_one
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
(r : R) :
theorem
tensor_power.algebra_map₀_one
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
theorem
tensor_power.algebra_map₀_mul
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{n : ℕ}
(r : R)
(a : tensor_power R n M) :
⇑(tensor_power.cast R M _) (graded_monoid.ghas_mul.mul (⇑tensor_power.algebra_map₀ r) a) = r • a
theorem
tensor_power.mul_algebra_map₀
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
{n : ℕ}
(r : R)
(a : tensor_power R n M) :
⇑(tensor_power.cast R M _) (graded_monoid.ghas_mul.mul a (⇑tensor_power.algebra_map₀ r)) = r • a
theorem
tensor_power.algebra_map₀_mul_algebra_map₀
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
(r s : R) :
@[protected, instance]
def
tensor_power.gsemiring
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
direct_sum.gsemiring (λ (i : ℕ), tensor_power R i M)
Equations
- tensor_power.gsemiring = {mul := graded_monoid.gmonoid.mul tensor_power.gmonoid, mul_zero := _, zero_mul := _, mul_add := _, add_mul := _, one := graded_monoid.gmonoid.one tensor_power.gmonoid, one_mul := _, mul_one := _, mul_assoc := _, gnpow := graded_monoid.gmonoid.gnpow tensor_power.gmonoid, gnpow_zero' := _, gnpow_succ' := _, nat_cast := λ (n : ℕ), ⇑tensor_power.algebra_map₀ ↑n, nat_cast_zero := _, nat_cast_succ := _}
@[protected, instance]
def
tensor_power.galgebra
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M] :
direct_sum.galgebra R (λ (i : ℕ), tensor_power R i M)
The tensor powers form a graded algebra.
Note that this instance implies algebra R (⨁ n : ℕ, ⨂[R]^n M) via direct_sum.algebra.
Equations
- tensor_power.galgebra = {to_fun := tensor_power.algebra_map₀.to_linear_map.to_add_monoid_hom, map_one := _, map_mul := _, commutes := _, smul_def := _}
theorem
tensor_power.galgebra_to_fun_def
{R : Type u_1}
{M : Type u_2}
[comm_semiring R]
[add_comm_monoid M]
[module R M]
(r : R) :