Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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.

share|improve this question
5  
It would be easier to answer this question if you could give the definitions of "simple nno", "parametrized nno", "strong nno," and "numerals", so people wouldn't have to hunt down the book in question. Also, do you mean "define" (i.e. define the notion of, without it necessarily existing) or "construct"? –  Mike Shulman Jan 18 '10 at 15:13
4  
I agree with Mike Shulman. While it seems to have been established recently that there is no obligation for a questioner on MO to include background material in order to make the question more self-contained, doing so certainly widens the audience and can only make the question more likely to be answered. In this case, I take the lack of response to be an indication that the MO regulars are not fluent in the language of "nno"'s. –  Pete L. Clark Jan 18 '10 at 19:08
    
Ok. Agree. I need more familiarity with the typing diagrams techniques. Thank you for the suggestion. –  Doctor Gibarian Jan 18 '10 at 19:20
2  
It's probably not necessary to show all the diagrams. I think it's reasonable to assume that the people who would be interested in answering this question (such as me) know what an ordinary NNO is, or can look it up, since that is a fairly standard notion, e.g. ncatlab.org/nlab/show/natural+numbers+object . But some brief remarks about how Lambek and Scott are using the adjectives "simple," "parametrized," and "strong" might be helpful for people without access to that particular book. –  Mike Shulman Jan 19 '10 at 2:17
add comment

3 Answers

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).

share|improve this answer
    
I don't understand very well: right exact functors between which categories? And..what you mean by relax cartesian closedness? With or without exponential objects? Thanks. –  Doctor Gibarian Jan 20 '10 at 13:53
    
Exponential objects would make the category cartesian closed, so every nno is parametrized by the first paragraph. I thought you wanted to generalize to cartesian categories which are not necessarily closed, did I misunderstand? –  François G. Dorais Jan 20 '10 at 14:31
    
Ah! I forgot to mention that the functors should preserve 1 (which is true for the relevant functors $(-)\times X:C \to C/X$). –  François G. Dorais Jan 20 '10 at 14:34
    
Yes, what you said about that slice functor was proved by Burroni over a topos. What I want is to know what kind of categories convert simple into parametrized nno not being CCC but only CC as Lambek and Scott suggest. Thanks again. –  Doctor Gibarian Jan 20 '10 at 16:53
    
Your question is still unclear. It is not true that a nno in a cartesian category is necessarily a parametrized nno. Presumably, the Lambek and Scott remark does not say that, but you haven't given a specific enough reference. –  François G. Dorais Jan 22 '10 at 20:12
show 6 more comments

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:

  1. Morphisms $\mathbb{N}^k \to \mathbb{N}^m$ with $m \neq 1$ are all set-theoretic functions.
  2. Morphisms $\mathbb{N}^0 \to \mathbb{N}^1$ are all set-theoretic functions, i.e., for each natural number there is one.
  3. 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.

share|improve this answer
add comment

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:

  1. 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$
  2. 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.

share|improve this answer
    
Does the distinction between strong/weak nnos match the distinction between strong/weak initial objects? –  François G. Dorais Jan 19 '10 at 17:02
    
Unfortunately, after all that, I have to say that I don't know the answer. I doubt it, but I don't have a counterexample offhand. –  Mike Shulman Jan 20 '10 at 5:39
    
In the definition of parameterized NNO I would expect $g : Y \times X \to Y$. Are you sure you got it right? –  Andrej Bauer Dec 29 '10 at 13:44
    
Mh...no, otherwise you had an extra variable with no sense. Am I correct? –  Doctor Gibarian Dec 29 '10 at 14:05
    
Well, then of course you have to also change the diagrams accordingly. Anyhow, just think about how primitive recursion with parameters works. Also, I think parametrized NNO can be expressed in terms of it being a simple NNO in all slices. –  Andrej Bauer Dec 29 '10 at 14:32
show 1 more 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.