# 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

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

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

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

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

Equations
Instances For
noncomputable 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.

Equations
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) :
(() (f ⊗ₜ[R] p)).prodMap 0 = (dualTensorHom R (M × N) (P × Q)) ((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)) ((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) :
() (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) :
() (() (bM.coord 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.

Equations
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) :
.symm (() 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) :
() (.symm x) = 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.

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

Equations
• One or more equations did not get rendered due to their size.
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.

Equations
• One or more equations did not get rendered due to their size.
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.

Equations
• One or more equations did not get rendered due to their size.
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