Fundamental theorem of topos theory

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

The pullback functor

For any morphism f in $𝐄$ there is an associated "pullback functor" $f^{\ast }:=-\mapsto f\times -\to f$ which is key in the proof of the theorem. For any other morphism g in $𝐄$ 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^{\ast }g$.

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

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

$f^{\ast }{B}^{\ast }:-\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^{\ast }$

so this is how the pullback functor $f^{\ast }$ maps objects of $𝐄/B$ to $𝐄/A$. Furthermore, note that any element C of the base topos is isomorphic to $\frac{1\times C}{1}=1^{\ast }C$, therefore if $f:A\to 1$ then $f^{\ast }:1^{\ast }\to A^{\ast }$ and $f^{\ast }:C\mapsto A^{\ast }C$ so that $f^{\ast }$ is indeed a functor from the base topos $𝐄$ to its slice $𝐄/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 $𝐄/[\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 $𝐄$ 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

• Template:Cite book