Timeline for Axiom of Replacement in Category Theory
Current License: CC BY-SA 2.5
17 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 14, 2010 at 16:52 | vote | accept | arsmath | ||
| Oct 7, 2010 at 21:53 | comment | added | Andreas Blass | I was indeed using "family" (in the context "set-indexed family") as meaning a set, not a class as in the definition quoted by arsmath. | |
| Oct 6, 2010 at 1:54 | comment | added | arsmath | Without replacement, you have to require that small diagrams have sets as ranges, not just domains. Maybe it's what we really meant all along, but it's still an additional restriction that requires us (in the absence of replacement) to check that all of the sets in a diagram satisfy a uniform bound on size, something that no one ever does. This isn't some huge gotcha that proves you have to accept replacement, but it's just that in practice people implicitly rely on replacement rather than check that the range of a small diagram is a set. | |
| Oct 6, 2010 at 1:53 | comment | added | arsmath | Despite the upvotes, I don't see how Andreas' answer can be right as stated. It turns on the definition of a set-indexed family of sets. If you require the family of sets to itself be a set, then it's true, but is that the usual definition? I just looked in Abstract and Concrete Categories, and it defines a set-indexed family to be a class function that has a set as a domain. You can define, without replacement, a class function from the natural numbers to Set that takes i to $P^i X$, which gives a you a set-indexed family without a coproduct. | |
| Oct 5, 2010 at 20:50 | answer | added | Martin Brandenburg | timeline score: 2 | |
| Oct 5, 2010 at 19:54 | answer | added | Peter LeFanu Lumsdaine | timeline score: 9 | |
| Oct 5, 2010 at 12:58 | comment | added | Andreas Blass |
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.
|
|
| Oct 5, 2010 at 12:33 | comment | added | Todd Trimble | @arsmath: yes, when the random mathematician is asked to describe cocompleteness, he already has in mind some external notion of set in the background; cf. my comment to David Roberts's answer. (This isn't arguing with you; I happen to be interested in an honest discussion of these issues.) | |
| Oct 5, 2010 at 12:20 | comment | added | arsmath | Maybe it's not <i>needed</i>, but the theorem <b>Set</i> is a complete and cocomplete category is a completely ordinary and commonly-quoted theorem in ordinary mathematics, one that apparently depends on replacement. We could probably get by with weaker statements like colimits of sets all smaller than a specific cardinal exists, but we don't. Ask a random mathematician on the street "Does the product of a countable family of topological spaces exist?" I think no one (other than a constructivist) would answer no, or "only if each individual space satisfies a cardinality restriction." | |
| Oct 5, 2010 at 12:07 | answer | added | François G. Dorais | timeline score: 3 | |
| Oct 5, 2010 at 11:52 | comment | added | Todd Trimble | @arsmath: yes, your union of iterated power sets is the classic example of a set that cannot be formed without replacement. In fact, starting with a universe $V$, the subuniverse of sets of ordinal rank less than $\omega + \omega$ is a model of ZC (remove the F = axiom of replacement). But I don't see how this construction is particularly needed by mathematicians who are not set-theorists. I would rather know: are there important constructions used in core mathematics, not counting the needs of set-theorists, which really require replacement? | |
| Oct 5, 2010 at 11:42 | comment | added | Carl Mummert | 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. | |
| Oct 5, 2010 at 11:41 | answer | added | David Roberts♦ | timeline score: 8 | |
| Oct 5, 2010 at 11:20 | comment | added | Carl Mummert | 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. | |
| Oct 5, 2010 at 9:25 | comment | added | Martin Brandenburg | Also, I don't think that we really need Replacement for basic or even advances topics of category theory. | |
| Oct 5, 2010 at 9:23 | comment | added | Martin Brandenburg | 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. | |
| Oct 5, 2010 at 8:59 | history | asked | arsmath | CC BY-SA 2.5 |