# Documentation

Mathlib.LinearAlgebra.Contraction

# Contractions #

Given modules $M, N$ over a commutative ring $R$, this file defines the natural linear maps: $M^* \otimes M \to R$, $M \otimes M^* \to R$, and $M^* \otimes N → Hom(M, N)$, as well as proving some basic properties of these maps.

## Tags #

contraction, dual module, tensor product

def contractLeft (R : Type u) (M : Type v₁) [] [] [Module R M] :

The natural left-handed pairing between a module and its dual.

Instances For
def contractRight (R : Type u) (M : Type v₁) [] [] [Module R M] :

The natural right-handed pairing between a module and its dual.

Instances For
def dualTensorHom (R : Type u) (M : Type v₁) (N : Type v₂) [] [] [] [Module R M] [Module R N] :

The natural map associating a linear map to the tensor product of two modules.

Instances For
@[simp]
theorem contractLeft_apply {R : Type u} {M : Type v₁} [] [] [Module R M] (f : ) (m : M) :
↑() (f ⊗ₜ[R] m) = f m
@[simp]
theorem contractRight_apply {R : Type u} {M : Type v₁} [] [] [Module R M] (f : ) (m : M) :
↑() (m ⊗ₜ[R] f) = f m
@[simp]
theorem dualTensorHom_apply {R : Type u} {M : Type v₁} {N : Type v₂} [] [] [] [Module R M] [Module R N] (f : ) (m : M) (n : N) :
↑(↑() (f ⊗ₜ[R] n)) m = f m n
@[simp]
theorem transpose_dualTensorHom {R : Type u} {M : Type v₁} [] [] [Module R M] (f : ) (m : M) :
Module.Dual.transpose (↑() (f ⊗ₜ[R] m)) = ↑(dualTensorHom R () ()) (↑() m ⊗ₜ[R] f)
@[simp]
theorem dualTensorHom_prodMap_zero {R : Type u} {M : Type v₁} {N : Type v₂} {P : Type v₃} {Q : Type v₄} [] [] [] [] [] [Module R M] [Module R N] [Module R P] [Module R Q] (f : ) (p : P) :
LinearMap.prodMap (↑() (f ⊗ₜ[R] p)) 0 = ↑(dualTensorHom R (M × N) (P × Q)) (LinearMap.comp f () ⊗ₜ[R] ↑() p)
@[simp]
theorem zero_prodMap_dualTensorHom {R : Type u} {M : Type v₁} {N : Type v₂} {P : Type v₃} {Q : Type v₄} [] [] [] [] [] [Module R M] [Module R N] [Module R P] [Module R Q] (g : ) (q : Q) :
LinearMap.prodMap 0 (↑() (g ⊗ₜ[R] q)) = ↑(dualTensorHom R (M × N) (P × Q)) (LinearMap.comp g () ⊗ₜ[R] ↑() q)
theorem map_dualTensorHom {R : Type u} {M : Type v₁} {N : Type v₂} {P : Type v₃} {Q : Type v₄} [] [] [] [] [] [Module R M] [Module R N] [Module R P] [Module R Q] (f : ) (p : P) (g : ) (q : Q) :
TensorProduct.map (↑() (f ⊗ₜ[R] p)) (↑() (g ⊗ₜ[R] q)) = ↑(dualTensorHom R () ()) (↑() (f ⊗ₜ[R] g) ⊗ₜ[R] p ⊗ₜ[R] q)
@[simp]
theorem comp_dualTensorHom {R : Type u} {M : Type v₁} {N : Type v₂} {P : Type v₃} [] [] [] [] [Module R M] [Module R N] [Module R P] (f : ) (n : N) (g : ) (p : P) :
LinearMap.comp (↑() (g ⊗ₜ[R] p)) (↑() (f ⊗ₜ[R] n)) = g n ↑() (f ⊗ₜ[R] p)
theorem toMatrix_dualTensorHom {R : Type u} {M : Type v₁} {N : Type v₂} [] [] [] [Module R M] [Module R N] {m : Type u_1} {n : Type u_2} [] [] [] [] (bM : Basis m R M) (bN : Basis n R N) (j : m) (i : n) :
↑() (↑() (Basis.coord bM j ⊗ₜ[R] bN i)) =

As a matrix, dualTensorHom evaluated on a basis element of M* ⊗ N is a matrix with a single one and zeros elsewhere

noncomputable def dualTensorHomEquivOfBasis {ι : Type w} {R : Type u} {M : Type v₁} {N : Type v₂} [] [] [] [Module R M] [Module R N] [] [] (b : Basis ι R M) :

If M is free, the natural linear map $M^* ⊗ N → Hom(M, N)$ is an equivalence. This function provides this equivalence in return for a basis of M.

