# The coevaluation map on finite dimensional vector spaces #

Given a finite dimensional vector space V over a field K this describes the canonical linear map from K to V ⊗ Dual K V which corresponds to the identity function on V.

## Tags #

coevaluation, dual module, tensor product

## Future work #

• Prove that this is independent of the choice of basis on V.
def coevaluation (K : Type u) [] (V : Type v) [] [Module K V] [] :

The coevaluation map is a linear map from a field K to a finite dimensional vector space V.

Equations
• = let bV := ; (().constr K) fun (x : Unit) => i : (), bV i ⊗ₜ[K] bV.coord i
Instances For
theorem coevaluation_apply_one (K : Type u) [] (V : Type v) [] [Module K V] [] :
() 1 = let bV := ; i : (), bV i ⊗ₜ[K] bV.coord i
theorem contractLeft_assoc_coevaluation (K : Type u) [] (V : Type v) [] [Module K V] [] :
LinearMap.rTensor () () ∘ₗ (TensorProduct.assoc K () V ()).symm ∘ₗ LinearMap.lTensor () () = (TensorProduct.lid K ()).symm ∘ₗ (TensorProduct.rid K ())

This lemma corresponds to one of the coherence laws for duals in rigid categories, see CategoryTheory.Monoidal.Rigid.

theorem contractLeft_assoc_coevaluation' (K : Type u) [] (V : Type v) [] [Module K V] [] :
∘ₗ (TensorProduct.assoc K V () V) ∘ₗ = ().symm ∘ₗ ()

This lemma corresponds to one of the coherence laws for duals in rigid categories, see CategoryTheory.Monoidal.Rigid.