mathlib3 documentation

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) [comm_semiring R] [add_comm_monoid M] [module R M] :

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

Equations
def contract_right (R : Type u_2) (M : Type u_3) [comm_semiring R] [add_comm_monoid M] [module R M] :

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) [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [module R M] [module 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} [comm_semiring R] [add_comm_monoid M] [module R M] (f : module.dual R M) (m : M) :
(contract_left R M) (f ⊗ₜ[R] m) = f m
@[simp]
theorem contract_right_apply {R : Type u_2} {M : Type u_3} [comm_semiring R] [add_comm_monoid M] [module R M] (f : module.dual R M) (m : M) :
@[simp]
theorem dual_tensor_hom_apply {R : Type u_2} {M : Type u_3} {N : Type u_4} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [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
@[simp]
@[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} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R N] [module R P] [module R Q] (f : module.dual R M) (p : 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} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid Q] [module R M] [module R N] [module R P] [module R Q] (g : module.dual R N) (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} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [add_comm_monoid 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) :
@[simp]
theorem comp_dual_tensor_hom {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P] [module R M] [module R N] [module R P] (f : module.dual R M) (n : N) (g : module.dual R N) (p : P) :
((dual_tensor_hom R N P) (g ⊗ₜ[R] p)).comp ((dual_tensor_hom R M N) (f ⊗ₜ[R] n)) = g n (dual_tensor_hom R M P) (f ⊗ₜ[R] p)
theorem to_matrix_dual_tensor_hom {R : Type u_2} {M : Type u_3} {N : Type u_4} [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] {m : Type u_1} {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) :

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] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [decidable_eq ι] [fintype ι] (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
@[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] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [decidable_eq ι] [fintype ι] (b : basis ι R M) (ᾰ : tensor_product R (module.dual R M) N) :
@[simp]
@[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] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [decidable_eq ι] [fintype ι] (b : basis ι R M) (x : tensor_product R (module.dual R M) N) :
@[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] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [decidable_eq ι] [fintype ι] (b : basis ι R M) (x : M →ₗ[R] N) :
@[simp]
noncomputable def dual_tensor_hom_equiv (R : Type u_2) (M : Type u_3) (N : Type u_4) [comm_ring R] [add_comm_group M] [add_comm_group N] [module R M] [module R N] [module.free R M] [module.finite R M] [nontrivial R] :

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] [add_comm_group M] [add_comm_group P] [add_comm_group Q] [module R M] [module R P] [module R Q] [module.free R M] [module.finite R M] [nontrivial R] :

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] [add_comm_group M] [add_comm_group P] [add_comm_group Q] [module R M] [module R P] [module R Q] [module.free R M] [module.finite R M] [nontrivial R] :

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
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] [add_comm_group M] [add_comm_group N] [add_comm_group P] [add_comm_group 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] [nontrivial R] :

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] [add_comm_group M] [add_comm_group N] [add_comm_group P] [add_comm_group 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] [nontrivial R] :
@[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] [add_comm_group M] [add_comm_group N] [add_comm_group P] [add_comm_group 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] [nontrivial R] (x : tensor_product R (M →ₗ[R] P) (N →ₗ[R] Q)) :