# 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

source
def contractLeft (R : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] :
TensorProduct R (Module.Dual R M) M →ₗ[R] R

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

Equations

- contractLeft R M = (TensorProduct.uncurry (RingHom.id R) (Module.Dual R M) M R).toFun LinearMap.id

Instances For

source
def contractRight (R : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] :
TensorProduct R M (Module.Dual R M) →ₗ[R] R

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

Equations

- contractRight R M = (TensorProduct.uncurry (RingHom.id R) M (Module.Dual R M) R).toFun LinearMap.id.flip

Instances For

source
def dualTensorHom (R : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
TensorProduct R (Module.Dual R M) N →ₗ[R] M →ₗ[R] N

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

Equations

- dualTensorHom R M N = (TensorProduct.uncurry (RingHom.id R) (Module.Dual R M) N (M →ₗ[R] N)) LinearMap.smulRightₗ

Instances For

source
@[simp]
theorem contractLeft_apply {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Module.Dual R M) (m : M) :
(contractLeft R M) (f ⊗ₜ[R] m) = f m
source
@[simp]
theorem contractRight_apply {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Module.Dual R M) (m : M) :
(contractRight R M) (m ⊗ₜ[R] f) = f m
source
@[simp]
theorem dualTensorHom_apply {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : Module.Dual R M) (m : M) (n : N) :
((dualTensorHom R M N) (f ⊗ₜ[R] n)) m = f m • n
source
@[simp]
theorem transpose_dualTensorHom {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Module.Dual R M) (m : M) :
Module.Dual.transpose ((dualTensorHom R M M) (f ⊗ₜ[R] m)) = (dualTensorHom R (Module.Dual R M) (Module.Dual R M)) ((Module.Dual.eval R M) m ⊗ₜ[R] f)
source
@[simp]
theorem dualTensorHom_prodMap_zero {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : Module.Dual R M) (p : P) :
((dualTensorHom R M P) (f ⊗ₜ[R] p)).prodMap 0 = (dualTensorHom R (M × N) (P × Q)) ((f ∘ₗ LinearMap.fst R M N) ⊗ₜ[R] (LinearMap.inl R P Q) p)
source
@[simp]
theorem zero_prodMap_dualTensorHom {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : Module.Dual R N) (q : Q) :
LinearMap.prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) = (dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ LinearMap.snd R M N) ⊗ₜ[R] (LinearMap.inr R P Q) q)
source
theorem map_dualTensorHom {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : Module.Dual R M) (p : P) (g : Module.Dual R N) (q : Q) :
TensorProduct.map ((dualTensorHom R M P) (f ⊗ₜ[R] p)) ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) = (dualTensorHom R (TensorProduct R M N) (TensorProduct R P Q)) ((TensorProduct.dualDistrib R M N) (f ⊗ₜ[R] g) ⊗ₜ[R] (p ⊗ₜ[R] q))
source
@[simp]
theorem comp_dualTensorHom {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : Module.Dual R M) (n : N) (g : Module.Dual R N) (p : P) :
(dualTensorHom R N P) (g ⊗ₜ[R] p) ∘ₗ (dualTensorHom R M N) (f ⊗ₜ[R] n) = g n • (dualTensorHom R M P) (f ⊗ₜ[R] p)
source
theorem toMatrix_dualTensorHom {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {m : Type u_7} {n : Type u_8} [Fintype m] [Finite n] [DecidableEq m] [DecidableEq n] (bM : Module.Basis m R M) (bN : Module.Basis n R N) (j : m) (i : n) :
(LinearMap.toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) = Matrix.single i j 1

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

source
noncomputable def dualTensorHomEquivOfBasis {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Module.Basis ι R M) :
TensorProduct R (Module.Dual R M) N ≃ₗ[R] M →ₗ[R] N

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

- dualTensorHomEquivOfBasis b = LinearEquiv.ofLinear (dualTensorHom R M N) (∑ i : ι, (TensorProduct.mk R (Module.Dual R M) N) (b.dualBasis i) ∘ₗ LinearMap.applyₗ (b i)) ⋯ ⋯

Instances For

source
@[simp]
theorem dualTensorHomEquivOfBasis_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Module.Basis ι R M) (x : TensorProduct R (Module.Dual R M) N) :
(dualTensorHomEquivOfBasis b) x = (dualTensorHom R M N) x
source
@[simp]
theorem dualTensorHomEquivOfBasis_toLinearMap {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Module.Basis ι R M) :
↑(dualTensorHomEquivOfBasis b) = dualTensorHom R M N
source
@[simp]
theorem dualTensorHomEquivOfBasis_symm_cancel_left {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Module.Basis ι R M) (x : TensorProduct R (Module.Dual R M) N) :
(dualTensorHomEquivOfBasis b).symm ((dualTensorHom R M N) x) = x
source
@[simp]
theorem dualTensorHomEquivOfBasis_symm_cancel_right {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Module.Basis ι R M) (x : M →ₗ[R] N) :
(dualTensorHom R M N) ((dualTensorHomEquivOfBasis b).symm x) = x
source
noncomputable def dualTensorHomEquiv (R : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Free R M] [Module.Finite R M] :
TensorProduct R (Module.Dual R M) N ≃ₗ[R] M →ₗ[R] N

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

