The coevaluation map on finite dimensional vector spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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)
[add_comm_group V]
[module K V]
[finite_dimensional K V] :
K →ₗ[K] tensor_product K V (module.dual K V)
The coevaluation map is a linear map from a field K to a finite dimensional
vector space V.
Equations
- coevaluation K V = let bV : basis ↥(basis.of_vector_space_index K V) K V := basis.of_vector_space K V in ⇑((basis.singleton unit K).constr K) (λ (_x : unit), finset.univ.sum (λ (i : ↥(basis.of_vector_space_index K V)), ⇑bV i ⊗ₜ[K] bV.coord i))
theorem
coevaluation_apply_one
(K : Type u)
[field K]
(V : Type v)
[add_comm_group V]
[module K V]
[finite_dimensional K V] :
⇑(coevaluation K V) 1 = let bV : basis ↥(basis.of_vector_space_index K V) K V := basis.of_vector_space K V in finset.univ.sum (λ (i : ↥(basis.of_vector_space_index K V)), ⇑bV i ⊗ₜ[K] bV.coord i)
theorem
contract_left_assoc_coevaluation
(K : Type u)
[field K]
(V : Type v)
[add_comm_group V]
[module K V]
[finite_dimensional K V] :
(linear_map.rtensor (module.dual K V) (contract_left K V)).comp ((tensor_product.assoc K (module.dual K V) V (module.dual K V)).symm.to_linear_map.comp (linear_map.ltensor (module.dual K V) (coevaluation K V))) = (tensor_product.lid K (module.dual K V)).symm.to_linear_map.comp (tensor_product.rid K (module.dual K V)).to_linear_map
This lemma corresponds to one of the coherence laws for duals in rigid categories, see
category_theory.monoidal.rigid.
theorem
contract_left_assoc_coevaluation'
(K : Type u)
[field K]
(V : Type v)
[add_comm_group V]
[module K V]
[finite_dimensional K V] :
(linear_map.ltensor V (contract_left K V)).comp ((tensor_product.assoc K V (module.dual K V) V).to_linear_map.comp (linear_map.rtensor V (coevaluation K V))) = (tensor_product.rid K V).symm.to_linear_map.comp (tensor_product.lid K V).to_linear_map
This lemma corresponds to one of the coherence laws for duals in rigid categories, see
category_theory.monoidal.rigid.