nLab (infinity,1)-topos

Idea

Recall the following familiar 1-categorical statement:

• Working in the 1-category Set of 0-categories amounts to doing set theory. The point of sheaf toposes is to pass to parameterized 0-categories, namely presheaf categories. Although these topoi behave much like the 1-topos Set, their objects are generalized spaces that may carry more structure. For instance, a (pre)sheaf on Diff is a generalized smooth space.

The idea of $(\infty,1)$-toposes is to generalize the above situation from $1$ to $(\infty,1)$ (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 $(\infty,1)$-topoi behave much like the $(\infty,1)$-topos ∞Grpd, their objects are generalized spaces with higher homotopies that may carry more structure. More generally we have topoi of sheaves, and $(\infty,1)$-topoi of (∞,1)-sheaves. For instance, an ∞-Lie groupoid is an (∞,1)-sheaf on CartSp.

Definition

As a geometric embedding into a $(\infty,1)$-presheaf category

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:

Definition

A Grothendieck–Rezk–Lurie $(\infty,1)$-topos $\mathbf{H}$ is an accessible left exact reflective sub-(∞,1)-category of an (∞,1)-category of (∞,1)-presheaves

$$\mathbf{H} \stackrel{\overset{lex}{\leftarrow}}{\hookrightarrow} PSh_{(\infty,1)}(C) \,.$$

If the above localization is a topological localization then $\mathbf{H}$ is an (∞,1)-category of (∞,1)-sheaves.

By Giraud-Rezk-Lurie axioms

Equivalently:

Proposition

(Giraud-Rezk-Lurie axioms)
An $(\infty,1)$-topos $\mathbf{H}$ is

an (∞,1)-category that satisfies the $(\infty,1)$-category-theoretic analogs of Giraud's axioms:

• $\mathbf{H}$ is presentable;

• (∞,1)-colimits in $\mathbf{H}$ are universal;

• coproducts in $\mathbf{H}$ are disjoint;

• every groupoid object in $\mathbf{H}$ 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:

Proposition

An (∞,1)-topos is

• a presentable (∞,1)-category with universal colimits

• that has object classifiers.

Remark

An object classifier is a (small) self-reflection of the $\infty$-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:

Proposition

An (∞,1)-topos is

• a presentable (∞,1)-category

• in which all colimits are van Kampen colimits.

Morphisms

A morphism between $(\infty,1)$-toposes is an (∞,1)-geometric morphism.

The (∞,1)-category of all $(\infty,1)$-topos is (∞,1)Toposes.

Types of $(\infty,1)$-toposes

Topological localizations / $(\infty,1)$-sheaf toposes

for the moment see

• topological localization

Hypercomplete $(\infty,1)$-toposes

for the moment see

• hypercomplete (∞,1)-topos

Cubical type theory

The Cartesian cubical model of cubical type theory and homotopy type theory is conjectured to be an (∞,1)-topos not equivalent to (∞,1)-groupoids.

Models

Another main theorem about $(\infty,1)$-toposes is that models for ∞-stack (∞,1)-toposes are given by the model structure on simplicial presheaves. See there for details

Properties

Global sections geometric morphism

Every ∞-stack $(\infty,1)$-topos $\mathbf{H}$ has a canonical (∞,1)-geometric morphism to the terminal $\infty$-stack $(\infty,1)$-topos ∞Grpd: the direct image is the global sections (∞,1)-functor $\Gamma$, the inverse image is the constant ∞-stack functor

$$(LConst \dashv \Gamma) \;\colon\; \mathbf{H} \underoverset {\underset{\Gamma}{\longrightarrow}} {\overset{LConst}{\longleftarrow}} {\;\;\; \bot \;\;\;} \infty Grpd \,.$$

In fact, this is unique, up to equivalence: Since every $\infty$-groupoid is an $(\infty,1)$-colimit (namely over itself, by this Prop.) of the point (hence of the terminal object), and since the inverse image $\infty$-functor $LConst$ needs to preserve these $\infty$-colimits (being a left adjoint) as well as the point (being a lex functor).

Closed monoidal structure

Proposition

Every $(\infty,1)$-topos is a cartesian closed (∞,1)-category.

Proof

By the fact that every $(\infty,1)$-topos $\mathbf{H}$ has universal colimits it follows that for every object $X$ the (∞,1)-functor

$$X \times (-) : \mathbf{H} \to \mathbf{H}$$

preserves all (∞,1)-colimits. Since every $(\infty,1)$-topos is a locally presentable (∞,1)-category it follows with the adjoint (∞,1)-functor theorem that there is a right adjoint (∞,1)-functor

$$(X \times (-) \dashv [X,-]) : \mathbf{H} \stackrel{\overset{X \times (-)}{\leftarrow}}{\underset{[X,-]}{\to}} \mathbf{H} \,.$$

Proposition

For $C$ an (∞,1)-site for $\mathbf{H}$ we have that the internal hom (mapping stack) $[X,-]$ is given on $A \in \mathbf{H}$ by the (∞,1)-sheaf

$$[X,A] \,\colon\, U \mapsto \mathbf{H}(X \times L y(U), A) \,,$$

where $y : C \to \mathbf{H}$ is the (∞,1)-Yoneda embedding and $L : PSh_C \to \mathbf{H}$ denotes ∞-stackification.

Proof

The argument is entirely analogous to that of the closed monoidal structure on sheaves.

We use the full and faithful geometric embedding $(L \dashv i) : \mathbf{H} \hookrightarrow PSh_C$ and the (∞,1)-Yoneda lemma to find for all $U \in C$ the value

$$[X,A](U) \simeq PSh_C(y U, [X,A])$$

and then the fact that ∞-stackification $L$ is left adjoint to inclusion to get

$$\cdots \simeq \mathbf{H}(L y(U), [X,A]) \,.$$

Then the defining adjunction $(X \times (-) \dashv [X,-])$ gives

$$\cdots \simeq \mathbf{H}(X \times L y(U) , A) \,.$$

Powering of $\infty$-toposes over $\infty$-groupoids

We discuss how the powering of $\infty$-toposes over $Grpd_\infty$ is given by forming mapping stacks out of locally constant $\infty$-stacks. All of the following formulas and their proogfs hold verbatim also for Grothendieck toposes, as they just use general abstract properties.

Let $\mathbf{H}$ be an $\infty$-topos

• with terminal geometric morphism denoted

  (1)$$\mathbf{H} \underoverset {\underset{\Gamma}{\longrightarrow}} {\overset{LConst}{\longleftarrow}} {\;\;\;\;\bot\;\;\;\;} Grp_\infty \,,$$

  where the inverse image constructs locally constant $\infty$-stacks,

• and with its internal hom (mapping stack) adjunction denoted

  (2)$$\mathbf{H} \underoverset {\underset{Maps(X,-)}{\longrightarrow}} { \overset{ (-) \times X }{\longleftarrow} } {\;\;\;\; \bot \;\;\;\;} \mathbf{H}$$

  for $X \,\in\, \mathbf{H}$.

  Notice that this construction is also $\infty$-functorial in the first argument: $Maps\big( X \xrightarrow{f} Y ,\, A \big)$ is the morphism which under the $\infty$-Yoneda lemma over $\mathbf{H}$ (which is large but locally small, so that the lemma does apply) corresponds to

$$\mathbf{H} \big( (-) ,\, Maps(X,A) \big) \;\simeq\; \mathbf{H} \big( (-) \times X ,\, A \big) \xrightarrow{ \mathbf{H} \big( (-) \times f ,\, A \big) } \mathbf{H} \big( (-) \times Y ,\, A \big) \;\simeq\; \mathbf{H} \big( (-) ,\, Maps(X,A) \big) \,.$$

By definition, for any $S \in Grpd_\infty$ and $X \in \mathbf{H}$ the powering] is the (∞,1)-limit over the diagram constant on $X$

