The n-Category Café

Even if you demand only that every pair of sets has a smallest member, then you are asking that any two sets be comparable in size (there is an injection from one of them to the other), and this implies that any set can be well-ordered.

To see that any $S$ can be well-ordered, take it and its Hartogs number $\aleph(S)$, which is the collection of isomorphism classes of subsets of $S$ equipped with a well-ordering. Any two well-ordered sets are comparable, and it can be shown that $\aleph(S)$ is itself well-ordered under this comparability ordering. It can also be shown, along the lines of the Burali-Forti paradox, that $\aleph(S) \leq S$ leads to a contradiction.

So if $\aleph(S), S$ are comparable, then it must be that $S \lt \aleph(S)$, giving an injection from $S$ to a well-ordered set. But then $S$ becomes well-ordered, by restricting the order on $\aleph(S)$ to $S$.

Todd’s nice answer is related to an interesting point about successor sets $X^+$.

In the post, I said the following. We know that for every set $X$, there’s some other set strictly larger than $X$, so (using choice) there must be a smallest set $X^+$ strictly larger than $X$. This is a perfectly valid definition of $X^+$, but it leaves it somewhat nebulous. Unlike the power set, we have no explicit description of $X^+$, and even its existence depends on the axiom of choice. At least, that’s how it seems from the presentation I gave.

But happily, $X^+$ does have an explicit description, in the following sense. As Todd says, one can apply the Hartogs construction $\aleph$ to the set $X$, giving the well-ordered set $\aleph(X)$ that he describes. The underlying set of $\aleph(X)$ consists of the isomorphism classes of well-ordered sets of cardinality $\leq X$, and the important point is that it’s exactly $X^+$. Indeed, as the nLab page says, $\aleph(X)$ is the smallest well-ordered set with cardinality $X^+$.

To prove that the underlying set of $\aleph(X)$ is $X^+$ requires the axiom of choice. (We can’t possibly get away without choice: for as in Todd’s answer, if every set injects into some well-ordered set then every set can be well-ordered.) But no choice is needed to give the definition of $\aleph(X)$.

Without choice, would one then use well-preorders or well-quasiorders instead of well-orders?

Ha! Well caught. Thanks; I’ll fix that.

Yes, $\mathbb{N}$ is a strong limit. But the subconscious thought behind that slip was that it’s the trivial example. I’ve been confused several times by set theory texts silently assuming that sets were uncountable. And now I’ve gone and done the same thing myself.

Speaking of smallish strong limits, I think by your definition 0, 2 and $\mathbb{N}$ are strong limits, but not 1.

They would be, except that I explicitly put into my definition that strong limits must be infinite.

Somewhat relatedly, the story I told is really motivation for the concept of uncountable strong limit. An uncountable strong limit is a set that’s too big to be reached by ETCS. But I’m bowing to tradition by separating the concept of uncountablestronglimit into two.

True. I thought about putting the definition in, but decided against as I thought readers would easily surmise.

Given your comment, I’ll insert the definition into the post after all. But I’m curious: did you genuinely not know what I meant by $\lt$, or was your comment intended as the correction of an oversight?

I’m puzzled by this comment. Define it in any way that would be standard assuming classical logic, e.g., $x \leq y$ and $y \nleq x$. Is this not common understanding?

(Or is this another comment, but without saying so, about whether the background logic is constructive? I don’t think Tom said anything about that; my general understanding is that if nothing is said, go ahead and assume that the speaker is using classical logic throughout. If he did and I missed it, then I agree that a whole lot more care would be needed.)

Yup, classical logic throughout.

Strict categories are sets, so to say a strict category (such as Cat) contains itself runs into Burali-Forti’s paradox, and since sets are discrete categories themselves, it runs into Russell’s paradox as well, which is why we have large and small sets in the first place, and hence large and small strict categories.

