Is there any meaning or basis-free description for coevaluation in FDVect? It is a fact that the category $\textbf{FDVect}_k$ of finite-dimensional vector space is a rigid category, i.e. it is symmetric monoidal and has the notion of dual object and (co)evaluation satisfying some condition. In particular, the coevaluation of $V\in\textbf{FDVect}_k$ is given by
$$\text{coev}_V:k\to V\otimes V^*,\quad 1\mapsto \sum_{i=1}^n v_i\otimes v_i^*$$
where $\{v_1,\cdots,v_n\}$ is a basis of $V$ and $\{v_i^*,\cdots,v_n^*\}$ is the corresponding basis of $V^*$ (given by $v_i^*(v_j)=\delta_{ij}$). The coevaluation is, in fact, independent from the choice of basis. So is there any "fundamental" relationship (or meaning) between this mysterious quantity $\text{coev}_V(1)=\sum_{i=1}^n v_i\otimes v_i^*$ and $V$? Or alternatively, is there any basis-free description for $\text{coev}_V(1)$?
 A: For a finite-dimensional vector space $V$, the tensor product $V \otimes V^{\ast}$ is naturally isomorphic to $\text{End}(V)$. Its action on $V$ is given by the map
$$(V \otimes V^{\ast}) \otimes V \cong V \otimes (V^{\ast} \otimes V) \to V$$
given by applying the evaluation map $V^{\ast} \otimes V \to k$. Now, $\text{End}(V)$ has a distinguished element in it, namely the unit $\text{id}_V \in \text{End}(V)$, and if you transport this map across the isomorphism above you get exactly the coevaluation map (keeping in mind the natural identification between vectors in $W$ and linear maps $k \to W$). This is just the statement that the "coevaluation tensor" $\sum v_i \otimes v_i^{\ast}$ satisfies
$$ \left( \sum_i v_i \otimes v_i^{\ast} \right) \left( \sum_j c_j v_j \right) = \sum_{i, j} c_j v_i ( v_i^{\ast}(v_j)) = \sum_{i, j} c_j v_i \delta_{ij} = \sum_i c_i v_i$$
which is equivalent to the definition of the dual basis. This is also a simple explanation why the evaluation and coevaluation maps are sometimes called the counit and unit.
A: Worth adding to Quiachu Yuan's answer that the action on $V$ is described in the post is equivalent to an (injective) morphism $V\otimes V^* \to \mathrm{End}(V)$, even if $V$ is infinite dimensional.
If $X$ is a basis of $V$, we can identify $\mathrm{End}(V)$ with the subvector space of $\mathrm{Fun}(X\times X,k)$ consisting with functions $M$ such that for any $x\in X$, $M(x,-)$ has finite range. The isomorphism is given by
$$
[f \mapsto[(x,y)\mapsto y^*f(x)]]
$$
where $y^*(f(x))$ is the $y$-coordinate of the vector $f(x)$.
The inverse of this map is given by
$$
[M\mapsto [x\mapsto \sum_{y\in X}M(x,y)y]].
$$
Under this isomorphism the space $V\otimes V^*$ is the space of functions $M$ such that there is a finite subset $J\subset X$, such that $\forall (x,y) \in X\times (X-J)$, $M(x,y) = 0$.
If you think of matrices $x$ representing rows, $y$ representing columns, the endomorphisms are given by matrices such that each row has finite range, and elements of $V\otimes V^*$ are given by matrices that have a finite number of non zero columns. They both coincide if and only if $X$ is finite and if and only if the identity is in $V\otimes V^*$.
If the isomorphism holds, then since the space is of finite dimension, the sum $\sum_{x\in X} x\otimes x^*$ makes sense, and note that for any other base $Y$, $\sum_{x\in X} x\otimes x^* = \sum_{y\in Y} y\otimes y^*$. Let's then of course note that element $id_V$. One way to capture how many elements there are in the basis is then to compute $ev_{V}(id_V)$, this is the dimension of the vector space $V$, and it can be defined without ever referencing a basis, you just need the evaluation and coevaluation. Note that of course if you have a basis $X$, then it is necesseraly finite, and $ev_{V}(id_V) = card(X)$.
If $id_V$ is in $V\otimes V^*$, write $id_V$ as a finite sum of pure tensors, for example $id_V = \sum_{(x,y)\in X \times Y }x\otimes y$, where $X\subset V$ is a finite subset, and $Y\subset V^*$ is a finite subset. Then $X$ is a generating family since for every $v \in V$, $v = \sum_{(x,y)\in X\times Y} y(v)x$. From there, a finite base can be extracted.
So maybe to show that the dimension is an integer, when the field is of caracteristic 0, one has to show the theorem of extraction of basis from a generating family.
