# Developing category theory inside ETCS

Trying to understand how Lawvere's [E]lementary [T]heory of the [C]ategory of [S]ets can be used as a foundation for mathematics alternative to ZFC, I am getting stuck with the question on how to develop category theory within ETCS.

It's neither a problem in ZFC nor in ETCS to define the notion of a category, at least internally, when objects and morphisms are "sets". However, what is problematic in developing category theory completely internal to ZFC, i.e. without use of proper classes and metatheorems, is the choice of what we want to call the category of sets inside ZFC. One way to solve this is to introduce Grothendieck universes and to take them as the "base-categories of sets", on which category theory within ZFC can be built.

My question now is: What are the possibilites in ETCS to ensure a reasonable "category of sets" based on which category theory can be developed inside ETCS?

Are there any good sources for this question?

Thanks!

Hanno

-
My inclination would be that as long as you're using ETCS you might as well take categories to be your primitive notion and then you don't have to reaxiomatize categories. –  Qiaochu Yuan Jun 29 '13 at 10:00
Note that $\sf ETCS$ is much weaker than $\sf ZFC$, since it lacks the replacement schema (or anything equivalent/stronger). So $\sf ZFC$ can prove the consistency of $\sf ETCS$. If you could define categories fully in $\sf ETCS$ then you could in $\sf ZFC$ as well. –  Asaf Karagila Jun 29 '13 at 11:44
Qiaochu: Thank you for your comment! Could you elaborate a bit? So far I don't yet understand what you mean. –  Hanno Jun 29 '13 at 12:31
Asaf: Thank you! Ok, so one should at first add the replacement axiom scheme to ETCS. My question is then: What do we need in addition to this? –  Hanno Jun 29 '13 at 12:34
Universe in a topos. Note that this formulation is stricly relating to Zhen Lin's answer. –  Andrea Gagna Jun 29 '13 at 16:13

The point of ETCS is that a model of ETCS is already a category, so I suppose what you are asking for is how to do universes in ETCS. Well, ETCS is equivalent in a strong sense to Mac Lane set theory, and in Mac Lane set theory, Grothendieck universes are models of (second-order!) ZFC. So if you're willing to go down that route it suffices to axiomatise strongly inaccessible cardinals within ETCS – and this is straightforward.

Now suppose $X$ is a set of strongly inaccessible cardinality. We construct within ETCS a category of small sets based on $X$. First, let $O$ be the subset of $\mathscr{P}(X)$ consisting of those subsets of $X$ strictly smaller than $X$, and let $E \subseteq X \times O$ be the binary relation obtained by restricting $[\in]_X \subseteq X \times \mathscr{P}(X)$. We may regard the projection $E \to O$ as an $O$-indexed family of sets, and we may then form $F \to O \times O$ such that the fibre of $F$ over an element $(Y, Z)$ of $O$ is the set $Z^Y$. This has the expected universal property in the slice category $\mathbf{Set}_{/ O \times O}$. Once we have $F \to O \times O$, it is a straightforward matter to build an internal category which, when externalised, is the full subcategory of $\mathbf{Set}$ spanned by the small subsets of $X$. Note that the assumption that the cardinality of $X$ is a regular cardinal implies that the resulting category is a model of not just ETCS but also the axiom of replacement.

Of course, if one really believes ETCS is an adequate foundation for mathematics, then one can also make do with less. For instance, the same construction could be carried out for a set whose cardinality is a strong limit, and the resulting internal category of sets will still be a model of ETCS though not necessarily of replacement.

-
Zhen, thank you very much for this interesting and helpful answer! Could you explain in some detail what you mean by "when externalized, ..."? In the concrete situation, I think I know what you mean: we do not only have a category in ETCS, but in fact a category the objects of which "are" again sets in such a way that the morphism sets of the category we consider are the corresponding power sets. Still, this is rather an ad-hoc interpretation of what you're saying, without knowing what "externalizing" means in general, so could you maybe elaborate? –  Hanno Jun 29 '13 at 16:14
It essentially means to interpret internal structures as instances of those structures in the meta-logic. It is not meant to be precise. –  Zhen Lin Jun 29 '13 at 16:39
Is it true that the family $E(X)\to O(X)$ you constructed from $X$ is a universe, and that any universe $E\to U$ arises in this way? Like in ZFC where the Grothendieck universes are precisely the $V_\kappa$ with $\kappa$ strongly inaccessible? –  Hanno Jun 30 '13 at 6:00
It should be a universe, but I have no checked. Not all universes are of this form, I think. –  Zhen Lin Jun 30 '13 at 6:18

First, note that the theory of categories is one-sorted in nature, despite it is usually presented as two-sorted (objects, arrows), since you can identify an object with its identity arrow.

The ETCS is actually part of a larger formal system, the Elementary Theory of the Category of Categories [ETCC], where alphabet's variables represent morphisms between categories. The most important objects, that have to be axiomatized, are the categories $\mathbf{0, 1, 2, 3}$. A good reference may be: Elementary Categories, Elementary Toposes.

Lawvere, in his beautiful PhD thesis, suggested to deal with dimensional problems in a way very similar to ZF3 (i.e., ZF enhanced with universes $\omega = \theta_0 \in \theta_1\in \theta_2$). Thus, he proposed to axiomatize the existence of two categories (i.e., variables)

• $\mathcal C_1$ which has to be thought as the category of small categories. Here, the most important category of sets is $\mathbf{FinSet}$ (Bill calls it $\mathcal S_0$). One requires it to have all the nice properties of $\mathbf{Cat}$.
• $\mathcal C_2$ which has to be thought as the category of large categories. One requires it has all the nice properties of $\mathcal C_1$ and more an identity arrow (i.e., an object, a category) with all its property (that is, $\mathcal C_1$). Of course, the category of small sets may be think as an object of $\mathcal C_2$, i.e., an arrow $\{\mathcal S_1\}\colon \mathbf 1 \to \mathcal C_2$.

In this general framework, one can axiomatize ETCS.

Also, take a look to these 3d on MO: 1, 2.

-
Thank you, Andrea! I am rather interested in adding axioms to ETCS while keeping the formal system fixed instead of passing to a larger system; still, ETCC sounds very interesting and I will definitely have a look in McLarty's book - thank you! Concerning the third paragraph: In which formal system do the two axioms stating the existence of ${\mathcal C}_1$ and ${\mathcal C}_2$ live? Are they ETCS formulae? If yes, then what do you mean with your last comment? –  Hanno Jun 29 '13 at 12:44
In Lawvere's world, $\mathcal C_i, i=1, 2$ live in ETCC. Actually, you need less than all ETCC to formalize ETCS. Take a curious look at this page on nlab. As you can see, axioms are really easy. –  Andrea Gagna Jun 29 '13 at 13:27