mathlib3documentation

linear_algebra.pi_tensor_product

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define the tensor product of an indexed family s : ι → Type* of modules 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 #

• 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.
• tprod R f with f : Π i, s i is the tensor product of the vectors f i over all i : ι. This is bundled as a multilinear map from Π i, s i to ⨂[R] i, s i.
• lift_add_hom constructs 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.
• lift φ with φ : multilinear_map R s E is the corresponding linear map (⨂[R] i, s i) →ₗ[R] E. This is bundled as a linear equivalence.
• pi_tensor_product.reindex e re-indexes the components of ⨂[R] i : ι, M along e : ι ≃ ι₂.
• pi_tensor_product.tmul_equiv equivalence between a tensor_product of pi_tensor_products and a single pi_tensor_product.

Notations #

• ⨂[R] i, s i is defined as localized notation in locale tensor_product
• ⨂ₜ[R] i, f i with f : Π i, f i is defined globally as the tensor product of all the f i's.

Implementation notes #

• We define it via free_add_monoid (R × Π i, s i) with the R representing a "hidden" tensor factor, rather than free_add_monoid (Π i, s i) to ensure that, if ι is an empty type, the space is isomorphic to the base ring R.
• We have not restricted the index type ι to be a fintype, as nothing we do here strictly requires it. However, problems may arise in the case where ι is infinite; use at your own caution.
• Instead of requiring decidable_eq ι as an argument to pi_tensor_product itself, we include it as an argument in the constructors of the relation. A decidability isntance still has to come from somewhere due to the use of function.update, but this hides it from the downstream user. See the implementation notes for multilinear_map for an extended discussion of this choice.

TODO #

• Define tensor powers, symmetric subspace, etc.
• API for the various ways ι can be split into subsets; connect this with the binary tensor product.
• Include connection with holors.
• Port more of the API from the binary tensor product over to this case.

Tags #

multilinear, tensor, tensor product

