Natural number object

From Wikipedia, the free encyclopedia
Jump to: navigation, search

In category theory, a natural number 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 (alternately, a topos), an NNO N is given by:

  1. a global element z : 1 → N, and
  2. an arrow s : NN,

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

  1. uz = q, and
  2. us = fu.

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

NNO definition

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

  1. u (z) = q
  2. yE Nu (s y) = f (u (y))

NNOs are defined up to isomorphism. Every NNO is an initial object of the category of diagrams of the form

NNO as a terminal object

If the arrow u as defined above merely has to exist, i.e. uniqueness is not required, then N is called a weak NNO. If a cartesian closed category has weak NNOs, then every slice of it also has a weak NNO. NNOs in CCCs or topoi are sometimes defined in the following equivalent way (due to Lawvere): for every pair of arrows g : AB and f : BB, there is a unique h : N × AB such that the squares in the following diagram commute.

alternate NNO definition

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

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.

See also[edit]