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 F, and it is written that the canonical maps
homF(Nk,N)βhomSet(βk,β)surject onto the primitive recursive maps. Why couldnβt βsurjectβ be replaced by βbijectβ?
Perhaps itβs a question of extensionality? The morphisms NkβN 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 F).
Maybe, but Iβd really like to see a specific example of that.
Hmmm. Well, consider the primitive recursive βfunctionβ G defined by G(n)=1 if n codes the proof of a contradiction in Peano arithmetic, and G(n)=0 otherwise. (This is primitive recursive because no unbounded searches are required to verify the validity of a proof.) In the standard model of arithmetic, G is the constant 0 function, but we could equally consider the elementary topos corresponding to a model of ZFC+Β¬Con(PA), in which G is not the constant 0 function. Thus G and the constant 0 function must be distinct in the category F.
Ah yes, that certainly seems to work. Nice!
But wait: ZFC proves that PA is consistent (since one can establish ordinal induction up to Ξ΅0 in ZFC).
Edit: Well, I think the conclusion must still hold anyway: in the initial structure, it cannot be established that G=0, since that would amount to provability of that statement within primitive recursive arithmetic. So G and 0 are distinct there.
Oops, quite right. I suppose ZFC+Β¬Con(ZFC), 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 AΓβ? 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
F(x):=xβ1, 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βπ©?
I think that in VectK for a field K 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 Kβ.
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: Kβ 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 VectK for a field K 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 Kβ.
and Todd Trimble said
(Small nit: Kβ 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 K[X] whose underlying vector space is the free vector space K[β]. Kβ is equivalent to the power series ring K[[X]], and the underlying vector space of K[[X]] is not freely generated by the natural numbers β.
Other similarities between the natural numbers β in Set and the polynomial ring K[X] in VectK: β is the free commutative monoid object on one generator in Set, while K[X] is the free commutative monoid object on one generator in VectK.
Yes, and the strong symmetric monoidal functor Xβ¦Kβ X that carries a set X to the free K-vector space on X carries the commutative monoid object β in Set to the commutative monoid objects Kβ ββ K[x] in VectK.
I wonder if (the underlying vector space of) the power series ring K[[X]] or the sequence algebra Kβ plays the role in VectK that the extended natural numbers does in Set, as the terminal coalgebra of the endofunctor Vβ¦KβV.
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 Kββ coincides with KΓβ (biproducts), and KΓβ 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 KΓβ as a composite
VectΞβVectΓVectcKΓ1βVectΓVectprodβVectwhere the right adjoints Ξ,prod obviously preserve connected limits, and the constant functor cK also preserves connected limits. (Actually, diagonal functors Ξ:C1βC1+1 always preserve limits, regardless of whether itβs a right adjoint, because limits in functor categories are computed pointwise.)
1 to 27 of 27