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.

noncomputable 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 = have bV := Module.Basis.ofVectorSpace K V; ∑ i : ↑(Module.Basis.ofVectorSpaceIndex K V), bV i ⊗ₜ[K] bV.coord i

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

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