9

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?

Tim Campion
  • 60,951
  • 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. – Noah Schweber Jan 28 '21 at 18:14
  • Meanwhile, I don't quite get the emphasis on Replacement, since that's part of $\mathsf{ZFC}$ already. Looking at Replacement seems connected rather with the question of going below $\mathsf{ZFC}$ rather than to $\mathsf{ZFC}$. – Noah Schweber Jan 28 '21 at 18:15
  • @NoahSchweber Thanks for the clarification about schema. My understanding from the discussion over at Peter Scholze's question is that it's important to think about how much replacement $V_\kappa$ has -- ZFC won't prove that there exists a $\kappa$ such that $V_\kappa$ models all of ZFC, but it will prove there exists a $\kappa$ such that $V_\kappa$ models a version of ZFC where replacement has been weakened. In order to use this fact, we must go back to our proofs and check that they only use the weakened version of replacement. – Tim Campion Jan 28 '21 at 18:19
  • As to the question itself, I think a good first step would be to analyze just the statement "The pair $(\mathcal{L},\mathcal{R})$ defined as above exists" (where by "defined" I refer to the definition "$\mathcal{L}$ comprises [stuff], $\mathcal{R}$ comprises [stuff]." I expect that showing that this pair (given that it exists) is a weak factorization system and is appropriately minimal will be pretty easy, and I have no idea about the functoriality part. – Noah Schweber Jan 28 '21 at 18:19
  • Re: your comment of a minute ago, your understanding is correct, but that seems to address (1), not (2); I was talking specifically about (2). Note incidentally that since we can talk about truth in set-sized structures, approach (1) will not force us into the realm of axiom schemes: we can say e.g. "For every $n$ and every $V_\kappa$ satisfying $\Sigma_{n}$-Replacement." – Noah Schweber Jan 28 '21 at 18:20
  • Ah, right. Yes, I agree that approach (2) seems much less problematic in this limited context. So really the issue is that we want to make approach (1) work for reasons of fitting this theorem into a broader context, and now we have to deal with the concomitant headaches. – Tim Campion Jan 28 '21 at 18:21
  • 1
    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. – Tim Campion Jan 28 '21 at 18:24
  • 1
    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. – Noah Schweber Jan 28 '21 at 18:25
  • 14
    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. – Jacob Lurie Jan 28 '21 at 18:28
  • @NoahSchweber Can you say how your extension is morally NBG in disguise? The model of your extension you get from Con(ZFC) plus a compactness argument is omega-nonstandard. So it seems to me that it's doing something quite different from what NBG does. But maybe I'm misunderstanding what you're trying to do. – Kameryn Williams Jan 28 '21 at 18:42
  • 1
    @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. – Noah Schweber Jan 28 '21 at 19:02
  • @JacobLurie Like this? Let $\mathcal C$ be locally $\lambda$-presentable with respect to $V_\kappa$. For $\lambda \leq \mu < \kappa$ regular, let $\mathcal C_\mu$ be a skeleton of the full subcategory of $\mu$-presentable objects. Let $ |Mor\mathcal C_\lambda| < \nu$ with $\mu$ regular. If $\mu, \nu \ll \rho$ in the sense of your book ($\mu \ll \rho$ if $\rho$ if $\mu, \rho$ are regular and $\mu' < \mu, \rho' < \rho \Rightarrow (\rho')^{\mu'} < \rho$), then $|Mor\mathcal C_\mu| < \rho$, or something like that. The size of the next stage happens to be bound-able by the number of morphisms – Tim Campion Jan 28 '21 at 19:02
  • So if $X \to Y$ is between $\mu$-presentable objects, then the next stage of the construction will be between $\rho$-presentable objects. The construction can be terminated at step $\sigma$ if all morphisms of $I$ are between $\sigma$-presentable objects. So if one knows that $\kappa$ is regular and that there is a function $\phi: \kappa \to \kappa$ with $\mu \ll \phi(\mu)$, then to factor a $\mu$-presentable $X \to Y$, the construction takes place in the $\kappa$-small category $\mathcal C_{\phi^\sigma(\mu)}$. And thus we don't need $V_\kappa$ to satisfy any (further?) form of replacement. – Tim Campion Jan 28 '21 at 19:02
  • To clarify for myself: because everything takes place within a small category, every time we might think we need replacement, we can really just use separation to identify the image of our function within this set-sized codomain. – Tim Campion Jan 28 '21 at 19:29

1 Answers1

2

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

Tim Campion
  • 60,951
  • 1
    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. – Tim Campion Jan 28 '21 at 21:10
  • 2
    "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}$.) – Noah Schweber Jan 28 '21 at 21:17
  • So I don't immediately see why $\kappa$ has to be a limit cardinal. – Noah Schweber Jan 28 '21 at 21:19
  • @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. – Tim Campion Jan 28 '21 at 21:22
  • I've now spent way too much time thinking about the necessary preliminaries and I'm stuck at the following conundrum. ZFC won't give us $\kappa$ which is both regular and a $\beth$-fixed-point. If $\kappa$ isn't regular, then we can't run transfinite induction for arbitrary lengths $\sigma <\kappa$ and we'll get a weaker theorem. If $\kappa$ isn't a $\beth$-fixed-point, then we can't just say that every set of cardinality $<\kappa$ is bijective with a set in $V_\kappa$. We'll have to cook up more elaborate ways of controlling "size". I'm starting to think this would be a nontrivial endeavor. – Tim Campion Jan 29 '21 at 02:49
  • "If $\kappa$ isn't a $\beth$-fixed-point, then we can't just say that every set of cardinality $<\kappa$ is bijective with a set in $V_\kappa$" Every set of cardinality $<\kappa$ is in bijection with some ordinal $<\kappa$ which is an element of $V_\kappa$, so $\beth$-fixed-pointness isn't needed here at all. Did you mean something else? – Noah Schweber Jan 29 '21 at 02:52
  • Sorry, I meant that we don't get an "if and only if". If $\kappa$ isn't a $\beth$-fixed-point, then there are sets in $V_\kappa$ of cardinality $\geq \kappa$, right? – Tim Campion Jan 29 '21 at 02:53
  • Yes, that's right. – Noah Schweber Jan 29 '21 at 02:54
  • In the discussion at Peter Scholze's question, it emerged that if $V_\kappa$ models $\Sigma_n$-replacement, then typically $\kappa$ will be very far from regular, leading me to think that the "canonical" approach would be to weaken the regularity assumption. But if we do that, then I can't imagine that the theorem can possibly be proven for sets of morphisms $I$ whose domains and codomains have presentability rank $\geq cf(\kappa)$. So the resulting theorem will be weaker. Perhaps it would still be applicable "in practice". Ugh. This stuff is annoying. – Tim Campion Jan 29 '21 at 03:01
  • And although this might seem like a different issue than the one I originally asked about, it really can still be seen as a question about replacement, since if $V_\kappa$ models some pretty weak replacement ($\Sigma_1$ or something), then it models that every well-order is isomorphic to an ordinal, and hence $\kappa$ must be a $\beth$-fixed-point anyway. – Tim Campion Jan 29 '21 at 03:05
  • Yes, that's right - and it's exactly $\Sigma_1$ replacement that's needed. (As an unrelated aside, this is a key point in generalized computability theory, where that's the amount of replacement we have at admissible ordinals and is crucial for developing basic computability-theoretic results - although that doesn't end the story.) – Noah Schweber Jan 29 '21 at 03:07
  • 1
    Is $\Sigma_1$-replacement equivalent over $ZC$ to "every set is bijective to an ordinal"? – Tim Campion Jan 29 '21 at 03:21
  • I think my imagination was a bit weak earlier. If the regularity assumption is weakened, then sure, we'll get a weak "external" version of the theorem where the presentability ranks are weakened. But so long as $V_\kappa$ models enough of ZFC, there will also be an "internal" version of the theorem where we use as many "internal to $V_\kappa$" concpets as possible... I'm unclear on how it will all play out. – Tim Campion Feb 06 '21 at 03:51