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] :
tensor_product R (module.dual R M) M →ₗ[R] R
The natural left-handed pairing between a module and its dual.
Equations
- contract_left R M = (tensor_product.uncurry R (module.dual R M) M R).to_fun linear_map.id
def
contract_right
(R : Type u)
(M : Type v)
[comm_ring R]
[add_comm_group M]
[module R M] :
tensor_product R M (module.dual R M) →ₗ[R] R
The natural right-handed pairing between a module and its dual.
Equations
- contract_right R M = (tensor_product.uncurry R M (module.dual R M) R).to_fun linear_map.id.flip
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] :
tensor_product R (module.dual R M) N →ₗ[R] M →ₗ[R] N
The natural map associating a linear map to the tensor product of two modules.
Equations
- dual_tensor_hom R M N = let M' : Type (max v u) := module.dual R M in ⇑(tensor_product.uncurry R M' N (M →ₗ[R] N)) linear_map.smul_rightₗ
@[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) :
@[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) :