Fundamental theorem of topos theory

From HandWiki

In mathematics, The fundamental theorem of topos theory states that the slice [math]\displaystyle{ \mathbf{E} / X }[/math] of a topos [math]\displaystyle{ \mathbf{E} }[/math] over any one of its objects [math]\displaystyle{ X }[/math] is itself a topos. Moreover, if there is a morphism [math]\displaystyle{ f : A \rightarrow B }[/math] in [math]\displaystyle{ \mathbf{E} }[/math] then there is a functor [math]\displaystyle{ f^*: \mathbf{E} / B \rightarrow \mathbf{E} / A }[/math] which preserves exponentials and the subobject classifier.

The pullback functor

For any morphism f in [math]\displaystyle{ \mathbf{E} }[/math] there is an associated "pullback functor" [math]\displaystyle{ f^* := - \mapsto f \times - \rightarrow f }[/math] which is key in the proof of the theorem. For any other morphism g in [math]\displaystyle{ \mathbf{E} }[/math] which shares the same codomain as f, their product [math]\displaystyle{ f \times g }[/math] is the diagonal of their pullback square, and the morphism which goes from the domain of [math]\displaystyle{ f \times g }[/math] 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 [math]\displaystyle{ f^*g }[/math].

Note that a topos [math]\displaystyle{ \mathbf{E} }[/math] is isomorphic to the slice over its own terminal object, i.e. [math]\displaystyle{ \mathbf{E} \cong \mathbf{E} / 1 }[/math], so for any object A in [math]\displaystyle{ \mathbf{E} }[/math] there is a morphism [math]\displaystyle{ f : A \rightarrow 1 }[/math] and thereby a pullback functor [math]\displaystyle{ f^* : \mathbf{E} \rightarrow \mathbf{E} / A }[/math], which is why any slice [math]\displaystyle{ \mathbf{E} / A }[/math] is also a topos.

For a given slice [math]\displaystyle{ \mathbf{E} / B }[/math] let [math]\displaystyle{ X \over B }[/math] denote an object of it, where X is an object of the base category. Then [math]\displaystyle{ B^* }[/math] is a functor which maps: [math]\displaystyle{ - \mapsto {B \times - \over B} }[/math]. Now apply [math]\displaystyle{ f^* }[/math] to [math]\displaystyle{ B^* }[/math]. This yields

[math]\displaystyle{ f^* B^* : - \mapsto {B \times - \over B} \mapsto {{A \over B} \times {B \times - \over B} \over {A \over B}} \cong {\Big({A \times_B \, B \times - \over B}\Big) \over {A \over B}} \cong {A \times_B B \times - \over A} \cong {A \times - \over A} = A^* }[/math]

so this is how the pullback functor [math]\displaystyle{ f^* }[/math] maps objects of [math]\displaystyle{ \mathbf{E} / B }[/math] to [math]\displaystyle{ \mathbf{E} / A }[/math]. Furthermore, note that any element C of the base topos is isomorphic to [math]\displaystyle{ {1 \times C \over 1} = 1^* C }[/math], therefore if [math]\displaystyle{ f : A \rightarrow 1 }[/math] then [math]\displaystyle{ f^*: 1^* \rightarrow A^* }[/math] and [math]\displaystyle{ f^* : C \mapsto A^* C }[/math] so that [math]\displaystyle{ f^* }[/math] is indeed a functor from the base topos [math]\displaystyle{ \mathbf{E} }[/math] to its slice [math]\displaystyle{ \mathbf{E} / A }[/math].

Logical interpretation

Consider a pair of ground formulas [math]\displaystyle{ \phi }[/math] and [math]\displaystyle{ \psi }[/math] whose extensions [math]\displaystyle{ [\_|\phi] }[/math] and [math]\displaystyle{ [\_|\psi] }[/math] (where the underscore here denotes the null context) are objects of the base topos. Then [math]\displaystyle{ \phi }[/math] implies [math]\displaystyle{ \psi }[/math] if and only if there is a monic from [math]\displaystyle{ [\_|\phi] }[/math] to [math]\displaystyle{ [\_|\psi] }[/math]. If these are the case then, by theorem, the formula [math]\displaystyle{ \psi }[/math] is true in the slice [math]\displaystyle{ \mathbf{E} / [\_|\phi] }[/math], because the terminal object [math]\displaystyle{ [\_|\phi] \over [\_|\phi] }[/math] of the slice factors through its extension [math]\displaystyle{ [\_|\psi] }[/math]. In logical terms, this could be expressed as

[math]\displaystyle{ \vdash \phi \rightarrow \psi \over \phi \vdash \psi }[/math]

so that slicing [math]\displaystyle{ \mathbf{E} }[/math] by the extension of [math]\displaystyle{ \phi }[/math] would correspond to assuming [math]\displaystyle{ \phi }[/math] as a hypothesis. Then the theorem would say that making a logical assumption does not change the rules of topos logic.

See also

References



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