# Finite-dimensional space naturally isomorphic to its double dual?

The example that a finite vector space is naturally isomorphic to its double dual seems to be the canonical example of natural isomorphisms.

Concretely, there are two functors $\mathsf{Id}, {-^*}^* : \mathsf{FDVect} \to \mathsf{FDVect}$ which represent the identity functor and the double dual functor, and one can construct a natural transformation $\alpha : \mathsf{Id} \Rightarrow {-^*}^*$ as follows: $$\alpha_V(v)(f) = f(v)$$

However, in order to show that $\alpha$ is a natural isomorphism, one needs to find an inverse $\alpha^{-1}$.

I know that each $\alpha_V$ has an inverse, as the vector spaces are finite dimensional. I also know that if $\alpha$ is a natural transformation, then I can construct an inverse natural transformation by using the $\alpha_V^{-1}$'s.

However, the fact that $\alpha_V$ has an inverse $\alpha_V^{-1}$ does not seem very "natural" to me. I had to use a base of $V$ in order to construct $\alpha_V^{-1}$, and people always say that "choosing a base is not natural" (at least that is the reason why $V \cong V^*$ is not natural, right?). Despite of that, I know that $\alpha^{-1}$ is natural.

What is going on? Am I choosing a wrong $\alpha^{-1}$? Choosing a basis like that for $\alpha_V^{-1}$ is natural?

The fact that $\alpha_V$ has an inverse is indeed less natural. As you know, $\alpha_V$ is a well defined natural embedding also when $V$ is infinite dimensional, but then it does not have an inverse usually. This implies that the construction of the inverse has to be somewhat less elegant than that of $\alpha_V$.
For comparison, this is not the case when constructing an isomorphism $V\to V^*$. In this case, the isomorphism does depend on choice of basis.
Note that many natural constructions involve some choice, and then one needs to show the choice does not effect the result. One simple example is the universal property of the quotient. Take abelian groups for instance. Say you have a homomorphism $\varphi:A\to B$, such that $\varphi(C)=0$ for some subgroup $C\subset A$. So $\varphi$ induces a homomorphism $\tilde{\varphi}:A/C\to B$. How does one construct this homomorphism? Given an element in the quotient $A/C$, one has to choose a representative in $A$. But of course, the choice does not change the image, and so this construction is universal.
You are not required to exhibit an inverse, only to prove existence. Thus, in the finite case, where the always-injective map to the second dual is actually a bijection, by dimension-counting, you can prove existence of an inverse without choosing anything: given $w$ in the second dual, there is unique $v\in V$ mapping to $w$. "Defined" $\alpha^{-1}(w)=v$.