Lex total categories and Grothendieck toposes IV

Previous post in this series; next post.

The aim of this post is to complete the proof that well-powered lex total categories are elementary toposes, by proving that they have subobject classifiers.


But first let's do something simpler, namely prove that a total category ${\bf A}$ has a terminal object. (We will use the same strategy later for constructing the subobject classifier of a well-powered lex total category.)

$\bf Terminal\; object$

It is clear that ${\bf A}$ has a terminal object iff the constant functor ${\bf A}^{op}\to Sets: A\mapsto 1$ is representable; its representing object is a terminal object.  Further, in general, the colimit of a representable functor considered as a discrete fibration is the representing object. But the constant functor considered as a discrete fibration over ${\bf A}$ is the identity functor $1_{\bf A}:{\bf A}\to {\bf A}$ which has small fibres and so we can form $colim(1_{\bf A})$, which we write informally as $colim_{A\in {\bf A}}A$ and also $Q$ for short. We claim that this object is the terminal object of ${\bf A}$.

Denote the universal cocone from $1_{\bf A}$ to $Q$ as $\lambda_A:A\to Q \; (A\in {\bf A})$. The $\lambda_A$ provide the existence of arrows from each object to $Q$; what remains to show is the uniqueness. Notice that for each $f:A\to Q$ we have the cocone property $\lambda_{Q}f=\lambda_A$, so in particular taking $f=\lambda_A:A\to Q$ we have $\lambda_Q\lambda_A=\lambda_A=1_A\lambda_A$. By the uniqueness property of the universal cocone this implies that $\lambda_Q=1_Q$. Then returning to the equation $\lambda_{Q}f=\lambda_A$ we see that $f=\lambda_A$ for any $f:A\to Q$, the uniqueness.

It is clear, by the way, that a similar argument shows that totally cocomplete categories have all small limits.

$\bf Subobject\; classifier$

We want to do the same thing now representing a different functor $sub:{\bf A}^{op}\to Sets:A\mapsto sub(A)$ where $sub(A)$ is the set of subojects of $A$ which is small by assumption. We will denote the subobject of $A$ containing the mono $U\to A$ as $[U\to A]$ or just $[U]$. The effect of $sub$ on arrow $f:A\to B$ is $[U\to B]\mapsto [f^{-1}(U)]$. To obtain the subobject classifier we take the colimit of the corresponding fibration which we denote as $colim_{[U\to A]}A$ or more briefly as $\Omega$. Denote the universal cocone of the colimit as $\lambda_{[U\to A]}:A\to \Omega$ $(A\in {\bf A})$. Let $I$ be the terminal object of ${\bf A}$, and denote $\lambda_{[1_I:I\to I]}:I\to \Omega$ as $true:I\to \Omega$.

Now to show that $\Omega$ is the subobject classifier we will prove (i) that given any $U\to A$ then the pullback of $true:I\to \Omega$ along $\lambda_{[U\to A]}:A\to \Omega$ is $U\to A$, and (ii) if $f:A\to \Omega$ satisfies $f^{-1}(true)=U\to A$ then $f=\lambda_{[U\to A]}:A\to \Omega$. Now (i) requires the left exactness of colimit, and we shall delay proving (i).

First assuming (i) we will prove (ii).
Consider $f:A\to \Omega$ such that $f^{-1}(true)=U\to A$. Then $f$ is a morphism from $(A,[U])$ to $(\Omega,[true])$ in the domain of the fibration $sub$ and hence we have the equation (*) $\lambda_{true}f=\lambda_{[U]}$. Assuming (i) we may put $f=\lambda_{[U]}$ in this equation to yield $\lambda_{true}\lambda_{[U]}=\lambda_{[U]}=1_{\Omega}\lambda_{[U]}$. The uniqueness property of the universal cocone implies that $\lambda_{true}=1_{\Omega}$. Substituting this in (*) we obtain $f=\lambda_{[U]}$.

Now to prove (i).
I am getting tired so I will just state the necessary facts and leave you to check them.
Consider mono $U\to A$. Consider the following arrows in $Sets^{{\bf A}^{[op]}}$: (i) $Hom(-,A)\to sub:1_A\mapsto [U]$, (ii) $Hom(-,I)\to sub:1_A\mapsto [1_I]$. It is easy to check that the pullback of these two arrows is $Hom(-,U)$ with the obvious projections. It is a little less easy to check, but straightforward, that $colim$ applied to this pullback diagram gives exactly the diagram we wish to show a pullback. Since $colim$ preserves finite limits we have the desired result.

$\bf Note$
I just realized that the first statement that well-powered lex total categories are elementary toposes was made in my lecture to The Isle of Thorns conference , July 25-31, 1976 entitled Total Cocompleteness.