inductive pi_tensor_product.eqv {ι : Type u_1} (R : Type u_4) (s : ι Type u_7) [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (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} (R : Type u_4) (s : ι Type u_7) [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] :
Type (max u_4 u_1 u_7)

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
Instances for pi_tensor_product
@[protected, instance]
def pi_tensor_product.add_comm_monoid {ι : Type u_1} {R : Type u_4} (s : ι Type u_7) [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] :
add_comm_monoid (λ (i : ι), s i))
Equations
@[protected, instance]
def pi_tensor_product.inhabited {ι : Type u_1} {R : Type u_4} (s : ι Type u_7) [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] :
inhabited (λ (i : ι), s i))
Equations
def pi_tensor_product.tprod_coeff {ι : Type u_1} (R : Type u_4) {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] (r : R) (f : Π (i : ι), s i) :
(λ (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} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] (f : Π (i : ι), s i) :
theorem pi_tensor_product.zero_tprod_coeff' {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] (z : R) (f : Π (i : ι), s i) (i : ι) (hf : f i = 0) :
theorem pi_tensor_product.add_tprod_coeff {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] [decidable_eq ι] (z : R) (f : Π (i : ι), s i) (i : ι) (m₁ m₂ : s i) :
i m₁) + i m₂) = i (m₁ + m₂))
theorem pi_tensor_product.add_tprod_coeff' {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] (z₁ z₂ : R) (f : Π (i : ι), s i) :
= (z₁ + z₂) f
theorem pi_tensor_product.smul_tprod_coeff_aux {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] [decidable_eq ι] (z : R) (f : Π (i : ι), s i) (i : ι) (r : R) :
i (r f i)) = (r * z) f
theorem pi_tensor_product.smul_tprod_coeff {ι : Type u_1} {R : Type u_4} {R₁ : Type u_5} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] [decidable_eq ι] (z : R) (f : Π (i : ι), s i) (i : ι) (r : R₁) [has_smul R₁ R] [ R R] [has_smul R₁ (s i)] [ R (s i)] :
i (r f i)) = (r z) f
def pi_tensor_product.lift_add_hom {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] {F : Type u_10} (φ : (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 : [_inst_9 : (r : R) (f : Π (i : ι), s i) (i : ι) (m₁ m₂ : s i), φ (r, m₁) + φ (r, m₂) = φ (r, (m₁ + m₂))) (C_add_scalar : (r r' : R) (f : Π (i : ι), s i), φ (r, f) + φ (r', f) = φ (r + r', f)) (C_smul : [_inst_10 : (r : R) (f : Π (i : ι), s i) (i : ι) (r' : R), φ (r, (r' f i)) = φ (r' * r, f)) :
(λ (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
@[protected]
theorem pi_tensor_product.induction_on' {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] {C : (λ (i : ι), s i) Prop} (z : (λ (i : ι), s i)) (C1 : {r : R} {f : Π (i : ι), s i}, C ) (Cp : {x y : (λ (i : ι), s i)}, C x C y C (x + y)) :
C z
@[protected, instance]
def pi_tensor_product.has_smul' {ι : Type u_1} {R : Type u_4} {R₁ : Type u_5} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] [monoid R₁] [ R] [ R R] :
has_smul R₁ (λ (i : ι), s i))
Equations
@[protected, instance]
def pi_tensor_product.has_smul {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] :
(λ (i : ι), s i))
Equations
theorem pi_tensor_product.smul_tprod_coeff' {ι : Type u_1} {R : Type u_4} {R₁ : Type u_5} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] [monoid R₁] [ R] [ R R] (r : R₁) (z : R) (f : Π (i : ι), s i) :
= (r z) f
@[protected]
theorem pi_tensor_product.smul_add {ι : Type u_1} {R : Type u_4} {R₁ : Type u_5} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] [monoid R₁] [ R] [ R R] (r : R₁) (x y : (λ (i : ι), s i)) :
r (x + y) = r x + r y
@[protected, instance]
def pi_tensor_product.distrib_mul_action' {ι : Type u_1} {R : Type u_4} {R₁ : Type u_5} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] [monoid R₁] [ R] [ R R] :
(λ (i : ι), s i))
Equations
@[protected, instance]
def pi_tensor_product.smul_comm_class' {ι : Type u_1} {R : Type u_4} {R₁ : Type u_5} {R₂ : Type u_6} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] [monoid R₁] [ R] [ R R] [monoid R₂] [ R] [ R R] [ R₂ R] :
R₂ (λ (i : ι), s i))
@[protected, instance]
def pi_tensor_product.is_scalar_tower' {ι : Type u_1} {R : Type u_4} {R₁ : Type u_5} {R₂ : Type u_6} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] [monoid R₁] [ R] [ R R] [monoid R₂] [ R] [ R R] [has_smul R₁ R₂] [ R₂ R] :
R₂ (λ (i : ι), s i))
@[protected, instance]
def pi_tensor_product.module' {ι : Type u_1} {R : Type u_4} {R₁ : Type u_5} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] [semiring R₁] [module R₁ R] [ R R] :
module R₁ (λ (i : ι), s i))
Equations
@[protected, instance]
def pi_tensor_product.module {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] :
(λ (i : ι), s i))
Equations
@[protected, instance]
def pi_tensor_product.smul_comm_class {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] :
(λ (i : ι), s i))
@[protected, instance]
def pi_tensor_product.is_scalar_tower {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] :
(λ (i : ι), s i))
def pi_tensor_product.tprod {ι : Type u_1} (R : Type u_4) {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] :
(λ (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} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] (z : R) (f : Π (i : ι), s i) :
= z
@[protected]
theorem pi_tensor_product.induction_on {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] {C : (λ (i : ι), s i) Prop} (z : (λ (i : ι), s i)) (C1 : {r : R} {f : Π (i : ι), s i}, C (r f)) (Cp : {x y : (λ (i : ι), s i)}, C x C y C (x + y)) :
C z
@[ext]
theorem pi_tensor_product.ext {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] {E : Type u_9} [ E] {φ₁ φ₂ : (λ (i : ι), s i) →ₗ[R] E}  :
φ₁ = φ₂
def pi_tensor_product.lift_aux {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] {E : Type u_9} [ E] (φ : E) :
(λ (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} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] {E : Type u_9} [ E] (φ : E) (f : Π (i : ι), s i) :
= φ f
theorem pi_tensor_product.lift_aux_tprod_coeff {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] {E : Type u_9} [ E] (φ : E) (z : R) (f : Π (i : ι), s i) :
= z φ f
theorem pi_tensor_product.lift_aux.smul {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] {E : Type u_9} [ E] {φ : E} (r : R) (x : (λ (i : ι), s i)) :
(r x) = r
def pi_tensor_product.lift {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] {E : Type u_9} [ E] :
E ≃ₗ[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} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] {E : Type u_9} [ E] {φ : E} (f : Π (i : ι), s i) :
f) = φ f
theorem pi_tensor_product.lift.unique' {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] {E : Type u_9} [ E] {φ : E} {φ' : (λ (i : ι), s i) →ₗ[R] E} (H : = φ) :
theorem pi_tensor_product.lift.unique {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] {E : Type u_9} [ E] {φ : E} {φ' : (λ (i : ι), s i) →ₗ[R] E} (H : (f : Π (i : ι), s i), φ' f) = φ f) :
@[simp]
theorem pi_tensor_product.lift_symm {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] {E : Type u_9} [ E] (φ' : (λ (i : ι), s i) →ₗ[R] E) :
@[simp]
theorem pi_tensor_product.lift_tprod {ι : Type u_1} {R : Type u_4} {s : ι Type u_7} [Π (i : ι), add_comm_monoid (s i)] [Π (i : ι), (s i)] :
def pi_tensor_product.reindex {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) (M : Type u_8) [ M] (e : ι ι₂) :
(λ (i : ι), M) ≃ₗ[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} {R : Type u_4} {M : Type u_8} [ M] (e : ι ι₂) (f : ι M) :
e) f) = (λ (i : ι₂), f ((e.symm) i))
@[simp]
theorem pi_tensor_product.reindex_comp_tprod {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_8} [ M] (e : ι ι₂) :
@[simp]
theorem pi_tensor_product.lift_comp_reindex {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_8} [ M] {E : Type u_9} [ E] (e : ι ι₂) (φ : (λ (_x : ι₂), M) E) :
@[simp]
theorem pi_tensor_product.lift_reindex {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_8} [ M] {E : Type u_9} [ E] (e : ι ι₂) (φ : (λ (_x : ι₂), M) E) (x : (λ (i : ι), M)) :
( e) x) =
@[simp]
theorem pi_tensor_product.reindex_trans {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} {M : Type u_8} [ M] (e : ι ι₂) (e' : ι₂ ι₃) :
e).trans e') = (e.trans e')
@[simp]
theorem pi_tensor_product.reindex_reindex {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} {M : Type u_8} [ M] (e : ι ι₂) (e' : ι₂ ι₃) (x : (λ (i : ι), M)) :
e') ( e) x) = (e.trans e')) x
@[simp]
theorem pi_tensor_product.reindex_symm {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} {M : Type u_8} [ M] (e : ι ι₂) :
e).symm =
@[simp]
theorem pi_tensor_product.reindex_refl {ι : Type u_1} {R : Type u_4} {M : Type u_8} [ M] :
= (λ (i : ι), M))
def pi_tensor_product.is_empty_equiv (ι : Type u_1) {R : Type u_4} {M : Type u_8} [ M] [is_empty ι] :
(λ (i : ι), M) ≃ₗ[R] R

