nLab universe enlargement

Contents

Contents

Idea

Let U\mathbf{U} and V\mathbf{V} be set-theoretic universes (such as Grothendieck universes or universes in an ambient topos) with V\mathbf{V} “bigger than” U\mathbf{U}, and let CC be a category “in the world of U\mathbf{U},” i.e. whose objects are U\mathbf{U}-small and which itself is U\mathbf{U}-large. Its universe enlargement is supposed to be a category “in the world of V\mathbf{V}” which is “the same” or at least similar to CC, and perhaps better behaved.

Notation

An enlargement of a specific category, such as Set, Cat, Grp, or Top, is often denoted by writing its name in all capitals: SET, CAT, GRP, TOP.

As a notation for the operation on a general category CC, the notation C\Uparrow C has been proposed.

Definitions

Since the enlargement is not well-specified by the above intuitive description, there are several different definitions, which are often equivalent but not always.

Henceforth we fix two universes U\mathbf{U} and V\mathbf{V} with UV\mathbf{U}\in \mathbf{V}. We will refer to sets in U\mathbf{U} as small, sets in V\mathbf{V} as large, and sets not necessarily in V\mathbf{V} (or in the next larger universe W\mathbf{W}) as very large.

Models of a theory

If CC is the category of small models of some theory, then we can take C\Uparrow C to be the category of large models of the same theory. For instance:

  • the large category Set of small sets is the category of small models of the theory with one sort and no operations or relations. The category of large models of this theory is just the very large category SETSET of large sets.

  • Similarly, from categories such as Grp, Cat, and Top of small groups, categories, and topological spaces, we obtain the categories GRPGRP, CATCAT, and TOPTOP of large groups, categories, and topological spaces.

Note that the theory could be algebraic, as for GrpGrp, or essentially algebraic, as for CatCat, or even higher-order, as for TopTop. We will refer to this as the logical enlargement. In practice, this enlargement usually suffices, but for theoretical reasons it would be nice to have a construction which works on any large category.

Locally presentable enlargement

For any large category CC, the very large presheaf category [C op,SET][C^{op},SET] contains CC as a full subcategory. Furthermore, [C op,SET][C^{op},SET] is SETSET-bicomplete, i.e. it has all large limits and colimits, whether or not CC was SetSet-complete or cocomplete, and the Yoneda embedding C[C op,SET]C \hookrightarrow [C^{op},SET] preserves all limits that exist in CC.

However, it hardly preserves any colimits (since it is a free cocompletion, after all). If we want an enlargement of CC which preserves some class Φ\Phi of colimits in CC, then we can restrict to the full subcategory of [C op,SET][C^{op},SET] consisting of the presheaves C opSETC^{op}\to SET which preserved limit the colimits Φ\Phi (i.e. take them to limits in SETSET). Let’s denote this category by ΦC\Uparrow_\Phi C. Since representable functors preserve all limits, the Yoneda embedding of CC factors through ΦC\Uparrow_\Phi C, and all the colimits in Φ\Phi are preserved by this restricted embedding.

Moreover, ΦC\Uparrow_\Phi C is closed under limits in [C op,SET][C^{op},SET], so it is itself SETSET-complete. And as long as the (diagrams sizes of the) colimits in Φ\Phi are at most large, then (by theorems of Day etc.) ΦC\Uparrow_\Phi C is reflective in [C op,SET][C^{op},SET], and hence also SETSET-cocomplete. Since usually, the only colimits we might care about in a large category CC are small, a natural choice for Φ\Phi is the class of all small colimits existing in CC.

We will refer to this ΦC\Uparrow_\Phi C as the locally presentable enlargement, since it is a locally presentable category relative to V\mathbf{V}. (In fact, it is locally κ\kappa-presentable, where κ\kappa is the cardinality of the first universe U\mathbf{U}.) Moreover, we have the following (where λCts(A,B)\lambda Cts(A,B) denotes the category of λ\lambda-small-limit preserving functors).

Theorem

