Question about equivalence relation defining integers in an elementary topos - MathOverflow most recent 30 from http://mathoverflow.net2013-05-23T18:05:28Zhttp://mathoverflow.net/feeds/question/40789http://www.creativecommons.org/licenses/by-nc/2.5/rdfhttp://mathoverflow.net/questions/40789/question-about-equivalence-relation-defining-integers-in-an-elementary-toposQuestion about equivalence relation defining integers in an elementary toposPhil Wild2010-10-01T20:29:48Z2010-10-01T22:42:11Z
<p>Hi all,</p>
<p>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</p>
<p>$f_1 \equiv \left< p_1 a, p_2 b \right>$</p>
<p>$f_2 \equiv \left< p_1 b, p_2 a \right>$</p>
<p>(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}$.</p>
<p>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?</p>
<p>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.</p>
http://mathoverflow.net/questions/40789/question-about-equivalence-relation-defining-integers-in-an-elementary-topos/40799#40799Answer by Todd Trimble for Question about equivalence relation defining integers in an elementary toposTodd Trimble2010-10-01T22:42:11Z2010-10-01T22:42:11Z<p>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. </p>
<p>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 </p>
<p>$$\exists_{j \in M} m' + n + j = m + n' + j$$ </p>
<p>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 </p>
<p>$$m' + n = m + n'$$ </p>
<p>which is what you want. </p>
<p>We thus need to show </p>
<p>$$\forall_{j \in \mathbb{N}} ((x + j = y + j) \Rightarrow (x = y))$$ </p>
<p>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}$). </p>