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]
:
The coevaluation map is a linear map from a field K
to a finite dimensional
vector space V
.
Equations
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]
:
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]
:
This lemma corresponds to one of the coherence laws for duals in rigid categories, see
CategoryTheory.Monoidal.Rigid
.