Proof that $[\top,\bot]$ is monic

Question

Let $\mathbf{C}$ be an elementary topos with $\top:\mathbf{1}\to\Omega$ as its subobject. Now, $\mathbf{C}$ is called $\textit{classical}$ if $[\top,\bot]:\mathbf{1}+\mathbf{1}\to\Omega$ is an iso arrow, where $\bot:\mathbf{1}\to\Omega$ is the character of the unique arrow $\mathbf{0}\to\mathbf{1}$.

In $\textit{Topoi: The categorial analysis of logic}$, by Goldblatt, it is stated that $[\top,\bot]$ is always monic. However, the proof rests on some corolaries of the Fundamental Theorem of Topos Theory and so is quite difficult to write. Is there a "simple" and direct proof? If not, why should I believe this result? Why is it "morally" true?

Answer 1

$\require{AMScd}$Let's prove that $m=[\top,\perp]$ is monic by trying to deduce that if $m\circ u = m\circ v$ then $u=v$, in the diagram

$$ \begin{CD} X @>u>> 1+1 \\ @VvVV @VVmV \\1+1 @>>m> \Omega\end{CD}$$

First, observe that every map $X\to 1+1$ splits its domain into two disjoint subobjects $X_0, X_1$, obtained as preimages of 0 and 1 (this is still at an intuitive level; you can characterise both via their classifying maps, see below; but you're using a topos-theoretic property, i.e. the fact that in a topos coproducts are disjoint). So, it suffices to show that $u|_{X_1}=v|_{X_1}$ holds (again, the notion of restriction is guided by intuition: $u|_{X_1} := u\circ j_1$ where $j_1 : X_1 \to X$ is the inclusion).

Now, you obtain that $u\circ j_1=v\circ j_1$ from the fact that the following three diagrams are pullbacks:

$$ \begin{CD} 1 @= 1 \\ @Vi_0VV @VV\top V \\1+1 @>>m> \Omega\end{CD}$$

$$ \begin{CD} X_{1,u} @>>> 1 \\ @VjVV @VVi_0V \\ X @>>u> 1+1\end{CD}$$

$$ \begin{CD} X_{1,v} @>>> 1 \\ @VjVV @VVi_0V \\ X @>>v> 1+1\end{CD}$$

Answer 2

This is fairly straightforward to prove using the internal language of a topos. Namely, in the proof language, suppose we have $x, y : 1 + 1$ and $(\top, \bot)(x) = (\top, \bot)(y) \mathrm{~true}$ in the context. Then by decomposition of $x$ and $y$, we can reduce to four cases according to whether $x = i_1[ () ]$ or $x = i_2[ () ]$, where $i_1, i_2 : 1 \to 1 + 1$ are the canonical maps and $() : 1$ denotes the unique element of the unit type, and similarly for $y$. In the "diagonal" cases $x = y = i_1[()]$ or $x = y = i_2[()]$, we have the desired conclusion $x = y \mathrm{~true}$. In the non-diagonal case $x = i_1[()]$ and $y = i_2[()]$ then the hypothesis $(\top, \bot)(x) = (\top, \bot)(y)$ reduces to $\top = \bot$. Thus, from ${=}E$ (elimination of equality, or substitution principle) applied to the axiom $\top \mathrm{~true}$, we conclude $\bot \mathrm{~true}$, and then using $\bot E$ (otherwise known as ex falso quodlibet) we can conclude $x = y \mathrm{~true}$. The other non-diagonal case $x = i_2[()]$ and $y = i_1[()]$ is similar. This gives a formal proof that $x : 1 + 1, y : 1 + 1, (\top, \bot)(x) = (\top, \bot)(y) \mathrm{~true} \vdash x = y \mathrm{~true}$.

Now, after a couple applications of ${\forall}I$ and ${\rightarrow}I$, we get a formal proof of $\vdash [\forall x, y : 1 + 1, (\top, \bot)(x) = (\top, \bot)(y) \rightarrow x = y] \mathrm{~true}$. It is a standard fact that the interpretation of this tautology gives that the morphism $(\top, \bot) : 1 + 1 \to \Omega$ is a monomorphism in any topos.

(If you unfold the proof of the validity of the internal language, the general outline of the resulting proof would be: suppose we have a test object $U$ and sections $x, y \in (1+1)(U)$ such that $(\top, \bot)(x) = (\top, \bot)(y)$. Then there exist objects $V_1, V_2$ with morphisms $\phi_i : V_i \to U$ such that $\phi_1^*(x) = i_1[()_{V_1}]$, $\phi_2^*(x) = i_2[()_{V_2}]$, and $(\phi_1, \phi_2) : V_1 + V_2 \to U$ is an epimorphism. And similarly, we can find $\psi_i : W_i \to U$ satisfying corresponding conditions for $y$. We now consider test objects $V_i \times_U W_j$, and eventually find $V_1 \times_U W_2$ and $V_2 \times_U W_1$ are initial objects, and so $V_1 \times_U W_1$ and $V_2 \times_U W_2$ cover $U$ epimorphically. And on both, $x = y$; since we had an epimorphic cover, we conclude that $x = y$ on $U$ as well.)