7

Does one need the axiom of replacement in the small object argument and in the transfinite construction of free algebras?

My motivation for the question is that I heard that the axiom of replacement is never needed in practice.

If the answer is "yes", how can one avoid the axiom of replacement in practical applications of these two theorems?

Note that one can't use ordinals if one doesn't allow the axiom of replacement (I think).

user333306
  • 375
  • By the way, what would be other suspicious-of-using-replacement candidates for pieces of "real" mathematics (meaning: non-foundational and non-set-theoretic)? – user333306 Aug 04 '21 at 20:08
  • 4
    Regarding the claim about ordinals, although indeed one needs replacement in order to prove the existence of infinite von Neumann ordinals, nevertheless one can still have numerous very large well-orderings without using any replacement, and these often suffice for carrying out transfinite constructions. – Joel David Hamkins Aug 04 '21 at 20:40
  • 3
    If I'm not mistaken, when using ordinals outside of set theory, Replacement most often comes in for an "exhaustion" argument: there are too many ordinals for such and such process to never terminate, so it must terminate. In the small object argument, as far as I can tell, there is no such exhaustion: the "termination ordinal" is set ahead of time (by the compactness of the domains of the maps). – Maxime Ramzi Aug 04 '21 at 22:21
  • 3
    I think a slightly more accurate heuristic would be to say that you need replacement when you are defining by induction or recursion a function whose codomain is a not a priori a set. The Hartogs theorem on wellorderings – in its original form – does not require replacement. – Zhen Lin Aug 04 '21 at 22:45
  • related https://mathoverflow.net/questions/382466/case-study-what-does-it-take-to-formulate-and-prove-quillens-small-object-argu – Tim Campion Aug 05 '21 at 21:47

1 Answers1

7

The way it is usually presented, certainly yes. As you point out it usually refers to possibly uncountable regular ordinals, which would usually mean von Neumann ordinals. Once you have the regular ordinal, say $\kappa$, then regardless of whether $\kappa$ is a von Neumann ordinal or just a well ordered set, you need to define a sequence of objects $K_\alpha$ for each $\alpha < \kappa$, and take colimits at each limit stage, and overall at the end. That kind of argument does seem to require replacement, as far as I can see. Certainly it is possible to define a sequence of sets, even of length $\omega$ whose colimit does not provably exist in the category of sets under $\mathbf{ZFC}$ minus replacement (since $V_{\omega + \omega}$ is a model of that theory, and we can define the sequence $K_n := V_{\omega + n}$).

On the other hand, there are two alternative versions of the small object argument in Swan, W-types with reductions and the small object argument that don't use replacement (and also don't use definitions by recursion into universes of small types, which is, roughly speaking, the type theoretic version of replacement). The first can be carried out in a topos with natural number object and satisfying the choice principle $\mathbf{WISC}$, which I believe holds for any Grothendieck topos under the assumptions of $\mathbf{ZFC}$ minus replacement. The second is specific to the case of monic generating cofibrations in presheaf toposes, but does not require $\mathbf{WISC}$, so would work in a metatheory of $\mathbf{ZF}$ minus replacement. Both arguments are for a slightly non standard definition of cofibrantly generated, and they have a different format to the usual proof using ordinals. Instead of defining a sequence of objects along an ordinal, there are just two steps, first define a $W$-type, and then either quotient it (for the first argument) or carve out a subobject (for the second).

aws
  • 3,836
  • I hadn't realized what you said in your first paragraph, thanks for that ! I think I'm a bit confused about internal vs external here though: suppose you have no replacement at all, then you can't actually define that sequence ($n\mapsto V_{\omega +n}$) as a sequence, even though you can define it by a formula. In particular it seems to me like Set is still cocomplete even without replacement. – Maxime Ramzi Aug 05 '21 at 13:25
  • (that does not change your argument from the first paragraph of course : to define the sequence of objects needed for the small object argument as usually presented, you still need replacement) – Maxime Ramzi Aug 05 '21 at 13:26
  • Yes, I agree - the best convention is to not count these "large" sequences as diagrams or maybe not call them sequences at all, so a category does not need to have their colimits in order to be considered cocomplete. – aws Aug 05 '21 at 13:31
  • @MaximeRamzi Any elementary topos is complete and cocomplete from “its own” point of view. This is a kind of trick using clever definitions and indeed in the context of this theorem the sequence in question is not a legitimate diagram. – Zhen Lin Aug 05 '21 at 14:30
  • @ZhenLin : thanks for pointing that out, I wasn't sure !! – Maxime Ramzi Aug 05 '21 at 14:33
  • It would seem that at least in common applications of the small object argument we do know that the transfinite sequence factors through a set. For instance, when constructing weak factorization systems in locally presentable categories, we can restrict to the subcategory of λ-presentable objects for a sufficiently large regular cardinal λ (which depends on the morphism being factorized), and this subcategory is an (essentially) small category. – Dmitri Pavlov Aug 05 '21 at 16:11
  • That could work, but I think it would be necessary to check a lot of the basic theory of $\kappa$-compact objects and locally presentable categories still goes through without replacement. – aws Aug 05 '21 at 17:04
  • Another reference for a "constructive small object argument", related to Swan's but more like a classical transfinite construction, is Fiore-Pitts-Steenkamp Quotients, inductive types, and quotient inductive types. – Mike Shulman Sep 07 '21 at 08:44
  • @MikeShulman Thanks! Regarding the question, if I recall correctly, one of their arguments does define a map into a universe by recursion, so it would use replacement if translated into set theory in the most straightforward way. Of course, there could be a way to avoid this. I think the argument Dmitri Pavlov suggested would make it non constructive, since it seems to require large amounts of choice, powerset and excluded middle, when I had a quick look at it - but maybe with enough work there could be a way to just use WISC. – aws Sep 07 '21 at 15:42
  • @aws You're probably right. – Mike Shulman Sep 07 '21 at 17:23