mathlib documentation

linear_algebra.coevaluation

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 #

noncomputable def coevaluation (K : Type u) [field K] (V : Type v) [add_comm_group V] [module K V] [finite_dimensional K V] :

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

Equations
theorem coevaluation_apply_one (K : Type u) [field K] (V : Type v) [add_comm_group V] [module K V] [finite_dimensional K V] :

This lemma corresponds to one of the coherence laws for duals in rigid categories, see category_theory.monoidal.rigid.

This lemma corresponds to one of the coherence laws for duals in rigid categories, see category_theory.monoidal.rigid.