On the other hand, if Cat is a weak category, then the underlying collection of objects is a weak groupoid rather than a set, so the usual Burali-Forti’s paradox and Russell’s paradox for sets wouldn’t apply here. However, there is still a version of Burali-Forti’s paradox for weak groupoids, which states that if a weak groupoid contains itself, then it is trivial, which is why we still speak of small and large weak groupoids and categories. This first appeared in type theory, where a type theoretic model of weak groupoids was constructed and where Burali-Forti’s paradox for types is called Girard’s paradox.

Josh, it’s not a stupid question at all.

As far as these posts are concerned, I’m not thinking about the size of categories at all. And my temporary use of the word “small” in part of this post wasn’t supposed to be related to “small category”; it was just a convenient word.

But zooming out, there are various ways of formalizing the small/large distinction for categories. One approach is to use sets vs. classes (which requires some axiomatic notion of class). Another is to say that even large categories are supposed to have a set of objects, and small categories are those whose set of objects is below some threshold. Inaccessibility often comes in here. I’ll get to inaccessibility in a few posts’ time, and though I won’t attempt to say anything about the connection with large/small categories, there are well informed people here who know all about that kind of thing.

In categorical approaches, the question of whether a set contains itself doesn’t make a whole lot of sense, because membership isn’t a relation defined on the collection of sets. (That is, given two sets $X$ and $Y$, it doesn’t make sense to ask whether $X \in Y$.) The same goes for categories containing themselves.

In categorical approaches, the question of whether a set contains itself doesn’t make a whole lot of sense, because membership isn’t a relation defined on the collection of sets.

But we can make sense of roughly the same intent using families: a family $p:A\to I$ “contains itself” if there exists an element $i\in I$ such that $A_i \cong I$.

This only addresses your question 2, but Colin McLarty has a paper that I very much like, Exploring categorical structuralism. Section 8 is on replacement.

Here’s how I’d explain it. In ETCS, a family of sets indexed by a set $I$ is naturally defined as a function $p: X \to I$ into $I$. The $i$th fibre $X_i = p^{-1}(i)$ can be called the “$i$th member of the family”, and $X$ is the coproduct $\sum_i X_i$.

Another idea of what a “family” should be is that it’s a formula for producing a set from each element of $I$. Formally, then, a family is a first order ETCS formula $R = R(i, X)$ in elements $i \in I$ and sets $X$, such that for each $i \in I$, there is a unique-up-to-isomorphism set $X$ such that $R(i, X)$ holds.

(The contrast between these two conceptions of family is similar to what I understand to have been the debate around the time that the notion of “function” was being nailed down: is a function an arbitrary collection of assigned values, or a formula for assigning those values? The former conception became the standard one, but the latter is important in logic.)

We can add to ETCS the axiom that any family in the second sense gives rise to a family in the first sense. That is, for any $R$ as above, there exist a set $X$ and a map $p: X \to I$ such that $R(i, p^{-1}(i))$ holds for every $i$.

One could call this axiom cocompleteness. (It only asserts the existence of small coproducts, but we already have coequalizers from ETCS alone, so we get all small colimits.) Or we could call it replacement, as McLarty does. He writes:

Probably few readers think this looks like the ZF axiom scheme [of replacement]. […] Our axiom is not a translation from ZF. It is a plain categorical version of Cantor’s idea.

ETCS with this replacement/cocompleteness axiom adjoined is biinterpretable with ZFC (that is, equivalent to it in the strongest sense).

Replacement is interesting and worth thinking about, but it’s not necessary to do basic category theory, and I don’t think it’s correct to call it “cocompleteness”. In particular, ETCS already proves that the category of sets is complete and cocomplete. The point is that in order to say something like “every family of sets has a product and coproduct” in ETCS, you have to first decide what a “family of sets” is in ETCS, and as Tom mentioned, the only sensible definition is that it’s a morphism $A\to I$ (where $I$ is the indexing set). The product and coproduct of such a family can then be defined in ETCS (in fact, the coproduct is just the set $A$).

It’s true that if you instead defined a “family of sets” using a logical formula then ETCS would not prove that the category of sets is cocomplete, but this is the wrong definition of “family of sets” for the purposes of category theory. In fact, with this definition of “family of sets”, ETCS cannot even formulate the statement that the category of sets is cocomplete, because it cannot quantify internally over logical formulas.

