Contents
Context
-Topos Theory
(∞,1)-topos theory
-
elementary (∞,1)-topos
-
(∞,1)-site
-
reflective sub-(∞,1)-category
-
(∞,1)-category of (∞,1)-sheaves
-
(∞,1)-topos
-
(n,1)-topos, n-topos
-
(∞,1)-quasitopos
-
(∞,2)-topos
-
(∞,n)-topos
-
hypercomplete (∞,1)-topos
-
over-(∞,1)-topos
-
n-localic (∞,1)-topos
-
locally n-connected (n,1)-topos
-
structured (∞,1)-topos
-
locally ∞-connected (∞,1)-topos, ∞-connected (∞,1)-topos
-
local (∞,1)-topos
-
cohesive (∞,1)-topos
structures in a cohesive (∞,1)-topos
Contents
Idea
By is denoted the collection of all (∞,1)-toposes. This is the (∞,1)-category-theory analog of Topos.
Definition
is the (non-full) sub-(∞,1)-category of (∞,1)Cat on (∞,1)-toposes and (∞,1)-geometric morphisms between them.
Morally, this should actually be an (∞,2)-category, just as Topos is a 2-category, but since the technology of -categories is not well developed, this point of view is not often taken yet.
Properties
In the following, will refer to the (superlarge) category of large -categories.
Existence of sites of definition
(…)
Existence of limits and colimits
We discuss existence of (∞,1)-limits and (∞,1)-colimits in .
Proposition
The -category has all small -colimits and functor
preserves small limits.
This is HTT, prop. 6.3.2.3. In the notation there, is the -category of toposes whose arrows are the inverse image morphisms, and thus opposite to .
Proposition
The -category has filtered (∞,1)-limits and the inclusion
preserves these.
This is HTT, prop. 6.3.3.1.
Proposition
The -category has all small (∞,1)-limits.
This is HTT, prop. 6.3.4.7.
This is HTT, remark 6.3.4.10.
This is HTT, Prop. 6.3.4.1, for details see at terminal geometric morphism.
Computation of limits and colimits
We discuss more or less explicit descriptions of (∞,1)-limits and (∞,1)-colimits in .
Proposition
Let
be a diagram of (∞,1)-toposes. Then its (∞,1)-pullback is computed, roughly, by the (∞,1)-pushout of their (∞,1)-sites of definition (see above).
More in detail: there exist (∞,1)-sites , , and with finite (∞,1)-limit and morphisms of sites
such that
Let then
be the (∞,1)-pushout of the underlying (∞,1)-categories in the full sub-(∞,1)-category (∞,1)Cat of -categories with finite -limits.
Let moreover
be the reflective sub-(∞,1)-category obtained by localization at the class of morphisms generated by the inverse image of the coverings of and the inverse image of the coverings of .
Then
is an (∞,1)-pullback square.
This is HTT, prop. 6.3.4.6.
Colimits of over-toposes
Proposition
For any topos , there is a colimit preserving functor sending an object to its over-topos , and sending an arrow to the essential geometric morphism .
Proof
HTT, Prop. 6.1.3.9 implies the “terminal vertex” Cartesian fibration is classified by a limit preserving functor , the -category of locally presentable -categories and colimit-preserving functors between them.
This functor factors through the subcategory that sends a geometric morphism to its inverse image part. By [HTT, Prop. 6.3.2.3] and [HTT, Prop. 5.5.1.13], it follows that this is also a limit preserving functor.
The opposite category is then formed by taking right adjoints.
-
Topos
-
Topos
References
section 6.3 in