Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
started an Examples-section at natural numbers object
btw, the natural numbers objects of a topos is unique, up to isomorphism, right? if so, we should say that
Yes, of course, since it has a universal property.
I have expanded a little at Transfer of NNOs along inverse images.
I added an explicit definition of parametrized NNO to natural numbers object.
I have a question: there is mention in that article of a categories with finite products and a parametrized NNO, and the initial such structure , and it is written that the canonical maps
surject onto the primitive recursive maps. Why couldn’t “surject” be replaced by “biject”?
Perhaps it’s a question of extensionality? The morphisms are surely constructed by syntactic means, and it’s conceivable that two such morphisms describe the same primitive recursive function in the standard model of arithmetic while not being provably equal (in whatever system of arithmetic corresponds to ).
Maybe, but I’d really like to see a specific example of that.
Hmmm. Well, consider the primitive recursive “function” defined by if codes the proof of a contradiction in Peano arithmetic, and otherwise. (This is primitive recursive because no unbounded searches are required to verify the validity of a proof.) In the standard model of arithmetic, is the constant function, but we could equally consider the elementary topos corresponding to a model of , in which is not the constant function. Thus and the constant function must be distinct in the category .
Ah yes, that certainly seems to work. Nice!
But wait: ZFC proves that PA is consistent (since one can establish ordinal induction up to in ZFC).
Edit: Well, I think the conclusion must still hold anyway: in the initial structure, it cannot be established that , since that would amount to provability of that statement within primitive recursive arithmetic. So and are distinct there.
Oops, quite right. I suppose , with the “function” that verifies proofs of inconsistency of ZFC, is what I meant.
Why is it that a parameterized NNO is the same as being preserved by all the functors to the coKelisli categories for the comonad ? I’m trying to see how this works as I’d like to think of an NNO as being an initial algebra for a polynomial endofunctor (arising from 1←1→1+1→1) and these two pictures aren’t meshing.
please doublecheck my correction. but it seems like the second pair is backwards. if we identify (\pi_1 \circ a, \pi_2 \circ b) and (\pi_2 \circ a, \pi_1 \circ b), that means we’re declaring i-l = j-k for i+j = k+l, whereas we actually want i-l = k-j. So we want to identify (\pi_1 \circ b, \pi_2 \circ a)
Yes, you seem to be correct. Good catch.
added pointer to:
@Guest
, where 1 is terminal (the coproduct is sometimes written as , especially in a disjunctive or extensive category). It’s a special case of the List monad, if that helps.
But perhaps you meant something else by your question?
Considering that pointed object in a monoidal category got created a few days ago, I wonder if it makes sense to talk about natural numbers objects in an arbitrary monoidal category as the initial object with an endomorphism and a morphism out of the tensor unit ?
I think that in for a field the natural numbers object as defined in the previous sentence would be the infinite-dimensional vector space with denumerable basis - or equivalently the underlying vector space of the sequence space .
Added references to two papers by Robert Paré on natural numbers, one of which discusses natural number objects in monoidal categories.
In the ordinary version where the monoidal product is cartesian, there are two standard tacks: (1) use this definition if the category is cartesian closed, or (2) use instead parametrized natural number objects (because without extra infrastructure like cartesian closure, it will be hard to get a satisfactory theory up and running with just the vanilla definition).
Your idea could be interesting. I’d want to review a little recursion theory before opining on whether I think it would fly.
(Small nit: will have basis of cardinality equal to the cardinality of the underlying set. MO post)
In the ordinary version where the monoidal product is cartesian, there are two standard tacks: (1) use this definition if the category is cartesian closed, or (2) use instead parametrized natural number objects (because without extra infrastructure like cartesian closure, it will be hard to get a satisfactory theory up and running with just the vanilla definition).
So I’d imagine in my proposed definition (1) would have to be in a closed monoidal category and (2) would use the tensor product in the definition of parametrised NNO.
That’s what I was thinking, Madeleine. Meanwhile, Bryce added a reference which is worth looking over.
I said earlier that
I think that in for a field the natural numbers object as defined in the previous sentence would be the infinite-dimensional vector space with denumerable basis - or equivalently the underlying vector space of the sequence space .
and Todd Trimble said
(Small nit: will have basis of cardinality equal to the cardinality of the underlying set. MO post)
I just realised where Todd is coming from. It is rather the polynomial ring whose underlying vector space is the free vector space . is equivalent to the power series ring , and the underlying vector space of is not freely generated by the natural numbers .
Other similarities between the natural numbers in and the polynomial ring in : is the free commutative monoid object on one generator in , while is the free commutative monoid object on one generator in .
Yes, and the strong symmetric monoidal functor that carries a set to the free -vector space on carries the commutative monoid object in to the commutative monoid objects in .
I wonder if (the underlying vector space of) the power series ring or the sequence algebra plays the role in that the extended natural numbers does in , as the terminal coalgebra of the endofunctor .
This happens to be true, and follows from Adamek’s theorem, or its dual, which gives a criterion for constructing terminal coalgebras. In detail, the endofunctor coincides with (biproducts), and preserves connected limits, in particular inverse limits of -chains, which is the crucial hypothesis in Adamek’s theorem. An easy way to verify this preservation property is to view as a composite
where the right adjoints obviously preserve connected limits, and the constant functor also preserves connected limits. (Actually, diagonal functors always preserve limits, regardless of whether it’s a right adjoint, because limits in functor categories are computed pointwise.)
1 to 27 of 27