Thank you to both you and Tom for your thoughts! I was just thinking quite simplistically about the following…

Take a model of ETCS, that is, a category satisfying the ETCS axioms. Let’s temporarily say that a set (in this model) is “small” if it is strictly smaller than every uncountable strong limit. Then the small sets are also a model of ETCS. For example, if $A$ and $B$ are small then for every uncountable strong limit X, we have $A \lt X$ and $B \lt X$, therefore $B^A \lt X$; hence $B^A$ is small. So we’ve shown:

For any model of ETCS, the sets smaller than every uncountable strong limit are also a model of ETCS.

…and observing that this argument does not work if, for example, the colimit

$$\mathbb{N} \rightarrow 2^{\mathbb{N}} \rightarrow 2^{2^\mathbb{N}} \rightarrow \ldots$$

is required to exist as part of the definition of ETCS in some way or other. Since it is replacement that guarantees the existence of this colimit in ZFC, co-completeness seems analogous to replacement at least to some degree.

Thanks, Richard. I take your point. And your comment looks forward nicely to some later posts. In particular, we’ll look at the supremum of $$\mathbb{N}, 2^{\mathbb{N}}, 2^{2^{\mathbb{N}}}, \ldots$$ and more generally, the supremum of $$X, 2^X, 2^{2^X}, \ldots$$ for any set $X$.

Part of the point of this whole series is that while replacement is natural enough and has a lot going for it, it’s not the only way of guaranteeing that sets like this exist. For example, one can directly add the axiom “sets like this exist”! I’ll get to that in a while.

As this series goes on, the sets involved will get ever larger. At first, replacement will be enough to guarantee their existence, but later it won’t be enough.

Actually replacement isn’t what guarantees the existence of the colimit of the diagram $\mathbb{N} \to 2^{\mathbb{N}} \to \cdots$. Replacement is what guarantees the existence of that diagram! (And in particular, ETCS cannot prove that that diagram exists.) Once you have the diagram, ETCS can prove that it has a colimit.

A little more precisely, replacement guarantees that that diagram is small. Zermelo set theory can show that that diagram exists as a proper class; ETCS can do something similar, although “proper classes” are a bit different in ETCS-land. But of course “cocompleteness” means only that all small diagrams have a colimit.

So again, I would say that the connection between replacement and cocompleteness is an illusion. Cocompleteness says that small diagrams have a colimit; replacement is just about how many small diagrams there are.

A little more precisely, replacement guarantees that that diagram is small. Zermelo set theory can show that that diagram exists as a proper class; ETCS can do something similar, although “proper classes” are a bit different in ETCS-land. But of course “cocompleteness” means only that all small diagrams have a colimit.

So replacement is more accurately a schemata of large cardinal axioms.

I don’t personally agree that this splitting of hairs is significant or changes anything (I think one can quibble in many ways here about what is implicit here or there, or about what is reasonable to consider in a ‘neutral’ context), but we are only discussing the validity of an analogy, so it doesn’t matter too much! I look forward to the rest of the series!

I haven’t yet absorbed enough of this to have a sense of whether $i \mapsto \tilde{S}_i$ is definable in ETCS. But if I’ve understood roughly what’s going on, it could be that replacement is much stronger than necessary. Perhaps it’s enough to add to ETCS the far weaker condition that “beths exist”, which is equivalent to:

for every well-ordered set $I$, there exists a map of sets $p: X \to I$ such that $i \lt j \implies 2^{|p^{-1}(i)|} \leq |p^{-1}(j)|$ for all $i, j \in I$.

This condition is in turn equivalent to a similar but apparently stronger one, in which all the fibres $p^{-1}(i)$ are required to be bigger than some prescribed set $Y$. So then, if we take $I = \mathbb{N}$, then for any set $Y$ we’re guaranteed the existence of an $\mathbb{N}$-indexed family $X \to \mathbb{N}$ whose $0$th fibre is $\geq Y$, whose $1$st fibre is $\geq 2^Y$, whose $2$nd fibre is $\geq 2^{2^Y}$, and so on. Is that enough to construct the hypercover?

