Case study: what does it take to formulate and prove Quillen's small object argument in ZFC?

Question

I'm getting a bit lost over at Peter Scholze's interesting question about removing the dependence on universes from theorems in category theory. In particular, I'm being forced to admit that I don't really know when replacement is being invoked, never mind when it is invoked "in an essential way". So I'd like to work through a reasonably concrete example of the phenomenon. I understand that replacement should "really" be thought of as the axiom which allows for transfinite recursion. My sense is that category theory tends not to use recursion in a heavy-duty way (although, more so than other branches of mathematics, it does have plenty of definitions which at least prima facie have nontrivial Levy complexity. For instance, I think the formula $\phi(x,y,z,p,q)$ saying that the set $z$ and functions $p: z \to x$ and $q: z \to y$ are a categorical product of the sets $x,y$ is syntactically $\Pi_1$, and the statement that binary products exist in the category of sets is syntactically $\Pi_3$ (ignoring bounded quantifiers of course)).

The following theorem is, I think, one of the notable exceptions to the category-theoretic-non-use-of-recursion:

---

Theorem [Quillen] "The small object argument": Let $\mathcal C$ be a locally presentable category, and let $I \subseteq Mor \mathcal C$ be a small set of morphisms. Let $\mathcal L \subseteq Mor \mathcal C$ be the class of retracts of transfinite composites of cobase-changes of coproducts of morphisms in $I$, and let $\mathcal R \subseteq Mor \mathcal C$ comprise those morphisms weakly right orthogonal to the morphsims of $I$. Then $(\mathcal L, \mathcal R)$ is a weak factorization system on $\mathcal C$.

---

For the proof, see the nlab. Basically, factorizations are constructed by transfinite recursion. The recursion seems "essential" to me because new data is introduced at each stage of the construction.

---

Formalization:

I think this theorem and its proof are straightforwardly formalizable in MK, where the category-theoretic "small/large" distinction is interpreted as MK's "set/class" distinction. I don't feel qualified to comment on whether the proof works in NBG, but the statement at least makes sense straightforwardly.

When it comes to formalizing in ZFC, we have choices to make regarding the small/large distinction:

1. One option is to introduce a "universe" $V_\kappa$ (which, if we're actually trying to work in ZFC, will be a weaker sort of universe than usual). We'll interpret "small" to mean "in $V_\kappa$". We won't consider "truly large objects" -- everything we talk about will be a set -- in particular, every category we talk about will be set-sized, even if not "small" per se. We'll interpret "locally presentable category" to mean "$\kappa$-cocomplete, locally $\kappa$-small category with a strong $\kappa$-small, $\lambda$-presentable generator for some regular $\lambda < \kappa$" (I don't know if it makes a difference to say that $V_\kappa$ thinks $\lambda$ is a regular cardinal).

2. Another option is to not introduce any universe, and just interpret "small" to mean "set-sized". In this case, any "large" object we talk about must be definable from small parameters. So we define a category to comprise a parameter-definable class of objects, a parameter-definable class of morphisms, etc. This might seem restrictive, but it will work fine in the locally presentable case, since we can define a locally presentable category $\mathcal C$ to be defined, relative to parameters $(\lambda, \mathcal C_\lambda)$ (where $\lambda$ is a regular cardinal and $\mathcal C_\lambda$ is a small $\lambda$-cocomplete category), as the category of $\lambda$-Ind objects in $\mathcal C_\lambda$.

Now, for the theorem at hand, approach (2) seems cleaner because the necessary "tranlsation" is straightforward, and once it is done, the original proof should work without modification. I think the main drawbacks of (2) come elsewhere. For instance it will probably be a delicate matter to formulate theorems about the category of locally presentable categories. In general, there will be various theorems about categories which have clean, conceptual formulations and proofs when the categories involved are small, but which require annoying technical modifications when the categories involved are large. It's for such reasons that approaches more like (1) tend to be favored for large-scale category-theoretic projects.

So let's assume we're following approach (1). The question then becomes:

Question 1: Exactly what kind of universe do we need to formulate and prove the above theorem following approach (1)?

Question 2: How many such universes are guaranteed to exist by ZFC?

Presumably, the answer to Question 2 will be that there are a lot of such universes -- enough so that we can do things like, given a category, pass to a universe large enough to make that category small and invoke the theorem for that universe.

Question 3: How far into the weeds must we go to answer Questions 1 and 2?

Do we have to analyze the proof of the Theorem in a deep way? Is there an easy rubric of criteria which allow us to glance at the proof and, for 99% of theorems like this, easily say that it "passes" without delving into things too much? Or is there even some formal metatheorem we can appeal to such that even a computer could check that things are fine?

Answer 1

Jacob Lurie's comment gives an answer to Question 1. Namely, assuming that the estimates I gave in my comment are correct, in order to formulate and prove the theorem it will suffice to suppose that

• $\kappa$ is regular

and that

• for every $\mu < \kappa$, there exists $\rho < \kappa$ such that $\mu \ll \rho$ (meaning that $\mu' < \mu, \rho' < \rho \Rightarrow (\rho')^{\mu'} < \rho$).

Perhaps this property of $\kappa$ might be viewed as a "form" of replacement. But really, what we have is two conditions on $\kappa$ which are purely set-theoretic rather than metamathematical, so that the answer to Question 1 is something much cleaner than I had supposed.

This allows us to address Question 2. Presumably, the result is that ZFC proves that there are lots and lots of $\kappa$ satisfying the two conditions above.

When it comes to Question 3, it would seem that in this approach we do in fact need to delve pretty deeply into the proof. In fact, it seems that in order to carry out this approach, we must add some genuine mathematical content to the proof, and actually prove a stronger statement. The further questions then become

1. Will it generally be possible to "constructivize" "most" category-theoretic theorems in this way, or will other issues show up in the course of the "ZFC-ify category theory" project?

2. If the answer to (1) is "yes" (or if it's generally "no" and we restrict our attention to the cases where it's "yes"), then "how much extra work" would such a project really be?

My guess is that the answer to (1) is that when it comes to the use of transfinite recursion in category theory, it will indeed typically be the case that the use of replacement can be eliminated in a similar way to this, but that more importantly I've missed the point: as Jacob Lurie argues in response to Peter Scholze's question, the thornier issues with ZFC-ifying category theory are not to do with transfinite recursion but rather with being able to freely go back and forth between "big categories" and "little categories" in various ways.

My guess is that the answer to (2) is that for "most" category-theoretic uses of transfinite recursion, it should actually be pretty straightforward to "constructivize" them so that they fit in a "baby universe" with the properties above or something similar, and that with just a little bit of practice, one could develop the ability to verify almost at a glance that it's possible, though still on a theorem-by-theorem basis. But I'd love to be proven wrong and shown a theorem in category theory where this sort of approach fails!

Finally, this leaves as an open question whether there's a "more automatic" way of doing all of this -- perhaps with a weaker conclusion than "our universe need not satisfy any form of replacement at all".