Fundamental theorem of topos theory

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

The pullback functor

For any morphism f in $\mathbf{𝐄}$ there is an associated "pullback functor" $f^{*}:=-\mapsto f\times -\to f$ which is key in the proof of the theorem. For any other morphism g in $\mathbf{𝐄}$ 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{𝐄}$ is isomorphic to the slice over its own terminal object, i.e. $\mathbf{𝐄}\cong \mathbf{𝐄}/1$, so for any object A in $\mathbf{𝐄}$ there is a morphism $f:A\to 1$ and thereby a pullback functor $f^{*}:\mathbf{𝐄}\to \mathbf{𝐄}/A$, which is why any slice $\mathbf{𝐄}/A$ is also a topos.

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

$f^{*}{B}^{*}:-\mapsto \frac{B\times -}{B}\mapsto \frac{\frac{A}{B}\times \frac{B\times -}{B}}{\frac{A}{B}}\cong \frac{\left(\frac{A{\times }_{B}B\times -}{B}\right)}{\frac{A}{B}}\cong \frac{A{\times }_{B}B\times -}{A}\cong \frac{A\times -}{A}=A^{*}$

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

Logical interpretation

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

$\frac{⊢\varphi \to \psi }{\varphi ⊢\psi }$

so that slicing $\mathbf{𝐄}$ by the extension of $\varphi$ would correspond to assuming $\varphi$ as a hypothesis. Then the theorem would say that making a logical assumption does not change the rules of topos logic.

See also

• Timeline of category theory and related mathematics
• Deduction Theorem

References

• McLarty, Colin (1992). "§17.3 The fundamental theorem". Elementary Categories, Elementary Toposes. Oxford Logic Guides. 21. Oxford University Press. pp. 158. ISBN 978-0-19-158949-2. https://books.google.com/books?id=V8cON1x39bIC&pg=PA158.