In mathematics, The fundamental theorem of topos theory states that the slice
E
/
X
of a topos
E
over any one of its objects
X
is itself a topos. Moreover, if there is a morphism
f
:
A
→
B
in
E
then there is a functor
f
∗
:
E
/
B
→
E
/
A
which preserves exponentials and the subobject classifier.
For any morphism f in
E
there is an associated "pullback functor"
f
∗
:=
−
↦
f
×
−
→
f
which is key in the proof of the theorem. For any other morphism g in
E
which shares the same codomain as f, their product
f
×
g
is the diagonal of their pullback square, and the morphism which goes from the domain of
f
×
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
E
is isomorphic to the slice over its own terminal object, i.e.
E
≅
E
/
1
, so for any object A in
E
there is a morphism
f
:
A
→
1
and thereby a pullback functor
f
∗
:
E
→
E
/
A
, which is why any slice
E
/
A
is also a topos.
For a given slice
E
/
B
let
X
B
denote an object of it, where X is an object of the base category. Then
B
∗
is a functor which maps:
−
↦
B
×
−
B
. Now apply
f
∗
to
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
∗
so this is how the pullback functor
f
∗
maps objects of
E
/
B
to
E
/
A
. Furthermore, note that any element C of the base topos is isomorphic to
1
×
C
1
=
1
∗
C
, therefore if
f
:
A
→
1
then
f
∗
:
1
∗
→
A
∗
and
f
∗
:
C
↦
A
∗
C
so that
f
∗
is indeed a functor from the base topos
E
to its slice
E
/
A
.
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
E
/
[
_
|
ϕ
]
, because the terminal object
[
_
|
ϕ
]
[
_
|
ϕ
]
of the slice factors through its extension
[
_
|
ψ
]
. In logical terms, this could be expressed as
⊢
ϕ
→
ψ
ϕ
⊢
ψ
so that slicing
E
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.
