Parametrized natural numbers object. - MathOverflow

Parametrized natural numbers object.

2010-01-18T10:44:26Z

Lambek and Scott demonstrate in Introduction to higher order categorical logic the existence of a parametrized nno when we are in a cartesian closed category (CCC) with a "simple nno" and suggest the possibility of define a parametrized nno in the context of a cartesian category (CC) with a simple nno. In which cases can it be done in the context of a CC? Could it be done only with numerals or (in the more general case of a) strong nno?

Ximo.

Answer by Doctor Gibarian for Parametrized natural numbers object.

2010-01-19T10:51:57Z

So, here are some definitions about Natural Numbers Object (nno), that is a key concept in category theory related to Computer Science. They are given in Lambek and Scott (LS) in the following form:

A (simple) nno is a group of three (N,z,s) where N is an object and z (as zero) and s (as successor) morphisms in a category and the diagram $1\overset{z}{\longrightarrow}N\overset{s}{\longrightarrow}N$ is initial among all the diagrams in the form $1\overset{f}{\longrightarrow}Y\overset{g}{\longrightarrow}Y$
A parametrized nno is a group of three as the one above where the diagram $X\overset{(z,1_X)}{\longrightarrow}N \times X\overset{s \times 1_X}{\longrightarrow}N \times X$ is initial among all the diagrams in the form $X\overset{f}{\longrightarrow}Y\overset{g}{\longrightarrow}Y$

Barr and Wells propose to say the latter simply a nno because is the only of our interest. It is closely related to a descrption of the primitive recursive functions. A nno makes an object of a category behave as the natural numbers.

With all of these my questions are: while LS demonstrate the existence of a parametrized nno when we are in a cartesian closed category (CCC) with a (simple) nno...in which cases can it be done in the context of a CC (not closed)? Could it be done only with numerals in the sense of arrows $1\longrightarrow N^{k}$ standard (built up in terms of z and s morphisms)?

To ask about weak and strong nno's I would need more definitions, so I let it here for the moment. Thank you in advance and sorry for my english.

Ximo.

Answer by François G. Dorais for Parametrized natural numbers object.

2010-01-19T16:56:59Z

If I understand correctly, by a parametrized nno in a category $C$ you mean a nno $N$ which is stable under pullbacks: $N \times X$ is a nno in the slice $C/X$ for every object $X$ of $C$. The reason why a nno in a cartesian closed category is automatically a parametrized nno is that any functor with a right adjoint will preserve nnos. Cartesian closedness is precisely equivalent to saying that the pullback functor $C \to C/X$ has a right adjoint.

Sometimes (e.g. in a topos) nnos can be characterized by the two axioms

$1 \xrightarrow{z} N \xleftarrow{s} N$ is a coproduct diagram, and
the coequalizer of $N\xrightarrow{s} N$ and the identity on $N$ is the terminal object $1$.

These correspond more closely to the Peano axioms rather than primitive recursion. In such cases, a right exact functor between such categories will preserve nnos. This may help you relax the cartesian closedness condition a little (though, obviously, not in the case of topoi).

Answer by Andrej Bauer for Parametrized natural numbers object.

2010-12-29T14:49:57Z

I give two examples of categories with finite products and simple NNO. In the first example the simple NNO is also a parameterized NNO, while in the second example it is not. Although it is difficult to understand your question, I believe the examples should clarify matters.

First, consider the category $\mathcal{C}$ whose objects are the finite powers of $\mathbb{N}$, namely $\mathbb{N}^0$, $\mathbb{N}^1$, $\mathbb{N}^2$, ... and morphisms are set-theoretic functions $f : \mathbb{N}^k \to \mathbb{N}^m$. This category clearly has finite products, is not cartesian-closed because there are too many morhisms $\mathbb{N} \to \mathbb{N}$, and it has a parameterized NNO, namely the obvious one.

Second, consider the category $\mathcal{D}$ whose objects are the finite powers of $\mathbb{N}$, like before, and whose morphisms are as follows:

Morphisms $\mathbb{N}^k \to \mathbb{N}^m$ with $m \neq 1$ are all set-theoretic functions.
Morphisms $\mathbb{N}^0 \to \mathbb{N}^1$ are all set-theoretic functions, i.e., for each natural number there is one.
Morphisms $\mathbb{N}^k \to \mathbb{N}^1$ with $k \neq 0$ are all set-theoretic functions $f : \mathbb{N}^k \to \mathbb{N}$ for which there exists a projection $\pi_j : \mathbb{N}^k \to \mathbb{N}$ and $g : \mathbb{N} \to \mathbb{N}$ such that $f = g \circ \pi_j$.

In other words, in $\mathcal{D}$ every function into $\mathbb{N}$ depends on only one of its parameters (exercise: prove that these are closed under composition.) The category $\mathcal{D}$ has finite products and a simple NNO, namely the obvious one, but no parameterized NNO. If it did, we could construct addition ${+} : \mathbb{N}^2 \to \mathbb{N}$ as a morphism in the category.