Natural number object
Encyclopedia
In category theory
, a natural number object (NNO) is an object endowed with a recursive structure similar to natural number
s. More precisely, in a category
E with a terminal object 1 (alternately, a topos
), an NNO N is given by:
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:
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
:
NNOs are defined up to
isomorphism
. Every NNO is an initial object of the category of diagram
s of the form
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 : 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.
NNOs can be used for non-standard model
s 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.
Category theory
Category theory is an area of study in mathematics that examines in an abstract way the properties of particular mathematical concepts, by formalising them as collections of objects and arrows , where these collections satisfy certain basic conditions...
, a natural number object (NNO) is an object endowed with a recursive structure similar to natural number
Natural number
In mathematics, the natural numbers are the ordinary whole numbers used for counting and ordering . These purposes are related to the linguistic notions of cardinal and ordinal numbers, respectively...
s. More precisely, in a category
Category (mathematics)
In mathematics, a category is an algebraic structure that comprises "objects" that are linked by "arrows". A category has two basic properties: the ability to compose the arrows associatively and the existence of an identity arrow for each object. A simple example is the category of sets, whose...
E with a terminal object 1 (alternately, a topos
Topos
In mathematics, a topos is a type of category that behaves like the category of sheaves of sets on a topological space...
), an NNO N is given by:
- a global elementGlobal elementIn category theory, a global element of an object A from a category is a morphismwhere 1 is a terminal object of the category. Roughly speaking, global elements are a generalization of the notion of “elements” from the category of sets, and they can be used to import set-theoretic...
z : 1 → N, and - an arrowMorphismIn mathematics, a morphism is an abstraction derived from structure-preserving mappings between two mathematical structures. The notion of morphism recurs in much of contemporary mathematics...
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
Recursive definition
In mathematical logic and computer science, a recursive definition is used to define an object in terms of itself ....
:
- ⊢ u (z) = q
- y ∈E N ⊢ u (s y) = f (u (y))
NNOs are defined up to
Up to
In mathematics, the phrase "up to x" means "disregarding a possible difference in x".For instance, when calculating an indefinite integral, one could say that the solution is f "up to addition by a constant," meaning it differs from f, if at all, only by some constant.It indicates that...
isomorphism
Morphism
In mathematics, a morphism is an abstraction derived from structure-preserving mappings between two mathematical structures. The notion of morphism recurs in much of contemporary mathematics...
. Every NNO is an initial object of the category of diagram
Commutative diagram
In mathematics, and especially in category theory, a commutative diagram is a diagram of objects and morphisms such that all directed paths in the diagram with the same start and endpoints lead to the same result by composition...
s of the form
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
Cartesian closed category
In category theory, a category is cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in mathematical logic and the theory of programming, in...
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 : 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.
NNOs can be used for non-standard model
Non-standard model
In model theory, a discipline within mathematical logic, a non-standard model is a model of a theory that is not isomorphic to the intended model . If the intended model is infinite and the language is first-order, then the Löwenheim-Skolem theorems guarantee the existence of non-standard models...
s of type theory
Type theory
In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
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
Coproduct
In category theory, the coproduct, or categorical sum, is the category-theoretic construction which includes the disjoint union of sets and of topological spaces, the free product of groups, and the direct sum of modules and vector spaces. The coproduct of a family of objects is essentially the...
diagram for NNOs; also, !N : N → 1 is a coequalizer
Coequalizer
In category theory, a coequalizer is a generalization of a quotient by an equivalence relation to objects in an arbitrary category...
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.