Natural numbers objects in topoi: Recursion in a parameter

Question

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.

Answer 1

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.

Answer 2

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\}$.