mathlib documentation

linear_algebra.pi_tensor_product

Tensor product of an indexed family of semimodules over commutative semirings #

We define the tensor product of an indexed family s : ι → Type* of semimodules over commutative semirings. We denote this space by ⨂[R] i, s i and define it as free_add_monoid (R × Π i, s i) quotiented by the appropriate equivalence relation. The treatment follows very closely that of the binary tensor product in linear_algebra/tensor_product.lean.

Main definitions #

Notations #

Implementation notes #

TODO #

Tags #

multilinear, tensor, tensor product

inductive pi_tensor_product.eqv {ι : Type u_1} [decidable_eq ι] (R : Type u_4) [comm_semiring R] (s : ι → Type u_6) [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] :
free_add_monoid (R × Π (i : ι), s i)free_add_monoid (R × Π (i : ι), s i) → Prop

The relation on free_add_monoid (R × Π i, s i) that generates a congruence whose quotient is the tensor product.

def pi_tensor_product {ι : Type u_1} [decidable_eq ι] (R : Type u_4) [comm_semiring R] (s : ι → Type u_6) [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] :
Type (max u_4 u_1 u_6)

pi_tensor_product R s with R a commutative semiring and s : ι → Type* is the tensor product of all the s i's. This is denoted by ⨂[R] i, s i.

Equations
@[instance]
def pi_tensor_product.add_comm_monoid {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] (s : ι → Type u_6) [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] :
add_comm_monoid (⨂[R] (i : ι), s i)
Equations
@[instance]
def pi_tensor_product.inhabited {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] (s : ι → Type u_6) [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] :
inhabited (⨂[R] (i : ι), s i)
Equations
def pi_tensor_product.tprod_coeff {ι : Type u_1} [decidable_eq ι] (R : Type u_4) [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] (r : R) (f : Π (i : ι), s i) :
⨂[R] (i : ι), s i

tprod_coeff R r f with r : R and f : Π i, s i is the tensor product of the vectors f i over all i : ι, multiplied by the coefficient r. Note that this is meant as an auxiliary definition for this file alone, and that one should use tprod defined below for most purposes.