$$X^K \,=\, {\lim_\leftarrow}_K X$$

while the tensoring is the (∞,1)-colimit over the diagram constant on $X$

$$K \cdot X \,=\, {\lim_{\to}}_K X \,.$$

Remark

Under Isbell duality, the powering operations on homotopy types $X$ corresponds to higher order Hochschild cohomology of suitable algebras of functions on $X$, as discussed there.

Proposition

The powering of $\mathbf{H}$ over $Grpd_\infty$ is given by the mapping stack out of the locally constant $\infty$-stacks:

$$\array{ Grpd_\infty^{op} \times \mathbf{H} & \overset{ LConst^{op} \times \mathrm{id} }{\longrightarrow} & \mathbf{H}^{op} \times \mathbf{H} & \overset{Maps(-,-)}{\longrightarrow} & \mathbf{H} }$$

in that this operation has the following properties:

1. For all $X,\,A \,\in\, \mathbf{H}$ and $S \,\in\, Grpd_\infty$ we have a natural equivalence

   $$\mathbf{H} \Big( X ,\, Maps \big( LConst(S) ,\, A \big) \Big) \;\; \simeq \;\; Grpd_\infty \Big( S ,\, \mathbf{H} \big( X ,\, A \big) \Big)$$

2. In its first argument the operation

   1. sends the terminal object (the point) to the identity:

      (3)$$Maps \big( LConst(\ast) ,\, X \big) \;\; \simeq \;\; X$$

   2. sends $\infty$-colimits to $\infty$-limits:

      (4)$$Maps \Big( \underset{ \longrightarrow }{\lim} \, LConst\big(S_\bullet\big) ,\, X \Big) \;\; \simeq \;\; \underset{ \longleftarrow }{\lim} \, Maps \Big( LConst\big(S_\bullet\big) ,\, X \Big) \,,$$

   where all equivalences shown are natural.

