Questions: 1. When do objects of a category form a set?
- Is there a choice function when I have a set of categories (as opposed to a set of sets)? Is there an axioma schema of separation for defining (full) subcategories?
Context: Proof of lemma 3.2 in
Martín Escardó et al. "Comparing Cartesian closed categories of (core) compactly generated spaces", (doi:10.1016/j.topol.2004.02.011)
In the argument, there is a space $X$ and a set $I$ of non-open subsets. For each $i\in I$, they choose a compact space $C_i$ with a map $p_i\colon C_i\to X$ satisfying some property. After this choice, they take a direct sum of these spaces.
The choice to each $i\in I$ is an object in a comma category $\mathcal{C}$ (of all maps from compact spaces to $X$).
First, what I mean by axiom of choice is that if I have a set $J$ of sets then there is a choice function from $J$ to the disjoint union of the sets in $J$. The question is about how to define this choice function.
I see two ways. One way is to form a set out of the objects of my category, then use the axiom of subsets to define a subset for each $i\in I$ and then use the AC as stated above.
However, the objects of a category don't usually form a set, see this answer for example. But as far as the proof above is concerned, all I need to know is that the objects in $\mathcal{C}$ form a set.
The second way to go about this is to define (full) subcategory where the objects are those that have such and such a property and then use a version of AC for when I have a set of categories. But this feels like I'm forming a set out of the objects and defining a subset there and then "lifting" it back to my category. (I am thinking here of forming subcategories like that of all two element sets or groups with every element having finite order etc.)
The third alternative is that the proof in the paper above works in an entirely different manner.
Best Answer
Arguments involving compact (or compact Hausdorff) spaces are a common place where size issues get a bit fiddly in category theory–see Scholze's work on condensed sets, for instance. But these issues very rarely determine the truth of a statement. It is true that, naively, the category of compact spaces over a fixed space has a proper class of objects, which can't be turned into a set even by applying an equivalence. Thus your first approach doesn't immediately work.
The second approach is the idea: replace the category of all compact spaces over a given set with a small category that still contains a compact space with the desired property. The nuclear option here is to consider spaces $X$ and compact spaces $C_i$ whose underlying sets are elements of some fixed inaccessible cardinal $\kappa$ (often called a Grothendieck universe in category theory.) The properties of inaccessibles (specifically, that $\kappa$ is a model of ZFC), means that it's impossible to state a theorem that requires choosing a $C_i$ outside of this category without quite explicitly quantifying over a set of size $\kappa.$ This strategy generally allows one to proceed as if every category has only a set of objects.
Less aggressively, it's usually the case that you can give some explicit bound on how large $C_i$ might need to be in terms of the cardinality of $X$: for instance, it's very rare to need to apply power set more than twice in concrete arguments outside of set theory proper. Thus you can usually (in practice, always, though not in theory since large cardinals prove consistency of ZFC) apply the second strategy for any particular argument without needing to assuming the existence of any large cardinals.
Yet another strategy is to work in a set theory like NBG, which is designed for working directly with proper classes in a way ZFC cannot. It implies an axiom of global choice (that you can choose an element from every class of nonempty classes) which allows for constructions like that in your question. In practice, many category theory books adopt a foundation which also involves conglomerates, roughly "classes of classes", to add more flexibility on that front, and you might assume the axiom of choice for conglomerates of classes. I do not know where or whether this theory is written down precisely, but it can be modelled using ZFC plus two Grothendieck universes (or even just one, as Zhen Lin points out below, assuming you don't want to do operations on classes which NBG won't allow you to do.)