Equations
theorem pi_tensor_product.zero_tprod_coeff {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] (f : Π (i : ι), s i) :
theorem pi_tensor_product.zero_tprod_coeff' {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] (z : R) (f : Π (i : ι), s i) (i : ι) (hf : f i = 0) :
theorem pi_tensor_product.add_tprod_coeff {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] (z : R) (f : Π (i : ι), s i) (i : ι) (m₁ m₂ : s i) :
theorem pi_tensor_product.add_tprod_coeff' {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] (z₁ z₂ : R) (f : Π (i : ι), s i) :
theorem pi_tensor_product.smul_tprod_coeff_aux {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] (z : R) (f : Π (i : ι), s i) (i : ι) (r : R) :
theorem pi_tensor_product.smul_tprod_coeff {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {R' : Type u_5} [comm_semiring R'] [algebra R' R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] (z : R) (f : Π (i : ι), s i) (i : ι) (r : R') [semimodule R' (s i)] [is_scalar_tower R' R (s i)] :
def pi_tensor_product.lift_add_hom {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] {F : Type u_9} [add_comm_monoid F] (φ : (R × Π (i : ι), s i) → F) (C0 : ∀ (r : R) (f : Π (i : ι), s i) (i : ι), f i = 0φ (r, f) = 0) (C0' : ∀ (f : Π (i : ι), s i), φ (0, f) = 0) (C_add : ∀ (r : R) (f : Π (i : ι), s i) (i : ι) (m₁ m₂ : s i), φ (r, function.update f i m₁) + φ (r, function.update f i m₂) = φ (r, function.update f i (m₁ + m₂))) (C_add_scalar : ∀ (r r' : R) (f : Π (i : ι), s i), φ (r, f) + φ (r', f) = φ (r + r', f)) (C_smul : ∀ (r : R) (f : Π (i : ι), s i) (i : ι) (r' : R), φ (r, function.update f i (r' f i)) = φ (r' * r, f)) :
⨂[R] (i : ι), s i →+ F

Construct an add_monoid_hom from (⨂[R] i, s i) to some space F from a function φ : (R × Π i, s i) → F with the appropriate properties.

Equations
@[instance]
def pi_tensor_product.has_scalar' {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {R' : Type u_5} [comm_semiring R'] [algebra R' R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] :
has_scalar R' (⨂[R] (i : ι), s i)
Equations
@[instance]
def pi_tensor_product.has_scalar {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] :
has_scalar R (⨂[R] (i : ι), s i)
Equations
theorem pi_tensor_product.smul_tprod_coeff' {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {R' : Type u_5} [comm_semiring R'] [algebra R' R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] (r : R') (z : R) (f : Π (i : ι), s i) :
theorem pi_tensor_product.smul_add {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {R' : Type u_5} [comm_semiring R'] [algebra R' R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] (r : R') (x y : ⨂[R] (i : ι), s i) :
r (x + y) = r x + r y
theorem pi_tensor_product.induction_on' {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] {C : ⨂[R] (i : ι), s i → Prop} (z : ⨂[R] (i : ι), s i) (C1 : ∀ {r : R} {f : Π (i : ι), s i}, C (pi_tensor_product.tprod_coeff R r f)) (Cp : ∀ {x y : ⨂[R] (i : ι), s i}, C xC yC (x + y)) :
C z
@[instance]
def pi_tensor_product.semimodule' {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {R' : Type u_5} [comm_semiring R'] [algebra R' R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] :
semimodule R' (⨂[R] (i : ι), s i)
Equations
@[instance]
def pi_tensor_product.semimodule {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {R' : Type u_5} [comm_semiring R'] [algebra R' R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] :
semimodule R' (⨂[R] (i : ι), s i)
Equations
def pi_tensor_product.tprod {ι : Type u_1} [decidable_eq ι] (R : Type u_4) [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] :
multilinear_map R s (⨂[R] (i : ι), s i)

The canonical multilinear_map R s (⨂[R] i, s i).

Equations
@[simp]
theorem pi_tensor_product.tprod_coeff_eq_smul_tprod {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] (z : R) (f : Π (i : ι), s i) :
theorem pi_tensor_product.induction_on {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] {C : ⨂[R] (i : ι), s i → Prop} (z : ⨂[R] (i : ι), s i) (C1 : ∀ {r : R} {f : Π (i : ι), s i}, C (r (pi_tensor_product.tprod R) f)) (Cp : ∀ {x y : ⨂[R] (i : ι), s i}, C xC yC (x + y)) :
C z
@[ext]
theorem pi_tensor_product.ext {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] {E : Type u_8} [add_comm_monoid E] [semimodule R E] {φ₁ φ₂ : ⨂[R] (i : ι), s i →ₗ[R] E} (H : φ₁.comp_multilinear_map (pi_tensor_product.tprod R) = φ₂.comp_multilinear_map (pi_tensor_product.tprod R)) :
φ₁ = φ₂
def pi_tensor_product.lift_aux {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] {E : Type u_8} [add_comm_monoid E] [semimodule R E] (φ : multilinear_map R s E) :
⨂[R] (i : ι), s i →+ E

Auxiliary function to constructing a linear map (⨂[R] i, s i) → E given a multilinear map R s E with the property that its composition with the canonical multilinear_map R s (⨂[R] i, s i) is the given multilinear map.

Equations
theorem pi_tensor_product.lift_aux_tprod {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] {E : Type u_8} [add_comm_monoid E] [semimodule R E] (φ : multilinear_map R s E) (f : Π (i : ι), s i) :
theorem pi_tensor_product.lift_aux_tprod_coeff {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] {E : Type u_8} [add_comm_monoid E] [semimodule R E] (φ : multilinear_map R s E) (z : R) (f : Π (i : ι), s i) :
theorem pi_tensor_product.lift_aux.smul {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] {E : Type u_8} [add_comm_monoid E] [semimodule R E] {φ : multilinear_map R s E} (r : R) (x : ⨂[R] (i : ι), s i) :
def pi_tensor_product.lift {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] {E : Type u_8} [add_comm_monoid E] [semimodule R E] :
multilinear_map R s E ≃ₗ[R] ⨂[R] (i : ι), s i →ₗ[R] E

Constructing a linear map (⨂[R] i, s i) → E given a multilinear_map R s E with the property that its composition with the canonical multilinear_map R s E is the given multilinear map φ.

Equations
@[simp]
theorem pi_tensor_product.lift.tprod {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] {E : Type u_8} [add_comm_monoid E] [semimodule R E] {φ : multilinear_map R s E} (f : Π (i : ι), s i) :
theorem pi_tensor_product.lift.unique' {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] {E : Type u_8} [add_comm_monoid E] [semimodule R E] {φ : multilinear_map R s E} {φ' : ⨂[R] (i : ι), s i →ₗ[R] E} (H : φ'.comp_multilinear_map (pi_tensor_product.tprod R) = φ) :
theorem pi_tensor_product.lift.unique {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] {E : Type u_8} [add_comm_monoid E] [semimodule R E] {φ : multilinear_map R s E} {φ' : ⨂[R] (i : ι), s i →ₗ[R] E} (H : ∀ (f : Π (i : ι), s i), φ' ((pi_tensor_product.tprod R) f) = φ f) :
@[simp]
theorem pi_tensor_product.lift_symm {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] {E : Type u_8} [add_comm_monoid E] [semimodule R E] (φ' : ⨂[R] (i : ι), s i →ₗ[R] E) :
@[simp]
theorem pi_tensor_product.lift_tprod {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {s : ι → Type u_6} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), semimodule R (s i)] :
def pi_tensor_product.reindex {ι : Type u_1} {ι₂ : Type u_2} [decidable_eq ι] [decidable_eq ι₂] (R : Type u_4) [comm_semiring R] (M : Type u_7) [add_comm_monoid M] [semimodule R M] (e : ι ι₂) :
⨂[R] (i : ι), M ≃ₗ[R] ⨂[R] (i : ι₂), M

Re-index the components of the tensor power by e.

For simplicity, this is defined only for homogeneously- (rather than dependently-) typed components.

Equations
@[simp]
theorem pi_tensor_product.reindex_tprod {ι : Type u_1} {ι₂ : Type u_2} [decidable_eq ι] [decidable_eq ι₂] {R : Type u_4} [comm_semiring R] {M : Type u_7} [add_comm_monoid M] [semimodule R M] (e : ι ι₂) (f : ι → M) :
@[simp]
@[simp]
theorem pi_tensor_product.lift_comp_reindex {ι : Type u_1} {ι₂ : Type u_2} [decidable_eq ι] [decidable_eq ι₂] {R : Type u_4} [comm_semiring R] {M : Type u_7} [add_comm_monoid M] [semimodule R M] {E : Type u_8} [add_comm_monoid E] [semimodule R E] (e : ι ι₂) (φ : multilinear_map R (λ (_x : ι₂), M) E) :
@[simp]
theorem pi_tensor_product.lift_reindex {ι : Type u_1} {ι₂ : Type u_2} [decidable_eq ι] [decidable_eq ι₂] {R : Type u_4} [comm_semiring R] {M : Type u_7} [add_comm_monoid M] [semimodule R M] {E : Type u_8} [add_comm_monoid E] [semimodule R E] (e : ι ι₂) (φ : multilinear_map R (λ (_x : ι₂), M) E) (x : ⨂[R] (i : ι), M) :
@[simp]
theorem pi_tensor_product.reindex_trans {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} [decidable_eq ι] [decidable_eq ι₂] [decidable_eq ι₃] {R : Type u_4} [comm_semiring R] {M : Type u_7} [add_comm_monoid M] [semimodule R M] (e : ι ι₂) (e' : ι₂ ι₃) :
@[simp]
theorem pi_tensor_product.reindex_symm {ι : Type u_1} {ι₂ : Type u_2} [decidable_eq ι] [decidable_eq ι₂] {R : Type u_4} [comm_semiring R] {M : Type u_7} [add_comm_monoid M] [semimodule R M] (e : ι ι₂) :
@[simp]
theorem pi_tensor_product.reindex_refl {ι : Type u_1} [decidable_eq ι] {R : Type u_4} [comm_semiring R] {M : Type u_7} [add_comm_monoid M] [semimodule R M] :
def pi_tensor_product.pempty_equiv {R : Type u_4} [comm_semiring R] {M : Type u_7} [add_comm_monoid M] [semimodule R M] :
⨂[R] (i : pempty), M ≃ₗ[R] R

The tensor product over an empty set of indices is isomorphic to the base ring

Equations
def pi_tensor_product.tmul_equiv {ι : Type u_1} {ι₂ : Type u_2} [decidable_eq ι] [decidable_eq ι₂] (R : Type u_4) [comm_semiring R] (M : Type u_7) [add_comm_monoid M] [semimodule R M] :
⨂[R] (i : ι), M ⨂[R] (i : ι₂), M ≃ₗ[R] ⨂[R] (i : ι ι₂), M

Equivalence between a tensor_product of pi_tensor_products and a single pi_tensor_product indexed by a sum type.

For simplicity, this is defined only for homogeneously- (rather than dependently-) typed components.

Equations
@[simp]
theorem pi_tensor_product.tmul_equiv_apply {ι : Type u_1} {ι₂ : Type u_2} [decidable_eq ι] [decidable_eq ι₂] (R : Type u_4) [comm_semiring R] (M : Type u_7) [add_comm_monoid M] [semimodule R M] (a : ι → M) (b : ι₂ → M) :
(pi_tensor_product.tmul_equiv R M) ((pi_tensor_product.tprod R) (λ (i : ι), a i) ⊗ₜ[R] (pi_tensor_product.tprod R) (λ (i : ι₂), b i)) = (pi_tensor_product.tprod R) (λ (i : ι ι₂), sum.elim a b i)
@[simp]
theorem pi_tensor_product.tmul_equiv_symm_apply {ι : Type u_1} {ι₂ : Type u_2} [decidable_eq ι] [decidable_eq ι₂] (R : Type u_4) [comm_semiring R] (M : Type u_7) [add_comm_monoid M] [semimodule R M] (a : ι ι₂ → M) :
((pi_tensor_product.tmul_equiv R M).symm) ((pi_tensor_product.tprod R) (λ (i : ι ι₂), a i)) = (pi_tensor_product.tprod R) (λ (i : ι), a (sum.inl i)) ⊗ₜ[R] (pi_tensor_product.tprod R) (λ (i : ι₂), a (sum.inr i))
@[instance]
def pi_tensor_product.add_comm_group {ι : Type u_1} [decidable_eq ι] {R : Type u_2} [comm_ring R] {s : ι → Type u_3} [Π (i : ι), add_comm_group (s i)] [Π (i : ι), module R (s i)] :
add_comm_group (⨂[R] (i : ι), s i)
Equations