Different Notions of a Topos
Table of Contents
1. TODO What notions are there? Elementary topoi, Grothendieck topoi, geometric topoi?
The first definition we give is just a copy of the definition in Chapter 4, Section 1 in “Sheaves in Geometry and Logic”. To us this doesn’t seem like the most natural definition neither like a least data definition.
A (elementary) topos \( \mathcal E \) consists of
- a category \( \mathcal E \),
- an object \( \Omega \) (called subobject classifier)
- a function \( P \colon \Ob \mathcal E \rightarrow \Ob \mathcal E \) (called power object),
- a natural isomorphism \( \Sub _{\mathcal E}(-) \cong \Hom _{\mathcal E}(-, \Omega) \),
- a natural isomorphism \( \mathcal E(- \times B, \Omega) \cong \mathcal E(-,PB) \) for every object \( B \),
such that
- \( \mathcal E \) has all finite limits.
2. QUESTION Is there a more natural definition of a topos?
3. TODO Least Data Definition of a Topos
A (elementary) topos \( \mathcal E \) consists of
- a category \( \mathcal E \),
- a functor \( P \colon \mathcal E ^{op} \rightarrow \mathcal E \),
- a natural isormophism \( \Sub _{\mathcal E}(- \times B) \cong \mathcal E(-,PB) \) for every object \( B \),
such that
- \( \mathcal E \) has all finite limits.
4. Elementary Definition of a Topos
A (elementary) topos \( \mathcal E \) consists of
- a category \( \mathcal E \),
- a pullback for every diagram \( A \rightarrow X \leftarrow B \),
- a terminal object \( 1 \),
- an object \( \Omega \) (subobject classifier),
- a monomorphism \( \true \colon 1 \rightarrow \Omega \) (true element),
- for every object \( B \) a object \( PB \) and a morphism \( \epsilon _B \colon PB \times B \rightarrow \Omega \) (evaluation),
such that
- for every monomorphism \( f \colon A \rightarrow B \) there is a unique \( \char f \colon B \rightarrow \Omega \) such that
is a pullback diagram. Sometimes we just write \( \char A \) for \( \char f \) called the characteristic or classifiying map of \( f \),
for every morphism \( f \colon A \times B \rightarrow \Omega \) there is a unique morphism \( g \colon A \rightarrow PB \) such that
\begin{equation*} \xymatrix{ A \times B \ar[rd]^f \ar[d] _{\id _B \times \exists ! g} & \\ PB \times B \ar[r] _{\epsilon _B} & \Omega } \end{equation*}commutes.