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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.