4
$\begingroup$

The first problem in Chapter VI of Sheaves in Geometry and Logic: A First Introduction to Topos Theory by Mac Lane and Moerdijk has two parts. The first part (which I have already done) can be found in this stackexchange post, and asks the reader to show that, in a topos, each arrow $\mathbf N \times X \xrightarrow{f} Y$ is given uniquely by some $X \xrightarrow{g} Y$ and another $X \times Y \xrightarrow{h} Y$ when the following diagram commutes.

\begin{array}{rclcl} 1 \times X & \xrightarrow{0_N \times 1_X} & \mathbf N \times X & \xrightarrow{s \times 1_X} & \mathbf N\times X \newline \pi_2 \downarrow & & \downarrow (f, \pi_2) & & \downarrow f \newline X & \xrightarrow{(g, 1_X)} & Y\times X & \xrightarrow{h} & Y \end{array} In the above diagram, $\pi_j$ is the $j$th projection, and $1 \xrightarrow{0_N} \mathbf N \xrightarrow{s} \mathbf N$ is a NNO. The second asks for several definitions that make use of recursion in a parameter: Addition, multiplication, and the subobject < of $\mathbf N \times \mathbf N$. Mac & Moe call this "recursion in a parameter".

Now, I have definitions for addition and multiplication worked out, but I can't seem to find the correct $g$ and $h$ for the subobject <. What I would like is a hint, not a solution, as to where to look.

A few thoughts on the matter: I imagine that I want $X = \mathbf N$ and $Y = \Omega$, where $\Omega$ is the subobject classifier, so that $\mathbf N \times \mathbf N \xrightarrow{f} \Omega$ is the classifying map for $< \subseteq \mathbf N \times \mathbf N$. My first attempt was to take $g(n)$ to be the formula "$0 < n$" ($g$ is the characteristic map of the pullback of $s$ along $1_\mathbf N$), and $h = \pi_1$. Here I was trying to model the example, "$2 < 5$ because $1 < 4$ because $0 < 3$," but that isn't how things turned out. Instead, in $\mathbf{Sets}$, this would give \begin{align} f (1, 1) &= f \circ (s \times 1_N) (0, 1)\newline &= f (0, 1), \end{align} which is not what I want. I also tried to prove a different theorem than the one in the first part, to make this idea work, in which the "$s \times 1_X$" is replaced by "$s \times s$" in the diagram, but this also came with issues.

$\endgroup$
4
$\begingroup$

The definition of $<$ in terms of addition, as in the last paragraph of Derek Elkins's answer, seems to be a favorite of many topos theorists. My own preference is to define $x<y$ by induction on $y$. (Formally, that means defining the curried version $\mathbb N\to\Omega^{\mathbb N}:y\mapsto(x\mapsto [x<y]$ of the predicate $<:\mathbb N^2\to\Omega$.) The inductive clauses are $$ [x<0] = \bot $$ and $$ [x<s(y)]=([x<y]\lor[x=y]). $$

$\endgroup$
1
$\begingroup$

Think about how you would compute this given just structural recursion on the naturals. You'd likely have a definition like: $$\begin{align}f(0,n)&=n\neq 0\\f(m+1,0)&=\bot\\f(m+1,n+1)&=f(m,n)\end{align}$$ This corresponds to a nested induction. We can make it fit the format better via: $$\begin{align}f(0)(n)&=n\neq 0\\f(m+1)(n)&=g(n)\\ g(0)&=\bot\\g(n+1)&=f(m)(n)\end{align}$$ This presents $f$ as $f:\mathbb N\to\Omega^\mathbb N$. However, $g$'s definition depends on $f$ and these are mutually recursive, so how can we deal with that. Easy, abstract. $$\begin{align}f(0)(n)&=n\neq 0\\f(m+1)(n)&=g(n,f(m))\\ g(0,h)&=\bot\\g(n+1,h)&=h(n)\end{align}$$ You can now define $g$ independently, and then define $f$ in terms of $g$. I'll leave it to you to formulate this in the language of an elementary topos.

As an alternative, we often define $m\leq n$ as $m\leq n \iff \exists k:\mathbb N.m+k=n$. We can easily define $<$ in terms of $\leq$. Given that you've already defined addition, this too can be articulated in the language of an elementary topos. In this case, it won't (directly) require the universal property of an NNO. It indirectly requires via the definition of addition, of course.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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