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?

  • 2
    $\begingroup$ 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$). $\endgroup$
    – fosco
    May 6, 2021 at 9:40
  • $\begingroup$ @fosco Nice! But how is it that the proof is so hard? It should be as clear as your comment $\endgroup$ May 6, 2021 at 9:46
  • $\begingroup$ 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! $\endgroup$
    – fosco
    May 6, 2021 at 9:54
  • $\begingroup$ 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$. $\endgroup$ May 7, 2021 at 8:26

2 Answers 2


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

  • $\begingroup$ Thanks a lot! I will try to understand and complete it and then accept $\endgroup$ May 6, 2021 at 10:26
  • $\begingroup$ 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). $\endgroup$
    – fosco
    May 6, 2021 at 10:28
  • $\begingroup$ Is $X\cong X_0 + X_1$ in general? Can you prove it? What are $X_{1,u}$ and $X_{1,v}$ ? $\endgroup$ May 6, 2021 at 13:37
  • $\begingroup$ Why is the first square a pullback? $\endgroup$ May 6, 2021 at 13:41
  • $\begingroup$ $m$ classifies the monic $i_0$, picking up $\top$ in $\{\top,\perp\}$ $\endgroup$
    – fosco
    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.)


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .