# mathlib3documentation

linear_algebra.contraction

# Contractions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 contract_left (R : Type u_2) (M : Type u_3) [ M] :
M) M →ₗ[R] R

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

Equations
def contract_right (R : Type u_2) (M : Type u_3) [ M] :
M) →ₗ[R] R

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

Equations
def dual_tensor_hom (R : Type u_2) (M : Type u_3) (N : Type u_4) [ M] [ N] :
M) N →ₗ[R] M →ₗ[R] N

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

Equations
@[simp]
theorem contract_left_apply {R : Type u_2} {M : Type u_3} [ M] (f : M) (m : M) :
M) (f ⊗ₜ[R] m) = f m
@[simp]
theorem contract_right_apply {R : Type u_2} {M : Type u_3} [ M] (f : M) (m : M) :
M) (m ⊗ₜ[R] f) = f m
@[simp]
theorem dual_tensor_hom_apply {R : Type u_2} {M : Type u_3} {N : Type u_4} [ M] [ N] (f : M) (m : M) (n : N) :
( M N) (f ⊗ₜ[R] n)) m = f m n
@[simp]
theorem transpose_dual_tensor_hom {R : Type u_2} {M : Type u_3} [ M] (f : M) (m : M) :
module.dual.transpose ( M M) (f ⊗ₜ[R] m)) = M) M)) ( M) m ⊗ₜ[R] f)
@[simp]
theorem dual_tensor_hom_prod_map_zero {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [ M] [ N] [ P] [ Q] (f : M) (p : P) :
( M P) (f ⊗ₜ[R] p)).prod_map 0 = (M × N) (P × Q)) M N) ⊗ₜ[R] P Q) p)
@[simp]
theorem zero_prod_map_dual_tensor_hom {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [ M] [ N] [ P] [ Q] (g : N) (q : Q) :
0.prod_map ( N Q) (g ⊗ₜ[R] q)) = (M × N) (P × Q)) M N) ⊗ₜ[R] P Q) q)
theorem map_dual_tensor_hom {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [ M] [ N] [ P] [ Q] (f : M) (p : P) (g : N) (q : Q) :
tensor_product.map ( M P) (f ⊗ₜ[R] p)) ( N Q) (g ⊗ₜ[R] q)) = M N) P Q)) ( N) (f ⊗ₜ[R] g) ⊗ₜ[R] (p ⊗ₜ[R] q))
@[simp]
theorem comp_dual_tensor_hom {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [ M] [ N] [ P] (f : M) (n : N) (g : N) (p : P) :
( N P) (g ⊗ₜ[R] p)).comp ( M N) (f ⊗ₜ[R] n)) = g n M P) (f ⊗ₜ[R] p)
theorem to_matrix_dual_tensor_hom {R : Type u_2} {M : Type u_3} {N : Type u_4} [ M] [ N] {m : Type u_1} {n : Type u_5} [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (bM : R M) (bN : R N) (j : m) (i : n) :
bN) ( M N) (bM.coord j ⊗ₜ[R] bN i)) =

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

noncomputable def dual_tensor_hom_equiv_of_basis {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [comm_ring R] [ M] [ N] [decidable_eq ι] [fintype ι] (b : R M) :
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
@[simp]
theorem dual_tensor_hom_equiv_of_basis_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [comm_ring R] [ M] [ N] [decidable_eq ι] [fintype ι] (b : R M) (ᾰ : M) N) :
= M N)
@[simp]
theorem dual_tensor_hom_equiv_of_basis_to_linear_map {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [comm_ring R] [ M] [ N] [decidable_eq ι] [fintype ι] (b : R M) :
@[simp]
theorem dual_tensor_hom_equiv_of_basis_symm_cancel_left {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [comm_ring R] [ M] [ N] [decidable_eq ι] [fintype ι] (b : R M) (x : M) N) :
( M N) x) = x
@[simp]
theorem dual_tensor_hom_equiv_of_basis_symm_cancel_right {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [comm_ring R] [ M] [ N] [decidable_eq ι] [fintype ι] (b : R M) (x : M →ₗ[R] N) :
M N) x) = x
@[simp]
noncomputable def dual_tensor_hom_equiv (R : Type u_2) (M : Type u_3) (N : Type u_4) [comm_ring R] [ M] [ N] [ M] [ M] [nontrivial R] :
M) N ≃ₗ[R] M →ₗ[R] N

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

