Classically, we have:
A Grothendieck topos is a category that admits a geometric embedding
in a presheaf category, i.e., a full and faithful functor that has a left exact left adjoint.
Since smallness can be relative, we also have:
For a given fixed category of sets , a Grothendieck topos over is a category of sheaves (-valued presheaves satisfying the sheaf condition) over a site which is small relative to , that is a site internal to .
Note that a Grothendieck topos is a topos because (or if) is.
This may be taken as an alternative definition of sheaf: since Lawvere-Tierney topologies are bijectively given by geometric embeddings, instead of explicitly defining a sheaf as a presheaf satisfying descent, one may define categories of sheaves as geometric embeddings into presheaf categories.
For details on the relation between the two perspectives see geometric embedding.
This perspective is useful for defining the vertical categorification of sheaves: stacks and ∞-stacks: the higher categories of these may be defined as geometric embeddings into higher categories of presheaves. This has been worked out in detail for (∞,1)-categories. See (∞,1)-category of (∞,1)-sheaves.
From the page total category, totality follows from the fact that a Grothendieck topos is
Dually, a Grothendieck topos is
Therefore a Grothendieck topos is also cototal.
Giraud characterized Grothendieck toposes as categories satisfying certain exactness and small completeness properties (where “small” is again relative to the given category of sets ). The exactness properties are elementary (not depending on ), and are satisfied in any elementary topos, or even a pretopos.
Giraud's theorem characterises a Grothendieck topos as follows:
These conditions are equivalent to
See the Elephant, theorem C.2.2.8. (There, the assumption of local smallness is not stated explicitly, but it is included in the definition of -pretopos by way of well-poweredness; on the nLab it is not so included, so we have to state it explicitly. To see that it is necessary, note that if and are Grothendieck universes with , then satisfies all the other conditions relative to , but is not locally small and is not a Grothendieck topos.) See also Wikipedia.
Sometimes (3,4) are combined and strengthened to the statement that the category has all small colimits, which are effective and pullback-stable. However, this is a mistake for two reasons: it is a significantly stronger axiomatisation (since without the small generating set, not every infinitary pretopos has this property), and it is not valid in weak foundations (while the definition given above is).
In more detail: we take as background set theory ZFC + “there is a strongly inaccessible cardinal” ; equivalently, the existence of a single Grothendieck universe (a set of “small sets”). Supposing given a model of , “category” shall then refer to category theory interpreted in . Let be the category of small sets; note that the set of morphisms of has size . Let be a locally small category.
(Street) A category is a Grothendieck topos iff it is lex total and the size of the set of isomorphism classes of objects is or less.
This result is in the spirit of saying “every Grothendieck topos is the category of sheaves with respect to the canonical topology on itself”. Putting aside set-theoretic issues, it suggests that Grothendieck toposes be seen as analogous to frames, which may be defined as lex total objects in -. In this setting, the appropriate morphisms are left exact left adjoints, so that Grothendieck toposes and geometric morphisms between them would be analogous to locales and continuous maps between them.
We have two definitions of a Grothendieck topos:
The theorem that these are equivalent can be proved in quite weak foundations, whether finitist, predicative, or constructive (or all three at once), as long as we axiomatize correctly given the caveats listed in the previous section. Some hard-nosed predicativists (and even hard-nosed ZFC fundamentalists) may object to the language (on the ground that large categories such as and other nontrivial Grothendieck toposes don't really exist), but they should accept the theorems when suitably phrased.
In predicative mathematics, however, we cannot prove that every Grothendieck topos is in fact a topos! In fact, it is immediate that the category of sets is a Grothendieck topos, but is an elementary topos if and only if power sets are small, which is precisely what predicativists doubt. One can use the term Grothendieck pretopos to avoid implying that we have an elementary topos. On the other hand, since Grothendeick toposes came first, perhaps it is the definition of ‘elementary topos’ that is too strong.
Similarly, in finitist mathematics, we cannot prove that every Grothendieck topos has a natural numbers object; while in strongly predicative mathematics, we cannot prove that every Grothendieck topos is cartesian closed. In each case, once a property is accepted of (the axiom of infinity and small function sets, in these examples), it can be proved for all Grothendieck toposes.
Constructivism as such is irrelevant; even in classical mathematics, most Grothendieck toposes are not boolean. However, for an analogous result, try the theorem that the category of presheaves on a groupoid (and hence any category of sheaves contained within it) is boolean. (Again, itself is an example of this.)
The theorem that every Grothendieck topos is cocomplete is a subtle point; it fails only in finitist predicative mathematics. (The key point in the proof is to generate the transitive closure of a binary relation . One proof defines to mean that for some , which is predicative but infinitary; another defines to mean that for every transitive relation that contains , which is finitary but impredicative.)
Locally presentable categories: Cocomplete possibly-large categories generated under filtered colimits by small generators under small relations. Equivalently, accessible localizations of free cocompletions. Accessible categories omit the cocompleteness requirement; toposes add the requirement of a left exact localization.
|(n,r)-categories||toposes||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)-topos theory||(∞,1)-toposes||locally presentable (∞,1)-categories||Simpson’s theorem||(∞,1)-presheaf (∞,1)-categories||accessible (∞,1)-categories|
A quick introduction of the basic facts of sheaf-topos theory is chapter I, “Background in topos theory” in
A standard textbook on this case is
Grothendieck topoi appear around section III,4 there. A proof of Giraud’s theorem is in appendix A.
The proof of Giraud’s theorem for (∞,1)-topoi is section 6.1.5 of
Street’s characterization of Grothendieck toposes is given in