On the large cardinals foundations of categories

(This question was posted on math.SE over two weeks ago, but received no answer. I am therefore posting it here as well.)

It is well-known that there are difficulties in developing basic category theory within the confines of $\sf ZFC$. One can overcome these problems when talking about small categories, and perhaps at one or two levels when talking about larger categories (e.g. if the objects and the morphisms are all definable uniformly, I suppose it is possible to do prove some basic things).

But often we want to talk about larger and larger categories, and for that we need the ability to deal with higher and higher level of classes.

The easiest route to solve this is to use the Tarski-Grothendiek set theory, but that is equiconsistent with the existence of a proper class of inaccessible cardinals. While not a mind-boggling assumption, it is still quite a strong one. Even if people are only interested in one or two levels, often they just assume that some suitable number of inaccessible cardinals exist.

But I kept asking myself, what is wrong with just assuming that you have an $\omega$, or $\omega+1$ chain of models of $\sf ZFC$?

That is, a chain $\langle M_n\mid n\in\omega\rangle$ such that $(M_n,\in)\models\sf ZFC$ and $M_n\in M_{n+1}$. Perhaps we want another $M$ which contains all the models and the sequence as well. We can even assume they are countable if we really want to. This is a much weaker assumption in terms of additional axioms, and should be roughly equivalent to $\rm Con^\omega(\sf ZFC+St)$, where $\sf St$ is the axiom asserting a standard model exists.

So why are people jumping to large cardinals? I am certain that they are needed for some construction, but if we just want to talk about categories of categories and so on and so forth, why isn't the above assumption sufficient? Is it just because large cardinals, or rather universes, are easier to explain to the working mathematician? Or is there something we really can't do with this sort of chain of models and we can do with inaccessible cardinals?

-
See related answer on weaker universe concepts here: mathoverflow.net/questions/24552/…. One can have a hierarchy of elementary substructures $V_\kappa\prec V$ while paying no consistency strength price---it is equiconsistent with ZFC. – Joel David Hamkins May 14 '13 at 10:44
@Joel, +1, that's a good comment and a very interesting answer! – Michal R. Przybylek May 15 '13 at 9:07

Allow me to make some comments as someone who converted to the universeful approach recently; but take it with a pinch of salt, as I have only been studying category theory for 2½ years.

I should briefly mention the trigger that led me to the pro-universe camp: about 6 months ago, I started learning about quasicategories and became convinced that the theory relied on far too much machinery to admit a workable elementary approach that would allow us to consider entities like the quasicategory of all Kan complexes within an NBG-like framework – which is the the raison d'être for quasicategories in the first place! So I decided that I would have to start taking universes seriously – and for this purpose the universes would not merely be for bookkeeping but for doing actual mathematics in.

If all we wanted to do was to ensure that sets of large cardinality and high complexity exist, it would probably be enough to just have a chain $M_0 \in M_1 \in M_2 \in \cdots$ of (transitive) models of set theory (say, ZFC), but I find this very unsatisfactory. For instance, consider theorems that assert that some object with some universal property exist: there is no guarantee that a universal object in $M_0$ remains universal in $M_1$. Indeed, one such theorem says that, for every set $X$, there exists a set $\mathscr{P}(X)$ and a binary relation $[\in]_X \subseteq X \times \mathscr{P}(X)$ such that, for every binary relation $R \subseteq X \times Y$, there is a unique map $r : Y \to \mathscr{P}(X)$ such that $\langle x, y \rangle \in R$ if and only if $\langle x, r(x) \rangle \in [\in]_X$. Of course, it is well-known that powersets need not be preserved when passing from one model of set theory to another. But if something as trivial as powersets is not preserved, what hope is there of preserving more complicated universal objects like the free ind-completion of a category, or even the free monoid on one generator (i.e. $\mathbb{N}$!)? For a category theorist, to work in a setting where universal objects have to be qualified by a universe parameter is simply untenable.

So, we have to find some kind of compromise: we need a chain of universes such that each universe is embedded in the next in as pleasant a way as possible, so that the mathematics in one universe agrees with the next as much as is feasible. The most ideal situation one could hope for goes something like this:

Let $\mathcal{C}$ be a category scheme, i.e. a definable function that assigns to each sufficiently nice universe $\mathbf{U}$ a category $\mathcal{C}(\mathbf{U})$ such that, for any universe $\mathbf{U}^+$ with a sufficiently nice embedding $\mathbf{U} \subseteq \mathbf{U}^+$, $\mathcal{C}(\mathbf{U})$ is a subcategory (in the strict sense) of $\mathcal{C}(\mathbf{U}^+)$.