Suppose CC is locally presentable relative to U\mathbf{U}, so that there is a small cardinal λ\lambda and a small category AA with λ\lambda-small colimits such that CλCts(A op,Set)C\simeq \lambda Cts(A^{op},Set). If Φ\Phi denotes the class of all small colimits in CC, then ΦCλCts(A op,SET)\Uparrow_\Phi C \simeq \lambda Cts(A^{op},SET).

Note that in this case, λCts(A op,SET)\lambda Cts(A^{op},SET) is the category of large models of the theory (namely A opA^{op}) of which CC is the category of small ones. Thus, the theorem says that when CC is locally presentable, the locally presentable enlargement is the same as the logical one.

Proof

Write CλCts(A op,SET)C' \coloneqq \lambda Cts(A^{op},SET). Then we have a full embedding CCC\hookrightarrow C', which preserves limits and colimits since they are calculated in the same way in both categories.

Now every object of CC is a small colimit of objects of AA, and the objects of AA are all λ\lambda-presentable in CC and in CC'. Thus, every object of CC is κ\kappa-presentable in CC', where κ\kappa is the size of the universe U\mathbf{U}. Conversely, since CC' is locally λ\lambda-presentable (relative to V\mathbf{V}), any κ\kappa-presentable object in it is a κ\kappa-small colimit of λ\lambda-presentable objects—so since CC is closed under small colimits in CC', it must consist exactly of the κ\kappa-presentable objects. However, since CC' is locally λ\lambda-presentable, it is also locally κ\kappa-presentable, so this implies that CκCts(C op,SET)C' \simeq \kappa Cts(C^{op},SET). But κCts(C op,SET)\kappa Cts(C^{op},SET) is precisely ΦC\Uparrow_\Phi C.

However, if CC is not locally presentable, then its logical and locally-presentable enlargements can disagree. In fact, they will usually disagree in this case, since if CC is not locally presentable relative to U\mathbf{U}, its logical enlargement will usually not be locally presentable relative to V\mathbf{V} either, whereas its locally-presentable enlargement is, by definition, locally presentable relative to V\mathbf{V}. For example, the logical and locally presentable enlargements of TopTop are quite different.

Accessible enlargement

There is a simple modification of the locally-presentable enlargement which makes it agree with the logical enlargement for all accessible categories, not just locally presentable ones. Namely, instead of κCts(C op,SET)\kappa Cts(C^{op},SET), we consider κFlat(C op,SET)\kappa Flat(C^{op},SET), the category of κ\kappa-flat functors (functors that “would preserve all κ\kappa-small limits if they existed”). We call this the accessible enlargement.

Essentially the same proof as for the theorem above shows that if CC is accessible relative to U\mathbf{U}, hence CλFlat(A op,Set)C\simeq \lambda Flat(A^{op},Set), then the accessible enlargement is equivalent to λFlat(A op,SET)\lambda Flat(A^{op},SET), which is of course the logical enlargement.

Note that if CC has all small limits, then its accessible and locally-presentable enlargements are the same, since a functor defined on a category with κ\kappa-small limits is κ\kappa-continuous iff it is κ\kappa-flat. However, if CC does not have small limits, then its locally-presentable enlargement does have all large limits, whereas its accessible enlargement does not.

Thus, when CC is “poorly behaved,” its accessible enlargement is “closer to it” (in particular, identical to its logical enlargement if CC is accessible) and thus equally poorly behaved, whereas its locally-presentable enlargement is further from it, but better behaved (complete and cocomplete). For some purposes one may want one of these behaviors; for other purposes one may want the other.

Monoidal enlargements

One may further ask for an enlargement which inherits whatever additional structure CC has, such as monoidal structure. The logical enlargement will usually inherit such structure trivially, while the Day convolution theorem implies that when CC is monoidal, so is its locally-presentable enlargement—and moreover, the latter is closed even if CC is not!

Examples

References

Last revised on January 11, 2015 at 14:23:02. See the history of this page for a list of all contributions to it.