Of course, it would be nice if you could do what you need to do using ETCS alone. But even if not, replacement may be much more than necessary.

I’m aware that others who know much more about set theory than me have argued that replacement is over-emphasized and owes some of its prominence to historical accident, and that in many instances, large cardinal axioms would suffice. In this case, “beths exist” is a not-so-large cardinal axiom, to borrow your phrase :-)

I guess Replacement is really quite ingrained in what I consider “naive” set theory.

I’m aware that others who know much more about set theory than me have argued that replacement is over-emphasized and owes some of its prominence to historical accident

On the other hand, one could construct a constructive material set-theoretic cumulative hierarchy $(V,\in)$ that satisfies replacement from a universe $U$ in the univalent type theory used in the Homotopy Type Theory textbook by the Univalent Foundations Project, such that when the axiom of choice sets is added to the type theory, constructing $(V,\in)$ results a model of classical ZFC. This might mean that bare ETCS and well-pointed 1-topos theory is too weak a theory for set theory for lack of enough set-truncated higher inductive types, and that replacement naturally follows from the axioms of a well-pointed $(\infty,1)$-topos.

This might mean that bare ETCS and well-pointed 1-topos theory is too weak a theory for set theory for lack of enough set-truncated higher inductive types, and that replacement naturally follows from the axioms of a well-pointed (∞,1)-topos.

In fact, I think the existence of object classifiers in any $(\infty,1)$-topos (which don’t exist in bare ETCS) is equivalent to the reflection principle in set theory, which could replace the axiom of replacement in any axiomatic set theory.

Whether or not the diagram $i\mapsto \tilde{S}_i$ is “defined” in ETCS depends on your definition of “diagram of sets”.

If $C$ is a small category, then one definition of a “$C$-indexed diagram of sets” consists of a $C_0$-indexed family of sets (meaning, as Tom has said, a function $A\to C_0$) together with an action $C_1 \times_{C_0} A \to A$ that is associative and unital. With this definition, ETCS cannot prove that $i\mapsto \tilde{S}_i$ is an $\mathbb{N}$-indexed diagram. In general, without replacement you cannot construct families of sets by recursion unless you can show that there exists a set giving a uniform bound for all the elements of the desired family.

Another definition of “$C$-indexed diagram of sets” involves instead a logical formula $R(c,A)$ such that for any $c\in C$ there is a set $A$, unique up to (perhaps unique) isomorphism, such that $R(c,A)$, plus functorial action. ETCS can show that $i\mapsto \tilde{S}_i$ is an $\mathbb{N}$-indexed diagram in this sense; but it cannot construct the colimit of this sort of diagram.

So your intuition is right, if by “diagram” you mean the second sort. But the point is that in ETCS, it’s the first kind of diagram that’s the “correct” one. For instance, if you want to talk about a the presheaf category of $C$, then its objects must be diagrams in the first sense. And, as mentioned above, $Set$ has limits and colimits of diagrams in the first sense, but not the second. Category theory just doesn’t work normally in the absence of replacement if you try to use diagrams in the second sense, but it works perfectly well for diagrams in the first sense. The only problem is that very occasionally, as in your case, one runs across a diagram in the second sense that isn’t one in the first sense without replacement.

Perhaps it’s enough to add to ETCS the far weaker condition that “beths exist”

That looks like it might be enough. But I’m surprised to hear that that’s far weaker than replacement. Can you give a brief intuition for why? I didn’t find anything in a quick google for “beths exist”.

So here’s the question: do you need the whole hypercover to make a concrete conclusion about the base space? For instance, to calculate a particular cohomology/Ext group? Suppose one took the truncated hypercover, just a few notches above the desired dimension, then the calculation would go ahead as per normal, with the same result.

For what purpose do you need the whole simplicial object? I guess one might want to pass to a suitable $(\infty,1)$-category of simplicial sheaves (condensed anima or what-have-you).

