On the definition of small categories in SGA4

Question

We assume ZFC+U. A category is an ordered pair $(\operatorname{Ob} \mathcal{C},\operatorname{Mor} \mathcal{C},\operatorname{dom},\operatorname{codom},e,∘)$ of sets (not classes) and maps satifying some conditions.

Let $\mathbb{U}$ be a Grothendieck universe. An element of $\mathbb{U}$ is called a $\mathbb{U}$-set. A set is called $\mathbb{U}$-small if it is isomorphic to a $\mathbb{U}$-set. In the following, we suppose that $\mathbb{N} \in \mathbb{U}$.

In SGA4, a category $\mathcal{C}$ is called $\mathbb{U}$-small if $(\operatorname{Ob} \mathcal{C},\operatorname{Mor} \mathcal{C},\operatorname{dom},\operatorname{codom},e,∘)$ is $\mathbb{U}$-small as a set (if my understanding is correct). However, I don't see this definition working well. For any set $a$ and $b$, an ordered pair $(a,b)$ is always $\mathbb{U}$-small since $(a,b)=\{\{a\},\{a,b\} \}$ is a set consisting of exactly two elements, which is isomophic to $2:=\{\emptyset,\{\emptyset\}\} \in \mathbb{U}$. Thus, $\mathbb{U}$-smallness imposes nothing on categories. In particular, it is not equivalent to $\operatorname{Ob} \mathcal{C}$ and $\operatorname{Mor} \mathcal{C}$ are $\mathbb{U}$-small.

I think I am mistaken somewhere, where is it?

Answer 1

You’re correct: read literally, those definitions are mismatched, for the reasons you give. The solution is to fix the definition of “$U$-small category” to say that “$\newcommand{\C}{\mathcal{C}}\newcommand{\mor}{\mathrm{mor}}\mor(\C)$ is $\newcommand{\ob}{\mathrm{ob}}U$-small” — this is what the authors of SGA4 clearly intended (as clarified in the footnote on p2 of this modern edition, pointed out by @abx in comments), but expressed in a way that doesn’t depend on the precise encoding of the definition of categories or of ordered pairs.

There are two general points here:

• Outside of explicit investigations of set-theoretically foundational issues (and usually even within such contexts), nothing should ever depend on the specific set-theoretic implementation of ordered pairs. Anything that seems to depend on it can very safely be assumed to be a misunderstanding, an abuse of notation, or a mismatch of definitions.

• More generally, mathematics is usually written in “implementation-independent” ways as far as possible. Of course, there are often lapses from this in practice, and that sometimes leads to mismatches, as here. When such mismatches happen, the right fix is to rewrite the later definitions in more implementation-independent ways, not to tweak the implementation of the earlier definitions so that the implementation-dependent later definitions work. In ordinary human-practiced mathematics, this usually isn’t a problem, because it’s clear what people meant. But in computer-formalised mathematics (and programming more generally), this is a serious concern: if you go back and change the implementation of the earlier definition to make one later definition work, then that may break anything else that was written in an implementation-specific way. Implementation-dependent definitions are inherently fragile — so fix them, don’t take them as god-given and twist other things around to try to work with them.

Answer 2

I have found a satisfactory solution to the above problem in this MO answer and would like to describe it here.

The ordered pair of sets $x$ and $y$ is a set $(x,y)$ which satisfies $$(x_1,y_1)=(x_2,y_2) \quad \Longrightarrow \quad x_1=x_2 \quad \text{and} \quad y_1=y_2.$$ The standard way to construct such sets is Kuratowski ordered pairs, which is used in my question above: $$\langle x,y \rangle:= \{ \{x\}, \{x,y\} \}.$$ However, there is another way to construct ordered pairs, which is described in the MO answer above: $$\lbrack x,y \rbrack:= x\times\{0\} \cup y\times\{1\}.$$ It is clear that $\lbrack x,y \rbrack$ also satisfies the condition of ordered pairs. This ordered pair is not standard but solve my question. We can easily see that $\lbrack x,y \rbrack$ is $\mathbb{U}$-small if and only if both $x$ and $y$ are $\mathbb{U}$-small. Thus, if we define a category as an ordered pair $\lbrack \operatorname{Ob} \mathcal{C},\operatorname{Mor} \mathcal{C},\operatorname{dom},\operatorname{codom},e,\circ \rbrack$ satisfying some conditions, then it is $\mathbb{U}$-small if and only if both $\operatorname{Ob} \mathcal{C}$ and $\operatorname{Mor} \mathcal{C}$ are $\mathbb{U}$-small as desired.

As suggested in the MO answer above, a suitable construction of ordered pair for category theory might be $\lbrack x,y \rbrack$.