Proof

For the first statement to be proven, consider the following sequence of natural equivalences:

$$\begin{array}{lll} \mathbf{H} \Big( X ,\, Maps \big( LConst(S) ,\, A \big) \Big) & \;\simeq\; \mathbf{H} \big( X \times LConst(S) ,\, A \big) & \text{(2)} \\ & \;\simeq\; \mathbf{H} \Big( LConst(S) ,\, Maps \big( X ,\, A \big) \Big) & \text{(2)} \\ & \;\simeq\; Grpd_\infty \Big( S ,\, \Gamma \, Maps \big( X ,\, A \big) \Big) & \text{ (1) } \\ & \;\simeq\; Grpd_\infty \bigg( S ,\, \mathbf{H} \Big( \ast_{\mathbf{H}} ,\, Maps \big( X ,\, A \big) \Big) \bigg) & \text{by}\;\text{<a href="https://ncatlab.org/nlab/show/terminal+geometric+morphism#DirectImageOfTerminalGeometricMoprhismIsHomOutOfTerminalObject">this Prop.</a>} \\ & \;\simeq\; Grpd_\infty \Big( S ,\, \mathbf{H} \big( \ast_{\mathbf{H}} \times X ,\, A \big) \Big) & \text{(2)} \\ & \;\simeq\; Grpd_\infty \Big( S ,\, \mathbf{H} \big( X ,\, A \big) \Big) \end{array}$$

For the second statement, recall that hom-functors preserve limits in that there are natural equivalences of the form

(5)$$\mathbf{H} \Big( \underset{\underset{i}{\longrightarrow}}{\lim} \,, X_i ,\, \underset{\underset{j}{\longleftarrow}}{\lim} \,, A_j \Big) \;\; \simeq \;\; \underset{\underset{i}{\longleftarrow}}{\lim} \, \underset{\underset{j}{\longleftarrow}}{\lim} \, \mathbf{H} \Big( X_i ,\, A_j \Big) \,,$$

and that $\infty$-toposes have universal colimits, in particular that the product operation is a left adjoint (2) and hence preserves colimits:

(6)$$(-) \,\times\, \underset{{\longrightarrow}}{\lim} \, S_\bullet \;\; \simeq \;\; \underset{{\longrightarrow}}{\lim} \, \big( (-) \,\times\, S_\bullet \big) \,.$$

