Axiom of Replacement in Category Theory - MathOverflow

Axiom of Replacement in Category Theory

2010-10-05T08:59:05Z

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.

Answer by David Roberts for Axiom of Replacement in Category Theory

2010-10-05T11:41:42Z

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.

Answer by François G. Dorais for Axiom of Replacement in Category Theory

2010-10-05T12:07:41Z

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 D^C. Without replacement, categories of presheaves, for example, are harder to formalize and do not necessarily have the expected properties.

Answer by Peter LeFanu Lumsdaine for Axiom of Replacement in Category Theory

2010-10-05T19:54:00Z

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:

$f$ is a class of pairs, such that…
$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?”.)

Answer by Martin Brandenburg for Axiom of Replacement in Category Theory

2010-10-05T20:50:18Z

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 ;-).