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
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
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
![{\displaystyle [\_|\phi ]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2b506a72356b03eb32bd5560da83c814aa1a56cd)
![{\displaystyle [\_|\psi ]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/12623fc36bff55d3052ea1a2e2b2fb488120e798)
![{\displaystyle \mathbf {E} /[\_|\phi ]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/81369f6097f4f490c77f0a7aa702048d536dadfb)
![{\displaystyle [\_|\phi ] \over [\_|\phi ]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/399ee0535effd211c3609c52f1c2a022068284e9)
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
References
- 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.