Classifying Toposes

The notion of a "topos" has its roots in two separate mathematical disciplines: On the one hand, an Elementary Topos can be viewed as a generalised mathematical universe; that is, as a foundation for higher-order intuitionistic logic rather than the classical set-theoretic setting. From this perspective, a topos is simply a category sufficiently rich in categorical structure that it admits an "internal language" which can be reasoned about according to the deduction rules of intuitionistic logic, and we have a natural notion of models of theories inside such categories.

The second viewpoint - Grothendieck Toposes - arose from Grothendieck's work in the 1960s reshaping algebraic geometry with the invention of scheme theory. This class of toposes is a generalisation of the category of sheaves on a topological space, and thus can be analysed via arguments of a geometric nature. Placing these "geometric" constraints on toposes imposes structure on their internal logic; in particular, we can show that the theories whose models are preserved by geometric morphisms between Grothendieck toposes (that is, functors which preserve the geometric structure) are those which admit axiomatisations whose axioms are all of a specific form. We call such theories geometric theories.

In this essay, we will introduce the basic theory of elementary and Grothendieck toposes, and show how logic can be interpreted in these categories. We will use the machinery we have built to show that for any geometric theory $\mathbb{T}$, there is a Grothendieck topos $\mathbf{Set}[\mathbb{T}]$ which contains a universal model of $\mathbb{T}$ inside, in the sense that any model of $\mathbb{T}$ in a Grothendieck topos can be viewed as the inverse image of this model along some geometric morphism. We call $\mathbf{Set}[\mathbb{T}]$ the classifying topos of $\mathbb{T}$.