Equations
noncomputable def ltensor_hom_equiv_hom_ltensor (R : Type u_2) (M : Type u_3) (P : Type u_5) (Q : Type u_6) [comm_ring R] [ M] [ P] [ Q] [ M] [ M] [nontrivial R] :
(M →ₗ[R] Q) ≃ₗ[R] M →ₗ[R] Q

When M is a finite free module, the map ltensor_hom_to_hom_ltensor is an equivalence. Note that ltensor_hom_equiv_hom_ltensor is not defined directly in terms of ltensor_hom_to_hom_ltensor, but the equivalence between the two is given by ltensor_hom_equiv_hom_ltensor_to_linear_map and ltensor_hom_equiv_hom_ltensor_apply.

Equations
noncomputable def rtensor_hom_equiv_hom_rtensor (R : Type u_2) (M : Type u_3) (P : Type u_5) (Q : Type u_6) [comm_ring R] [ M] [ P] [ Q] [ M] [ M] [nontrivial R] :
(M →ₗ[R] P) Q ≃ₗ[R] M →ₗ[R] Q

When M is a finite free module, the map rtensor_hom_to_hom_rtensor is an equivalence. Note that rtensor_hom_equiv_hom_rtensor is not defined directly in terms of rtensor_hom_to_hom_rtensor, but the equivalence between the two is given by rtensor_hom_equiv_hom_rtensor_to_linear_map and rtensor_hom_equiv_hom_rtensor_apply.

Equations
@[simp]
theorem ltensor_hom_equiv_hom_ltensor_to_linear_map (R : Type u_2) (M : Type u_3) (P : Type u_5) (Q : Type u_6) [comm_ring R] [ M] [ P] [ Q] [ M] [ M] [nontrivial R] :
@[simp]
theorem rtensor_hom_equiv_hom_rtensor_to_linear_map (R : Type u_2) (M : Type u_3) (P : Type u_5) (Q : Type u_6) [comm_ring R] [ M] [ P] [ Q] [ M] [ M] [nontrivial R] :
@[simp]
theorem ltensor_hom_equiv_hom_ltensor_apply {R : Type u_2} {M : Type u_3} {P : Type u_5} {Q : Type u_6} [comm_ring R] [ M] [ P] [ Q] [ M] [ M] [nontrivial R] (x : (M →ₗ[R] Q)) :
Q) x = x
@[simp]
theorem rtensor_hom_equiv_hom_rtensor_apply {R : Type u_2} {M : Type u_3} {P : Type u_5} {Q : Type u_6} [comm_ring R] [ M] [ P] [ Q] [ M] [ M] [nontrivial R] (x : (M →ₗ[R] P) Q) :
Q) x = x
noncomputable def hom_tensor_hom_equiv (R : Type u_2) (M : Type u_3) (N : Type u_4) (P : Type u_5) (Q : Type u_6) [comm_ring R] [ M] [ N] [ P] [ Q] [ M] [ M] [ N] [ N] [nontrivial R] :
(M →ₗ[R] P) (N →ₗ[R] Q) ≃ₗ[R] N →ₗ[R] Q

When M and N are free R modules, the map hom_tensor_hom_map is an equivalence. Note that hom_tensor_hom_equiv is not defined directly in terms of hom_tensor_hom_map, but the equivalence between the two is given by hom_tensor_hom_equiv_to_linear_map and hom_tensor_hom_equiv_apply.

Equations
@[simp]
theorem hom_tensor_hom_equiv_to_linear_map (R : Type u_2) (M : Type u_3) (N : Type u_4) (P : Type u_5) (Q : Type u_6) [comm_ring R] [ M] [ N] [ P] [ Q] [ M] [ M] [ N] [ N] [nontrivial R] :
N P Q).to_linear_map = Q
@[simp]
theorem hom_tensor_hom_equiv_apply {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [comm_ring R] [ M] [ N] [ P] [ Q] [ M] [ M] [ N] [ N] [nontrivial R] (x : (M →ₗ[R] P) (N →ₗ[R] Q)) :
N P Q) x = Q) x