| Version 5 |
Version 4 |
| \PMlinkescapeword{categorical} |
\PMlinkescapeword{categorical} |
| \PMlinkescapeword{Boolean} |
\PMlinkescapeword{Boolean} |
|
|
| There are two related kinds of categories which are called \emph{topos}. First, there is the Grothendieck topos, which was developed by Grothendieck as part of his general reconstruction of algebraic geometry. Second, there is the elementary topos, which was introduced by Lawvere as a setting for work in categorical logic. We give a brief overview of each kind of topos. |
There are two related kinds of categories which are called \emph{topos}. First, there is the Grothendieck topos, which was developed by Grothendieck as part of his general reconstruction of algebraic geometry. Second, there is the elementary topos, which was introduced by Lawvere as a setting for work in categorical logic. We give a brief overview of each kind of topos. |
|
|
| A \emph{Grothendieck topos} is a category equivalent to the category of sheaves on some site. %(Stub definition...) |
A \emph{Grothendieck topos} is a category equivalent to the category of sheaves on some site. %(Stub definition...) |
|
|
| An \emph{elementary topos} is category $\mathcal{T}$ which: |
An \emph{elementary topos} is category $\mathcal{T}$ which: |
| \begin{itemize} |
\begin{itemize} |
| \item |
\item |
| is a Cartesian closed category; and |
is a Cartesian closed category; and |
|
|
| \item |
\item |
| has a representable subobject functor. |
has a representable subobject functor. |
| \end{itemize} |
\end{itemize} |
| The first assumption guarantees the existence of finite limits and colimits as well as power objects. This allows $\mathcal{T}$ to model basic constructions of set theory such as products, disjoint unions, intersections, and powersets. It also guarantees that $\mathcal{T}$ has a terminal object $1$, which corresponds to a singleton set in $\mathbf{Set}$. We can model elements of an object $A$ by morphisms $1\to A$. |
The first assumption guarantees the existence of finite limits and colimits as well as power objects. This allows $\mathcal{T}$ to model basic constructions of set theory such as products, disjoint unions, intersections, and powersets. It also guarantees that $\mathcal{T}$ has a terminal object $1$, which corresponds to a singleton set in $\mathbf{Set}$. We can model elements of an object $A$ by morphisms $1\to A$. |
|
|
| The second assumption means that $\mathcal{T}$ has a notion of ``truth''. In particular, $\mathcal{T}$ must have a \emph{truth object} $\Omega$ and a morphism $\top\colon 1\to\Omega$ such that if $m\colon A\to B$ is any monomorphism of $\mathcal{T}$, then there is a unique associated \emph{characteristic morphism} $\chi\colon B\to\Omega$ such that the diagram |
The second assumption means that $\mathcal{T}$ has a notion of ``truth''. In particular, $\mathcal{T}$ must have a \emph{truth object} $\Omega$ and a morphism $\top\colon 1\to\Omega$ such that if $m\colon A\to B$ is any monomorphism of $\mathcal{T}$, then there is a unique associated \emph{characteristic morphism} $\chi\colon B\to\Omega$ such that the diagram |
| \[\xymatrix{ |
\[\xymatrix{ |
| A\ar[d]_{m}\ar[r] & 1\ar[d]^{\top} \\ |
A\ar[d]_{m}\ar[r] & 1\ar[d]^{\top} \\ |
| B\ar[r]^{\chi} & \Omega |
B\ar[r]^{\chi} & \Omega |
| }\] |
}\] |
| is a pullback square. Speaking loosely, this says that a subobject of $B$ arises as a collection of elements of $B$ satisfying a particular predicate $\chi$. The converse of this assumption corresponds to the comprehension axiom of set theory and follows from Cartesian closedness. |
is a pullback square. Speaking loosely, this says that a subobject of $B$ arises as a collection of elements of $B$ satisfying a particular predicate $\chi$. The converse of this assumption corresponds to the comprehension axiom of set theory and follows from Cartesian closedness. |
|
|
| An elementary topos is a \emph{Boolean topos} if its truth object has exactly two elements, ``true'' $\top\colon 1\to\Omega$ and ``false'' $\bot\colon 1\to\Omega$. It \emph{has choice} (admits the axiom of choice) if every epimorphism is split. It is a fact that every elementary topos with choice is Boolean. Note that not every elementary topos has choice. So elementary topoi can be used to model intuitionistic logic. |
An elementary topos is a \emph{Boolean topos} if its truth object has exactly two elements, ``true'' $\top\colon 1\to\Omega$ and ``false'' $\bot\colon 1\to\Omega$. It \emph{has choice} (admits the axiom of choice) if every epimorphism is split. It is a fact that every elementary topos with choice is Boolean. Note that not every elementary topos has choice. So elementary topoi can be used to model intuitionistic logic. |
|
|
| The category of sets is the canonical example of a Boolean topos. |
The category of sets is the canonical example of a Boolean topos. |
|
|
| \begin{thebibliography}{99} |
\begin{thebibliography}{99} |
| \bibitem{BaWe} |
\bibitem{BaWe} |
| M.~Barr and C.~Wells. {\it Toposes, Triples and Theories}. Montreal: McGill University, 2000. |
M.~Barr and C.~Wells. {\it Toposes, Triples and Theories}. Montreal: McGill University, 2000. |
|
|
| \bibitem{LaSc} |
\bibitem{LaSc} |
| J.~Lambek and P.~J.~Scott. {\it Introduction to higher order categorical logic}. Cambridge University Press, 1986. |
J.~Lambek and P.~J.~Scott. {\it Introduction to higher order categorical logic}. Cambridge University Press, 1986. |
|
|
| \bibitem{Ma} |
\bibitem{Ma} |
| S.~Mac~Lane. {\it Categories for the Working Mathematician}, 2nd ed. Springer-Verlag, 1997 |
S.~Mac~Lane. {\it Categories for the Working Mathematician}, 2nd ed. Springer-Verlag, 1997 |
|
|
| \bibitem{MaMo} |
\bibitem{MaMo} |
| S.~Mac~Lane and I.~Moerdijk. {\it Sheaves and Geometry in Logic: A First Introduction to Topos Theory}, Springer-Verlag, 1992. |
S.~Mac~Lane and I.~Moerdijk. {\it Sheaves and Geometry in Logic: A First Introduction to Topos Theory}, Springer-Verlag, 1992. |
| \end{thebibliography} |
\end{thebibliography} |
