Satisfaction of Peano postulates in topos with natural numbers object

Solution 1:

Let's consider the internalisation of this statement. In other words, consider the meaning of the statement $\forall n \in N (Sn \neq 0)$ in the internal logic of the topos. Your version of the internalisation is technically equivalent to the correct version, but there's an even simpler version: that the pullback of $z : 1 \to N$ and $s : N \to N$ is $0$. It's easy to verify that this is equivalent to your version.

Note that in set theory, the statement that the pullback of $z$ and $s$ is $0$ is equivalent to saying that $\{(x, y) \mid x \in 1, y \in N, zx = sy\} = \emptyset$. In other words, there is no $y$ such that $sy = 0$.

Generally, we prove something even stronger; that $(N, z, s)$ is the coproduct of $1$ and $N$.

To do this, we consider the coproduct $1 + N$ of $1$ and $N$ with injections $i_1 : 1 \to N$, $i_N : N \to N$. We then explicitly construct an isomorphism $1 + N \to N$ and its inverse $N \to 1 + N$.

To construct the map $f : 1 + N \to N$, we simply take the $f$ such that $f \circ i_1 = z$, $f \circ i_2 = s$.

To construct the inverse map, first define $s' : 1 + N \to 1 + N$ such that $s' \circ i_1 = i_2 \circ z$ and $s' \circ i_2 = i_2 \circ s$. For convenience, let $z' = i_1$. We then take the unique $g : N \to 1 + N$ such that $g \circ z = z'$ and $g \circ s = s' \circ g$.

We will now show that $g \circ f = 1_{1 + N}$. To do this, it suffices to show that $g \circ f \circ i_j = i_j$ for $j = 1, 2$.

First, I claim that $g \circ f \circ i_2 = i_2$. To do this, we first rewrite $g \circ f \circ i_2 = g \circ s = s' \circ g$. Now note that $s' \circ g \circ z = s' \circ z' = s' \circ i_1 = i_2 \circ z$. And also note that $s' \circ g \circ s = s' \circ s' \circ g$. We also have $i_2 \circ z = i_2 \circ z$ and $i_2 \circ s = s' \circ i_2$, so by the universal property of the NNO, we have $s' \circ g = i_2$ as required.

Now, note that $g \circ f \circ i_1 = g \circ z = z' = i_1$. Therefore, we may indeed conclude that $g \circ f = 1_{1 + N}$.

I conversely claim that $f \circ g = 1_N$. To do this, it suffices to show that $f \circ g \circ z = z$ and that $f \circ g \circ s = s \circ f \circ g$ and then cite the universal property of the NNO.

For the first part of this, we see clearly that $f \circ g \circ z = f \circ z' = f \circ i_1 = z$.

For the second part, we first show that $f \circ s' = s \circ f$. To do this, note that $f \circ s' \circ i_1 = f \circ i_2 \circ z = s \circ z = s \circ f \circ i_1$. And note that $f \circ s' \circ i_2 = f \circ i_2 \circ s = s \circ s = s \circ f \circ i_2$. Apply the universal property of the coproduct to conclude that $f \circ s' = s \circ f$.

Now, we note that $f \circ g \circ s = f \circ s' \circ g = s \circ f \circ g$.

So we indeed see that $f$ and $g$ are inverse isomorphisms $1 + N \cong N$. Furthermore, we see that $f \circ i_1 = z$ and $f \circ i_2 = s$, so therefore $(N, z, s)$ is a coproduct.

To finish the proof, we then cite the fact that in a topos, the injection maps for a coproduct are disjoint (see eg. Sheaves in Geometry and Logic Corollary IV.10.3). This shows us that $0$ is indeed the pullback of $z$ and $s$.

Note that this proof also gives you another Peano axiom for free. For we can conclude from here that since $s$ is a coproduct injection, it must be mono (again citing Corollary IV.10.3 which also states that coproduct injections are mono). And $s$ being mono is exactly the internalisation of the claim that $\forall n, m \in N (sn = sm \to n = m)$.