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) [Field K] (V : Type v) [AddCommGroup V] [Module K V] [FiniteDimensional K V] : K →ₗ[K] TensorProduct K V (Module.Dual K V)

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

theorem coevaluation_apply_one (K : Type u) [Field K] (V : Type v) [AddCommGroup V] [Module K V] [FiniteDimensional K V] : ↑(coevaluation K V) 1 = let bV := Basis.ofVectorSpace K V; Finset.sum Finset.univ fun i => ↑bV i ⊗ₜ[K] Basis.coord bV i

theorem contractLeft_assoc_coevaluation (K : Type u) [Field K] (V : Type v) [AddCommGroup V] [Module K V] [FiniteDimensional K V] : LinearMap.comp (LinearMap.rTensor (Module.Dual K V) (contractLeft K V)) (LinearMap.comp (↑(LinearEquiv.symm (TensorProduct.assoc K (Module.Dual K V) V (Module.Dual K V)))) (LinearMap.lTensor (Module.Dual K V) (coevaluation K V))) = LinearMap.comp ↑(LinearEquiv.symm (TensorProduct.lid K (Module.Dual K V))) ↑(TensorProduct.rid K (Module.Dual K V))

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) [Field K] (V : Type v) [AddCommGroup V] [Module K V] [FiniteDimensional K V] : LinearMap.comp (LinearMap.lTensor V (contractLeft K V)) (LinearMap.comp (↑(TensorProduct.assoc K V (Module.Dual K V) V)) (LinearMap.rTensor V (coevaluation K V))) = LinearMap.comp ↑(LinearEquiv.symm (TensorProduct.rid K V)) ↑(TensorProduct.lid K V)

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