Well-definedness of left adjoint functors Often, right adjoint functors are easy to describe, for example:

*

*Forgetful functors, such as $U: \textbf{Vect}_k \to \textbf{Set}$.

*Let $\textbf{C}$ and $\textbf{D}$ be categories such that $\textbf{D}$ has all colimits of shape $C$ and define $\Delta: \textbf{D} \to [\textbf{C}, \textbf{D}]$ by sending an object $Y$ to the constant functor $\Delta(Y)$ which sends every object to $Y$ and every morphism to $1_Y$.

*If $X$ and $Y$ are topological spaces and $f : X \to Y$ is a continuous map, denote by $\textbf{PSh}(X)$ the category of presheaves of, say, abelian groups on $X$. Then we have the direct image functor $f_*: \textbf{PSh}(X) \to \textbf{PSh}(Y)$ defined on objects by $f_*\mathscr{F}(V) = \mathscr{F}(f^{-1}(V))$.

These functors all have left adjoints:

*

*The free functor $\textbf{Vect}_k \leftarrow \textbf{Set}: F$

*The colimit functor $\textbf{D} \leftarrow [\textbf{C}, \textbf{D}]: \operatorname{colim}$

*The inverse image functor $\textbf{PSh}(X) \leftarrow \textbf{PSh}(Y): f^{-1}$
But as far as I can tell, all of these require some choice to construct:

*

*There are many free vector spaces on a set $S$, for example the one with underlying set the formal $k$-linear combinations of $\{ x_s | s \in S \}$ or the one with underlying set the formal $k$-linear combinations of $\{ y_s | s \in S \}$.

*A diagram of shape $\textbf{C}$ in $\textbf{D}$ may have many colimits.

*The inverse image functor is usually defined by $f^{-1} \mathscr{G}(U) = \operatorname{colim} \mathscr{G}(V)$ where the colimit is taken over the category $\textbf{Open}_{f(U)}(Y)$ of open sets in $Y$ which contain $f(U)$. As in the previous one, a diagram may have many colimits.

Of course by the universal property definition of adjoint functors, any two choices yield uniquely isomorphic functors. However (probably because my set theoretic foundations are shaky at best) I am concerned about existence. For example:


*If $\textbf{D}$ is not small (of course I don't really know how to fit proper classes in to my foundations anyway), then this seems to require a "not small" axiom of choice,

*I think that $\textbf{PSh}(Y)$ is not small, and for every presheaf $\mathscr{G}$ on $Y$ and every open set $U \subseteq X$ we must choose a colimit.

Can anyone help me sort this stuff out (or suggest a reference that would)? All of the places that I've seen this discussed don't address the set theory issues explicitly.
 A: You're right that in some cases, constructing a left adjoint (given that you know one must exist) may require a (large) axiom of choice.
Such an example would be constructing the colimit left adjoint $\varinjlim:[\def\sC{\mathscr{C}}\def\sJ{\mathscr{J}}\sJ,\sC]\to\sC$ of the diagonal functor $\Delta:\sC\to[\sJ,\sC]$ when you're only told that all such colimits exist.
If $\sC$ is large, then you would have to make a large number of choices (a colimit for each functor $F:\sJ\to\sC$).
However, in many (most?) cases, left adjoints are either already known, or at least have a very canonical construction, which removes the need for invoking any sort of choice axiom.
For instance, consider the left adjoint for the forgetful functor $U:\mathbf{Vect}_\Bbbk\to\mathbf{Set}$. Given a set $S$, the canonical choice for a free vector space on $S$ is just the set of formal $\Bbbk$-linear combinations of the elements of $S$ itself (rather than choosing a corresponding set $\{x_s | s\in S\}$ of letters to represent the basis).
Likewise (as @Maxime mentions in a comment), even in the case of the colimit left adjoint, usually a category has a "canonical" choice of colimit for any diagram (if it exists). In $\mathbf{Set}$, a canonical coproduct $\coprod_{i\in I}S_i$ is the disjoint union $\bigcup_{i\in I}(\{i\}\times S_i)$, and a canonical coequaliser of $f,g:S\to T$ is the set $T/(\sim)$ of equivalence classes in $T$ for the equivalence relation generated by $f(s)\sim g(s)$ for $s\in S$.
This gives us a canonical construction of arbitrary colimits in $\mathbf{Set}$, which saves us invoking a large axiom of choice (since $\mathbf{Set}$ is large).
The category of abelian groups have canonical colimits as well, after which the category of presheaves (in abelian groups or sets) will have canonical colimits since they can be computed levelwise (i.e., $(\varinjlim F)(U) = \varinjlim F(U)$ for all $U$).

The issue you might have with requiring the axiom of choice for left adjoints is probably intimately related to the issue you might have with large categories. To formalise / handle categories "too large" to fit in a set, one standard trick is to implicitly work in some universe.
Fix an underlying set theory (like ZFC), then a universe is loosely some set $V$ in your theory that "is big enough to do maths inside," meaning that the usual constructions of mathematics using elements of $V$ should remain in $V$.
For instance, this would mean that if $S\in V$, then $2^S\in V$ to allow for power sets.
Or, if $(S_i)_{i\in I}$ is a family of sets $S_i\in V$ and the index set lies in $V$ also, then $\bigcup_{i\in I}S_i\in V$.
Then, declare a set to be "small" if it lies in $V$, and "large" otherwise.
Now, "large" categories relative to this universe are still sets (so for example, $\mathbf{Set}$ is really the category of "small" sets relative to $V$, and so the class of objects in $\mathbf{Set}$ is just $V$).
Since the ambient set theory (ZFC) permits the axiom of choice for all sets (including "large" sets that do not lie in $V$), invocation of the axiom of choice over large categories is still no problem.
There are other workarounds (such as using a set theory that also considers proper classes, like NBG), but universes is the one I see most often (when it's even mentioned at all).
