Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

I am currently trying to prove an exercise from Sheaves in Geometry and Logic: A First Introduction to Topos Theory by Mac Lane and Moerdijk about natural numbers objects.

First, we have the following definition:

Definition. A natural numbers object in a topos $\mathcal E$ is an object $N$ with arrows $$ 1\overset 0 \longrightarrow N \overset s \longrightarrow N $$ such that for any object $X$ of $\mathcal E$ with arrows $x$ and $f$, as below, there is a unique arrow $h$ which makes the following diagram commute: $$ \begin{array}{cclcl} 1 & \overset 0 \longrightarrow & N & \overset s \longrightarrow & N \\ || & & \downarrow h & & \downarrow h \\ 1 & \underset x \longrightarrow & X & \underset f \longrightarrow & X. \end{array} $$

Next, the exercise in question is as follows:

Exercise. Let $N$, with arrows $0:1\to N$ and $s:N\to N$, be a natural numbers object in a topos $\mathcal E$. Prove that the following form of recursion "in a parameter": for objects $X$ and $Y$ of $\mathcal E$ and maps $g:X\to Y$ and $h:Y\times X\to Y$, there is a unique $f:N\times X\to Y$ such that the following diagrams commute: $$ \begin{array}{ccccclcc} \phantom{\cong}1\times X & \overset{0\times\mathrm{id}}\longrightarrow & N\times X\phantom{f} & & \phantom{(f,\pi_2)}N\times X & \overset{s\times\mathrm{id}}\longrightarrow & N\times X \\ \cong\downarrow & & \downarrow f && (f,\pi_2)\downarrow && \downarrow f \\ \phantom{\cong}X & \underset g \longrightarrow & Y \phantom{f!} && \phantom{(f,\pi_2)}Y\times X & \underset h \longrightarrow & Y. \phantom{f} \end{array} $$ [In $\mathbf{Sets}$, this would mean that $f$ is the function defined by $f(0,x)=g(x)$, $f(n+1,x)=h(f(n,x),x)$.]

Now, the proof is very straightforward in $\mathbf{Sets}$, but I can't figure it out for a general topos. It seems like there should be some sort of exponential/adjunction argument, but I'm not getting it. I hope I'm not missing anything obvious!

I'm looking forward to peoples' responses. Thanks in advance!


Edit (2013-03-24): For completeness, I decided to include my proof of the exercise that works in $\mathbf{Sets}$.

Proof. Let $N$ be a natural numbers object in $\mathbf{Sets}$ (with the necessary functions $0:1\to N$ and $s:N\to N$), let $X$ and $Y$ be sets, and let $$ g: X \to Y \qquad\text{and}\qquad h : Y \times X \to Y $$ be functions. We wish to show that there exists a unique function $f:N\times X\to Y$ such that $$ f(0,x) = g(x) \qquad\text{and}\qquad f(n+1,x) = h(f(n,x),x) $$ for all $n\in N$ and $x\in X$.

Given $x\in X$, define $h_x:Y\to Y$ by $h_x(y)=h(y,x)$ (this implicitly uses the $$ \mathrm{Hom}_{\mathbf{Sets}}(Y\times X,Y) \cong \mathrm{Hom}_{\mathbf{Sets}}(X, Y^Y) $$ adjunction). Then for each $x\in X$ we have a diagram $$ 1 \overset{g(x)} \longrightarrow Y \overset{h_x} \longrightarrow Y $$ which induces a unique arrow $f_x:N\to Y$ such that the following diagram commutes: $$ \begin{array}{cclcl} 1 & \overset 0 \longrightarrow & N & \overset s \longrightarrow & N \\ || & & \downarrow f_x & & \downarrow f_x \\ 1 & \underset{g(x)} \longrightarrow & Y & \underset {h_x} \longrightarrow & Y. \end{array} $$ Then we define $f:N\times X\to Y$ by $f(n,x)=f_x(n)$, and it is easy to see that this $f$ satisfies the desired properties and is unique.

This is the proof that I am struggling to generalize. Maybe this is the wrong approach altogether for a general proof, although I feel like it should generalize. Any help would be greatly appreciated.

share|improve this question
2  
Insta +1 for all the work in the question. –  Git Gud Mar 18 '13 at 21:10
    
