Fundamental theorem of topos theory

For any morphism f in $\backslash mathbf\{E\}$ there is an associated "pullback functor" $f^*\; :=\; -\; \backslash mapsto\; f\; \backslash times\; -\; \backslash rightarrow\; f$ which is key in the proof of the theorem. For any other morphism g in $\backslash mathbf\{E\}$ which shares the same codomain as f, their product $f\; \backslash times\; g$ is the diagonal of their pullback square, and the morphism which goes from the domain of $f\; \backslash 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 $\backslash mathbf\{E\}$ is isomorphic to the slice over its own terminal object, i.e. $\backslash mathbf\{E\}\; \backslash cong\; \backslash mathbf\{E\}\; /\; 1$, so for any object A in $\backslash mathbf\{E\}$ there is a morphism $f\; :\; A\; \backslash rightarrow\; 1$ and thereby a pullback functor $f^*\; :\; \backslash mathbf\{E\}\; \backslash rightarrow\; \backslash mathbf\{E\}\; /\; A$, which is why any slice $\backslash mathbf\{E\}\; /\; A$ is also a topos.

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

: $f^*\; B^*\; :\; -\; \backslash mapsto\; \{B\; \backslash times\; -\; \backslash over\; B\}\; \backslash mapsto\; \{\{A\; \backslash over\; B\}\; \backslash times\; \{B\; \backslash times\; -\; \backslash over\; B\}\; \backslash over\; \{A\; \backslash over\; B\}\}\; \backslash cong\; \{\backslash Big(\{A\; \backslash times\_B\; \backslash ,\; B\; \backslash times\; -\; \backslash over\; B\}\backslash Big)\; \backslash over\; \{A\; \backslash over\; B\}\}\; \backslash cong\; \{A\; \backslash times\_B\; B\; \backslash times\; -\; \backslash over\; A\}\; \backslash cong\; \{A\; \backslash times\; -\; \backslash over\; A\}\; =\; A^*$

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

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

:$\backslash vdash\; \backslash phi\; \backslash rightarrow\; \backslash psi\; \backslash over\; \backslash phi\; \backslash vdash\; \backslash psi$

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

• Timeline of category theory and related mathematics
• Deduction Theorem

• {{cite book |first=Colin |last=McLarty |chapter=§17.3 The fundamental theorem |chapter-url={{GBurl|V8cON1x39bIC|p=158}} |title=Elementary Categories, Elementary Toposes |publisher=Oxford University Press |series=Oxford Logic Guides |volume=21 |date=1992 |isbn=978-0-19-158949-2 |pages=158 }}

Category:Topos theory

Category:Mathematical theorems