Formalising Statements in Category Theory with Regards to Universes (with an example of the end of a functor)

I am currently in the process of changing the way I think about category theory, by adopting the notion of Grothendiek universe and trying not to think of proper classes.

Think of a statement such as

If $\mathcal C$ and $\mathcal D$ are categories, and $F,G \colon \mathcal C \to \mathcal D$ are functors, then $$\int_{c \colon \mathcal C} \mathcal D(Fc, Gc) = \mathrm{Nat}(F,G).$$

This doesn't make much sense as written, since depending on the foundations you use there are potentially size problems and $\mathsf{Set}$ might not recive the functor $\mathcal D(F-,G-)$.

Suppose that we are using MacLane's foundations of set theory, so that $\mathrm{Nat}(F,G)$ is a set, and the objects of a category form a set, as do all the arrows. Let $\mathrm{Set}[U]$ be the category of sets whose object set is the universe $U$. Is the following an appropriate formalisation of the above statement?

Let $\mathcal C$ and $\mathcal D$ be categories, and let $F,G \colon \mathcal C \to \mathcal D$ be functors. Let $U$ be a Grothendiek universe such that $\mathsf{Set}[U]$ receives each functor $\mathcal D (F-, G-)$ and $U$ contains $\mathrm{Nat}(F,G)$. Then $\mathrm{Nat} (F,G)$ is the end of $\mathcal{D}(F-,G-).$

Have I got the right end of the stick? Is that even true?

Does $U$ necessarily have to be a universe for the above to be true?

Also if given a universe $U$, and a bigger one $U'$, is it true that the inclusion $\mathsf{Set}[U] \hookrightarrow \mathsf{Set}[U']$ will always preserve limits? Would it at least always preserve ends?

-

1 Answer

Let's quickly review the proof of the claim. Suppose we had a small set $X$ equipped with an extranatural transformation to $\mathcal{D}(F(-), G(-))$. That means, for each object $c$ in $\mathcal{C}$, we have an $X$-indexed family of morphisms $F c \to G c$, such that for every morphism $f : c \to c'$ in $\mathcal{C}$, the square below commutes: $$\begin{array}{ccc} F c & \rightarrow & G c \\ \downarrow & & \downarrow \\ F c' & \rightarrow & G c' \end{array}$$ But by definition this is nothing more than an $X$-indexed family of natural transformations, so $$\textrm{Nat}(F, G) \cong \int_{c : \mathcal{C}} \mathcal{D}(F c, G c)$$ as claimed.

What did we use in the above argument? Not much at all. We only needed to know that $\textrm{Nat}(F, G)$ is in the universe, and that all maps $X \to \textrm{Nat}(F, G)$ as well as all maps $\textrm{Nat}(F, G) \to \mathcal{D}(F c, G c')$ are in the universe. In other words, the calculation is valid in any full subcategory of $\textbf{SET}$ containing the above-mentioned sets – it doesn't have to be a subcategory of the form $\textbf{Set}[U]$ for some Grothendieck universe $U$.

More generally, if $\mathcal{S}'$ is a full subcategory of $\mathcal{S}$, then the inclusion $\mathcal{S}' \hookrightarrow \mathcal{S}$ reflects all limits and colimits. The question of preservation is much more subtle. For inclusions of the form $\textbf{Set}[U] \hookrightarrow \textbf{Set}[U']$ where $U = V_{\alpha}$ and $U' = V_{\alpha'}$ for some non-zero limit ordinals $\alpha$ and $\alpha'$, we can say this much:

• Equalisers/coequalisers of all parallel pairs exist in $\textbf{Set}[U]$ and are preserved.

• All finite products/coproducts exist in $\textbf{Set}[U]$ and are preserved.

• In particular, all finite limits exist in $\textbf{Set}[U]$ and are preserved.

• Let $(X_i : i \in I)$ be a family of sets, with $I \in U$ and each $X_i \in U$. If there is a set $X$ in $U$ with the cardinality of the disjoint union $\coprod_{i \in I} X_i$ (which is not a priori a coproduct!) then the product and the coproduct of $(X_i : i \in I)$ exists in $\textbf{Set}[U]$ (but only up to bijection), and they are preserved.

• If $p : X \to I$ is a map in $\textbf{Set}[U]$ and $X_i = p^{-1} \{ i \}$, then the disjoint union $\coprod_{i \in I} X_i$ exists in $U$ (and is isomorphic to $X$), and the product and coproduct of $(X_i : i \in I)$ can be constructed in the usual way.

These claims rely crucially on the explicit construction of products / coproducts / equalisers / coequalisers in $\textbf{SET}$. We can't make any promises about existence or preservation of limits and colimits over infinite diagrams in general, but if $U$ is a Grothendieck universe, then we can say this: $\textbf{Set}[U]$ has limits and colimits for all $U$-small diagrams and these are preserved. In particular, $\textbf{Set}[U]$ has ends and coends for all bifunctors indexed by $U$-small categories, and these are also preserved.

-