The tensor product over an empty index type ι is isomorphic to the base ring.

Equations
@[simp]
theorem pi_tensor_product.is_empty_equiv_symm_apply (ι : Type u_1) {R : Type u_4} {M : Type u_8} [ M] [is_empty ι] (r : R) :
@[simp]
theorem pi_tensor_product.is_empty_equiv_apply_tprod (ι : Type u_1) {R : Type u_4} {M : Type u_8} [ M] [is_empty ι] (f : ι M) :
@[simp]
theorem pi_tensor_product.subsingleton_equiv_symm_apply {ι : Type u_1} {R : Type u_4} {M : Type u_8} [ M] [subsingleton ι] (i₀ : ι) (m : M) :
= (λ (v : ι), m)
def pi_tensor_product.subsingleton_equiv {ι : Type u_1} {R : Type u_4} {M : Type u_8} [ M] [subsingleton ι] (i₀ : ι) :
(λ (i : ι), M) ≃ₗ[R] M

The tensor product over an single index is isomorphic to the module

Equations
@[simp]
theorem pi_tensor_product.subsingleton_equiv_apply_tprod {ι : Type u_1} {R : Type u_4} {M : Type u_8} [ M] [subsingleton ι] (i : ι) (f : ι M) :
= f i
def pi_tensor_product.tmul_equiv {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) (M : Type u_8) [ M] :
(λ (i : ι), M)) (λ (i : ι₂), M)) ≃ₗ[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
• = tmul_symm _ _
@[simp]
theorem pi_tensor_product.tmul_equiv_apply {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) (M : Type u_8) [ M] (a : ι M) (b : ι₂ M) :
(λ (i : ι), a i) ⊗ₜ[R] (λ (i : ι₂), b i)) = (λ (i : ι ι₂), b i)
@[simp]
theorem pi_tensor_product.tmul_equiv_symm_apply {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) (M : Type u_8) [ M] (a : ι ι₂ M) :
.symm) (λ (i : ι ι₂), a i)) = (λ (i : ι), a (sum.inl i)) ⊗ₜ[R] (λ (i : ι₂), a (sum.inr i))
@[protected, instance]
def pi_tensor_product.add_comm_group {ι : Type u_1} {R : Type u_2} [comm_ring R] {s : ι Type u_3} [Π (i : ι), add_comm_group (s i)] [Π (i : ι), (s i)] :
add_comm_group (λ (i : ι), s i))
Equations