9
$\begingroup$

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?

$\endgroup$
14
  • $\begingroup$ Note that in approach (2), you should expect to wind up with theorem schemes - namely, for each $n$ a theorem asserting the result for all $\Sigma_n$-definable class objects. This isn't particularly bad, but it's worth keeping in mind. $\endgroup$ Jan 28 at 18:14
  • 1
    $\begingroup$ Maybe I should strip down the statement. The core of the proof is actually to construct factorizations exist via transfinite recursion. Once that's done, the rest of the theorem follows easily. $\endgroup$
    – Tim Campion
    Jan 28 at 18:24
  • 1
    $\begingroup$ Re: your second-most-recent comment: interesting, I actually find $(1)$ less problematic! Aside, there's a third approach: work in $\mathsf{ZFC}$ extended by adding a constant symbol $c$, an axiom saying that $c$ is an ordinal, and the relativization to $V_c$ of every $\mathsf{ZFC}$-axiom. This makes $V_c$ pretty dang good, but is conservative over $\mathsf{ZFC}$ (basically, $\mathsf{ZFC}$ can't prove that $V_x$ actually satisfies all of $\mathsf{ZFC}$, and each finite fragment is guaranteed "safe" by reflection). This is morally just $\mathsf{NBG}$ in disguise but may feel more palatable. $\endgroup$ Jan 28 at 18:25
  • 13
    $\begingroup$ Roughly speaking, replacement is needed to justify constructions by transfinite recursion where the objects being constructed don't live in some codomain that is fixed ahead of time. In the case of the small object argument, you can write down a priori bounds on the sizes of the objects you will need to build, so replacement is not needed. $\endgroup$ Jan 28 at 18:28
  • 1
    $\begingroup$ @KamerynWilliams I'm being a bit loose with my morals here :). I think of a model of the third approach above as being an "extension" of $V_{c+1}$, the latter of which is a model of $\mathsf{NBG}$. So in my mind what's going on is that we're talking about a way to "smoothly" keep building more and more levels on top of a model of $\mathsf{NBG}$. But this is pretty loose. $\endgroup$ Jan 28 at 19:02
2
$\begingroup$

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

$\endgroup$
13
  • 1
    $\begingroup$ Hang on -- after running through my limited knowledge of cardinal arithmetic I'm thinking that perhaps the estimates I gave are not good enough. I believe I've been told it's consistent that every regular limit cardinal is strongly inaccessible (I think this always holds in L?). The conditions I gave imply that $\kappa$ is a regular limit cardinal. Ergo, ZFC does not prove that there exists a $\kappa$ with the properties I described. Probably I've just missed how to get a better estimate. $\endgroup$
    – Tim Campion
    Jan 28 at 21:10
  • 2
    $\begingroup$ "Regular limit cardinal" is just weakly inaccessible and already $\mathsf{ZFC}$ doesn't prove the existence of those. However, I don't think what you've written corresponds to that. In particular, consider what happens if $\kappa=\theta^+$ for some "very closed" $\theta$ (since successors are regular): we might as well take $\mu=\theta$, but then $\rho=\theta$ works since we only consider $\mu'<\mu$ and $\rho'<\rho$ and $\theta$ is "very closed." (Specifically, given your favorite $\lambda$ take $\theta$ to be the limit of the sequence $\theta_0=\lambda$, $\theta_{i+1}=\theta_i^{\theta_i}$.) $\endgroup$ Jan 28 at 21:17
  • $\begingroup$ So I don't immediately see why $\kappa$ has to be a limit cardinal. $\endgroup$ Jan 28 at 21:19
  • $\begingroup$ @NoahSchweber I'm not sure what "very closed" means, but if $\theta \ll \theta$ doesn't imply that $\theta$ is strongly inaccessible, then most likely my use of it in the estimate is actually in error. I should probably work out the estimate in more detail. $\endgroup$
    – Tim Campion
    Jan 28 at 21:22
  • 1
    $\begingroup$ Is $\Sigma_1$-replacement equivalent over $ZC$ to "every set is bijective to an ordinal"? $\endgroup$
    – Tim Campion
    Jan 29 at 3:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.