It's frequently said, informally, that a natural isomorphism is one that doesn't depend on arbitrary choices.
But the phrase "arbitrary choices" lends itself to different interpretations. Consider the following examples, all concerning a finite-dimensional vector space $V$ over a field $k$:
A. The natural isomorphism $V\rightarrow V\otimes_kk$ (by which I mean the obvious natural transformation from the identity functor to the functor $ -\otimes_kk$) is defined by a basis-free formula $v\mapsto v \otimes 1$, and is easily proved to be an isomorphism without ever invoking the existence of a basis.
B. The natural isomorphism $V\rightarrow V^{**}$ is defined by a basis-free formula $v\mapsto \Big(\phi\mapsto \phi(v)\Big)$, but to prove this is an isomorphism, it seems I have to choose a basis. Likewise for the natural isomorphism $V^*\otimes_k V\mapsto Hom_k(V,V)$.
C. The natural isomorphism $Hom_k(V,V)\mapsto V^*\otimes_kV$ cannot, I think, even be defined by any basis-free formula. To define the map, one first chooses a basis and then proves that the definition is independent of that choice.
Is there a more formal way to distinguish such cases? I'm looking for a precise definition of what it means to be "definable by a basis-free formula" or "provably an isomorphism without ever mentioning a basis" — precise enough so that it's possible to prove (not just suggest, as above) that a given isomorphism satisfies one, the other, both, or neither of these conditions.
(I suppose that the business about "provably an isomorphism without ever mentioning a basis" is perhaps no more interesting than "provably an isomorphism without ever using $X$", where $X$ is some other known property of vector spaces. But the business about being "definable by a basis-free formula" seems to me to be more interesting.)
Edited to add: I appreciate the responses, but I fear the main thing I've learned from them is that I failed to make the question clear. This wasn't intended as a question about vector spaces; the vector spaces were meant to illustrate something more general. I quite understand the reasons why the map $V^{**}\rightarrow V$ can't be constructed without reference to a basis (most notably, this map doesn't exist in the infinite dimensional case, so there's no hope to construct it without using the finite dimensionality, which means referring to a basis). The question is not why this is true but how to state it in a rigorous way. How, formally, and in more general contexts than vector spaces, does one formalize the notion of "not constructible without making some choices that turn out to be irrelevant at the end"?
Best Answer
The issue here is that the inverses to $V\rightarrow V^{**}$ and $V^*\otimes V\rightarrow \mathrm{Hom}(V,V)$ don't exist in the infinite dimensional case. So in order to show that they exist one has to assume that $V$ is finite dimensional. Now, if your definition of "finite dimensional" is "has a finite basis", then of course you have to use a basis at some point.
One option is to instead take your definition of "finite dimensional" to be "the natural map $V^*\otimes V\rightarrow \mathrm{Hom}(V,V)$ has an inverse". Then you can prove many facts about finite dimensional vector spaces without using a basis at all, and in particular you can construct an inverse to the map $V\rightarrow V^{**}$.