Question about equivalence relation defining integers in an elementary topos

Question

Hi all,

Let $\mathcal{E}$ be an elementary topos with natural number object $N$, and let $+: N \times N \to N$ be the the addition arrow; I expect that the nature of $N$ and $+$ will turn out to be irrelevant to my question, but if so they should at least make its motivation clear. Let $E$ be the pullback of $+$ along itself, with projections $p, q: E \to N \times N$; for example if $\mathcal{E}$ is the topos of sets then $E$ may simply be taken to be the set of quadruples $(n, m, n', m') \in N^4$ such that $n + m' = n' + m$, with $a(n, m, n', m') = (n, m')$, $b(n, m, n', m') = (n', m)$. Let $f_1, f_2: E \to N \times N$ be given by

$f_1 \equiv \left< p_1 a, p_2 b \right>$

$f_2 \equiv \left< p_1 b, p_2 a \right>$

(here $p_1, p_2: N \times N \to N$ are the projections and $\left< f, g \right>$ denotes the product arrow $X \to N \times N$ of arrows $f, g: X \to N$). For example in the topos of sets again, $f_1 (n, m, n', m') = (n, m)$ etc.. Let $c: N \times N \to Z$ be the coequaliser of $f_1$ and $f_2$, so $Z$ is the integer object in $\mathcal{E}$.

My question is: if $g, h, g', h': X \to N$ are such that $c \left< g, h \right> = c \left< g', h' \right>$, is it always the case that $+ \left< g, h' \right> = + \left< g', h \right>$? Equivalently, is $E$ with the arrows $f_1$, $f_2$ the pullback of $c$ along itself?

I've spent a while trying to prove it is but I just keep going round in circles, so any hints will be much appreciated.

Answer 1

I think what you want first is a lemma that $\mathbb{N}$ is a cancellative monoid (which is the case in any topos). Just think about how you would prove your statement in the category of sets using ordinary elements, and I think it will become clear.

The usual construction of the left adjoint to the forgetful functor from abelian groups to abelian monoids involves the observation that, for $m, n, m', n'$ in an abelian monoid $M$, the relation

$$\exists_{j \in M} m' + n + j = m + n' + j$$

defines an equivalence relation $\langle m, n \rangle \sim \langle m', n' \rangle$ on $M \times M$. (Only transitivity need be checked.) Cancellation means that from this we can infer

$$m' + n = m + n'$$

which is what you want.

We thus need to show

$$\forall_{j \in \mathbb{N}} ((x + j = y + j) \Rightarrow (x = y))$$

in the natural numbers object. This is done by induction on $j$ (the subobject of such $j$ contains 0 and ... and therefore is all of $\mathbb{N}$).