Fundamental theorem of topos theory

In mathematics, 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 $\phi$ and $\psi$ whose extensions $[\_|\phi ]$ and $[\_|\psi ]$ (where the underscore here denotes the null context) are objects of the base topos. Then $\phi$ implies $\psi$ iff there is a monic from $[\_|\phi ]$ to $[\_|\psi ]$. If these are the case then, by theorem, the formula $\psi$ 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 $\phi$ would correspond to assuming $\phi$ 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