Fundamental theorem of topos theory

The fundamental theorem of topos theory states that the slice $\mathbf{E} / X$ of a topos $\mathbf{E}$ over any one of its objects $X$ is itself a topos. Moreover, if there is a morphism $f : A \rightarrow B$ in $\mathbf{E}$ then there is a functor $f^*: \mathbf{E} / B \rightarrow \mathbf{E} / A$ which preserves exponentials and the subobject classifier.

The pullback functor

For any morphism f in $\mathbf{E}$ there is an associated "pullback functor" $f^* := - \mapsto f \times - \rightarrow f$ which is key in the proof of the theorem. For any other morphism g in $\mathbf{E}$ which shares the same codomain as f, their product $f \times g$ is the diagonal of their pullback square, and the morphism which goes from the domain of $f \times g$ 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 $f^*g$.

Note that a topos $\mathbf{E}$ is isomorphic to the slice over its own terminal object, i.e. $\mathbf{E} \cong \mathbf{E} / 1$, so for any object A in $\mathbf{E}$ there is a morphism $f : A \rightarrow 1$ and thereby a pullback functor $f^* : \mathbf{E} \rightarrow \mathbf{E} / A$, which is why any slice $\mathbf{E} / A$ is also a topos.

For a given slice $\mathbf{E} / B$ let $X \over B$ denote an object of it, where X is an object of the base category. Then $B^*$ is a functor which maps: $- \mapsto {B \times - \over B}$. Now apply $f^*$ to $B^*$. This yields

$f^* B^* : - \mapsto {B \times - \over B} \mapsto {{A \over B} \times {B \times - \over B} \over {A \over B}} \cong {\Big({A \times_B \, B \times - \over B}\Big) \over {A \over B}} \cong {A \times_B B \times - \over A} \cong {A \times - \over A} = A^*$

so this is how the pullback functor $f^*$ maps objects of $\mathbf{E} / B$ to $\mathbf{E} / A$. Furthermore, note that any element C of the base topos is isomorphic to ${1 \times C \over 1} = 1^* C$, therefore if $f : A \rightarrow 1$ then $f^*: 1^* \rightarrow A^*$ and $f^* : C \mapsto A^* C$ so that $f^*$ is indeed a functor from the base topos $\mathbf{E}$ to its slice $\mathbf{E} / A$.

Logical interpretation

Consider a pair of ground formulas φ and ψ whose extensions $[\_|\phi]$ and $[\_|\psi]$ (where the underscore here denotes the null context) are objects of the base topos. Then φ implies ψ iff there is a monic from $[\_|\phi]$ to $[\_|\psi]$. If these are the case then, by theorem, the formula ψ is true in the slice $\mathbf{E} / [\_|\phi]$, because the terminal object $[\_|\phi] \over [\_|\phi]$ of the slice factors through its extension $[\_|\psi]$. In logical terms, this could be expressed as

$\vdash \phi \rightarrow \psi \over \phi \vdash \psi$

so that slicing $\mathbf{E}$ 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.

References

• Colin McLarty, Elementary Categories, Elementary Toposes, Oxford University Press (1995), p. 158