Defining subcategories and axiom of choice

Question

Questions: 1. When do objects of a category form a set?

2. 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.

Answer 1

When do objects of a category form a set?

It is not possible to answer this question except in a tautological way, and in any case, to answer the question even for specific categories depends on your choice of foundations.

(For example, if you use the setup of SGA 4, then every category has a set of objects; the price you pay for this is that every category has to be cut off by a universe parameter, and sometimes you have to juggle universes. Or if you use the setup of Categories for the working mathematician, then categories always have sets of objects, but metacategories are not so constrained.)

That said, in practice, you will not go wrong if you only assume that small categories have a set of objects.

Is there a choice function when I have a set of categories (as opposed to a set of sets)?

Again, it depends on your foundations, and also your definitions. In the standard set-theoretic understanding of these words, if you genuinely have a set of categories, then those categories are necessarily small. (Do you think that $\{ \textbf{Set} \}$, where $\textbf{Set}$ is the category of all sets, is a set? If you do, and you worry about set-theoretic issues, then you should probably go consult a set theory textbook first.)

But in my experience I think mathematicians are more likely to mean that they have a family of categories parametrised/indexed by a set, rather than a literal set of categories. Such a thing is not necessarily a set (or even a class). If you have the axiom of global choice, this is no obstacle: since the individual objects of each category are elements of the universe, if the universe is well-ordered, we could certainly pick an object in each category (and then apply the axiom of replacement to get a choice function).

Is there an axiom schema of separation for defining (full) subcategories?

In principle this depends on your foundations, but in commonly used class/set theories there is an axiom schema of separation for classes. Sometimes there are limitations on the complexity of predicates that can be used: for example, in NBG, the axiom schema of separation is only assumed for predicates where all bound variables are restricted to be sets. (If you are not comfortable with thinking about the complexity of predicates, there is a finite axiomatisation of NBG where the axiom schema of separation can be derived as a theorem.)

Answer 2

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.)