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
- One or more equations did not get rendered due to their size.
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 : ↑(Basis.ofVectorSpaceIndex K V)) => 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.rTensor (Module.Dual K V) (contractLeft K V) ∘ₗ
↑(LinearEquiv.symm (TensorProduct.assoc K (Module.Dual K V) V (Module.Dual K V))) ∘ₗ
LinearMap.lTensor (Module.Dual K V) (coevaluation K V) = ↑(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.lTensor V (contractLeft K V) ∘ₗ
↑(TensorProduct.assoc K V (Module.Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V) = ↑(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.