Instances For
@[simp]
theorem dualTensorHomEquivOfBasis_apply {ι : Type w} {R : Type u} {M : Type v₁} {N : Type v₂} [] [] [] [Module R M] [Module R N] [] [] (b : Basis ι R M) (x : TensorProduct R () N) :
= ↑() x
@[simp]
theorem dualTensorHomEquivOfBasis_toLinearMap {ι : Type w} {R : Type u} {M : Type v₁} {N : Type v₂} [] [] [] [Module R M] [Module R N] [] [] (b : Basis ι R M) :
=
@[simp]
theorem dualTensorHomEquivOfBasis_symm_cancel_left {ι : Type w} {R : Type u} {M : Type v₁} {N : Type v₂} [] [] [] [Module R M] [Module R N] [] [] (b : Basis ι R M) (x : TensorProduct R () N) :
↑() (↑() x) = x
@[simp]
theorem dualTensorHomEquivOfBasis_symm_cancel_right {ι : Type w} {R : Type u} {M : Type v₁} {N : Type v₂} [] [] [] [Module R M] [Module R N] [] [] (b : Basis ι R M) (x : M →ₗ[R] N) :
↑() () = x
noncomputable def dualTensorHomEquiv (R : Type u) (M : Type v₁) (N : Type v₂) [] [] [] [Module R M] [Module R N] [] [] :

If M is finite free, the natural map $M^* ⊗ N → Hom(M, N)$ is an equivalence.

Instances For
noncomputable def lTensorHomEquivHomLTensor (R : Type u) (M : Type v₁) (P : Type v₃) (Q : Type v₄) [] [] [] [] [Module R M] [Module R P] [Module R Q] [] [] :

When M is a finite free module, the map lTensorHomToHomLTensor is an equivalence. Note that lTensorHomEquivHomLTensor is not defined directly in terms of lTensorHomToHomLTensor, but the equivalence between the two is given by lTensorHomEquivHomLTensor_toLinearMap and lTensorHomEquivHomLTensor_apply.

Instances For
noncomputable def rTensorHomEquivHomRTensor (R : Type u) (M : Type v₁) (P : Type v₃) (Q : Type v₄) [] [] [] [] [Module R M] [Module R P] [Module R Q] [] [] :

When M is a finite free module, the map rTensorHomToHomRTensor is an equivalence. Note that rTensorHomEquivHomRTensor is not defined directly in terms of rTensorHomToHomRTensor, but the equivalence between the two is given by rTensorHomEquivHomRTensor_toLinearMap and rTensorHomEquivHomRTensor_apply.

Instances For
@[simp]
theorem lTensorHomEquivHomLTensor_toLinearMap (R : Type u) (M : Type v₁) (P : Type v₃) (Q : Type v₄) [] [] [] [] [Module R M] [Module R P] [Module R Q] [] [] :
↑() =
@[simp]
theorem rTensorHomEquivHomRTensor_toLinearMap (R : Type u) (M : Type v₁) (P : Type v₃) (Q : Type v₄) [] [] [] [] [Module R M] [Module R P] [Module R Q] [] [] :
↑() =
@[simp]
theorem lTensorHomEquivHomLTensor_apply {R : Type u} {M : Type v₁} {P : Type v₃} {Q : Type v₄} [] [] [] [] [Module R M] [Module R P] [Module R Q] [] [] (x : TensorProduct R P (M →ₗ[R] Q)) :
↑() x = ↑() x
@[simp]
theorem rTensorHomEquivHomRTensor_apply {R : Type u} {M : Type v₁} {P : Type v₃} {Q : Type v₄} [] [] [] [] [Module R M] [Module R P] [Module R Q] [] [] (x : TensorProduct R (M →ₗ[R] P) Q) :
↑() x = ↑() x
noncomputable def homTensorHomEquiv (R : Type u) (M : Type v₁) (N : Type v₂) (P : Type v₃) (Q : Type v₄) [] [] [] [] [] [Module R M] [Module R N] [Module R P] [Module R Q] [] [] [] [] :

When M and N are free R modules, the map homTensorHomMap is an equivalence. Note that homTensorHomEquiv is not defined directly in terms of homTensorHomMap, but the equivalence between the two is given by homTensorHomEquiv_toLinearMap and homTensorHomEquiv_apply.

Instances For
@[simp]
theorem homTensorHomEquiv_toLinearMap (R : Type u) (M : Type v₁) (N : Type v₂) (P : Type v₃) (Q : Type v₄) [] [] [] [] [] [Module R M] [Module R N] [Module R P] [Module R Q] [] [] [] [] :
↑(homTensorHomEquiv R M N P Q) =
@[simp]
theorem homTensorHomEquiv_apply {R : Type u} {M : Type v₁} {N : Type v₂} {P : Type v₃} {Q : Type v₄} [] [] [] [] [] [Module R M] [Module R N] [Module R P] [Module R Q] [] [] [] [] (x : TensorProduct R (M →ₗ[R] P) (N →ₗ[R] Q)) :
↑(homTensorHomEquiv R M N P Q) x = ↑() x