Fundamental theorem of topos theory

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

edit

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

 

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

edit

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   if and only if 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

 

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.

See also

edit

References

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