(∞,1)-category of (∞,1)-sheaves
Extra stuff, structure and property
locally n-connected (n,1)-topos
locally ∞-connected (∞,1)-topos, ∞-connected (∞,1)-topos
structures in a cohesive (∞,1)-topos
Fix a Grothendieck universe and a smaller universe . Let be the reference-universe, so that sets in are called small sets, sets in are called large, and sets not necessarily in are called very large.
Write ∞Grpd for the (large) (∞,1)-category of small ∞-groupoids and for the very-large -category of large -groupoids.
Then the general procedures of universe enlargement can be applied to any large -category to produce a very-large one. Specifically, we have the locally presentable enlargement: for a large (∞,1)-category with small (∞,1)-colimits, write
for the full sub-(∞,1)-category of the (∞,1)-category of (∞,1)-functors that preserves small (∞,1)-limits. As described at universe enlargement, if is locally presentable, then can be identified with the naive enlargement, which consists of the large models of the “theory” of which consists of the small models.
In particular, when is an (∞,1)-sheaf (∞,1)-topos of small (∞,1)-sheaves, then can be identified with a (∞,1)-category of large (∞,1)-sheaves on the same site. (That is, with a suitable accessible left-exact-reflective subcategory of rather than —it is not yet known how to specify such a reflective subcategory purely in terms of data on .) Thus, we refer to as the very large -sheaf -topos on .
Note that since every topos can be identified with the category of sheaves on itself for the canonical topology, it is also reasonable to denote by . can also also be identified with the category of ind-objects of , for a suitable regular cardinal (namely, the cardinal of ).
For every -topos there is an (∞,1)-functor
that preserves large (∞,1)-colimits and finite (∞,1)-limits. It is defined by sending to the composite
This is HTT, lemma 188.8.131.52.
This is discussed in section 6.3 of
The definition of is in Notation 184.108.40.206 and Remark 220.127.116.11. The relation to ind-objects appears as remark 18.104.22.168.