Fundamental theorem of topos theory

The pullback functor

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

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 .

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 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.