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.
Equations
- coevaluation K V = ((Basis.singleton Unit K).constr K) fun (x : Unit) => ∑ i : ↑(Basis.ofVectorSpaceIndex K V), (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i
Instances For
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;
∑ i : ↑(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.