mathlib documentation

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

source
def contract_left (R : Type u_1) (M : Type u_2) [add_comm_group M] [comm_ring R] [module R M] :
module.dual R M ⊗ M →ₗ[R] R

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

Equations
source
def contract_right (R : Type u_1) (M : Type u_2) [add_comm_group M] [comm_ring R] [module R M] :
M ⊗ module.dual R M →ₗ[R] R

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

Equations
source
def dual_tensor_hom (R : Type u_1) (M : Type u_2) (N : Type u_3) [add_comm_group M] [add_comm_group N] [comm_ring R] [module R M] [module R N] :
module.dual R M ⊗ N →ₗ[R] M →ₗ[R] N

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

Equations
source
@[simp]
theorem contract_left_apply {R : Type u_1} {M : Type u_2} [add_comm_group M] [comm_ring R] [module R M] (f : module.dual R M) (m : M) :
⇑(contract_left R M) (f ⊗ₜ[R] m) = ⇑f m
source
@[simp]
theorem contract_right_apply {R : Type u_1} {M : Type u_2} [add_comm_group M] [comm_ring R] [module R M] (f : module.dual R M) (m : M) :
⇑(contract_right R M) (m ⊗ₜ[R] f) = ⇑f m
source
@[simp]
theorem dual_tensor_hom_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [comm_ring R] [module R M] [module R N] (f : module.dual R M) (m : M) (n : N) :
⇑(⇑(dual_tensor_hom R M N) (f ⊗ₜ[R] n)) m = ⇑f m • n
source
theorem to_matrix_dual_tensor_hom {R : Type u_1} {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [comm_ring R] [module R M] [module R N] {m : Type u_4} {n : Type u_5} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (bM : basis m R M) (bN : basis n R N) (j : m) (i : n) :
⇑(linear_map.to_matrix bM bN) (⇑(dual_tensor_hom R M N) (bM.coord j ⊗ₜ[R] ⇑bN i)) = matrix.std_basis_matrix i j 1

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

source
noncomputable def dual_tensor_hom_equiv_of_basis {R : Type u_1} {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [comm_ring R] [module R M] [module R N] {ι : Type u_4} [decidable_eq ι] [fintype ι] (b : basis ι R M) :
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
source
@[simp]
theorem dual_tensor_hom_equiv_of_basis_symm_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [comm_ring R] [module R M] [module R N] {ι : Type u_4} [decidable_eq ι] [fintype ι] (b : basis ι R M) (ᾰ : M →ₗ[R] N) :
⇑((dual_tensor_hom_equiv_of_basis b).symm) ᾰ = ∑ (x : ι), b.coord x ⊗ₜ[R] ⇑ᾰ (⇑b x)
source
@[simp]
theorem dual_tensor_hom_equiv_of_basis_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [comm_ring R] [module R M] [module R N] {ι : Type u_4} [decidable_eq ι] [fintype ι] (b : basis ι R M) (ᾰ : module.dual R M ⊗ N) :
⇑(dual_tensor_hom_equiv_of_basis b) ᾰ = ⇑(dual_tensor_hom R M N) ᾰ
source
@[simp]
theorem dual_tensor_hom_equiv_of_basis_to_linear_map {R : Type u_1} {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [comm_ring R] [module R M] [module R N] {ι : Type u_4} [decidable_eq ι] [fintype ι] (b : basis ι R M) :
(dual_tensor_hom_equiv_of_basis b).to_linear_map = dual_tensor_hom R M N
source
@[simp]
noncomputable def dual_tensor_hom_equiv {R : Type u_1} {M : Type u_2} {N : Type u_3} [add_comm_group M] [add_comm_group N] [comm_ring R] [module R M] [module R N] [module.free R M] [module.finite R M] [nontrivial 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