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

def contract_left (R : Type u) (M : Type v) [comm_ring R] [add_comm_group M] [module R M] :

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

Equations
def contract_right (R : Type u) (M : Type v) [comm_ring R] [add_comm_group M] [module R M] :

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

Equations
def dual_tensor_hom (R : Type u) (M N : Type v) [comm_ring R] [add_comm_group M] [add_comm_group 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} {M : Type v} [comm_ring R] [add_comm_group 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} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (f : module.dual R M) (m : M) :
@[simp]
theorem dual_tensor_hom_apply {R : Type u} {M N : Type v} [comm_ring R] [add_comm_group M] [add_comm_group 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