We say that an inclusion $\mathbf{U} \subseteq \mathbf{U}^+$ is adequate for a category scheme $\mathcal{C}$ if the following conditions are satisfied:

1. $\mathcal{C}(\mathbf{U})$ is a full subcategory of $\mathcal{C}(\mathbf{U}^+)$: we do not get any new morphisms between objects in $\mathcal{C}(\mathbf{U})$ when passing to a larger universe.
2. The inclusion $\mathcal{C}(\mathbf{U}) \hookrightarrow \mathcal{C}(\mathbf{U}^+)$ preserves all limits and colimits that exist in $\mathcal{C}$ for $\mathbf{U}$-small diagrams: the most elementary kind of universal constructions are preserved when passing to a larger universe.
3. Moreover $\mathcal{C}(\mathbf{U})$ is closed in $\mathcal{C}(\mathbf{U}^+)$ under all limits and colimits for $\mathbf{U}$-small diagrams: so passing to a larger universe does not create new universal objects where none existed before.

So, when is $\mathbf{U} \subseteq \mathbf{U}^+$ adequate for the category scheme $\mathbf{Set}$, if $\mathbf{U} \in \mathbf{U}^+$? We take it as given that $\mathbf{U}$ and $\mathbf{U}^+$ are transitive models of ZFC. The first condition implies that this extension has no new subsets, and if there are no new subsets, there are no new functions either – so (1) holds if and only if the extension preserves powersets. By considering explicit constructions, one sees that equalisers are preserved, and as soon as we know (1), products are also preserved. We may then use the monadicity of $\mathscr{P} : \mathbf{Set}^\mathrm{op} \to \mathbf{Set}$ to deduce that colimits are preserved, so (1) implies (2). In particular, directed unions are preserved, so it follows that $\mathbf{U}$ embeds as an initial segment of the cumulative hierarchy of $\mathbf{U}^+$. What about (3)? Well, take a $\mathbf{U}$-set $I$ and a map $X : I \to \mathbf{U}$ in $\mathbf{U}^+$. By replacement in $\mathbf{U}^+$, we can form the disjoint union $\coprod_{i \in I} X(i)$, and if (3) holds, the cardinal of this set is in $\mathbf{U}$. Thus, $\mathbf{U}$ must actually be embedded as a Grothendieck universe in $\mathbf{U}^+$. Conversely, if $\mathbf{U}$ is embedded as a Grothendieck universe in $\mathbf{U}^+$, then (1), (2), and (3) are easily verified.

But are Grothendieck universes enough? For instance, it would be good if the following were true:

Let $\kappa$ be the smallest (uncountable strongly) inaccessible cardinal, let $\mathbb{B}$ be a $\mathbf{V}_{\kappa}$-small category, and let $\mathcal{M}$ be the category scheme obtained by defining $\mathcal{M}(\mathbf{U})$ to be the free ind-completion of $\mathbb{B}$ relative to $\mathbf{U}$ for each Grothendieck universe $\mathbf{U}$. Suppose $\mathcal{M}(\mathbf{V}_{\kappa})$ admits a cofibrantly generated model structure. Then, for all Grothendieck universes $\mathbf{U}$, there is a (unique) cofibrantly generated model structure on $\mathcal{M} (\mathbf{U})$ extending the one on $\mathcal{M}(\mathbf{V}_{\kappa})$.

However, I do not know if this is true. What I do know is that embeddings of Grothendieck universes are adequate for $\mathcal{M}$; in fact, locally presentable categories and adjunctions between them are very well behaved under this kind of universe enlargement.

