The functor $\mathscr V \to \operatorname{fdVec}_k$ gives an equivalence of categories Let $\mathscr V$ be the category whose objects are the $k$-vector spaces $k^n$ for each $n\ge 0$ (there is one vector space for each $n$) and whose morphisms are linear transformations. Show that $\mathscr V \to \operatorname{fdVec}_k$ gives an equivalence of categories by describing an “inverse” functor.
Reference: Ravi Vakil's The Rising Sea, Foundations of Algebraic Geometry.

The functor $F: \mathscr V \to \operatorname{fdVec}_k$ is the obvious one, sending each vector space $k^n$ to itself and morphisms between $k^n$ and $k^m$ to themselves. We must construct an inverse functor $G: \operatorname{fdVec}_k\to \mathscr V$ such that $F\circ G$ and $G\circ F$ are naturally isomorphic to the identity functors in the appropriate category. I propose the following. Let $G$ send any $n$-dimensional vector space $V$ to $k^n$, and a map between vector spaces $f: V \to W$ to a map between the corresponding objects in $\mathscr V$, i.e., if $\dim V = m$, and $\dim W = n$, then, with respect to bases $\{e_1, \ldots, e_m\}$ (for $V$) and $\{e_1', \ldots, e_n'\}$ (for $W$), we have $G(f): k^m \to k^n$ defined by $$G(f): (x_1, \ldots, x_m) \mapsto \left(f_1\left(\sum_{i=1}^m x_ie_i \right), \ldots, f_n\left(\sum_{i=1}^m x_ie_i \right) \right)$$
where $f_i\left(\sum_{i=1}^m x_ie_i \right)$ is simply the $i^{\text{th}}$ coordinate of $f\left(\sum_{i=1}^m x_ie_i \right)$ with respect to the basis $\{e_1', \ldots, e_n'\}$. One can check the natural isomorphism properties of $F\circ G$ and $G\circ F$.
At least intuitively, this makes sense. However, the author remarks that there are dangerous set-theoretic issues to keep in mind and take care of here. In particular, the author's suggestion is to use Gödel-Bernays set theory or else replace $\operatorname{fdVec}_k$ with a very similar small category. Apparently, the problem lies in simultaneously choosing bases for all objects in $\operatorname{fdVec}_k$.

*

*What are the set-theoretic issues at hand? I am not an expert when it comes to set theory, but I guess the axiom of choice may have to play a role.


*Depending on the answer to $(1)$, could someone explain how replacing $\operatorname{fdVec}_k$ with a very similar small category solves the problem? Moreover, which category is being referred to here?
Thanks a lot!
 A: The set-theoretic issues have to do with the amount of choice you need. From your question, you seem to use the following definition of equivalence of categories.

Definition (1). A functor $F: \mathcal{C} \to \mathcal{D}$ is an equivalence if there is a functor $G: \mathcal{D} \to \mathcal{C}$ such that $FG$ and $GF$ are naturally isomorphic to the identity functors on $\mathcal{D}$ and $\mathcal{C}$ respectively.

Sometimes, you will also encounter a different definition of equivalence of categories, as below.

Definition (2). A functor $F: \mathcal{C} \to \mathcal{D}$ is an equivalence if $F$ is:

*

*full, so it is surjective on Hom-sets;

*faithful, so it is injective on Hom-sets;

*essentially surjective, for every object $D$ in $\mathcal{D}$ there is $C$ in $\mathcal{C}$ such that $F(C)$ is isomorphic to $D$.


Now the two are generally considered equivalence. In fact, $(1) \implies (2)$ is quite easy. However, $(2) \implies (1)$ requires global choice*, because for every $D$ in $\mathcal{D}$ we have to choose a $C$ in $\mathcal{C}$ and an isomorphism $F(C) \cong D$. Once you have chosen these things then you can put them together and build your 'inverse' functor $G$. Note that this is exactly what you do by choosing a basis for every vector space, which is equivalent to choosing an isomorphism to $k^n$. See also this question and its answers for more discussion on this topic.
As for your second question, I initially thought about the category of finite dimensional $k$-vector spaces, equipped with a choice of basis. The arrows will just be linear maps again. So you solve your choice problem by just assuming your choices have already been made.
However, even though that category admits an equivalence with $\mathscr{V}$, without using any choice, Kevin Arlin pointed out in the comments that Vakil's suggestion was about a small category. The category I suggest above is not small. As Kevin also points out in his comment, we could approach this by fixing an infinite dimensional $k$-vector space $V$ and considering the category of its finite dimensional subspaces with linear maps between them. Now the amount of choice you need depends on whether or not $V$ comes equipped with a basis: if $V$ has a basis then this induces a basis on each finite dimensional subspace. If $V$ does not have a basis then you would need the axiom of choice (the regular one, so not the global one) to fix a basis for $V$.
These kinds of approaches also show why many people are happy to assume things like global choice anyway (at least for this purpose), because in practical scenarios you can often get around it anyway.

*: Recall that the axiom of global choice is the stronger variant of the axiom of choice that can be applied to proper classes, as well as sets. That is, for any class $K$ of non-empty sets there would be a class function picks out an element of every set in $K$. Formally: it asserts the existence of a global function $\tau$ such that $\tau(X) \in X$ for every non-empty set $X$.
