In mathematics, The fundamental theorem of topos theory states that the slice
of a topos
over any one of its objects
is itself a topos. Moreover, if there is a morphism
in
then there is a functor
which preserves exponentials and the subobject classifier.
The pullback functor
For any morphism f in
there is an associated "pullback functor"
which is key in the proof of the theorem. For any other morphism g in
which shares the same codomain as f, their product
is the diagonal of their pullback square, and the morphism which goes from the domain of
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
.
Note that a topos
is isomorphic to the slice over its own terminal object, i.e.
, so for any object A in
there is a morphism
and thereby a pullback functor
, which is why any slice
is also a topos.
For a given slice
let
denote an object of it, where X is an object of the base category. Then
is a functor which maps:
. Now apply
to
. This yields
![{\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^{*}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/accfc918563c2b027e967ae913f04ebe488ffa10)
so this is how the pullback functor
maps objects of
to
. Furthermore, note that any element C of the base topos is isomorphic to
, therefore if
then
and
so that
is indeed a functor from the base topos
to its slice
.
Logical interpretation
Consider a pair of ground formulas
and
whose extensions
and
(where the underscore here denotes the null context) are objects of the base topos. Then
implies
iff there is a monic from
to
. If these are the case then, by theorem, the formula
is true in the slice
, because the terminal object
of the slice factors through its extension
. In logical terms, this could be expressed as
![{\displaystyle \vdash \phi \rightarrow \psi \over \phi \vdash \psi }](https://wikimedia.org/api/rest_v1/media/math/render/svg/08693aee01d9e4a17148cdb6d20aee557c3f8836)
so that slicing
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