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
.
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;
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
.