(in category theory/type theory/computer science)
of all homotopy types
of (-1)-truncated types/h-propositions
Let and be set-theoretic universes (such as Grothendieck universes or universes in an ambient topos) with “bigger than” , and let be a category “in the world of ,” i.e. whose objects are -small and which itself is -large. Its universe enlargement is supposed to be a category “in the world of ” which is “the same” or at least similar to , and perhaps better behaved.
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 , the notation has been proposed.
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 and with . We will refer to sets in as small, sets in as large, and sets not necessarily in (or in the next larger universe ) as very large.
If is the category of small models of some theory, then we can take 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 of large sets.
Similarly, from categories such as Grp, Cat, and Top of small groups, categories, and topological spaces, we obtain the categories , , and of large groups, categories, and topological spaces.
Note that the theory could be algebraic, as for , or essentially algebraic, as for , or even higher-order, as for . 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.
For any large category , the very large presheaf category contains as a full subcategory. Furthermore, is -bicomplete, i.e. it has all large limits and colimits, whether or not was -complete or cocomplete, and the Yoneda embedding preserves all limits that exist in .
However, it hardly preserves any colimits (since it is a free cocompletion, after all). If we want an enlargement of which preserves some class of colimits in , then we can restrict to the full subcategory of consisting of the presheaves which preserved limit the colimits (i.e. take them to limits in ). Let’s denote this category by . Since representable functors preserve all limits, the Yoneda embedding of factors through , and all the colimits in are preserved by this restricted embedding.
Moreover, is closed under limits in , so it is itself -complete. And as long as the (diagrams sizes of the) colimits in are at most large, then (by theorems of Day etc.) is reflective in , and hence also -cocomplete. Since usually, the only colimits we might care about in a large category are small, a natural choice for is the class of all small colimits existing in .
We will refer to this as the locally presentable enlargement, since it is a locally presentable category relative to . (In fact, it is locally -presentable, where is the cardinality of the first universe .) Moreover, we have the following (where denotes the category of -small-limit preserving functors).
Suppose is locally presentable relative to , so that there is a small cardinal and a small category with -small colimits such that . If denotes the class of all small colimits in , then .
Note that in this case, is the category of large models of the theory (namely ) of which is the category of small ones. Thus, the theorem says that when is locally presentable, the locally presentable enlargement is the same as the logical one.
Write . Then we have a full embedding , which preserves limits and colimits since they are calculated in the same way in both categories.
Now every object of is a small colimit of objects of , and the objects of are all -presentable in and in . Thus, every object of is -presentable in , where is the size of the universe . Conversely, since is locally -presentable (relative to ), any -presentable object in it is a -small colimit of -presentable objects—so since is closed under small colimits in , it must consist exactly of the -presentable objects. However, since is locally -presentable, it is also locally -presentable, so this implies that . But is precisely .
However, if is not locally presentable, then its logical and locally-presentable enlargements can disagree. In fact, they will usually disagree in this case, since if is not locally presentable relative to , its logical enlargement will usually not be locally presentable relative to either, whereas its locally-presentable enlargement is, by definition, locally presentable relative to . For example, the logical and locally presentable enlargements of are quite different.
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 , we consider , the category of -flat functors (functors that “would preserve all -small limits if they existed”). We call this the accessible enlargement.
Essentially the same proof as for the theorem above shows that if is accessible relative to , hence , then the accessible enlargement is equivalent to , which is of course the logical enlargement.
Note that if has all small limits, then its accessible and locally-presentable enlargements are the same, since a functor defined on a category with -small limits is -continuous iff it is -flat. However, if does not have small limits, then its locally-presentable enlargement does have all large limits, whereas its accessible enlargement does not.
Thus, when is “poorly behaved,” its accessible enlargement is “closer to it” (in particular, identical to its logical enlargement if 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.
One may further ask for an enlargement which inherits whatever additional structure has, such as monoidal structure. The logical enlargement will usually inherit such structure trivially, while the Day convolution theorem implies that when is monoidal, so is its locally-presentable enlargement—and moreover, the latter is closed even if is not!
Sections 2.6 and 3.11–3.12 of Basic Concepts of Enriched Category.
Last revised on January 11, 2015 at 14:23:02. See the history of this page for a list of all contributions to it.