In mathematics, the fundamental theorem of topos theory states that the slice E / X {\displaystyle \mathbf {E} /X} of an elementary topos E {\displaystyle \mathbf {E} } over any one of its objects X {\displaystyle X} is itself a topos. Moreover, if there is a morphism f : A → B {\displaystyle f:A\rightarrow B} in E {\displaystyle \mathbf {E} } then there is a functor f ∗ : E / B → E / A {\displaystyle f^{*}:\mathbf {E} /B\rightarrow \mathbf {E} /A} which preserves exponentials and the subobject classifier.
The pullback functor For any morphism f in E {\displaystyle \mathbf {E} } there is an associated "pullback functor" f ∗ := − ↦ f × − → f {\displaystyle f^{*}:=-\mapsto f\times -\rightarrow f} which is key in the proof of the theorem. For any other morphism g in E {\displaystyle \mathbf {E} } which shares the same codomain as f, their product f × g {\displaystyle f\times g} is the diagonal of their pullback square, and the morphism which goes from the domain of f × g {\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 f ∗ g {\displaystyle f^{*}g} . Note that a topos E {\displaystyle \mathbf {E} } is isomorphic to the slice over its own terminal object, i.e. E ≅ E / 1 {\displaystyle \mathbf {E} \cong \mathbf {E} /1} , so for any object A in E {\displaystyle \mathbf {E} } there is a morphism f : A → 1 {\displaystyle f:A\rightarrow 1} and thereby a pullback functor f ∗ : E → E / A {\displaystyle f^{*}:\mathbf {E} \rightarrow \mathbf {E} /A} , which is why any slice E / A {\displaystyle \mathbf {E} /A} is also a topos. For a given slice E / B {\displaystyle \mathbf {E} /B} let X B {\displaystyle X \over B} denote an object of it, where X is an object of the base category. Then B ∗ {\displaystyle B^{*}} is a functor which maps: − ↦ B × − B {\displaystyle -\mapsto {B\times - \over B}} . Now apply f ∗ {\displaystyle f^{*}} to B ∗ {\displaystyle B^{*}} . This yields
f ∗ B ∗ : − ↦ B × − B ↦ A B × B × − B A B ≅ ( A × B B × − B ) A B ≅ A × B B × − A ≅ A × − A = A ∗ {\displaystyle 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 ∗ {\displaystyle f^{*}} maps objects of E / B {\displaystyle \mathbf {E} /B} to E / A {\displaystyle \mathbf {E} /A} . Furthermore, note that any element C of the base topos is isomorphic to 1 × C 1 = 1 ∗ C {\displaystyle {1\times C \over 1}=1^{*}C} , therefore if f : A → 1 {\displaystyle f:A\rightarrow 1} then f ∗ : 1 ∗ → A ∗ {\displaystyle f^{*}:1^{*}\rightarrow A^{*}} and f ∗ : C ↦ A ∗ C {\displaystyle f^{*}:C\mapsto A^{*}C} so that f ∗ {\displaystyle f^{*}} is indeed a functor from the base topos E {\displaystyle \mathbf {E} } to its slice E / A {\displaystyle \mathbf {E} /A} .
Logical interpretation Consider a pair of ground formulas ϕ {\displaystyle \phi } and ψ {\displaystyle \psi } whose extensions [ _ | ϕ ] {\displaystyle [\_|\phi ]} and [ _ | ψ ] {\displaystyle [\_|\psi ]} (where the underscore here denotes the null context) are objects of the base topos. Then ϕ {\displaystyle \phi } implies ψ {\displaystyle \psi } if and only if there is a monic from [ _ | ϕ ] {\displaystyle [\_|\phi ]} to [ _ | ψ ] {\displaystyle [\_|\psi ]} . If these are the case then, by theorem, the formula ψ {\displaystyle \psi } is true in the slice E / [ _ | ϕ ] {\displaystyle \mathbf {E} /[\_|\phi ]} , because the terminal object [ _ | ϕ ] [ _ | ϕ ] {\displaystyle [\_|\phi ] \over [\_|\phi ]} of the slice factors through its extension [ _ | ψ ] {\displaystyle [\_|\psi ]} . In logical terms, this could be expressed as
⊢ ϕ → ψ ϕ ⊢ ψ {\displaystyle \vdash \phi \rightarrow \psi \over \phi \vdash \psi }
so that slicing E {\displaystyle \mathbf {E} } by the extension of ϕ {\displaystyle \phi } would correspond to assuming ϕ {\displaystyle \phi } 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. Vol. 21. Oxford University Press. p. 158. ISBN 978-0-19-158949-2.