Comma category of a topos
It is an amazing fact that if $\mathscr E$ is an elementary topos and $a$ is an object of $\mathscr E$, then the comma category $\mathscr E\downarrow a$ is also an elementary topos. In this note, I'll attempt to build up some of the pieces needed for this proof.
Proposition 1. A comma category $\mathsf C\downarrow a$ always has a terminal object, namely $1_a:a\to a$.
Proof. A morphism $\alpha$ between the $\mathsf C\downarrow a$-objects $f:a'\to a$ and $1_a:a\to a$ consists of a morphism $\alpha$ of $\mathsf C$ making the following diagram commute:
However, if this diagram commutes, we must have $1_a\alpha=\alpha=f$, meaning that $\alpha$ is uniquely determined and $1_a$ is terminal. $\blacksquare$
Proposition 2. If $\mathsf C$ is a category with pullbacks , then a comma category $\mathsf C\downarrow a$ always has pullbacks.
Proof. Suppose we have the following $\mathsf C\downarrow a$-objects: as well as the following $\mathsf C\downarrow a$-morphisms: which can be assembled into the following diagram:
The pullback of $\alpha$ and $\beta$ in $\mathsf C\downarrow a$ can be determined by pulling back $\alpha$ and $\beta$ in $\mathsf C$ and using the common composite arrow $f_w = f_y\delta=f_z\beta\delta=f_z\alpha\gamma=f_x\gamma$ as the $\mathsf C\downarrow a$-object that is the pullback of $\alpha$ and $\beta$, like this:
For if there is any third $\mathsf C\downarrow a$-object $f_{w'}:w'\to a$ with $\gamma':f_{w'}\to f_x$ and $\delta':f_{w'}\to f_y$ making an outer square commute in $\mathsf C\downarrow a$, then $\gamma':w'\to x$ and $\delta':w'\to y$ make an outer square commute in $\mathsf C$, meaning that we have a unique morphism $w'\to w$ making the entire diagram commute, which extends to a unique morphism of $\mathsf C\downarrow a$ making the diagram commute. Hence, we have that $f_w$ comprises a pullback of as desired. $\blacksquare$
Proposition 3. If $\mathsf C$ has products, a terminal object and a subobject classifier , then any comma category $\mathsf C\downarrow a$ also has a subobject classifier.
Proof. To find a subobject classifier, we seek a $\mathsf C\downarrow a$-object $\omega:\Omega'\to a$ and a $\mathsf C\downarrow a$-morphism $\top':1_a\to \omega$ such that for any monic $\alpha:f_w\to f_x$, there exists a unique $\chi'_\alpha$ making the following a pullback square:
We claim that the following choices of $\Omega',\omega,\top'$ accomplish this: and further, given specific values of $f_w:w\to a$ and $f_x:x\to a$ and monic $\alpha:f_w\to f_x$, the characteristic morphism $\chi'\alpha$ is given by which is a valid construction because $\alpha$ being monic in the comma category implies that it is also a monic arrow in the original category $\mathsf C$. Clearly this choice of $\chi'\alpha$ makes the diagram commute (okay, maybe it's not clear, but it can be checked with a bit of patience), so now we just need to verify that it makes the above a pullback square, and that it is the unique $\mathsf C\downarrow a$-morphism accomplishing this. The fact that it is in fact a pullback square follows from the fact that taking the second projection of $\Omega'$ yields a pullback square (due to the nature of the subobject classifier in $\mathsf C$):
Finally, the fact that $\chi'\alpha$ is uniquely determined to make this a pullback square follows from the fact that its second component $\chi\alpha$ is uniquely determined (again, because of how the subobject classifier works in $\mathsf C$), and there is only one choice of a first component capable of making the following subdiagram commute:
In particular, we must have $\text{pr}1\circ \chi'\alpha = f_x$, meaning that the first component of $\chi'_\alpha$ must equal $f_x$, making it uniquely determined as claimed. Thus, we have procured a subobject classifier in the comma category $\mathsf C\downarrow a$ as we intended. $\blacksquare$
For me, there's a particularly enlightening way of interpreting the above proposition in the context of $\mathsf{Set}$. Given a set $c$, we may interpret the comma category $\mathsf C\downarrow c$ as a category of "colored sets" in which the elements of $c$ are "colors" and each element of a set is "colored" by one of them; further, morphisms in this category are required to be color-preserving. We can then interpret each of the pieces of the subobject classifier as follows:
-
$1_c:c\to c$ is a set with precisely one object of each color.
-
The unique color-preserving function $!~ :w\to c$ sends each element of $w$ to the unique element of $c$ of that color.
-
$\alpha:w\to x$, being monic, must induce a monic mapping of the elements of $w$ of each particular color to the elements of $x$ of that color.
-
$\omega:\Omega'\to c$ represents a set with precisely two objects of each color, one called "true" and the other "false".
-
$\top':1_c\to\omega$ sends each element of $c$ to the "true" object of the same color in $\omega$.
-
Finally, $\chi'_\alpha$ sends each element of $x$ to the unique element of $\omega$ with the same color and a truth value corresponding to whether that element is in the image of $\alpha$ or not.