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

This article is issued from Wikipedia - version of the 4/16/2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.