Background
Basic concepts
equivalences in/of -categories
Universal constructions
Local presentation
Theorems
Extra stuff, structure, properties
Models
(2,1)-quasitopos?
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):
Recall that sheaf toposes are equivalently the left exact reflective subcategories of presheaf toposes and that the inclusion functor is necessarily an accessible functor. This characterization has the following immediate generalization to a definition in (∞,1)-category theory, where the only subtlety is that accessibility needs to be explicitly required:
A Grothendieck–Rezk–Lurie -topos is an accessible left exact reflective sub-(∞,1)-category of an (∞,1)-category of (∞,1)-presheaves
If the above localization is a topological localization then is an (∞,1)-category of (∞,1)-sheaves.
Equivalently:
(Giraud-Rezk-Lurie axioms)
An -topos is
an (∞,1)-category that satisfies the -category-theoretic analogs of Giraud's axioms:
is presentable;
coproducts in are disjoint;
every groupoid object in is effective (i.e. has a delooping).
This is part of the statement of HTT, theorem 6.1.0.6.
This is derived from the following equivalent one:
An object classifier is a (small) self-reflection of the -topos inside itself (type of types, internal universe). See also (WdL, book 2, section 1).
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.
for the moment see
for the moment see
The Cartesian cubical model of cubical type theory and homotopy type theory is conjectured to be an (∞,1)-topos not equivalent to (∞,1)-groupoids.
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
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
In fact, this is unique, up to equivalence: Since every -groupoid is an -colimit (namely over itself, by this Prop.) of the point (hence of the terminal object), and since the inverse image -functor needs to preserve these -colimits (being a left adjoint) as well as the point (being a lex functor).
Every -topos is a cartesian closed (∞,1)-category.
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
We discuss how the powering of -toposes over is given by forming mapping stacks out of locally constant -stacks. All of the following formulas and their proofs hold verbatim also for Grothendieck toposes, as they just use general abstract properties.
Let be an -topos
with terminal geometric morphism denoted
where the inverse image constructs locally constant -stacks,
and with its internal hom (mapping stack) adjunction denoted
for .
Notice that this construction is also -functorial in the first argument: is the morphism which under the -Yoneda lemma over (which is large but locally small, so that the lemma does apply) corresponds to
By definition, for any and the powering] is the (∞,1)-limit over the diagram constant on
while the tensoring is the (∞,1)-colimit over the diagram constant on
Under Isbell duality, the powering operations on homotopy types corresponds to higher order Hochschild cohomology of suitable algebras of functions on , as discussed there.
The powering of over is given by the mapping stack out of the locally constant -stacks:
in that this operation has the following properties:
For all and we have a natural equivalence
In its first argument the operation
sends the terminal object (the point) to the identity:
where all equivalences shown are natural.
For the first statement to be proven, consider the following sequence of natural equivalences:
For the second statement, recall that hom-functors preserve limits in that there are natural equivalences of the form
and that -toposes have universal colimits, in particular that the product operation is a left adjoint (2) and hence preserves colimits:
With this, we get the following sequences of natural equivalences:
This implies (4) by the -Yoneda lemma over (which is large but locally small, so that the lemma does apply).
Finally (3) is immediate from the fact that preserves the terminal object, by definition:
For an -topos and an object, the slice-(∞,1)-category is itself an -topos – an over-(∞,1)-topos. The projection part of an essential geometric morphism
This is HTT, prop. 6.3.5.1.
The -topos could be called the gros topos of . A geometric morphism that factors as is called an etale geometric morphism.
-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
should be.
flavors of higher toposes
Locally presentable categories: Cocomplete possibly-large categories generated under filtered colimits by small generators under small relations. Equivalently, accessible reflective localizations of free cocompletions. Accessible categories omit the cocompleteness requirement; toposes add the requirement of a left exact localization.
In retrospect, at least the homotopy categories of (∞,1)-toposes have been known since
presented there via categories of fibrant objects among simplicial presheaves. The enhancement of this to model categories of simplicial presheaves originates wit:h
André Joyal, Letter to Alexander Grothendieck, 11. 4. 1984, (pdf scan).
John F. Jardine, Simplicial presheaves, Journal of Pure and Applied Algebra 47 (1987), 35-87 (pdf)
A more intrinsic characterization of these “model toposes” (Rezk 2010) as -toposes (the term seems to first appear here in Simpson 1999) is due to:
The generalization of these model toposes from 1-sites to simplicial model sites is due to
The term -topos is due to
The term model topos was later coined in:
A comprehensive conceptualization and discussion of (∞,1)-toposes is then due to
building on Rezk 2010. 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.
Overview:
Denis-Charles Cisinski, Catégories supérieures et théorie des topos, Séminaire Bourbaki, 21.3.2015, pdf.
Charles Rezk, Lectures on Higher Topos Theory, Leeds (2019) [pdf, pdf]
A useful collection of facts of simplicial homotopy theory and (infinity,1)-topos theory is in
A quick introduction to the topic is in
On -toposes internal to other -toposes;
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
Proof that all ∞-stack (∞,1)-topos have presentations by model categories which interpret (provide categorical semantics) for homotopy type theory with univalent type universes:
Last revised on October 31, 2023 at 16:37:14. See the history of this page for a list of all contributions to it.