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

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?

• It is "morally" true because $\Omega$ is a Heyting algebra, and $[\top,\perp]$ chooses its top and bottom. There can be nothing in the middle, so $\Omega$ is just 1+1=2, or there can be something, so $[\top,\perp]$ is an embedding (if $\Omega$ has at least two "elements", $0\ne 1$). May 6, 2021 at 9:40
• @fosco Nice! But how is it that the proof is so hard? It should be as clear as your comment May 6, 2021 at 9:46
• Well, the intuition makes use of elements. You don't have elements in a category (well, you do, but it's slightly more complicated than that). I'm writing a (sketchy) answer! Stay tuned! May 6, 2021 at 9:54
• Category theory offers the language of generalized elements, and they work pretty well. And they are just morphisms into the given object, not really complicated I would say. For example, a morphism $f : X \to Y$ is a monic iff for all generalized elements $a,b \in X$ of the same shape we have $f(a)=f(b) \iff a=b$. May 7, 2021 at 8:26

$$\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}$$

• Thanks a lot! I will try to understand and complete it and then accept May 6, 2021 at 10:26
• There are a couple of confusing steps, but unfortunately I have to go; the idea is that $u=v$ if and only if they coincide over the preimage of 1, if and only if they coincide over the preimage of 0; the equality $mu=mv$ implies the second condition (or the third, depends on who is the "1" mapped to true, and who is the "1" mapped to false). May 6, 2021 at 10:28
• Is $X\cong X_0 + X_1$ in general? Can you prove it? What are $X_{1,u}$ and $X_{1,v}$ ? May 6, 2021 at 13:37
• Why is the first square a pullback? May 6, 2021 at 13:41
• $m$ classifies the monic $i_0$, picking up $\top$ in $\{\top,\perp\}$ May 6, 2021 at 14:24

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.)