I’d argue that [Replacement is] a perfectly natural axiom that I probably have used quite often, and would not want to miss. (Surely any use I made can be weakened, but I’d argue that we want to have axioms that are as permissive and unobstructing as possible, and now I’m quite sure that removing Replacement would feel quite obstructing to me.)

I mostly agree with this. Many, perhaps even most, uses of Replacement are inessential and can be avoided by taking care to define small diagrams correctly and so on, which essentially amounts to working with “indexed categories” throughout. McLarty did essentially this, in material set theory, in The large structures of Grothendieck founded on finite-order arithmetic. But as important and interesting as the ability to do this is, it rather uglifies the mathematics; no one in practice is going to start doing things this way.

However, I believe there’s a middle way. By passing into the stack semantics of a model of ETCS, we can put ourselves in a world where Replacement holds automatically. Semantically, this essentially means the uglification is happening “under the hood” and the “user” doesn’t have to concern themselves with it. The tradeoff is that we have to give up the full axiom of separation, and the axioms of excluded middle and choice when applied to “large” formulas. But most of category theory is very constructive anyhow, most of the rest of mathematics takes place with “small” formulas, and one can argue that uses of unbounded separation are rarer than uses of replacement.

Mike

By passing into the stack semantics of a model of ETCS, we can put ourselves in a world where Replacement holds automatically. Semantically, this essentially means the uglification is happening “under the hood” and the “user” doesn’t have to concern themselves with it. The tradeoff is that we have to give up the full axiom of separation, and the axioms of excluded middle and choice when applied to “large” formulas.

So do you think Peter’s construction would go through in this world where Replacement holds? I guess one only needs to have Stone–Čech compactifications of discrete spaces, but we’d need the usual properties to hold. Presumably one could pass to a locale if absolutely necessary, which would have better constructive properties.

Unfortunately (?), Peter’s construction is one of those cases that really needs additional strength beyond ETCS, rather than being arguable away at the cost of uglification. In Zermelo set theory, it fails due to the lack of replacement. But in the stack semantics set theory, it fails instead due to the lack of full separation. Constructing a family of sets by induction over $\mathbb{N}$ in general requires both replacement and separation; separation to form “the set of all $n$ such that $A_n$ exists” so that you can use induction to prove that it’s all of $\mathbb{N}$, and then replacement to collect together those sets $A_n$ into a single family.

I’m happy to agree that replacement is a cocompleteness property of $Set$, in the general sense of asserting that certain colimits exist. It’s just that it’s not the property usually called “cocompleteness”, because that asserts only that small diagrams have colimits, which is provable in ETCS for $Set$. Replacement is a stronger cocompleteness property which instead asserts that certain a-priori large diagrams have colimits (or, equivalently, that those diagrams are in fact small).

I think the most natural way to prove the existence of $X^+$ is the one I alluded to in the post:

when I defined $A^+$, I implicitly assumed the fact that any family $(A_i)_{i \in I}$ of sets, indexed over some nonempty set I, has a smallest member. (For without this fact, how would we know that there’s a smallest set strictly bigger than $A$?) This can be proved using Zorn’s lemma, or by arbitrarily well-ordering each member.

Let’s take this fact for granted. Given a set $X$, we know there’s at least one set bigger than $X$, namely, $2^X$. Now consider the set of subsets $Y$ of $2^X$ such that $X \lt Y \leq 2^X$. This family of sets is nonempty, since we can take $Y = 2^X$. So by the fact above, it has a smallest member $Z$. Then $Z$ is nothing but $X^+$; that is, $X \lt Z$ and whenever $Z'$ is a set satisfying $X \lt Z'$, then $Z \leq Z'$.

(A point in the background here is that $X^+$, like everything in ETCS, is only defined up to isomorphism.)

An alternative way of coming at it would be to use the Hartogs construction, as in the comment above. In other words, we can construct $X^+$ as the set of isomorphism classes of well-ordered sets of cardinality $\leq X$.