Generally speaking, a proof in $\textbf{Set}$ will translate to a proof in a general topos once it is written out explicitly in terms of arrows and universal properties, provided it is constructive. Contextual parameters are treated using the exponential adjunction. –  Zhen Lin Mar 19 '13 at 0:43
add comment

2 Answers

up vote 2 down vote accepted

Your struggles, I think, are that the definition of a NNO is given externally; but a direct translation of your proof requires an internal version in the form of a map $r:Y \times Y^Y \to Y^N$ that takes a "generalized element" of $Y$ and a "generalized map" from $Y$ to $Y$ and produces a "generalized map" $N \to Y$.

Set theoretically, this map would be given by

$$ r(y,h)(n) = k^{(n)}(y) $$

where $k^{(n)}$ is the $n$-fold iterate of $k$.

If we have this map $r$, then your argument is constructing the map $X \to Y \times Y^Y \to Y^N$, which you transpose to get $f$. (phrase things in terms of generalized elements if you like)

In the interest of preserving the specific argument you wish to make, let's see if we can construct $r$.

There are lots of ways we can rewrite things with natural isomorphisms. This one seems most promising to me:

$$ \hom(Y \times Y^Y, Y^N) \cong \hom(N \times Y \times Y^Y, Y) \cong \hom(N, Y^{Y \times Y^Y}) $$

Set theoretically, $r$ would correspond to the map

$$ n \mapsto \left( (y,k) \mapsto k^{(n)}(y) \right) $$

This one is promising, because it looks like I can define this one by recursion! If I attach $k$ to the output so that I can "remember" it, I can recursively define a function $s_n$ by:

  • $s_0(y,k) = (y,k)$
  • $s_{n+1}(y,k) = (k(y), k)$

So we set up the corresponding diagram

$$1 \to (Y \times Y^Y)^{Y \times Y^Y} \to (Y \times Y^Y)^{Y \times Y^Y}$$

Obtain

$$N \to (Y \times Y^Y)^{Y \times Y^Y} $$

Then convert to

$$ N \times Y \times Y^Y \to Y \times Y^Y \to Y $$

(the last map is projection, not evaluation).

If there's any justice in the world, the transpose of this is $r : Y \times Y^Y \to Y^N$. I'm too exhausted (and rusty) by this point to verify it all works out.


With that said, attacking the problem from scratch I probably would have curried differently: try to define a function $N \to Y^X$. Although it's plausible I would have wound up making a similar argument as to the one above.

share|improve this answer
add comment

Here is an elementary proof of the existence part.

Let $\varepsilon$ denote the evaluation morphism and $\Lambda(x)$ the exponential transpose of $x$.

Given your $g$ and $h$ let $i$ be the canonical isomorphism from $1\times X \to X$ and define two morphisms $u = \Lambda(i ; g) : 1 \to Y^X$ and $v = \Lambda\left(\langle\varepsilon, \pi_2\rangle ; h\right) : Y^X \to Y^X$. Then there exists a unique $\hat{f} : N \to Y^X$ such that $0 ; \hat{f} = u$ and $s ; \hat{f} = \hat{f} ; v$. Define $f = \hat{f} \times id ; \varepsilon : N\times X \to Y$. Computing a bit we get

\begin{align*} s\times id ; f &= (s ; \hat{f}) \times id ; \varepsilon = (\hat{f} ; v) \times id ; \varepsilon\\ &= (\hat{f}\times id) ; \left(\Lambda\left(\langle\varepsilon, \pi_2\rangle ; h\right)\times id\right) ; \varepsilon\\ &=(\hat{f}\times id) ; \langle \varepsilon, \pi_2\rangle ; h\\ &= \langle f, \pi_2\rangle ; h \end{align*}

and

\begin{align*} 0\times id ; f = (0 ; \hat{f}) \times id ; \varepsilon = \Lambda(i ; g) \times id ; \varepsilon = i ; g \end{align*}

This shows the existence of $f$. Uniqueness is straightforward as any such $f$ induces an $\hat{f}$ satisfying the required two equations by setting $\hat{f} = \Lambda(f)$. This assignment is easily seen, using the universal property of exponentials, to be a bijection.

Notice that you don't really need a topos, you only need a cartesian closed category to carry out the argument.

In Set, this reduces to defining $u$ and $v$ point-wise as \begin{align*} u(\star)(x) &= g(x)\\ v(\phi)(x) &= h(\phi(x), x) \end{align*} where $1 = \{\star\}$.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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