Logical disjunction in elementary toposes

Question

I'm following Goldbaltt's Topoi: The categorial analysis of logic. I use this book's notation, but it is quite standard.

At some point, he defines disjunction as the morphism $$\curlyvee:\Omega\times\Omega\longrightarrow\Omega$$ which is the character of the image of the morphism $$w=[\langle\top_\Omega,\mathbf{1}_{\Omega}\rangle,\langle\mathbf{1}_\Omega,\top_\Omega\rangle]:\Omega+\Omega\longrightarrow\Omega\times\Omega$$ Using the epi-mono factorization $$w=\text{im}(w)w^*:\Omega+\Omega\to w(\Omega+\Omega)\to\Omega\times\Omega$$ I have managed to prove that $$\top\curlyvee\top = \curlyvee\langle\top,\top\rangle=\curlyvee\langle\top !_\Omega\top,\mathbf{1}_\Omega\top\rangle=\curlyvee\langle\top !_\Omega,\mathbf{1}_\Omega\rangle\top=\curlyvee wi_1\top=$$ $$=\curlyvee\text{im}(w)w^*i_1\top=\top!_{w(\Omega+\Omega)}w^*i_1\top=\top!_{\Omega+\Omega}i_1\top=\top !_\Omega\top=\top$$ And similary, using $\curlyvee\text{im}(w)w^*i_1\bot$ and $\curlyvee\text{im}(w)w^*i_2\bot$ it can be proven that $$\top\curlyvee\bot=\bot\curlyvee\top = \top$$

I'm having lots of trouble proving that $\bot\curlyvee\bot = \bot$. Goldblatt himself leaves this unproven until much later in the book, after he has developed other tools to work with truth values. However I would like a diagram-chasing proof that doesn't require introducing new definitions and lemmas.

I've already tried many things (and failed): trying to replicate a proof from the topos of sets, trying to use the universal property of the image of $w$ together with the $\Omega$-axiom...

Whatever I try, I can't complete the diagram with the key morphism.

Is it possible to find the proof I'm looking for? Thanks in advance!

Answer 1

Unfortunately, I was not able to find a direct series of computations as you were asking for. However, I did find an argument that hopefully is reasonably elementary.

First, considering the monomorphism $(\bot, \bot) : 1 \to \Omega \times \Omega$, observe that since $(\bot_\Omega, 1_\Omega) : \Omega \to \Omega \times \Omega$ is the pullback of $\bot : 1 \to \Omega$ along $\pi_1 : \Omega\times\Omega \to \Omega$, we have $$\chi_{(\bot,\bot)} \circ (\top_\Omega, 1_\Omega) \le \chi_{(\bot_\Omega, 1_\Omega)} \circ (\top_\Omega, 1_\Omega) = \chi_\bot \circ \pi_1 \circ (\top_\Omega, 1_\Omega) = \chi_\bot \circ \top \circ {!}_\Omega = \bot !_\Omega.$$ Now, since $\bot !_\Omega$ is the minimum element of $\operatorname{Hom}(\Omega, \Omega)$, we conclude that $\chi_{(\bot,\bot)} \circ (\top_\Omega, 1_\Omega) = \bot !_\Omega$. A similar argument, using $\pi_2$ in place of $\pi_1$, shows that $\chi_{(\bot,\bot)} \circ (1_\Omega, \top_\Omega) = \bot !_\Omega$ also. Therefore, $\chi_{(\bot,\bot)} \circ w = \bot !_{\Omega+\Omega}$.

Now, since $\bar w$ is an epimorphism, we get that $\chi_{(\bot,\bot)} \circ \operatorname{im} (w) = \bot !_{w(\Omega\times\Omega)}$. As a result, we have a pullback diagram $$\require{AMScd}\begin{CD} 0 @>>> w(\Omega\times\Omega) \\ @VVV @VV \operatorname{im}(w) V \\ 1 @> (\bot,\bot) >> \Omega\times\Omega. \end{CD}$$ Now flipping this diagram and reading it the other way, we can conclude that $\curlyvee \circ (\bot,\bot) = \chi_{\operatorname{im}(w)} \circ (\bot,\bot) = \bot$.

Answer 2

For those interested, I post here what I've worked out.

Thanks to the great answer by Daniel Schelper I managed to get the type of proof I wanted by completing some (easily provable) details:

1. In an elementary topos (more generally a cartesian-closed category) it is true that every morphism $f:x\to \mathbf{0}$ is iso, so that $x\cong\mathbf{0}$

2. For all objects $x$, it is true that $$\chi_{\mathbf{0}_x}=\bot !_x$$

3. If $\top !_x=\bot !_x$, then $x\cong \mathbf{0}$

4. $[\mathbf{0}_x]$ is the minimum of $\text{Sub}_\mathbf{C}(x)$ for any object $x$

and at least 6 rather simple observations (which I made in spanish for my own notes on the subject, but shouldn't be difficult to translate):