Fundamental theorem of topos theory

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

The pullback functor

For any morphism f in ${\displaystyle \mathbf{E}}$ there is an associated "pullback functor" ${\displaystyle f^{\ast }:=-\mapsto f\times -\to 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^{\ast }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\to 1}$ and thereby a pullback functor ${\displaystyle f^{\ast }:\mathbf{E}\to \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 \frac{X}{B}}$ denote an object of it, where X is an object of the base category. Then ${\displaystyle B^{\ast }}$ is a functor which maps: ${\displaystyle -\mapsto \frac{B\times -}{B}}$. Now apply ${\displaystyle f^{\ast }}$ to ${\displaystyle B^{\ast }}$. This yields

${\displaystyle f^{\ast }{B}^{\ast }:-\mapsto \frac{B\times -}{B}\mapsto \frac{\frac{A}{B}\times \frac{B\times -}{B}}{\frac{A}{B}}\cong \frac{(\frac{A{\times }_{B}B\times -}{B})}{\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 ${\displaystyle f^{\ast }}$ 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 \frac{1\times C}{1}=1^{\ast }C}$, therefore if ${\displaystyle f:A\to 1}$ then ${\displaystyle f^{\ast }:1^{\ast }\to A^{\ast }}$ and ${\displaystyle f^{\ast }:C\mapsto A^{\ast }C}$ so that ${\displaystyle f^{\ast }}$ is indeed a functor from the base topos ${\displaystyle \mathbf{E}}$ to its slice ${\displaystyle \mathbf{E}/A}$.

Logical interpretation

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

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

so that slicing ${\displaystyle \mathbf{E}}$ by the extension of ${\displaystyle \varphi }$ would correspond to assuming ${\displaystyle \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. 

0.00 (0 votes) Original source: https://en.wikipedia.org/wiki/Fundamental theorem of topos theory. Read more