(∞,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
Classes of bundles
Examples and Applications
For an (∞,1)-topos and any object, the over-(∞,1)-category is itself an -topos: the over--topos .
If we think of as a big topos, then for we may think of (∞,1)-topos as the little topos-incarnation of . The objects of we may think of as (∞,1)-sheaves on .
This correspondence between objects of and their little-topos incarnation is entirly natural: is equivalently recovered as the (∞,1)-category whose objects are over--toposes and whose morphisms are (∞,1)-geometric morphisms over .
For an (∞,1)-topos and an object also the over-(∞,1)-category is an -topos. This is the over--topos of over .
This is HTT, prop 220.127.116.11 1).
Base change to the point
There is a canonical (∞,1)-geometric morphism
where the extra left adjoint is the obvious projection , and is given by forming the (∞,1)-product with .
This is called an etale geometric morphism. See there for more details.
If is a locally ∞-connected (∞,1)-topos then for all also the over--topos is locally -connected.
The composite of (∞,1)-geometric morphisms
is itself a geometric morphism. Since ∞Grpd is the terminal object in (∞,1)Topos this must be the global section geometric morphism for . Since it has the extra left adjoint it is locally -connected.
Let be the full sub-(∞,1)-category on the etale geometric morphisms . Then there is an equivalence
See etale geometric morphism for more details.
General base change
See base change geometric morphism.
As -sheaves on the big -site of an object
We spell out how is the (∞,1)-category of (∞,1)-sheaves over the big site of .
This appears as HTT, 18.104.22.168. For more on this see (∞,1)-category of (∞,1)-presheaves.
By the discussion of adjoint (∞,1)-functors on over-(∞,1)-categories adjoint (∞,1)-functors we have that the adjunction
passes to an adjunction on the over-(∞,1)-categories
(where we are using that by the assumption that the coverage is subcanonical, so that the representable is a (∞,1)-sheaf), such that is still a full and faithful (∞,1)-functor (where we are using that the unit is an equivalence, since is a sheaf).
Since moreover the (∞,1)-limits in are computed as limits in over diagrams with a bottom element adjoined (as discussed at limits in over-(∞,1)-categories) it follows that with preserving all finite limits, so does .
In summary we have that is a reflective sub-(∞,1)-category of hence is the (∞,1)-category of (∞,1)-sheaves on the category for some (∞,1)-site-structure. But since inverts precisely those morphisms that are inverted by under the projection , it follows that this is the big site structure on (this is the defining property of the big site).
Specifically for the -topos ∞Grpd we also have the following characterization.
For ∞Grpd we have that for any ∞-groupoid the corresponding over--topos is equivalent to the (∞,1)-category of (∞,1)-presheaves on :
The following proposotion asserts that the over--topos over an -truncated object indeed behaves like a generalized n-groupoid
For and an n-localic (∞,1)-topos, then the over--topos is -localic precisely if the object is -truncated.
This is (StrSp, lemma 2.3.16).
If is an object classifier for -small objects, then the projection regarded as an object in the slice is a -small object classifier in .
In homotopy type theory
If a homotopy type theory is the internal language of , then then theory in context is the internal language of .
The general notion is discussed in section 6.3.5 of
Some related remarks are in