Fundamental theorem of topos theory

This article may be too technical for most readers to understand. Please help improve it to make it understandable to non-experts, without removing the technical details. (April 2016) (Learn how and when to remove this template message)

|

In mathematics, The fundamental theorem of topos theory states that the slice 𝐄/X of a topos 𝐄 over any one of its objects X is itself a topos. Moreover, if there is a morphism f:A->B in 𝐄 then there is a functor f*:𝐄/B->𝐄/A which preserves exponentials and the subobject classifier.

## Contents

* 1 The pullback functor
* 2 Logical interpretation
* 3 See also
* 4 References

## The pullback functor

For any morphism f in 𝐄 there is an associated "pullback functor" f*:=−↦f×−->f which is key in the proof of the theorem. For any other morphism g in 𝐄 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 𝐄 is isomorphic to the slice over its own terminal object, i.e. 𝐄≅𝐄/1, so for any object A in 𝐄 there is a morphism f:A->1 and thereby a pullback functor f*:𝐄->𝐄/A, which is why any slice 𝐄/A is also a topos.

For a given slice 𝐄/B let XB 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↦AB×B×−BAB≅(A×BB×−B)AB≅A×BB×−A≅A×−A=A*

so this is how the pullback functor f* maps objects of 𝐄/B to 𝐄/A. Furthermore, note that any element C of the base topos is isomorphic to 1×C1=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 𝐄 to its slice 𝐄/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 ψ 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

* Timeline of category theory and related mathematics
* Deduction Theorem

## References

* McLarty, Colin (1992). "§17.3 The fundamental theorem". Elementary Categories, Elementary Toposes. Oxford Logic Guides. 21. Oxford University Press. pp. 158. ISBN 978-0-19-158949-2. https://books.google.com/books?id=V8cON1x39bIC&pg=PA158.

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/Fundamental theorem of topos theory. Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=Fundamental_theorem_of_topos_theory&oldid=4230348"