Fundamental theorem of topos theory

The fundamental theorem of topos theory states that the slice ${\displaystyle \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 ${\displaystyle 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" ${\displaystyle 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 ${\displaystyle f\times g}$ is the diagonal of their pullback square, and the morphism which goes from the domain of ${\displaystyle 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 ${\displaystyle f^{*}g}$.

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

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

${\displaystyle 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 ${\displaystyle \mathbf {E} /B}$ to ${\displaystyle \mathbf {E} /A}$. Furthermore, note that any element C of the base topos is isomorphic to ${\displaystyle {1\times C \over 1}=1^{*}C}$, therefore if ${\displaystyle f:A\rightarrow 1}$ then ${\displaystyle f^{*}:1^{*}\rightarrow A^{*}}$ and ${\displaystyle f^{*}:C\mapsto A^{*}C}$ so that $f^{*}$ is indeed a functor from the base topos $\mathbf {E}$ to its slice ${\displaystyle \mathbf {E} /A}$.

Logical interpretation

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

${\displaystyle \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