Misplaced Pages

Fundamental theorem of topos theory

Article snapshot taken from Wikipedia with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
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 message)

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

The pullback functor

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

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

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

f B : B × B A B × B × B A B ( A × B B × B ) A B A × B B × A A × A = A {\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^{*}}

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

Logical interpretation

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

ϕ ψ ϕ ψ {\displaystyle \vdash \phi \rightarrow \psi \over \phi \vdash \psi }

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

See also

References

Category: