# mathlibdocumentation

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] [ M] :
M M →ₗ[R] R

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

Equations
def contract_right (R : Type u) (M : Type v) [comm_ring R] [ M] :
M M →ₗ[R] R

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] [ 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} {M : Type v} [comm_ring R] [ M] (f : M) (m : M) :
M) (f ⊗ₜ[R] m) = f m
@[simp]
theorem contract_right_apply {R : Type u} {M : Type v} [comm_ring R] [ M] (f : M) (m : M) :
M) (m ⊗ₜ[R] f) = f m
@[simp]
theorem dual_tensor_hom_apply {R : Type u} {M N : Type v} [comm_ring R] [ M] [ N] (f : M) (m : M) (n : N) :
( M N) (f ⊗ₜ[R] n)) m = f m n