mathlib3 documentation

linear_algebra.tensor_power

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: #

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
@[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) :

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] :

As a graded monoid, ⨂[R]^i M has a 1 : ⨂[R]^0 M.

Equations
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 : } :

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] :

As a graded monoid, ⨂[R]^i M has a (*) : ⨂[R]^i M → ⨂[R]^j M → ⨂[R]^(i + j) M.

Equations
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) :

Cast between "equal" tensor powers.

Equations
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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :

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

Equations
@[protected, instance]
def tensor_power.galgebra {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] :

The tensor powers form a graded algebra.

Note that this instance implies algebra R (⨁ n : ℕ, ⨂[R]^n M) via direct_sum.algebra.

Equations