Fundamental theorem of topos theory

For any morphism f in ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle 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 ${\displaystyle 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 ${\displaystyle f^{*}}$ is indeed a functor from the base topos ${\displaystyle \mathbf {E} }$ to its slice ${\displaystyle \mathbf {E} /A}$.

Consider a pair of ground formulas ${\displaystyle \phi }$ and ${\displaystyle \psi }$ whose extensions ${\displaystyle [\_|\phi ]}$ and ${\displaystyle [\_|\psi ]}$ (where the underscore here denotes the null context) are objects of the base topos. Then ${\displaystyle \phi }$ implies ${\displaystyle \psi }$ iff there is a monic from ${\displaystyle [\_|\phi ]}$ to ${\displaystyle [\_|\psi ]}$. If these are the case then, by theorem, the formula ${\displaystyle \psi }$ 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 ${\displaystyle \mathbf {E} }$ by the extension of ${\displaystyle \phi }$ would correspond to assuming ${\displaystyle \phi }$ as a hypothesis. Then the theorem would say that making a logical assumption does not change the rules of topos logic.

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