# Axiom of Replacement in Category 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.

-
The coproduct of a familiy of sets $X_i$ is the union of all the $X_i \times \{i\}$. No replacement, just union axiom is used. – Martin Brandenburg Oct 5 '10 at 9:23
Also, I don't think that we really need Replacement for basic or even advances topics of category theory. – Martin Brandenburg Oct 5 '10 at 9:25
You do need replacement to iterate powerset along $\omega$ starting with an infinite set. The issue is that the sequence $\langle \{i\} \times X_i \rangle$ has to exist before you can take its union. Without replacement, there's no reason to think that that sequence exists in the first place. – Carl Mummert Oct 5 '10 at 11:20
The reason I don't view this as an answer, necessarily, is that the definition of (co)limits is in terms of diagrams, which in turn rely on functors. If we look at small categories, it's reasonable to define functors as sets, in which case the diagram itself is a set that can be used to construct the (co)limit. On the other hand, if we look at large categories and formalize functors as definable relations, then a diagram may be a proper class, in which case it does appear that without replacement Set may not be closed under (co)limits. I'm not certain how these things are usually formalized. – Carl Mummert Oct 5 '10 at 11:42
Rephrasing for emphasis what Carl Mummert said above: The problem with $\bigcup_n P^n(X)$ in the absence of replacement is not the coproduct but the iteration of the power set. It is provable in Zermelo set theory (ZF without replacement) that any set-indexed family of sets has a coproduct that is a set. (Limits and colimits of small-indexed diagrams of sets are OK too.) But Zermelo set theory does not prove the existence of the sequence of iterated power sets $n\mapsto P^n(X)$ when $X$ is, for example, the set of natural numbers. – Andreas Blass Oct 5 '10 at 12:58

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?”.)

-
I now realise Carl Mummert had already pointed out this ambiguity in a comment 8 hours ago! However, there wasn’t yet an answer taking it into account, so I hope this is still adding something :-) – Peter LeFanu Lumsdaine Oct 5 '10 at 19:56
Do people in practice assume the latter? Wikipedia just requires the domain of the diagram functor to be a set. Likewise for Abstract and Concrete Categories. I just looked at Categories for the Working Mathematician, and MacLane explicitly imposes replacement. The usual example of where replacement is needed in analysis is Borel determinancy. – arsmath Oct 6 '10 at 1:07
At least some people do! I'm not sure which Wikipedia article(s) you're looking at, but I find “diagram” defined in terms of “functor”, in turn defined in terms of “function”, and the first definition of function given is: “One precise definition of a function is that it consists of an ordered triple of sets, which may be written as (X, Y, F). X is the domain of the function, Y is the codomain, and F is a set of ordered pairs.” As it later points out, X and/or Y are often omitted, but F is still required to be a set. – Peter LeFanu Lumsdaine Oct 6 '10 at 1:33
(cont’d) As you say, though, replacement is generally assumed, implicitly or explicitly — ZFC, however we feel about it, is still pretty much the “industry standard” foundation. So most authors, I think, wouldn’t consider there to be a significant difference between the two definitions. – Peter LeFanu Lumsdaine Oct 6 '10 at 1:42
oh, and (sorry for so many comments) yep, Borel determinacy is certainly a place where it’s needed, but is that really considered analysis? More significantly, is it used by analysts? I'd always thought of it as being descriptive set theory, and have heard it talked about by set theorists much more than by anyone else. But IANAA. – Peter LeFanu Lumsdaine Oct 6 '10 at 2:10

Let me recommend to you, in lieu of a real answer, Mike Shulman's paper Set theory for category theory, which as he remarks in the introduction,

We will see in later sections that given the other (also non-categorical) axioms of zfc, replacement in fact allows us to construct much larger sets than would otherwise be possible. But we will also see that above and beyond this, replacement plays a subtle and important role in category theory—so much so that this paper could easily have been subtitled “a tale of the replacement axiom”!

and to quote from later in the paper, where he discusses ways to prove the existence of larger and larger sets,

The axiom of replacement guarantees that the union of any family of sets indexed by a set is also a set

so this tells us that $Set$ has small coproducts, something essential for $Set$ to be cocomplete.

-
It may be relevant to remark though that an elementary topos is also "cocomplete" relative to definable families internal to the topos; see for example the discussion on the nLab here: ncatlab.org/nlab/show/cocomplete+well-pointed+topos. So the cocompleteness we are discussing here is external cocompleteness, which depends on a background notion of set. – Todd Trimble Oct 5 '10 at 12:16
– Todd Trimble Oct 5 '10 at 12:17
Why can't I get a URL here? – Todd Trimble Oct 5 '10 at 12:17
Todd, your URL works fine, but it doesn't display the full link. (It takes me to the nLab page for a cocomplete well-pointed topos, which seems to be what you were discussing in your first post.) – dvitek Oct 5 '10 at 17:51

The axiom of replacement guarantees that any functor from a small category C to another (potentially large) category D is itself a set. This is what allows us to make sense of the functor category DC. Without replacement, categories of presheaves, for example, are harder to formalize and do not necessarily have the expected properties.

-

The other answers and comments so far indicate that the axiom of replacement is needed to show the existence of coproducts in Set. This is not true if we adjust the definitions properly ;).

The existence of coproducts in a category $C$ may be formulated that if $F$ is a set of objects in $C$, then there is a object $\coprod F$ with the usual universal property. Note that the usual formulation uses a function from a set to the class of objects of $C$ (a "family"), which almost always requires an application of the axiom of replacement, which is somehow artificial.

Now in the category of sets, let $F$ be a set of sets. Then $x \mapsto x \times \{x \}$ is a function $F \to F \times P(F)$. By comprehension, the image exists and this will be $\coprod F$.

I believe that most of (all?) category theory can be developed with definitions as above and then we do not have to use replacement to show the standard category theoretic properties of the categories in practice.

There is a nice exercise in Kunen's Set theory (IV, Ex. 9), in which the reader has to develope 99 % of modern mathematicss in ZC, which is ZFC without replacement ;-).

-
You could do it, but I find it interesting that in practice people just act as if replacement is true. Honestly, I personally had no idea that I was implicitly relying on replacement when thinking about categorical constructions, since at first glance it really does sound like a technical axiom you would never use. I feel like Moliere's Monsieur Jourdain discovering he's been speaking in prose his whole life. – arsmath Oct 6 '10 at 1:15
I find that interesting too, but I don't think it proves much one way or the other. In previous periods, people implicitly assumed things like unrestricted comprehension (as shown to be inconsistent, by Russell), and continuity of all functions (not quite inconsistent, as things like SDG show, but certainly at odds with other more basic intuitions like the excluded middle). The things we implicitly use, and completely natural, often turn out to be just the standard assumptions of the culture we were educated in, not necessarily any more than that… – Peter LeFanu Lumsdaine Oct 6 '10 at 2:17