-
I feel, reading your comment, that I lack the understanding of what people use universes for. I suppose this is a topic for a whole other question though (or rather to find out on my own). Because I still don't see the issue about keeping track in which universe your objects and categories are in, and taking the proper collections at each point. It's just a lot messier. I didn't ask whether it's more convenient to use a chain of models, and I'm sure it's not. Just whether or not from a foundational point of view if that's a solid foundation which can replace large cardinals. – Asaf Karagila May 15 '13 at 8:28
@Asaf, because you've asked an imprecise question, you get posts answering different issues of the concept of "universe". Perhaps the only answer to the question "is it sufficient..." (and take it really serious) is: "it is sufficient to define a category as number 22; it is also sufficient to define a category as number 2 --- if one does not believe in existence of such large natural numbers as 22". – Michal R. Przybylek May 15 '13 at 9:05
@Asaf: My point is that sometimes one is doing much more than mere bookkeeping. It should go without saying that for the first 2 years that I studied category theory I was in the anti-universe camp because I thought it was all just a matter of being careful with various things, but I have now seen that this just isn't feasible in some areas. I'm afraid there's nothing more I can say if you don't know the category theory involved! – Zhen Lin May 15 '13 at 9:17
Zhen Lin, I am certain that I will not be able to understand a lot of the things involved. Exactly like how it can be immensely difficult to understand forcing without knowing quite a bit of set theory at first. And again, it's clear to me there is more than just bookkeeping involved, and that there are things which are probably not feasible without having universes which are very nicely extended from one step to the next. But if you want to talk about the category of large categories, going to $M_3$ and considering the set of those elements of $M_2$ which are large categories in $M_1$ works – Asaf Karagila May 15 '13 at 9:23
Yes, that much is easy. Actually I prefer not to use any universes at all and just work in NBG for such simple scenarios: because, say, locally small categories are actual objects in the universe of discourse, I can then form the metacategory of locally small categories at the syntactic level and do what I need there. My belief is that, so long as nothing sophisticated is being done, iterating the ZFC-to-NBG construction $\omega$ times should be enough to guarantee the existence of any definable categories one might like to use. The difficulty is when one wants to do universal constructions... – Zhen Lin May 15 '13 at 10:53

There is nothing wrong with that idea, execpt perhaps the questionable taste for countable models of ZFC. (That was half a joke. (That was 3/4 a joke. (I am sure you can see where this is going, so let us just agree that we have one whole joke.)))

In type theory it is common to have a countable sequence of universes $\mathcal{U}_0, \mathcal{U}_1, \mathcal{U_2}, \ldots$ This works pretty well and covers most of what people want, and category theory has been formulated like that. However, the annoying thing we want to avoid is book-keeping of universe levels. There are two techniques that we employ which greatly simplify matters:

1. We use universe polymorphism, i.e., by default we never refer to a specific universe but instead phrase all arguments so that they apply to any universe (or configuration of universes). This is like starting every theorem with "for any universe $\mathcal{U}_i$, ..." and then proving everything for that universe. (If several universes are involved, then the statement becomes more complicated.)

2. We use typical ambiguity, i.e., we say just "category" instead of "$\mathcal{U}$-small category" because we want to be ambiguous as to what level we are talking about. This gives the illusion that there is just a single universe. Nontheless, the illusion is quite useful.

There are some pitfalls. For example, one must never use the "function" $i \mapsto \mathcal{U}_i$, or any other construction which "climbs up the universe hierarchy". An example would be the sequence $$A_0 = \mathcal{U}_{0},$$

$$A_{n+1} = A_n \to \mathcal{U}_0.$$

Luckily, one rarely feels the temptation to think of such sequences. But more importantly, proof assistants handle universe polymorphism and ambiguity very well, so we actually do not have to worry about them in practice.

-
It appears to me that when one is doing sophisticated things with category theory, one must be prepared to climb up the universe hierarchy. For instance, the quasicategory of small quasicategories in a universe is going to be a simplicial set in the next universe, so we would have to juggle the Joyal model structure on large simplicial sets with the Joyal model structure on small simplicial sets. It seems crucial that not only the same theorems be proved about all things (universe polymorphism) but also that we get nice embeddings of each thing into their respective enlargement. – Zhen Lin May 14 '13 at 8:33
The nice embedding is guaranteed by universe cummulativity. By the way, the entire Coq standard library fits into three or four universes. – Andrej Bauer May 14 '13 at 8:47
Do these universes have to be universes in the full sense of the word, or just a chain of models [of set theory] that we can distinguish between? – Asaf Karagila May 14 '13 at 15:08
@Andrej, I've spent almost half an hour trying to prove that your sequence of nested jokes converges to a whole joke, and still can't figure out how this could be true. Are you sure that your sentence is really a joke? :-) – Michal R. Przybylek May 14 '13 at 23:20
@Asaf: the notion of a universe in type theory is quite flexible. It's good if the universe is closed under many operations, perhaps so many that it forms a small model of type theory, but it doesn't have to. Actually, I am not sure what you're getting at. What does "distinguish between them" mean? – Andrej Bauer May 15 '13 at 5:17

