[Math] Axiom of Replacement in Category Theory

ct.category-theoryset-theory

Does the usual development of category theory (within Goedel-Bernays set theory, for example) require the axiom of replacement? I would have asserted that this was obviously true, but it seems to be common wisdom that the axiom of replacement is an exotic axiom not used outside of axiomatic set theory. Also, sadly the overlap between things that I have thought were obviously true and were in fact false is larger than I would like to admit…

The axiom of replacement basically says that if a class is the same size as a set, then it is a set. This allows us to identify classes that are sets as being small and those that are proper classes as large. Without replacement, you could have countable classes that not sets.

I don't see how to construct most limits and colimits in familiar categories such as Set or Top without the use of replacement. Already, for an infinite set $X$, I don't see how you construct
$$
\coprod_{i=0}^\infty P^i X,
$$
where $P^i$ is the $i$-th power set of $X$ (i.e. $P^0 X = X$ and $P^i X = P (P^{i-1}X$)).

Using replacement, it's easy to construct. You form the set
$$
\bigcup_{i=0}^\infty P^i X,
$$
and then the coproduct is isomorphic to the set of pairs $(i, x)$, where $x \in P^i X$. Am I completely misunderstanding the issue here, and this coproduct can be proven to exist without replacement?

I suppose you could cook up a definition of diagram so that in the absence of replacement, you cannot even form the diagram for this particular coproduct, but that would be sort-of unsatisfying.

Best Answer

There’s one issue underlying a lot of the discrepancies between people’s answers, I think:

How are we defining “$f$ is a function $s \to V$”, where $s$ is a set and $V$ is a (possibly proper) class?

(hence also, how we define subsequent things like “a small-category-indexed diagram of sets”) There are at least two main options here:

  1. $f$ is a class of pairs, such that…

  2. $f$ is a set of pairs, such that…

At least in most traditional presentations, I think it’s defined as the latter, but some people here also seem to be using the former. The answer to this question depends on which we take.

If we take the “a function is just a class” definition, then as suggested in the original question, and as stated in François’ answer, we definitely have some big problems without replacement: Set is no longer complete and co-complete, etc. (nor are the various important categories we construct from it); we can’t easily form categories of presheaves; and so on. Under this approach, we certainly get crippling problems in the absence of replacement.

On the other hand, if we take the “a function must be a set” definition, we get some different problems (as pointed out in Carl Mummert’s comments), but it’s not so clear whether they’re big problems or not. We now can form limits of set-indexed families of sets; presheaf categories work how we’d hope; and so on. The problem now is that we can’t form all the set-indexed families we might expect: for instance, we if we’ve got some construction $F$ acting on a class (precisely: if $F$ is a function-class), we can’t generally form the set-indexed family $\langle F^n(X)\ |\ n \in \mathbb{N} \rangle$.

This is why we still can’t form something like $\bigcup_n \mathcal{P}^n(X)$, or $\aleph_\omega$. On the other hand, such examples don’t seem to come up (much, or at all?) outside set theory and logics themselves! Most mathematical constructions that do seem to be of this form — e.g. free monoids $F(X) = \sum_n X^n$, and so on — can in fact be done without replacement, one way or another.

Now… I seem to remember having been shown an example that was definitely “core maths” where replacement was needed; but I can’t now remember it! So if we take this approach, then we certainly still lose something; but now it’s less clear quite how much we really needed what we lost.

(This approach is very close to the question “What maths can be developed over an arbitrary elementary topos?”.)

Related Question