nLab
natural numbers object

Redirected from "NNO".

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Induction

Natural numbers object

Idea

Recall that a topos is a category that behaves likes the category Set of sets.

A natural numbers object (NNO) in a topos is an object that behaves in that topos like the set of natural numbers does in Set; thus it provides a formulation of the “axiom of infinity” in structural set theory (such as ETCS). The definition is due to William Lawvere.

Definition

In a topos or cartesian closed category

A natural numbers object in a topos (or any cartesian closed category) E with terminal object 1 is

1 z s q u u A f A\array{ 1 &\stackrel{z}{\to}& \mathbb{N} &\stackrel{s}{\to}& \mathbb{N} \\ & {}_q\searrow & \downarrow^{u} && \downarrow^{u} \\ && A &\stackrel{f}{\to} & A }

All this may be summed up by saying that a natural numbers object is an initial algebra for the endofunctor X1+X. Equivalently, it is an initial algebra for the endo-profunctor Hom E(1,=)×Hom E(,=).

By the universal property, the natural numbers object is unique up to isomorphism.

In a general category with finite products

Note that this definition actually makes sense in any category E having finite products. However, if E is not cartesian closed, then it is better to explicitly assume a stronger version of this definition “with parameters” (which follows automatically when E is cartesian closed, such as when E is a topos). What this amounts to is demanding that (,z,s) not only be a natural numbers object (in the above, unparametrized sense) in E, but that also, for each object A, this is preserved by the free coalgebra functor into the Kleisli category of the comonad XA×X (which may be thought of as the category of maps parametrized by A). (Put another way, the finite product structure of E gives rise to a canonical self-indexing, and we are demanding the existence of an (unparametrized) NNO within this indexed category, rather than just within the base E).

The functions which are constructable out of the structure of a category with finite products and such a “parametrized NNO” are precisely the primitive recursive? ones. Specifically, the unique structure-preserving functor from the free such category F into Set yields a bijection between Hom F(1,) and the actual natural numbers, as well as surjections from Hom F( m,) onto the primitive recursive functions of arity m for each finite m. With cartesian closure, however, this identification no longer holds, since non-primitive recursive functions (such as the Ackermann function?) become definable as well.

In type theory

For the moment see at inductive type the section Examples - Natural numbers

Finite colimit characterization

In a topos, the natural numbers object is uniquely characterized by the following colimit conditions due to Peter Freyd: a triple (,0:1,s:) is a natural numbers object if and only if

  1. The morphism (0,s):1+ is an isomorphism;

  2. The diagram

    1s1\mathbb{N} \stackrel{\overset{s}{\to}}{\underset{1}{\to}} \mathbb{N} \to 1

    is a coequalizer.

The necessity of the first condition holds in any category with binary coproducts and a terminal object, and the necessity of the second holds in any category whatsoever.

Proof of necessity

For a category C with binary coproducts and 1, the natural numbers object can be equivalently described as an initial algebra structure (0,s):1+ for the endofunctor F(c)=1+c defined on C. Then condition 1 is a special case of Lambek's theorem, that the algebra structure map of an initial algebra is an isomorphism.

As for condition 2, given f:X such that f=fs, the claim is that f factors as

!1xX\mathbb{N} \overset{!}{\to} 1 \overset{x}{\to} X

for some unique x, in fact for x=f(0). Uniqueness is clear since !:1, being a retraction for 0:1, is epic. On the other hand, substituting either f or f(0)! for g in the diagram

1 0 s f(0) g g X 1 X X\array{ 1 & \overset{0}{\to} & \mathbb{N} & \overset{s}{\to} & \mathbb{N} \\ & ^\mathllap{f(0)} \searrow & \downarrow ^g & & \downarrow ^g \\ & & X & \underset{1_X}{\to} & X }

this diagram commutes, so that f=f(0)! by the uniqueness clause in the universal property for .

Proof of sufficiency

We give a brief outline, referring to (Johnstone), section D.5.1, for full details. Let N be an object satisfying the two colimit conditions of Freyd. One first shows that N has no nontrivial F-subalgebras. Next, let A be any F-algebra, and let i:BN×A be the intersection of all F-subalgebras of N×A. One shows that π 1i:BN is an (F-algebra) isomorphism. Thus we have an F-algebra map f:NA. If g:NA is any F-algebra map, then the equalizer of f and g is an F-subalgebra of N, and therefore N itself, which means f=g.

Examples

In any Grothendieck topos E=Sh(C) the natural numbers object is given by the constant sheaf on the set of ordinary natural numbers, i.e. by the sheafification of the presheaf C opSet that is constant on the set .

There are interesting cases in which such sheaf toposes contain objects that look like they ought to be natural numbers objects but do not satisfy the above axioms: for instance some of the models described at Models for Smooth Infinitesimal Analysis are sheaf toposes that contain besides the standard natural number object a larger object of smooth natural numbers that has generalized elements which are “infinite natural numbers” in the sense of nonstandard analysis.

Properties

Transfer along inverse images

Proposition

Natural number objects are preserved by inverse images:

let f=(f *f *):f *f * be a geometric morphism of toposes. If is a natural numbers object, then its inverse image f * is a natural numbers object in .

(Johnstone, lemma A.4.1.14).

Example

If is a sheaf topos, then there is a unique geometric morphism (ΔΓ):ΓΔSet, the global section geometric morphism, with the inverse image being the locally constant sheaf functor, it follows that

Δ()Δ( n:1) n:NΔ1 n:1,\Delta(\mathbb{N}) \cong \Delta(\sum_{n: \mathbb{N}} 1) \cong \sum_{n: N} \Delta 1 \cong \sum_{n: \mathbb{N}} 1,

with the evident successor and constant 0, is the natural nunbers object in .

Example

If is a topos and X an object, then the slice topos sits by an etale geometric morphism over

/XX *X *,\mathcal{E}_{/X} \stackrel{\overset{X^*}{\leftarrow}}{\underset{X_*}{\to}} \mathcal{E} \,,

where the inverse image form the product with X. Hence for a natural numbers object, the projection (X×X) is a natural numbers object in /X.

Given a natural numbers object in a pretopos, we can construct an integers object as follows. Let a,b:E× be the kernel pair of the addition map +:×, and let π 1,π 2:× be the product projections. We define to be the coequalizer of the congruence (π 1a,π 2b),(π 2a,π 1b):E. A similar construction yields a rational numbers object .

For a real numbers object, rather more care is needed; see real numbers object.

References