A topos is a categorical interpretation of boolean logic. We will start with some prerequisite set theory and category theory, build up the intuition for subobject classifiers, give an interpretation of set theory, and then move to formalizing boolean algebra using sheaves. The study of topoi is the study of cartesian-closed categories with subobject classifiers, and a category of sheaves over
Some set theoretic foundations
The study of set theory starts with the study of Russell's paradox, and axiomatization into Zermelo-Frankel set theory with no paradoxes. To understand Russell's paradox, we first introduce the principle of comprehension:
In ZF set theory, we say that a set can only be built up from another set using logical connectives like
In category theory, the central concept of membership of an element in a set is replaced by the concept of a morphism between objects whose internal structures (elements) are opaque.
Functions to elementary category theory
We would first like to ask how functions are formalized in terms of sets. A function
the relation. Note that functions are composable yielding a unique
We can further abstract functions to arrows between objects in a category. The notion of "set membership" is an "internal notion" between the various members of the object, and needs to be "externalized". Let's start with some category theory.
A pre-order is defined as a category in which there is at most one arrow,
Reflexivity: for each
, we have , the identity arrow.
and , we have .
The typical example is to think of two non-comparable subsets of a set. With identity arrows omitted, this looks like:
With one additional property described below, a pre-order becomes a partial ordering:
and , we have .
With one additional property, a partial ordering becomes a total ordering:
Connexity: For all
, , pRq or qRp.
This is a total order.
Let us now consider categories with more than one arrow between two objects. A monoid is defined as an algebraic structure
All objects of
are objects of .
; all arrows of are present in .
A full subcategory
Before introducing comma categories, let us briefly introduce arrow categories as a prerequisite. An arrow category
A comma category can be viewed as a special case of an arrow categories with fixed domain or codomain.
Similarly, we can define
Set membership, categorically
To work our way up to subobject classifiers, we need to build some prerequisite material. First, let us introduce the notion of monic and epic arrows, corresponding to injective and surjective functions in
In other words, a monic is said to be left-cancelable.
In other words, an epic is said to be right-cancelable.
An iso arrow, indicated as
Every iso is both monic and epic, but "iso" isn't equivalent to "monic and epic". Consider
An initial object
All initial objects are isomorphic to each other. By duality, all terminal objects are also isomorphic to each other.
By uniqueness of identity arrow,
By definition of product, since this diagram commutes,
The following diagram commutes:
For isomorphism, there needs to exist