Parametrized natural numbers object. - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-18T08:14:47Z http://mathoverflow.net/feeds/question/12184 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/12184/parametrized-natural-numbers-object Parametrized natural numbers object. Doctor Gibarian 2010-01-18T10:44:26Z 2010-12-29T14:49:57Z <p>Lambek and Scott demonstrate in <strong>Introduction to higher order categorical logic</strong> the existence of a parametrized <strong>nno</strong> when we are in a cartesian closed category (CCC) with a "simple nno" and suggest the possibility of define a parametrized <strong>nno</strong> in the context of a cartesian category (CC) with a <strong>simple nno</strong>. 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>strong nno</strong>?</p> <p>Ximo.</p> http://mathoverflow.net/questions/12184/parametrized-natural-numbers-object/12296#12296 Answer by Doctor Gibarian for Parametrized natural numbers object. Doctor Gibarian 2010-01-19T10:51:57Z 2010-12-29T13:41:58Z <p>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:</p> <ol> <li>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 <code>$1\overset{z}{\longrightarrow}N\overset{s}{\longrightarrow}N$</code> is initial among all the diagrams in the form <code>$1\overset{f}{\longrightarrow}Y\overset{g}{\longrightarrow}Y$</code> </li> <li>A parametrized nno is a group of three as the one above where the diagram <code>$X\overset{(z,1_X)}{\longrightarrow}N \times X\overset{s \times 1_X}{\longrightarrow}N \times X$</code> is initial among all the diagrams in the form <code>$X\overset{f}{\longrightarrow}Y\overset{g}{\longrightarrow}Y$</code> </li> </ol> <p>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.</p> <p>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 <code>$1\longrightarrow N^{k}$</code> standard (built up in terms of z and s morphisms)?</p> <p>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.</p> <p>Ximo.</p> http://mathoverflow.net/questions/12184/parametrized-natural-numbers-object/12321#12321 Answer by François G. Dorais for Parametrized natural numbers object. François G. Dorais 2010-01-19T16:56:59Z 2010-01-19T16:56:59Z <p>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.</p> <p>Sometimes (e.g. in a topos) nnos can be characterized by the two axioms</p> <ul> <li><p><code>$1 \xrightarrow{z} N \xleftarrow{s} N$</code> is a coproduct diagram, and</p></li> <li><p>the coequalizer of $N\xrightarrow{s} N$ and the identity on $N$ is the terminal object $1$.</p></li> </ul> <p>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).</p> http://mathoverflow.net/questions/12184/parametrized-natural-numbers-object/50660#50660 Answer by Andrej Bauer for Parametrized natural numbers object. Andrej Bauer 2010-12-29T14:49:57Z 2010-12-29T14:49:57Z <p>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.</p> <p>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 <em>not</em> cartesian-closed because there are too many morhisms $\mathbb{N} \to \mathbb{N}$, and it has a parameterized NNO, namely the obvious one.</p> <p>Second, consider the category $\mathcal{D}$ whose objects are the finite powers of $\mathbb{N}$, like before, and whose morphisms are as follows:</p> <ol> <li>Morphisms $\mathbb{N}^k \to \mathbb{N}^m$ with $m \neq 1$ are all set-theoretic functions.</li> <li>Morphisms $\mathbb{N}^0 \to \mathbb{N}^1$ are all set-theoretic functions, i.e., for each natural number there is one.</li> <li>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$.</li> </ol> <p>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.</p>