One thing that a universe $U$ gives you is that the sets and function in it form an internal full subcategory $USet$ of your ambient category $Set$ of sets . The idea is that the collection of objects forms a set, hence an object of $Set$. Then the collection of functions in $U$ from $X$ to $Y$, say, forms a set $USet(X,Y)$. However, the 'fullness' condition is that we can consider $X$ and $Y$ themselves as objects of $Set$, by considering the sets of their elements, $\underline{X} := USet(1,X)$ and $\underline{Y} := USet(1,Y)$ respectively, and then the set of functions $Set(\underline{X},\underline{Y})$ is the same as the set of functions $USet(X,Y)$ (isomorphic, not equal, generally). This is what Zhen refers to when he mentions hom-sets are preserved.

Notice here that $X$ and $Y$ are not sets, rather they are functions $1 \to Obj(USet)$, and to see them as sets we have to externalise them (note that for a category theorist, functions aren't necessarily sets).

For category theorists: a universe gives you a logical, full sub-fibred-topos of the fibred topos $cod\colon Set^\mathbf{2} \to Set$, and this definition extends to any topos $E$ replacing $Set$. This is a much nicer (from a category-theoretical perspective), and purely category-theoretic definition of a universe, independent of how one defines the category of sets. To consider only a model of set theory, one would take a model of the geometric theory 'well-pointed topos with AC and NNO' in $Set$, or worse (:-P) an internal relation modelling $\in$ from ZFC. You would have no control on the hom-sets of such a thing, and there would be no relation between 'internal' truth and 'external' truth.

-
A universe in the sense of Grothendieck et al. satisfies a second-order replacement axiom. How do we guarantee this using the fibred topos language? – Zhen Lin May 14 '13 at 8:24
Actually, I should say that a universe in a topos is an internal category which is a topos, and whose externalisation is a logical full subtopos of the codomain topos (as fibred toposes). So I imagine that the internal logic of the ambient topos, which is higher order, can give you this. I meant to link to the nlab page ncatlab.org/nlab/show/universe+in+a+topos, where this can probably be seen rather more easily. – David Roberts May 15 '13 at 0:29
Yes, that definition is much closer to that of a Grothendieck universe. – Zhen Lin May 15 '13 at 9:19

First of all, most people would be rather unhappy with a chain like yours of countable models of ZFC. You can do mathematics in these countable models, but it is still mind bending. An inaccessible certainly has the advantage that all of normal mathematics happens below this cardinal. A proper class of inaccessibles means that you can do whatever you want, in the full universe of sets, and then you can still capture everything (assuming you did not use actual proper classes) in a set model of ZFC.

Btw., recall that one of the largest cardinal notions that has been looked at is Vopenka's principle, which has a natural formulation in terms of categories, even though this statement is of a very different nature compared to the existence of Grothendieck universe and such.

-
Well, if you work within the first model, then your categories are elements of the second model, and so on and so forth. As I remarked in the final paragraph, it's more than reasonable that large cardinals just simplify things; but can we get away with that much less? And in this breath, let me point out that the distance between a proper class of inaccessible, and Vopenka's principle is quite the huge gap in strength, and philosophically much more than the gap between the sequence of models and universes. – Asaf Karagila May 14 '13 at 6:52
As a practising categorist, let me emphasise how mind-bending it is to work in an arbitrary chain of models: when I think about expanding the universe, I don't expect cardinals to suddenly collapse together, or for sets to gain new subsets, or any of the other things that set theorists are used to! Rather, my basic minimum criterion is that hom-sets are preserved, and that implies there are no new functions and no new subsets. – Zhen Lin May 14 '13 at 7:21
Zhen Lin, one can require that the models are end-extensions (which is equiconsistent with the chain of models, I believe, if we take them all to satisfy $V=L$ as well, for example). Would that put your mind at ease? – Asaf Karagila May 14 '13 at 7:44
Asaf, can you say more precisly what you mean by end-extension? Even if your models are, say, countable $L_{\alpha}$'s, $\omega$ is still getting more subsets as you go up the chain. If you want a chain of $L_\alpha$'s where this does not happen, you want them to be closed under taking constructible subsets of elements. But then maybe you also want the $\alpha$'s to be regular so that you don't get new cofinal maps later on. And voila, here is your inaccessible cardinal (in $L$, at least). – Stefan Geschke May 14 '13 at 9:44
Perhaps, if all you are doing is really just bookkeeping. But for other purposes (e.g. the one considered in my preprint) it is absolutely crucial that no new functions be added. – Zhen Lin May 14 '13 at 17:17