English
The coevaluation map embeds the base field into the tensor product with the dual, in terms of a chosen vector space basis.
Русский
Ко-оценивание внедряет основание через базис в тензорное произведение с двойственным пространством.
LaTeX
$$coevaluation_K_V = Basis.singleton Unit_K ⋯ sum_{i} b_V(i) ⊗ b_V.coord(i).$$
Lean4
theorem coevaluation_apply_one :
(coevaluation K V) (1 : K) =
let bV := Basis.ofVectorSpace K V
∑ i : Basis.ofVectorSpaceIndex K V, bV i ⊗ₜ[K] bV.coord i :=
by
simp only [coevaluation]
rw [(Basis.singleton Unit K).constr_apply_fintype K]
simp only [Fintype.univ_punit, Finset.sum_const, one_smul, Basis.singleton_repr, Basis.equivFun_apply,
Basis.coe_ofVectorSpace, Finset.card_singleton]