With this, we get the following sequences of natural equivalences:

$$\begin{array}{lll} & \mathbf{H} \bigg( (-) ,\, Maps \Big( \underset{\longrightarrow}{\lim} \, LConst(S_\bullet) ,\, X \Big) \bigg) \\ & \;\simeq\; \mathbf{H} \Big( (-) \times \underset{\longrightarrow}{\lim} \, LConst(S_\bullet) ,\, X \Big) & \text{ (2) } \\ & \;\simeq\; \mathbf{H} \Big( \underset{\longrightarrow}{\lim} \big( (-) \times LConst(S_\bullet) \big) ,\, X \Big) & \text{ (6) } \\ & \;\simeq\; \underset{\longleftarrow}{\lim} \, \mathbf{H} \big( (-) \times LConst(S_\bullet) ,\, X \big) & \text{ (5) } \\ & \;\simeq\; \underset{\longleftarrow}{\lim} \, \mathbf{H} \Big( (-) ,\, Maps \big( LConst(S_\bullet) ,\, X \big) \Big) & \text{ (2) } \\ & \;\simeq\; \mathbf{H} \Big( (-) ,\, \underset{\longleftarrow}{\lim} \, Maps \big( LConst(S_\bullet) ,\, X \big) \Big) & \text{ (5) } \,. \end{array}$$

This implies (4) by the $\infty$-Yoneda lemma over $\mathbf{H}$ (which is large but locally small, so that the lemma does apply).

Finally (3) is immediate from the fact that $LConst$ preserves the terminal object, by definition:

$$Maps \big( LConst(\ast) ,\, X \big) \;\simeq\; Maps \big( \ast_{\mathbf{H}} ,\, X \big) \;\simeq\; X \,.$$

Slice-$(\infty,1)$-toposes

Proposition

For $\mathbf{H}$ an $(\infty,1)$-topos and $X \in \mathbf{H}$ an object, the slice-(∞,1)-category $\mathbf{H}_{/X}$ is itself an $(\infty,1)$-topos – an over-(∞,1)-topos. The projection $\pi_! : \mathbf{H}_{/X} \to \mathbf{H}$ part of an essential geometric morphism

$$\pi : \mathbf{H}_{/X} \stackrel{\overset{\pi_!}{\to}}{\stackrel{\overset{\pi^*}{\leftarrow}}{\underset{\pi_*}{\to}}} \mathbf{H} \,.$$

This is HTT, prop. 6.3.5.1.

The $(\infty,1)$-topos $\mathbf{H}_{/X}$ could be called the gros topos of $X$. A geometric morphism $\mathbf{K} \to \mathbf{H}$ that factors as $\mathbf{K} \xrightarrow{\simeq} \mathbf{H}_{/X} \stackrel{\pi}{\to} \mathbf{H}$ is called an etale geometric morphism.

Syntax in univalent homotopy type theory

$(\infty,1)$-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

• model of type theory in an (infinity,1)-topos

• relation between type theory and category theory – Univalent homotopy type theory and infinity-toposes

$(\infty,1)$-Topos theory

Most of the standard constructions in topos theory have or should have immediate generalizations to the context of $(\infty,1)$-toposes, since all notions of category theory exist for (∞,1)-categories.

For instance there are evident notions of

• geometric morphisms between $(\infty,1)$-toposes, such as the global section geometric morphism to the terminal (∞,1)-sheaf $(\infty,1)$-topos ∞Grpd.

Moreover, it turns out that $(\infty,1)$-toposes come with plenty of internal structures, more than canonically present in an ordinary topos. Every $(\infty,1)$-topos comes with its intrinsic notion of

• cohomology in an (∞,1)-topos

and with an intrinsic notion of

• homotopy in an (∞,1)-topos.

In classical topos theory, cohomology and homotopy of a topos $E$ are defined in terms of simplicial objects in $C$. If $E$ is a sheaf topos with site $C$ 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 $C$.

The beginning of a list of all the structures that exist intrinsically in a big $(\infty,1)$-topos is at

