Natural numbers object

In category theory in mathematics, a natural numbers object (NNO) is an object endowed with a recursive structure similar to natural numbers. More precisely, in a category E with a terminal object 1, an NNO N is given by:

a global element z : 1 → N, and

an arrow s : N → N,

such that for any object A of E, global element q : 1 → A, and arrow f : A → A, there exists a unique arrow u : N → A such that:

u ∘ z = q, and

u ∘ s = f ∘ u.

In other words, the triangle and square in the following diagram commute.

The pair (q, f) is sometimes called the recursion data for u, given in the form of a recursive definition:

⊢ u (z) = q

y ∈E N ⊢ u (s y) = f (u (y))

The above definition is the universal property of NNOs, meaning they are defined up to canonical isomorphism. If the arrow u as defined above merely has to exist, that is, uniqueness is not required, then N is called a weak NNO.

Equivalent definitions

NNOs in cartesian closed categories (CCCs) are sometimes defined in the following equivalent way (due to Lawvere): for every pair of arrows g : A → B and f : B → B, there is a unique h : N × A → B such that the squares in the following diagram commute.

This same construction defines weak NNOs in cartesian categories that are not cartesian closed.

In a category with a terminal object 1 and binary coproducts (denoted by +), an NNO can be defined as the initial algebra of the endofunctor that acts on objects by X ↦ 1 + X and on arrows by f ↦ id1 + f.

Properties

Every NNO is an initial object of the category of diagrams of the form

1

→

q

A

→

f

A

{\displaystyle 1{\xrightarrow {~\quad q\quad ~}}A{\xrightarrow {~\quad f\quad ~}}A}

If a cartesian closed category has weak NNOs, then every slice of it also has a weak NNO.

NNOs can be used for non-standard models of type theory in a way analogous to non-standard models of analysis. Such categories (or topoi) tend to have "infinitely many" non-standard natural numbers. (Like always, there are simple ways to get non-standard NNOs; for example, if z = s z, in which case the category or topos E is trivial.)

Freyd showed that z and s form a coproduct diagram for NNOs; also, !N : N → 1 is a coequalizer of s and 1N, i.e., every pair of global elements of N are connected by means of s; furthermore, this pair of facts characterize all NNOs.