Equations

- dualTensorHomEquiv R M N = dualTensorHomEquivOfBasis (Module.Free.chooseBasis R M)

Instances For

source
noncomputable def lTensorHomEquivHomLTensor (R : Type u_2) (M : Type u_3) (P : Type u_5) (Q : Type u_6) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] [Module.Free R M] [Module.Finite R M] :
TensorProduct R P (M →ₗ[R] Q) ≃ₗ[R] M →ₗ[R] TensorProduct R P 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

source
noncomputable def rTensorHomEquivHomRTensor (R : Type u_2) (M : Type u_3) (P : Type u_5) (Q : Type u_6) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] [Module.Free R M] [Module.Finite R M] :
TensorProduct R (M →ₗ[R] P) Q ≃ₗ[R] M →ₗ[R] TensorProduct R P 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

source
@[simp]
theorem lTensorHomEquivHomLTensor_toLinearMap (R : Type u_2) (M : Type u_3) (P : Type u_5) (Q : Type u_6) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] [Module.Free R M] [Module.Finite R M] :
↑(lTensorHomEquivHomLTensor R M P Q) = TensorProduct.lTensorHomToHomLTensor (RingHom.id R) M P Q
source
@[simp]
theorem rTensorHomEquivHomRTensor_toLinearMap (R : Type u_2) (M : Type u_3) (P : Type u_5) (Q : Type u_6) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] [Module.Free R M] [Module.Finite R M] :
↑(rTensorHomEquivHomRTensor R M P Q) = TensorProduct.rTensorHomToHomRTensor (RingHom.id R) M P Q
source
@[simp]
theorem lTensorHomEquivHomLTensor_apply {R : Type u_2} {M : Type u_3} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] [Module.Free R M] [Module.Finite R M] (x : TensorProduct R P (M →ₗ[R] Q)) :
(lTensorHomEquivHomLTensor R M P Q) x = (TensorProduct.lTensorHomToHomLTensor (RingHom.id R) M P Q) x
source
@[simp]
theorem rTensorHomEquivHomRTensor_apply {R : Type u_2} {M : Type u_3} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] [Module.Free R M] [Module.Finite R M] (x : TensorProduct R (M →ₗ[R] P) Q) :
(rTensorHomEquivHomRTensor R M P Q) x = (TensorProduct.rTensorHomToHomRTensor (RingHom.id R) M P Q) x
source
noncomputable def homTensorHomEquiv (R : Type u_2) (M : Type u_3) (N : Type u_4) (P : Type u_5) (Q : Type u_6) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] [Module.Free R M] [Module.Finite R M] [Module.Free R N] [Module.Finite R N] :
TensorProduct R (M →ₗ[R] P) (N →ₗ[R] Q) ≃ₗ[R] TensorProduct R M N →ₗ[R] TensorProduct R P 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

source
@[simp]
theorem homTensorHomEquiv_toLinearMap (R : Type u_2) (M : Type u_3) (N : Type u_4) (P : Type u_5) (Q : Type u_6) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] [Module.Free R M] [Module.Finite R M] [Module.Free R N] [Module.Finite R N] :
↑(homTensorHomEquiv R M N P Q) = TensorProduct.homTensorHomMap (RingHom.id R) M N P Q
source
@[simp]
theorem homTensorHomEquiv_apply {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] [Module.Free R M] [Module.Finite R M] [Module.Free R N] [Module.Finite R N] (x : TensorProduct R (M →ₗ[R] P) (N →ₗ[R] Q)) :
(homTensorHomEquiv R M N P Q) x = (TensorProduct.homTensorHomMap (RingHom.id R) M N P Q) x