• cohesive (∞,1)-topos.

But $(\infty,1)$-topos theory in the style of an $\infty$-analog of the Elephant is only barely beginning to be conceived.

There are some indications as to what the

• internal logic of an (∞,1)-topos

should be.

Related concepts

• elementary (∞,1)-topos, (∞,1)-pretopos

• model topos

• structured (∞,1)-topos

• compact topos, coherent (∞,1)-topos

• category object in an (∞,1)-topos

flavors of higher toposes

• 1-topos

  • (0,1)-topos

  • (1,1)-topos = topos

  • (2,1)-topos

  • $(n,1)$-topos

  • (∞,1)-topos ($n$-localic)

    $\;\;\;\;$ model topos

• 2-topos

  • (2,2)-topos ($n$-localic)

  • (∞,2)-topos

• $n$-topos

  • $(\infty,n)$-topos

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.

$\phantom{A}$(n,r)-categories$\phantom{A}$	$\phantom{A}$toposes$\phantom{A}$	locally presentable	loc finitely pres	localization theorem	free cocompletion	accessible
(0,1)-category theory	locales	suplattice	algebraic lattices	Porst’s theorem	powerset	poset
category theory	toposes	locally presentable categories	locally finitely presentable categories	Adámek-Rosický‘s theorem	presheaf category	accessible categories
model category theory	model toposes	combinatorial model categories		Dugger's theorem	global model structures on simplicial presheaves	n/a
(∞,1)-category theory	(∞,1)-toposes	locally presentable (∞,1)-categories		Simpson’s theorem	(∞,1)-presheaf (∞,1)-categories	accessible (∞,1)-categories

References

General

In retrospect, at least the homotopy categories of (∞,1)-toposes have been known since

• Kenneth Brown, Abstract homotopy theory and generalized sheaf cohomology, Transactions of the American Mathematical Society, Vol. 186 (1973), 419-458 (jstor:1996573).

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 $\infty$-toposes (the term seems to first appear here in Simpson 1999) is due to:

• Carlos Simpson, A Giraud-type characterization of the simplicial categories associated to closed model categories as $\infty$-pretopoi (arXiv:math/9903167)

The generalization of these model toposes from 1-sites to simplicial model sites is due to

• Bertrand Toën, Gabriele Vezzosi, Homotopical Algebraic Geometry I: Topos theory, Advances in Mathematics 193 2 (2005) 257-372 [arXiv:math.AG/0207028, doi:10.1016/j.aim.2004.05.004]

The term $\infty$-topos is due to

• Jacob Lurie, On $\infty$-Topoi (arXiv:math/0306109)

The term model topos was later coined in:

• Charles Rezk, Toposes and homotopy toposes, 2010 (pdf, pdf)

A comprehensive conceptualization and discussion of (∞,1)-toposes is then due to

• Jacob Lurie, section 6.1 of: Higher Topos Theory, Annals of Mathematics Studies 170, Princeton University Press 2009 (pup:8957, pdf)

building on Rezk 2010. There is is also proven that the Brown-Joyal-Jardine-Toën-Vezzosi models indeed precisely model $\infty$-stack $(\infty,1)$-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

• Zhen Lin Low, Notes on homotopical algebra

A quick introduction to the topic is in

• André Joyal, A crash course in topos theory – The big picture, lecture series at Topos à l’IHES, November 2015, Paris

Giraud-Rezk-Lurie axioms

A discussion of the $(\infty,1)$-universal colimits in terms of model category presentations is due to

• Charles Rezk, Fibrations and homotopy colimits of simplicial sheaves (pdf)

More on this with an eye on associated ∞-bundles is in

• Matthias Wendt, Classifying spaces and fibrations of simplicial sheaves (arXiv)

Homotopy type theory

Proof that all ∞-stack (∞,1)-topos have presentations by model categories which interpret (provide categorical semantics) for homotopy type theory with univalent type universes:

• Michael Shulman, All $(\infty,1)$-toposes have strict univalent universes (arXiv:1904.07004).