Natural isomorphisms and the axiom of choice

"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! :)

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.