Contractions

Given modules $M,N$ over a commutative ring $R$, this file defines the natural linear maps: $M^{\ast }\otimes M\to R$, $M\otimes M^{\ast }\to R$, and $M^{\ast }\otimes N\to 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₁) [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 R (Module.Dual R M) M R).toFun LinearMap.id

noncomputable def contractRight (R : Type u) (M : Type v₁) [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 R M (Module.Dual R M) R).toFun LinearMap.id.flip

noncomputable def dualTensorHom (R : Type u) (M : Type v₁) (N : Type v₂) [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 R (Module.Dual R M) N (M →ₗ[R] N)) LinearMap.smulRightₗ

@[simp]

theorem contractLeft_apply {R : Type u} {M : Type v₁} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Module.Dual R M) (m : M) : (contractLeft R M) (f ⊗ₜ[R] m) = f m

@[simp]

theorem contractRight_apply {R : Type u} {M : Type v₁} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Module.Dual R M) (m : M) : (contractRight R M) (m ⊗ₜ[R] f) = f m

@[simp]

theorem dualTensorHom_apply {R : Type u} {M : Type v₁} {N : Type v₂} [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

@[simp]

theorem transpose_dualTensorHom {R : Type u} {M : Type v₁} [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)

@[simp]

theorem dualTensorHom_prodMap_zero {R : Type u} {M : Type v₁} {N : Type v₂} {P : Type v₃} {Q : Type v₄} [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)

@[simp]

theorem zero_prodMap_dualTensorHom {R : Type u} {M : Type v₁} {N : Type v₂} {P : Type v₃} {Q : Type v₄} [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)

theorem map_dualTensorHom {R : Type u} {M : Type v₁} {N : Type v₂} {P : Type v₃} {Q : Type v₄} [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)

@[simp]

theorem comp_dualTensorHom {R : Type u} {M : Type v₁} {N : Type v₂} {P : Type v₃} [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)

theorem toMatrix_dualTensorHom {R : Type u} {M : Type v₁} {N : Type v₂} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {m : Type u_1} {n : Type u_2} [Fintype m] [Finite n] [DecidableEq m] [DecidableEq n] (bM : Basis m R M) (bN : Basis n R N) (j : m) (i : n) : (LinearMap.toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) = Matrix.stdBasisMatrix 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

noncomputable def dualTensorHomEquivOfBasis {ι : Type w} {R : Type u} {M : Type v₁} {N : Type v₂} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Basis ι R M) : TensorProduct R (Module.Dual R M) N ≃ₗ[R] M →ₗ[R] N

If M is free, the natural linear map $M^{\ast }\otimes N\to 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)) ⋯ ⋯

@[simp]

theorem dualTensorHomEquivOfBasis_apply {ι : Type w} {R : Type u} {M : Type v₁} {N : Type v₂} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Basis ι R M) (x : TensorProduct R (Module.Dual R M) N) : (dualTensorHomEquivOfBasis b) x = (dualTensorHom R M N) x

@[simp]

theorem dualTensorHomEquivOfBasis_toLinearMap {ι : Type w} {R : Type u} {M : Type v₁} {N : Type v₂} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Basis ι R M) : ↑(dualTensorHomEquivOfBasis b) = dualTensorHom R M N

@[simp]

theorem dualTensorHomEquivOfBasis_symm_cancel_left {ι : Type w} {R : Type u} {M : Type v₁} {N : Type v₂} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Basis ι R M) (x : TensorProduct R (Module.Dual R M) N) : (dualTensorHomEquivOfBasis b).symm ((dualTensorHom R M N) x) = x

@[simp]

theorem dualTensorHomEquivOfBasis_symm_cancel_right {ι : Type w} {R : Type u} {M : Type v₁} {N : Type v₂} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Basis ι R M) (x : M →ₗ[R] N) : (dualTensorHom R M N) ((dualTensorHomEquivOfBasis b).symm x) = x

noncomputable def dualTensorHomEquiv (R : Type u) (M : Type v₁) (N : Type v₂) [CommRing R] [AddCommGroup M] [AddCommGroup 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^{\ast }\otimes N\to Hom(M,N)$ is an equivalence.

Equations

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

noncomputable def lTensorHomEquivHomLTensor (R : Type u) (M : Type v₁) (P : Type v₃) (Q : Type v₄) [CommRing R] [AddCommGroup M] [AddCommGroup P] [AddCommGroup 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.

noncomputable def rTensorHomEquivHomRTensor (R : Type u) (M : Type v₁) (P : Type v₃) (Q : Type v₄) [CommRing R] [AddCommGroup M] [AddCommGroup P] [AddCommGroup 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.

@[simp]

theorem lTensorHomEquivHomLTensor_toLinearMap (R : Type u) (M : Type v₁) (P : Type v₃) (Q : Type v₄) [CommRing R] [AddCommGroup M] [AddCommGroup P] [AddCommGroup 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 R M P Q

@[simp]

theorem rTensorHomEquivHomRTensor_toLinearMap (R : Type u) (M : Type v₁) (P : Type v₃) (Q : Type v₄) [CommRing R] [AddCommGroup M] [AddCommGroup P] [AddCommGroup 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 R M P Q

@[simp]

theorem lTensorHomEquivHomLTensor_apply {R : Type u} {M : Type v₁} {P : Type v₃} {Q : Type v₄} [CommRing R] [AddCommGroup M] [AddCommGroup P] [AddCommGroup 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 R M P Q) x

@[simp]

theorem rTensorHomEquivHomRTensor_apply {R : Type u} {M : Type v₁} {P : Type v₃} {Q : Type v₄} [CommRing R] [AddCommGroup M] [AddCommGroup P] [AddCommGroup 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 R M P Q) x

noncomputable def homTensorHomEquiv (R : Type u) (M : Type v₁) (N : Type v₂) (P : Type v₃) (Q : Type v₄) [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [AddCommGroup 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.

@[simp]

theorem homTensorHomEquiv_toLinearMap (R : Type u) (M : Type v₁) (N : Type v₂) (P : Type v₃) (Q : Type v₄) [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [AddCommGroup 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 R M N P Q

@[simp]

theorem homTensorHomEquiv_apply {R : Type u} {M : Type v₁} {N : Type v₂} {P : Type v₃} {Q : Type v₄} [CommRing R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [AddCommGroup 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 R M N P Q) x