(∞,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
Recall the following familiar 1-categorical statement:
The idea of -toposes is to generalize the above situation from to (recall the notion of (n,r)-category and see the general discussion at ∞-topos):
- Working in the (∞,1)-category ∞Grpd of (∞,0)-categories amounts to doing homotopy theory. The point of (∞,1)-sheaves is to pass to parameterized (∞,0)-categories, namely (∞,1)-presheaf categories. Although these (∞,1)-topoi behave much like the -topos ∞Grpd, their objects are generalized spaces with higher homotopies that may carry more structure. For instance, an ∞-Lie groupoid is an (∞,1)-sheaf on CartSp.
As a geometric embedding into a -presheaf category
A Grothendieck–Rezk–Lurie -topos is an accesible left exact reflective sub-(∞,1)-category of an (∞,1)-category of (∞,1)-presheaves
If the localization in is a topological localization then is an (∞,1)-category of (∞,1)-sheaves.
By Giraud-Rezk-Lurie axioms
This is part of the statement of HTT, theorm 188.8.131.52.
This is derived from the following equivalent one:
A further equivalent one (essentially by an invocation of the adjoint functor theorem) is:
A morphism between -toposes is an (∞,1)-geometric morphism.
The (∞,1)-category of all -topos is (∞,1)Toposes.
Types of -toposes
Topological localizations / -sheaf toposes
for the moment see
for the moment see
Another main theorem about -toposes is that models for ∞-stack (∞,1)-toposes are given by the model structure on simplicial presheaves. See there for details
Global sections geometric morphism
Every ∞-stack -topos has a canonical (∞,1)-geometric morphism to the terminal -stack -topos ∞Grpd: the direct image is the global sections (∞,1)-functor , the inverse image is the constant ∞-stack functor
Powering and copowering over – Hochschild homology
Being a locally presentable (∞,1)-category, an -topos is powered and copowered over ∞Grpd, as described at (∞,1)-tensoring.
For any and the powering is the (∞,1)-limit over the diagram constant on
and the -copowering is is the (∞,1)-colimit over the diagram constant on
Under Isbell duality the powering operation corresponds to higher order Hochschild cohomology in , as discussed there.
Below we discuss that the powering is equivalently given by the internal hom (mapping stack) out of the constant ∞-stack on :
Closed monoidal structure
By the fact that every -topos has universal colimits it follows that for every object the (∞,1)-functor
preserves all (∞,1)-colimits. Since every -topos is a locally presentable (∞,1)-category it follows with the adjoint (∞,1)-functor theorem that there is a right adjoint (∞,1)-functor
For an (∞,1)-site for we have that the internal hom (mapping stack) is given on by the (∞,1)-sheaf
where is the (∞,1)-Yoneda embedding and denotes ∞-stackification.
The argument is entirely analogous to that of the closed monoidal structure on sheaves.
We use the full and faithful geometric embedding and the (∞,1)-Yoneda lemma to find for all the value
and then the fact that ∞-stackification is left adjoint to inclusion to get
Then the defining adjunction gives
Finite colimits may be taken out of the internal hom: For a finite -category and a diagram, we have for all
By the above proposition we have
By universal colimits in this is
Using the fact that the hom-functor sends colimits in the first argument to limits this is
By the internal hom adjunction and Yoneda this is
Since (∞,1)-limits in the (∞,1)-category of (∞,1)-presheaves are computed objectwise, this is
Finally, because is a left exact (∞,1)-functor this is also the (∞,1)-limit in .
By the above we have
As the notation indicates, is precisely : the ∞-stackification of the (∞,1)-presheaf that is literally constant on . Morover is a left exact (∞,1)-functor and hence commutes with (∞,1)-products, so that
By the defining geometric embedding this is
Since limits of (∞,1)-presheaves are taken objectwise, we have in the first argument the tensoring of over
By the defining property of tensoring and cotensoring (or explicitly writing out , taking the colimit out of the hom, thus turning it into a limit and then inserting that back in the second argument) this is
So finally with the (∞,1)-Yoneda lemma we have
For an -topos and an object, the over-(∞,1)-category is itself an -topos – an over-(∞,1)-topos. The projection part of an essential geometric morphism
This is HTT, prop. 184.108.40.206.
The -topos could be called the gros topos of . A geometric morphism that factors as is called an etale geometric morphism.
Syntax in univalent homotopy type theory
-Toposes provide categorical semantics for homotopy type theory with a univalent Tarskian type of types (which inteprets as the object classifier).
For more on this see at
Most of the standard constructions in topos theory have or should have immediate generalizations to the context of -toposes, since all notions of category theory exist for (∞,1)-categories.
For instance there are evident notions of
Moreover, it turns out that -toposes come with plenty of internal structures, more than canonically present in an ordinary topos. Every -topos comes with its intrinsic notion of
and with an intrinsic notion of
In classical topos theory, cohomology and homotopy of a topos are defined in terms of simplicial objects in . If is a sheaf topos with site and enough points, then this classical construction is secretly really a model for the intrinsic cohomology and homotopy in the above sense of the hypercomplete (∞,1)-topos of ∞-stacks on .
The beginning of a list of all the structures that exist intrinsically in a big -topos is at
But -topos theory in the style of an -analog of the Elephant is only barely beginning to be conceived.
There are some indications as to what the
Locally presentable categories: Large categories whose objects arise from small generators under small relations.
|(n,r)-categories…||satisfying Giraud's axioms||inclusion of left exact localizations||generated under colimits from small objects||localization of free cocompletion||generated under filtered colimits from small objects|
|(0,1)-category theory||(0,1)-toposes||algebraic lattices|| Porst’s theorem||subobject lattices in accessible reflective subcategories of presheaf categories|
|category theory||toposes||locally presentable categories|| Adámek-Rosický’s theorem||accessible reflective subcategories of presheaf categories||accessible categories|
|model category theory||model toposes||combinatorial model categories|| Dugger’s theorem||left Bousfield localization of global model structures on simplicial presheaves|
|(∞,1)-topos theory||(∞,1)-toposes||locally presentable (∞,1)-categories|| |
|accessible reflective sub-(∞,1)-categories of (∞,1)-presheaf (∞,1)-categories||accessible (∞,1)-categories|
In retrospect it turns out that the homotopy categories of (∞,1)-toposes have been known since
And the model category theory models have been known since Andre Joyal proposed the model structure on simplicial sheaves in his letter to Alexander Grothendieck.
This work used 1-categorical sites. The generalization to (∞,1)categorical sites – modeled by model sites – was discussed in
and “model topos”-theory was also developed in
The intrinsic category-theoretic definition of an (∞,1)-topos was given in section 6.1 of
building on ideas by Charles Rezk. There is is also proven that the Brown-Joyal-Jardine-Toën-Vezzosi models indeed precisely model -stack -toposes. Details on this relation are at models for ∞-stack (∞,1)-toposes.
An overview is in
A useful collection of facts of simplicial homotopy theory and (infinity,1)-topos theory is in
A discussion of the -universal colimits in terms of model category presentations is due to
More on this with an eye on associated ∞-bundles is in