An elementary topos is a category with finite limits, exponentials, and a subobject classifier $t:1\rightarrow\Omega$. We do not know from the definition that a topos has colimits. Surely we have theorems1 ensuring that a topos at least has finite colimits, but this is far from intuitive. We might ask for a more straightforward construction of certain colimits in a topos; we want more explicit expressions using limits, exponentials, and the subobject classifier. Thanks to online posts by Todd Trimble2, we have an intuitive way of constructing the initial object and coproducts. In the following, we focus on the construction of the initial object as a representative example of a colimit in a topos.
As already suggested in the proof of the Tripleability Theorem (which is used to prove that a topos has finite colimits), colimits such as the initial object can be realized in certain equalizers. Roughly speaking, taking exponentials allows us to get “larger” objects, and taking equalizers allows us to get “smaller” objects. Therefore, working with set-theoretic intuition, we might start by taking a certain equalizer, hoping the result serves as the initial object. However, this approach is too difficult to carry out: even though we have the equalizer and hope it is the initial object, where do we get the unique map from this equalizer to any object in the topos?
Therefore, we need a more systematic approach to solve this problem. The idea is to construct a so-called internal intersection operation, and then take the “intersection of all subsets” to get the desired initial object. We will work with set-theoretic intuition, and, for example, we imagine subobjects as subsets.
More precisely, for any object $X$, we construct a morphism $PPX \xrightarrow{\bigcap} PX$. Here, $PX$ is a shorthand for $\Omega^X$, and similarly $PPX$ is a shorthand for $\Omega^{\Omega^X}$. Intuitively, we imagine $\Omega$ as an object of truth values, and $PX$ is the collection of subsets of $X$, and $PPX$ is the collection of all sets of subsets of $X$, and $\bigcap:PPX \rightarrow PX$ is like, given any set of subsets of $X$, we take the intersection of them, and the intersection is a subset of $X$. Once we have such a morphism, we will be able to take the intersection of all subsets of $X$, then hopefully this intersection will act as the initial object.
So the issue is how we construct the morphism $\bigcap:PPX\rightarrow PX$ with our bare hands. To proceed, we first need to develop some logical symbols within the topos. Why do we need logical symbols? Because they help us understand what we are constructing, and they indicate the properties that certain constructions have. Indeed, the only logical symbols we need are $\land$, $\Rightarrow$, and $\forall_A$. Luckily, unlike other logical symbols such as $\lor$, these three logical symbols are easy to construct in a topos, meaning that within a few steps of construction using finite limits, exponentials and subobject classifier, we will be able to have them.
The details of constructing them are irrelevant here. We only summarize the important properties they have. Fix an object $X$. When speaking of subobjects of $X$, we imagine they are subsets of $X$. We will use the letters $M$, $N$, and $K$ for subobjects of $X$.
-
$\land$, or $\cap$: For subobjects $M$ and $N$, the intersection of $M$ and $N$ is written as $M\cap N$. We have that if $K\leq M$ and $K\leq N$, then $K\leq M\cap N$. As this property suggests, we know that $M\cap N$ can be gotten by taking pullbacks.
-
$\Rightarrow$: We have the implication $M\Rightarrow N$ for any $M,N$. Then for any $K$, we have that $K\cap M\leq N$ if and only if $K\leq M\Rightarrow N$.
-
$\forall_A$: For another object $A$, we consider the product $X \times A$. We imagine subobjects of $X \times A$ as subsets of the product $X \times A$. So given any such subobject $Z \subseteq X \times A$, intuitively, we can collect those $x \in X$ such that for every $a \in A$, we have $(x,a) \in Z$. We write the resulting subobject of $X$ as $\forall_A.Z$. The property we expect from $\forall_A$ is the following: for any subobject $M$ of $X$ and any subobject $Z$ of $X \times A$, we have $M \times A \leq Z$ if and only if $M \leq \forall_A.Z$.
We still need some internal set-theoretic notions before constructing the map $\bigcap:PPX \rightarrow PX$. Indeed, we can reason about the $\in$-relation. For any object $X$, $\in_X$ is a subobject of $X \times PX$, and again, intuitively, it collects the pairs $(x,A)$, where $x$ is an element of $X$, $A$ is a subset of $X$, and $x\in A$.
Now, we have all the ingredients for constructing the map $\bigcap:PPX \rightarrow PX$. Intuitively, any element of $PPX$ is a set of subsets of $X$; we write it as $F$. Then what is the intersection $\bigcap F$? It is the set of all $x \in X$ satisfying the property that for any subset $B$ of $X$, if $B$ is in $F$, then $x$ is in $B$. Writing this compactly, it is characterized by $\forall B \in PX.(B \in F \Rightarrow x \in B)$. So we imagine that this formula gives us a subset of $PPX \times X$, which are pairs $(F,x)$ that satisfy the property $\forall B \in PX.(B \in F \Rightarrow x \in B)$. Finally, we know that a subobject of $PPX \times X$ corresponds to a map $PPX \rightarrow \Omega^X$, i.e., a map $PPX \rightarrow PX$, which is the desired internal intersection map.
Although we have omitted most technical details, let us now complete the argument. From some easy observations, we can show that if $F$ and $G$ are subobjects of $PX$, and if $F \leq G$, then we have $\bigcap G \leq \bigcap F$.
One more important property, which, to my knowledge, is not mentioned in the posts of Todd, is that the composition $PX \xrightarrow{\{\cdot\}} PPX \xrightarrow{\bigcap} PX$ is the same as the identity. Here, the map $\{\cdot\}: PX \rightarrow PPX$ is like given any element $M$ in $PX$, we get an element $\{M\}$ in $PPX$. The intuition is clear: $\bigcap\{M\}=M$.
Finally, with all the observations above, we know that:
-
For any $X$, write $0_X$ to be the intersection of “all subsets of $X$”. We can show that $0_X$ is the smallest subobject of $X$. Then if $M$ is a subobject of $X$, then $0_M$ is isomorphic to $0_X$.
-
Now, for any object $X$, we know there is always a monomorphism $1 \rightarrow PX$, which picks the object $X$ as a subobject of itself. Then we know $0_1$ is isomorphic to $0_{PX}$. We also know that $0_X$ is isomorphic to $0_{PX}$, since via the singleton map $\{\cdot\} : X \rightarrow PX$, we know $X$ can be viewed as a subobject of $PX$. We thus get the map $0_1 \rightarrow X$.
-
To show that maps from $0_1$ to any $X$ is unique: take equalizer!
Thus, we have a concrete construction of the initial object. With the internal intersection, one can also construct coproducts concretely. Again, the idea is that we can always take exponentials to go “up”, and then take certain intersections, etc., to go “down.” However, how to construct coequalizers in this fashion is unclear to me at the moment, and I suspect it will not be as economical as in the case of finite coproducts.
In conclusion, I am satisfied to have found an intuitive and straightforward construction of the initial object in a topos. While the above discussion offers nothing essentially new to the subject, and may even be too limited when it comes to constructing more complicated structures, perhaps the point I want to make is this: although there are powerful theorems guaranteeing the existence of certain structures, it is sometimes enjoyable, and maybe even inspiring, to find a more direct construction, as we did here with the initial object.
Bibliography
contributors, nLab. 2021. “Trimble on ETCS III.” 2021. ncatlab.org/nlab/show/Trimble+on+ETCS+III .
Trimble, Todd. 2008. “ETCS: Internalizing the Logic.” 2008. https://topologicalmusings.wordpress.com/2008/09/10/etcs-internalizing-the-logic/ .