# Documentation

Mathlib.LinearAlgebra.PiTensorProduct

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

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 FreeAddMonoid (R × ∀ i, s i) quotiented by the appropriate equivalence relation. The treatment follows very closely that of the binary tensor product in LinearAlgebra/TensorProduct.lean.

## Main definitions #

• PiTensorProduct 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.
• liftAddHom constructs an AddMonoidHom from (⨂[R] i, s i) to some space F from a function φ : (R × ∀ i, s i) → F with the appropriate properties.
• lift φ with φ : MultilinearMap R s E is the corresponding linear map (⨂[R] i, s i) →ₗ[R] E. This is bundled as a linear equivalence.
• PiTensorProduct.reindex e re-indexes the components of ⨂[R] i : ι, M along e : ι ≃ ι₂.
• PiTensorProduct.tmulEquiv equivalence between a TensorProduct of PiTensorProducts and a single PiTensorProduct.

## Notations #

• ⨂[R] i, s i is defined as localized notation in locale TensorProduct.
• ⨂ₜ[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 FreeAddMonoid (R × ∀ i, s i) with the R representing a "hidden" tensor factor, rather than FreeAddMonoid (∀ 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 DecidableEq ι as an argument to PiTensorProduct itself, we include it as an argument in the constructors of the relation. A decidability instance 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 MultilinearMap 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 PiTensorProduct.Eqv {ι : Type u_1} (R : Type u_4) [] (s : ιType u_7) [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
FreeAddMonoid (R × ((i : ι) → s i))FreeAddMonoid (R × ((i : ι) → s i))Prop

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

Instances For
def PiTensorProduct {ι : Type u_1} (R : Type u_4) [] (s : ιType u_7) [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
Type (max (max u_1 u_4) u_7)

PiTensorProduct 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.

Instances For
Instances For

notation for tensor product over some indexed type

Instances For
instance PiTensorProduct.instAddCommMonoidPiTensorProduct {ι : Type u_1} {R : Type u_4} [] (s : ιType u_7) [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
AddCommMonoid (⨂[R] (i : ι), s i)
instance PiTensorProduct.instInhabitedPiTensorProduct {ι : Type u_1} {R : Type u_4} [] (s : ιType u_7) [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
Inhabited (⨂[R] (i : ι), s i)
def PiTensorProduct.tprodCoeff {ι : Type u_1} (R : Type u_4) [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (r : R) (f : (i : ι) → s i) :
⨂[R] (i : ι), s i

tprodCoeff 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.

Instances For
theorem PiTensorProduct.zero_tprodCoeff {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (f : (i : ι) → s i) :
= 0
theorem PiTensorProduct.zero_tprodCoeff' {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (z : R) (f : (i : ι) → s i) (i : ι) (hf : f i = 0) :
= 0
theorem PiTensorProduct.add_tprodCoeff {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [] (z : R) (f : (i : ι) → s i) (i : ι) (m₁ : s i) (m₂ : s i) :
theorem PiTensorProduct.add_tprodCoeff' {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (z₁ : R) (z₂ : R) (f : (i : ι) → s i) :
+ = PiTensorProduct.tprodCoeff R (z₁ + z₂) f
theorem PiTensorProduct.smul_tprodCoeff_aux {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [] (z : R) (f : (i : ι) → s i) (i : ι) (r : R) :
theorem PiTensorProduct.smul_tprodCoeff {ι : Type u_1} {R : Type u_4} [] {R₁ : Type u_5} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [] (z : R) (f : (i : ι) → s i) (i : ι) (r : R₁) [SMul R₁ R] [IsScalarTower R₁ R R] [SMul R₁ (s i)] [IsScalarTower R₁ R (s i)] :
def PiTensorProduct.liftAddHom {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (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 : ] (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 : ∀ [inst : ] (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 AddMonoidHom from (⨂[R] i, s i) to some space F from a function φ : (R × ∀ i, s i) → F with the appropriate properties.

Instances For
theorem PiTensorProduct.induction_on' {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {C : (⨂[R] (i : ι), s i) → Prop} (z : ⨂[R] (i : ι), s i) (C1 : {r : R} → {f : (i : ι) → s i} → C ()) (Cp : {x y : ⨂[R] (i : ι), s i} → C xC yC (x + y)) :
C z
instance PiTensorProduct.hasSMul' {ι : Type u_1} {R : Type u_4} [] {R₁ : Type u_5} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [] [SMulCommClass R₁ R R] :
SMul R₁ (⨂[R] (i : ι), s i)
instance PiTensorProduct.instSMulPiTensorProduct {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
SMul R (⨂[R] (i : ι), s i)
theorem PiTensorProduct.smul_tprodCoeff' {ι : Type u_1} {R : Type u_4} [] {R₁ : Type u_5} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [] [SMulCommClass R₁ R R] (r : R₁) (z : R) (f : (i : ι) → s i) :
theorem PiTensorProduct.smul_add {ι : Type u_1} {R : Type u_4} [] {R₁ : Type u_5} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [] [SMulCommClass R₁ R R] (r : R₁) (x : ⨂[R] (i : ι), s i) (y : ⨂[R] (i : ι), s i) :
r (x + y) = r x + r y
instance PiTensorProduct.distribMulAction' {ι : Type u_1} {R : Type u_4} [] {R₁ : Type u_5} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [] [SMulCommClass R₁ R R] :
DistribMulAction R₁ (⨂[R] (i : ι), s i)
instance PiTensorProduct.smulCommClass' {ι : Type u_1} {R : Type u_4} [] {R₁ : Type u_5} {R₂ : Type u_6} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [] [SMulCommClass R₁ R R] [Monoid R₂] [] [SMulCommClass R₂ R R] [SMulCommClass R₁ R₂ R] :
SMulCommClass R₁ R₂ (⨂[R] (i : ι), s i)
instance PiTensorProduct.isScalarTower' {ι : Type u_1} {R : Type u_4} [] {R₁ : Type u_5} {R₂ : Type u_6} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Monoid R₁] [] [SMulCommClass R₁ R R] [Monoid R₂] [] [SMulCommClass R₂ R R] [SMul R₁ R₂] [IsScalarTower R₁ R₂ R] :
IsScalarTower R₁ R₂ (⨂[R] (i : ι), s i)
instance PiTensorProduct.module' {ι : Type u_1} {R : Type u_4} [] {R₁ : Type u_5} {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] [Semiring R₁] [Module R₁ R] [SMulCommClass R₁ R R] :
Module R₁ (⨂[R] (i : ι), s i)
instance PiTensorProduct.instModulePiTensorProductToSemiringInstAddCommMonoidPiTensorProduct {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
Module R (⨂[R] (i : ι), s i)
instance PiTensorProduct.instSMulCommClassPiTensorProductInstSMulPiTensorProduct {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
SMulCommClass R R (⨂[R] (i : ι), s i)
instance PiTensorProduct.instIsScalarTowerPiTensorProductToSMulToSemiringIdInstSMulPiTensorProduct {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
IsScalarTower R R (⨂[R] (i : ι), s i)
def PiTensorProduct.tprod {ι : Type u_1} (R : Type u_4) [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
MultilinearMap R s (⨂[R] (i : ι), s i)

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

Instances For

pure tensor in tensor product over some index type

Instances For
theorem PiTensorProduct.tprod_eq_tprodCoeff_one {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
@[simp]
theorem PiTensorProduct.tprodCoeff_eq_smul_tprod {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] (z : R) (f : (i : ι) → s i) :
= z ↑() f
theorem PiTensorProduct.induction_on {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {C : (⨂[R] (i : ι), s i) → Prop} (z : ⨂[R] (i : ι), s i) (C1 : {r : R} → {f : (i : ι) → s i} → C (r ↑() f)) (Cp : {x y : ⨂[R] (i : ι), s i} → C xC yC (x + y)) :
C z
theorem PiTensorProduct.ext {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [] [Module R E] {φ₁ : (⨂[R] (i : ι), s i) →ₗ[R] E} {φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E} :
φ₁ = φ₂
def PiTensorProduct.liftAux {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [] [Module R E] (φ : ) :
(⨂[R] (i : ι), s i) →+ E

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

Instances For
theorem PiTensorProduct.liftAux_tprod {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [] [Module R E] (φ : ) (f : (i : ι) → s i) :
↑() (↑() f) = φ f
theorem PiTensorProduct.liftAux_tprodCoeff {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [] [Module R E] (φ : ) (z : R) (f : (i : ι) → s i) :
↑() () = z φ f
theorem PiTensorProduct.liftAux.smul {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [] [Module R E] {φ : } (r : R) (x : ⨂[R] (i : ι), s i) :
↑() (r x) = r ↑() x
def PiTensorProduct.lift {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [] [Module R E] :
≃ₗ[R] (⨂[R] (i : ι), s i) →ₗ[R] E

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

Instances For
@[simp]
theorem PiTensorProduct.lift.tprod {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [] [Module R E] {φ : } (f : (i : ι) → s i) :
↑(PiTensorProduct.lift φ) (↑() f) = φ f
theorem PiTensorProduct.lift.unique' {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [] [Module R E] {φ : } {φ' : (⨂[R] (i : ι), s i) →ₗ[R] E} (H : ) :
φ' = PiTensorProduct.lift φ
theorem PiTensorProduct.lift.unique {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [] [Module R E] {φ : } {φ' : (⨂[R] (i : ι), s i) →ₗ[R] E} (H : ∀ (f : (i : ι) → s i), φ' (↑() f) = φ f) :
φ' = PiTensorProduct.lift φ
@[simp]
theorem PiTensorProduct.lift_symm {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] {E : Type u_9} [] [Module R E] (φ' : (⨂[R] (i : ι), s i) →ₗ[R] E) :
↑(LinearEquiv.symm PiTensorProduct.lift) φ' =
@[simp]
theorem PiTensorProduct.lift_tprod {ι : Type u_1} {R : Type u_4} [] {s : ιType u_7} [(i : ι) → AddCommMonoid (s i)] [(i : ι) → Module R (s i)] :
PiTensorProduct.lift () = LinearMap.id
def PiTensorProduct.reindex {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [] (M : Type u_8) [] [Module R M] (e : ι ι₂) :
(⨂[R] (x : ι), M) ≃ₗ[R] ⨂[R] (x : ι₂), M

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

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

Instances For
@[simp]
theorem PiTensorProduct.reindex_tprod {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [] {M : Type u_8} [] [Module R M] (e : ι ι₂) (f : ιM) :
↑() (↑() f) = ⨂ₜ[R] (i : ι₂), f (e.symm i)
@[simp]
theorem PiTensorProduct.reindex_comp_tprod {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [] {M : Type u_8} [] [Module R M] (e : ι ι₂) :
@[simp]
theorem PiTensorProduct.lift_comp_reindex {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [] {M : Type u_8} [] [Module R M] {E : Type u_9} [] [Module R E] (e : ι ι₂) (φ : MultilinearMap R (fun x => M) E) :
LinearMap.comp (PiTensorProduct.lift φ) ↑() = PiTensorProduct.lift (MultilinearMap.domDomCongr e.symm φ)
@[simp]
theorem PiTensorProduct.lift_reindex {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [] {M : Type u_8} [] [Module R M] {E : Type u_9} [] [Module R E] (e : ι ι₂) (φ : MultilinearMap R (fun x => M) E) (x : ⨂[R] (x : ι), M) :
↑(PiTensorProduct.lift φ) (↑() x) = ↑(PiTensorProduct.lift (MultilinearMap.domDomCongr e.symm φ)) x
@[simp]
theorem PiTensorProduct.reindex_trans {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} [] {M : Type u_8} [] [Module R M] (e : ι ι₂) (e' : ι₂ ι₃) :
@[simp]
theorem PiTensorProduct.reindex_reindex {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} [] {M : Type u_8} [] [Module R M] (e : ι ι₂) (e' : ι₂ ι₃) (x : ⨂[R] (x : ι), M) :
↑() (↑() x) = ↑(PiTensorProduct.reindex R M (e.trans e')) x
@[simp]
theorem PiTensorProduct.reindex_symm {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [] {M : Type u_8} [] [Module R M] (e : ι ι₂) :
@[simp]
theorem PiTensorProduct.reindex_refl {ι : Type u_1} {R : Type u_4} [] {M : Type u_8} [] [Module R M] :
= LinearEquiv.refl R (⨂[R] (x : ι), M)
@[simp]
theorem PiTensorProduct.isEmptyEquiv_symm_apply (ι : Type u_1) {R : Type u_4} [] {M : Type u_8} [] [Module R M] [] (r : R) :
= r ↑() isEmptyElim
def PiTensorProduct.isEmptyEquiv (ι : Type u_1) {R : Type u_4} [] {M : Type u_8} [] [Module R M] [] :
(⨂[R] (x : ι), M) ≃ₗ[R] R

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

Instances For
@[simp]
theorem PiTensorProduct.isEmptyEquiv_apply_tprod (ι : Type u_1) {R : Type u_4} [] {M : Type u_8} [] [Module R M] [] (f : ιM) :
↑() (↑() f) = 1
@[simp]
theorem PiTensorProduct.subsingletonEquiv_symm_apply {ι : Type u_1} {R : Type u_4} [] {M : Type u_8} [] [Module R M] [] (i₀ : ι) (m : M) :
= ⨂ₜ[R] (x : ι), m
def PiTensorProduct.subsingletonEquiv {ι : Type u_1} {R : Type u_4} [] {M : Type u_8} [] [Module R M] [] (i₀ : ι) :
(⨂[R] (x : ι), M) ≃ₗ[R] M

Tensor product of M over a singleton set is equivalent to M

Instances For
@[simp]
theorem PiTensorProduct.subsingletonEquiv_apply_tprod {ι : Type u_1} {R : Type u_4} [] {M : Type u_8} [] [Module R M] [] (i : ι) (f : ιM) :
↑() (↑() f) = f i
def PiTensorProduct.tmulEquiv {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [] (M : Type u_8) [] [Module R M] :
TensorProduct R (⨂[R] (x : ι), M) (⨂[R] (x : ι₂), M) ≃ₗ[R] ⨂[R] (x : ι ι₂), M

Equivalence between a TensorProduct of PiTensorProducts and a single PiTensorProduct indexed by a Sum type.

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

Instances For
@[simp]
theorem PiTensorProduct.tmulEquiv_apply {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [] (M : Type u_8) [] [Module R M] (a : ιM) (b : ι₂M) :
↑() ((⨂ₜ[R] (i : ι), a i) ⊗ₜ[R] ⨂ₜ[R] (i : ι₂), b i) = ⨂ₜ[R] (i : ι ι₂), Sum.elim a b i
@[simp]
theorem PiTensorProduct.tmulEquiv_symm_apply {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [] (M : Type u_8) [] [Module R M] (a : ι ι₂M) :
↑() (⨂ₜ[R] (i : ι ι₂), a i) = (⨂ₜ[R] (i : ι), a ()) ⊗ₜ[R] ⨂ₜ[R] (i : ι₂), a ()
instance PiTensorProduct.instAddCommGroupPiTensorProductToCommSemiringToAddCommMonoid {ι : Type u_1} {R : Type u_2} [] {s : ιType u_3} [(i : ι) → AddCommGroup (s i)] [(i : ι) → Module R (s i)] :
AddCommGroup (⨂[R] (i : ι), s i)