nLab
topos

Contents

Idea

A topos is a category that resembles the category Set of sets and functions enough that we can use it as a ‘universe’ to do ordinary mathematics in. Ordinary mathematical reasoning (with some restrictions) suffices to prove results internal to any topos.

A topos in this sense is sometimes called an elementary topos or a Lawvere–Tierney topos to distinguish it from the original but more specific Grothendieck topos.

For a longer introduction, try:

Definition

A quick formal definition is that an (elementary) topos is a category which

  1. has finite limits,
  2. is cartesian closed, and
  3. has a subobject classifier.

There are alternative ways to state the definition; for instance,

  1. finite limits and
  2. power objects.

In a way, however, these concise definitions can be misleading, because a topos has a great deal of other structure, which plays a very important role but just happens to follow automatically from these basic axioms. Most importantly, a topos is:

The last two imply that it has an internal logic that resembles ordinary mathematical reasoning, and the presence of exponentials and power objects means that this logic is higher order.

Reasoning in a topos

Any result in ordinary mathematics whose proof is finitist and constructive automatically holds in any topos. If you remove the restriction that the proof be finitist, then the result holds in any topos with a natural numbers object; if you remove the restrictions that the proof be constructive, then the result holds in any boolean topos. On the other hand, if you add the restriction that the proof be predicative in the weaker sense used by constructivists, then the result may fail in some toposes but holds in any Π-pretopos; if you add the restriction that the proof by predicative in a stronger sense, then the result holds in any Heyting pretopos.

Therefore, one can prove results in toposes and similar categories by reasoning, not about the objects and morphisms in the topos themselves, but instead about sets and functions in the normal language of structural set theory, which is more familiar to most mathematicians. One merely has to be careful about what axioms one uses to get results of sufficient generality.

For more on this idea, see internal logic.

Examples

  • The archetypical topos is Set. Notice that this happens to be a Grothendieck topos: this is the category of sheaves on the point.

    The full subcategory FinSet is also a topos, and the inclusion functor FinSetSet is a logical morphism.

    More generally, for κ a strong limit cardinal the full subcategory Set κ of sets or cardinality less than κ is a topos.

  • For C any (small) site, the category of sheaves Sh(C) is a Grothendieck topos. Either by definition or by Giraud's theorem, every Grothendieck topos arises in this way. Important examples include:

  • If G is a topological group, then the category Cont(G) of sets with a continuous action of G (that is, the action map G×XX is continuous, where X has the discrete topology) is a topos, and in fact a Grothendieck topos (though this may not be obvious). More generally, G may be a topological groupoid?, or even a localic groupoid. In fact, it is a theorem that every Grothendieck topos can be presented as the topos of “continuous sheaves” on a localic groupoid.

  • Again if G is a topological group, the category Unif(G) of uniformly continuous? G-sets is also a topos, but not (in general) one of Grothendieck’s. For example, if G is the profinite completion? of , then a continuous G-set is a -set all of whose orbits are finite, while a uniformly continuous one is a -set with a finite upper bound on the size of all its orbits.

  • An obvious example of an elementary topos that is not a Grothendieck topos is the category FinSet of finite sets. More generally, for any strong limit cardinal? κ, the category of sets of cardinality <κ is an elementary topos, and as long as κ>ω it has a NNO.

  • Since the definition of elementary topos is “algebraic,” there exist free topos?es generated by various kinds of data. In particular, the category of toposes (and logical functors) has an initial object which is sometimes called the free topos. More generally, any higher-order type theory (of the sort which can be interpreted in the internal logic of a topos) generates a free topos containing a model of that theory. Such toposes (for a consistent theory) are never Grothendieck’s.

  • If G is a large groupoid with a small set of objects, then the category [G,Set] (which makes sense if we define “large” and “small” relative to a Grothendieck universe) is a topos, but not in general a Grothendieck topos. Note that this topos is in fact complete and cocomplete, but it does not have a small generating set.

  • If is a filter of subterminal objects in any topos E, then there is a filterquotient? topos E//. Grothendieck-ness (and completeness and cocompleteness) are not in general preserved by this construction.

  • If C and D are toposes and F:CD is a lex functor, then there is a topos Gl(F) called the Artin gluing? of C and D along F, and defined to be the comma category (D/F). If C and D are Grothendieck toposes and F is accessible, then Gl(F) is again Grothendieck, but in general it may not be. (Note, though, that it is not clear whether it can be proven in ZFC that there exist any inaccessible lex functors between Grothendieck toposes, although from a proper class of measurable cardinal?s one can construct an inaccessible lex endofunctor of Set.)

  • The category of coalgebras for any lex comonad on a topos is again a topos, and if the comonad is accessible, this construction preserves Grothendieck-ness. The Artin gluing Gl(F) is equivalent to the category of coalgebras for the comonad on the topos C×D defined by (c,d)(c,d×F(c)).

  • Todd Trimble has a notion called a “modal operator” on a topos, from which one can construct a new topos of ”G-structures”: see Three topos theorems in one. A possibly related idea is Toby Kenney’s notion of lex distributive diad?, from which one can also construct a topos.

  • From any partial combinatory algebra one can construct a realizability topos, whose internal logic is “computable” or “effective” mathematics relative to that PCA. In particular, for Kleene's first algebra, one obtains the effective topos, the most-studied of realizability toposes. Realizability toposes are generally not Grothendieck toposes.

  • A topos can also be constructed from any tripos. This includes realizability toposes as well as toposes of sheaves on locales.

Special classes

For various applications one uses toposes that have extra structure or properties.

Higher toposes

The analogs of topos theory in higher category theory is higher topos theory.

A well developed case is that of (∞,1)-toposes.

References

Another survey is in

  • Ross Street, A survey of topos theory (notes for students, 1978) pdf

A standard textbook is

  • Peter Johnstone, Topos theory, London Math. Soc. Monographs 10, Acad. Press 1977, xxiii+367 pp.

This later grew into the more detailed

A quick introduction of the basic facts of Grothendieck topos theory is chapter I, “Background in topos theory” in

  • Ieke Moerdijk, Classifying Spaces and Classifying Topoi Lecture Notes in Mathematics 1616, Springer (1995)

A standard textbook on this case is

There is also

  • R. Goldblatt, Topoi. The categorial analysis of logic, Studies in Logic and the Foundations of Math. 98, North-Holland Publ. Co., Amsterdam, 1979, 1984; (Rus. transl. Mir Publ., Moscow 1983).