Fundamental theorem of topos theory


In mathematics, The fundamental theorem of topos theory states that the slice of a topos over any one of its objects is itself a topos. Moreover, if there is a morphism in then there is a functor which preserves exponentials and the subobject classifier.

The pullback functor

For any morphism f in there is an associated "pullback functor" which is key in the proof of the theorem. For any other morphism g in which shares the same codomain as f, their product is the diagonal of their pullback square, and the morphism which goes from the domain of to the domain of f is opposite to g in the pullback square, so it is the pullback of g along f, which can be denoted as.
Note that a topos is isomorphic to the slice over its own terminal object, i.e., so for any object A in there is a morphism and thereby a pullback functor, which is why any slice is also a topos.
For a given slice let denote an object of it, where X is an object of the base category. Then is a functor which maps:. Now apply to. This yields
so this is how the pullback functor maps objects of to. Furthermore, note that any element C of the base topos is isomorphic to, therefore if then and so that is indeed a functor from the base topos to its slice.

Logical interpretation

Consider a pair of ground formulas and whose extensions and are objects of the base topos. Then implies iff there is a monic from to. If these are the case then, by theorem, the formula is true in the slice, because the terminal object of the slice factors through its extension. In logical terms, this could be expressed as
so that slicing by the extension of would correspond to assuming as a hypothesis. Then the theorem would say that making a logical assumption does not change the rules of topos logic.