Natural isomorphisms and the axiom of choice The definitions of "natural transformation", "natural isomorphism between functors", and "natural isomorphism between objects" captures - among other things - the intuitive notion of "an isomorphism that does not depend on an arbitrary choice" (from Wikipedia). The standard example is a finite dimensional vector space $V$ being naturally isomorphic to its double dual $V$** because the isomorphism doesn't depend on the choice of basis.
What I wonder:

Does this informal notion of choice have to do
with the formal notion of choice in the axiom of
choice?
Is "being naturally
isomorphic" somehow related
to "being provably isomorphic from $ZF$ without $AC$"?
Or are these completely unrelated concepts?

 A: Short answer: The formal definition of “natural isomorphism” is completely unrelated to any notion of choosing, let alone the axiom of choice.
Silly answer: There are natural isomorphisms which depend on arbitrary choices. For example, under the axiom of global (!) choice, the category of sets is equivalent to the category of cardinals, which is a full subcategory of the category of sets. As such, every set is “naturally” isomorphic to its cardinal! Indeed, for each set $X$, fix a bijection $\eta_X : X \to \# X$, where $\# X$ is the cardinal of $X$. (If $X = \# X$, for simplicity we require $\eta_X = \text{id}_X$. This data suffices to specify a functor $\# : \textbf{Set} \to \textbf{Card}$, which acts on arrows $f : X \to Y$ by $\# f = \eta_Y \circ f \circ {\eta_X}^{-1}$. Let $U : \textbf{Card} \hookrightarrow \textbf{Set}$ be the inclusion. Then, $\#$ is left adjoint to $U$ with counit $\eta$, since by construction
$$\begin{matrix}
X & \xrightarrow{\eta_X} & \# X \newline
{\scriptstyle f} \big \downarrow & & \big\downarrow {\scriptstyle \# f} \newline
Y & \xrightarrow{\eta_Y} & \# Y
\end{matrix}$$
commutes for every arrow $f : X \to Y$, and obviously both functors are full and faithful. This shows that $\eta$ is the “natural” isomorphism we seek.
A: This is far from a complete answer, but rather a remark on natural maps and the axiom of choice.
It is possible without the axiom of choice to have a vector space which is not finitely generated and isomorphic to its double dual $[1]$ (we can find ones which are isomorphic to their first dual, and we can find those which are not isomorphic to their first dual but still isomorphic to the second dual).
If you think about it, assuming the axiom of choice, the natural map is always injective. This is not the case without the axiom of choice. It is possible to have nontrivial vector spaces that have no non-zero functionals, so the natural map is constantly zero $[2,3]$.
So the axiom of choice actually plays a role in restricting the class of vector spaces which are naturally isomorphic to their double duals (the axiom of choice giveth and the axiom of choice taketh).
Further reading (MathOverflow):


*

*Does the fact that this vector space is not isomorphic to its double-dual require choice?

*What’s an example of a space that needs the Hahn-Banach Theorem?

*Is the non-triviality of the algebraic dual of an infinite-dimensional vector space equivalent to the axiom of choice?
A: The categorical meaning of "natural" means that your definition is "invariant by morphism" (e.g. change of coordinates in vector spaces). This is a very strong property which implies the definition is somehow canonical, but not necessarily  obvious.
Although using the axiom of choice is likely to lead to non-natural constructions, not all non-natural constructions use this axiom, even if there might be some "choice" involved in the definition ("choice" in the colloquial sense does not always imply actual use of the axiom). For example, to embed any vector space in its dual, you need a basis (and thus the axiom of choice). But to do that for a finite-dimensional vector space, the axiom of choice is not needed. The construction is never natural.
Finally, it may also very well happen that a construction using the axiom of choice turns out to be natural (I'll admit I don't know of any example).
A: "Naturality" in a categorical sense is much more than "not depending on choices", and, also, is essentially unrelated to issues about the Axiom of Choice.
In the example of vector spaces over a field, we can look at the category of _finite_dimensional_ vector spaces, to avoid worrying about using AxCh to find elements of the dual. The non naturality of any isomorphisms of finite-dimensional vectorspaces with their duals resides in the fact that, provably, as a not-hard exercise, there is no collection of isomorphisms $\phi_V:V\rightarrow V^*$ of isomorphisms of f.d. v.s.'s $V$ to their duals, compatible with all v.s. homs $f:V\rightarrow W$. 
In contrast, the isomorphism $\phi_V:V\rightarrow V^{**}$ to the second dual, by $\phi_V(v)(\lambda)=\lambda(v)$ is compatible with all homs, as an easy exericise! This latter compatibility is the serious meaning of "naturality".
True, if capricious or random choices play a role, the chance that the outcome is natural in this sense is certainly diminished! But that aspect is not the defining property!
Edit (16 Apr '12): as alancalvitti notes, the ubiquity of adjunctions, and the naturality and sense of "naturality", and counter-examples to naive portrayals, deserve wider treatment at introductory levels. After all, this can be done with almost no serious "formal" category-theoretic overhead, and pays wonderful returns, at the very least organizing one's thinking. Distinguishing "characterization" from "construction-to-prove-existence" is related. E.g., "Why is the product topology so coarse?": to say that "it's the definition" is unhelpful; to take the categorical definition of "product" and _find_out_ what topology on the cartesian product of sets is the categorical product topology is a do-able, interesting exercise! :)
A: I'm no expert but I think they're different. My understanding is that "natural isomorphism" has always been a little vaguely defined but the concept is fairly intuitive.
It's a case where there is clearly a "best" or simplest isomorphism. Like the Chinese Remainder Theorem perhaps. Cmn ~ Cm x Cn where m, n are relatively prime. There may be more than one isomorphism but one stands out as the most natural or most obvious, I guess.
Generally the "natural" isomorphisms are easily and unambiguously provable. It's recognising that such a connection exists that's the real art. Funnily enough I find the axiom of choice much vaguer (and have never been a fan).
I'm probably way off...
