Fundamental theorem of topos theory explained

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.

The pullback functor

For any morphism f in

E there is an associated "pullback functor" f ^{*} : = - \mapsto f x - → 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 x g is the diagonal of their pullback square, and the morphism which goes from the domain of f x 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 \cong 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 \over B denote an object of it, where X is an object of the base category. Then B ^{*} is a functor which maps: - \mapsto {B x - \over B} . Now apply f ^{*} to B ^{*} . This yieldsf ^{*} B ^{*} : - \mapsto {B x - \over B} \mapsto {{A \over B} x {B x - \over B} \over {A \over B}} \cong { ( {A x _{B} B x - \over B} ) \over {A \over B}} \cong {A x _{B} B x - \over A} \cong {A x - \over 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 x C \over 1 } = 1 ^{*} C , therefore if f : A → 1 then f ^{*:} 1 ^{*} → A ^{*} and f ^{*} : C \mapsto 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

\phi and \psi whose extensions [\ _{|\phi]} and [\ _{|\psi]} (where the underscore here denotes the null context) are objects of the base topos. Then \phi implies \psi if and only if there is a monic from [\ _{|\phi]} to [\ _{|\psi]} . If these are the case then, by theorem, the formula \psi is true in the slice E / [\ _{|\phi]} , because the terminal object [\ _{|\phi]} \over [\ _{|\phi]} of the slice factors through its extension [\ _{|\psi]} . In logical terms, this could be expressed as\vdash \phi → \psi \over \phi \vdash \psi so that slicing E by the extension of \phi would correspond to assuming \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

• Book: McLarty, Colin . §17.3 The fundamental theorem . . Elementary Categories, Elementary Toposes . Oxford University Press . Oxford Logic Guides . 21 . 1992 . 978-0-19-158949-2 . 158 .