\documentclass[12pt,titlepage]{article} \usepackage{amsmath} \usepackage{mathrsfs} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{graphicx} \usepackage{color} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{xparse} \usepackage{hyperref} %----Macros---------- % % Unresolved issues: % % \righttoleftarrow % \lefttorightarrow % % \color{} with HTML colorspec % \bgcolor % \array with options (without options, it's equivalent to the matrix environment) % Of the standard HTML named colors, white, black, red, green, blue and yellow % are predefined in the color package. Here are the rest. \definecolor{aqua}{rgb}{0, 1.0, 1.0} \definecolor{fuschia}{rgb}{1.0, 0, 1.0} \definecolor{gray}{rgb}{0.502, 0.502, 0.502} \definecolor{lime}{rgb}{0, 1.0, 0} \definecolor{maroon}{rgb}{0.502, 0, 0} \definecolor{navy}{rgb}{0, 0, 0.502} \definecolor{olive}{rgb}{0.502, 0.502, 0} \definecolor{purple}{rgb}{0.502, 0, 0.502} \definecolor{silver}{rgb}{0.753, 0.753, 0.753} \definecolor{teal}{rgb}{0, 0.502, 0.502} % Because of conflicts, \space and \mathop are converted to % \itexspace and \operatorname during preprocessing. % itex: \space{ht}{dp}{wd} % % Height and baseline depth measurements are in units of tenths of an ex while % the width is measured in tenths of an em. \makeatletter \newdimen\itex@wd% \newdimen\itex@dp% \newdimen\itex@thd% \def\itexspace#1#2#3{\itex@wd=#3em% \itex@wd=0.1\itex@wd% \itex@dp=#2ex% \itex@dp=0.1\itex@dp% \itex@thd=#1ex% \itex@thd=0.1\itex@thd% \advance\itex@thd\the\itex@dp% \makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}} \makeatother % \tensor and \multiscript \makeatletter \newif\if@sup \newtoks\@sups \def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}% \def\reset@sup{\@supfalse\@sups={}}% \def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else% \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}% \else \append@sup#2 \@suptrue \fi% \expandafter\mk@scripts\fi} \def\tensor#1#2{\reset@sup#1\mk@scripts#2_/} \def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2% \reset@sup\mk@scripts#3_/} \makeatother % \slash \makeatletter \newbox\slashbox \setbox\slashbox=\hbox{$/$} \def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$} \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa \copy\slashbox \kern-\@tempdima \box\@tempboxa} \def\slash{\protect\itex@pslash} \makeatother % math-mode versions of \rlap, etc % from Alexander Perlis, "A complement to \smash, \llap, and lap" % http://math.arizona.edu/~aprl/publications/mathclap/ \def\clap#1{\hbox to 0pt{\hss#1\hss}} \def\mathllap{\mathpalette\mathllapinternal} \def\mathrlap{\mathpalette\mathrlapinternal} \def\mathclap{\mathpalette\mathclapinternal} \def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}} \def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}} \def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}} % Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2} \let\oldroot\root \def\root#1#2{\oldroot #1 \of{#2}} \renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}} % Manually declare the txfonts symbolsC font \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n} \DeclareFontSubstitution{U}{txsyc}{m}{n} % Manually declare the stmaryrd font \DeclareSymbolFont{stmry}{U}{stmry}{m}{n} \SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n} % Manually declare the MnSymbolE font \DeclareFontFamily{OMX}{MnSymbolE}{} \DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n} \SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n} \DeclareFontShape{OMX}{MnSymbolE}{m}{n}{ <-6> MnSymbolE5 <6-7> MnSymbolE6 <7-8> MnSymbolE7 <8-9> MnSymbolE8 <9-10> MnSymbolE9 <10-12> MnSymbolE10 <12-> MnSymbolE12}{} % Declare specific arrows from txfonts without loading the full package \makeatletter \def\re@DeclareMathSymbol#1#2#3#4{% \let#1=\undefined \DeclareMathSymbol{#1}{#2}{#3}{#4}} \re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46} \re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12} \re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64} \re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6} \re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77} \re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77} \makeatother % \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE \makeatletter \def\Decl@Mn@Delim#1#2#3#4{% \if\relax\noexpand#1% \let#1\undefined \fi \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}} \def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}} \def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}} \Decl@Mn@Open{\llangle}{mnomx}{'164} \Decl@Mn@Close{\rrangle}{mnomx}{'171} \Decl@Mn@Open{\lmoustache}{mnomx}{'245} \Decl@Mn@Close{\rmoustache}{mnomx}{'244} \makeatother % Widecheck \makeatletter \DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}} \def\@widecheck#1#2{% \setbox\z@\hbox{\m@th$#1#2$}% \setbox\tw@\hbox{\m@th$#1% \widehat{% \vrule\@width\z@\@height\ht\z@ \vrule\@height\z@\@width\wd\z@}$}% \dp\tw@-\ht\z@ \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@ \setbox\tw@\hbox{% \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box \tw@}}}% {\ooalign{\box\tw@ \cr \box\z@}}} \makeatother % \mathraisebox{voffset}[height][depth]{something} \makeatletter \NewDocumentCommand\mathraisebox{moom}{% \IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{% \IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}% }{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}% \mathpalette\@temp{#4}} \makeatletter % udots (taken from yhmath) \makeatletter \def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.} \mkern2mu\raise4\p@\hbox{.}\mkern1mu \raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}} \makeatother %% Fix array \newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}} %% \itexnum is a noop \newcommand{\itexnum}[1]{#1} %% Renaming existing commands \newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}} \newcommand{\widevec}{\overrightarrow} \newcommand{\darr}{\downarrow} \newcommand{\nearr}{\nearrow} \newcommand{\nwarr}{\nwarrow} \newcommand{\searr}{\searrow} \newcommand{\swarr}{\swarrow} \newcommand{\curvearrowbotright}{\curvearrowright} \newcommand{\uparr}{\uparrow} \newcommand{\downuparrow}{\updownarrow} \newcommand{\duparr}{\updownarrow} \newcommand{\updarr}{\updownarrow} \newcommand{\gt}{>} \newcommand{\lt}{<} \newcommand{\map}{\mapsto} \newcommand{\embedsin}{\hookrightarrow} \newcommand{\Alpha}{A} \newcommand{\Beta}{B} \newcommand{\Zeta}{Z} \newcommand{\Eta}{H} \newcommand{\Iota}{I} \newcommand{\Kappa}{K} \newcommand{\Mu}{M} \newcommand{\Nu}{N} \newcommand{\Rho}{P} \newcommand{\Tau}{T} \newcommand{\Upsi}{\Upsilon} \newcommand{\omicron}{o} \newcommand{\lang}{\langle} \newcommand{\rang}{\rangle} \newcommand{\Union}{\bigcup} \newcommand{\Intersection}{\bigcap} \newcommand{\Oplus}{\bigoplus} \newcommand{\Otimes}{\bigotimes} \newcommand{\Wedge}{\bigwedge} \newcommand{\Vee}{\bigvee} \newcommand{\coproduct}{\coprod} \newcommand{\product}{\prod} \newcommand{\closure}{\overline} \newcommand{\integral}{\int} \newcommand{\doubleintegral}{\iint} \newcommand{\tripleintegral}{\iiint} \newcommand{\quadrupleintegral}{\iiiint} \newcommand{\conint}{\oint} \newcommand{\contourintegral}{\oint} \newcommand{\infinity}{\infty} \newcommand{\bottom}{\bot} \newcommand{\minusb}{\boxminus} \newcommand{\plusb}{\boxplus} \newcommand{\timesb}{\boxtimes} \newcommand{\intersection}{\cap} \newcommand{\union}{\cup} \newcommand{\Del}{\nabla} \newcommand{\odash}{\circleddash} \newcommand{\negspace}{\!} \newcommand{\widebar}{\overline} \newcommand{\textsize}{\normalsize} \renewcommand{\scriptsize}{\scriptstyle} \newcommand{\scriptscriptsize}{\scriptscriptstyle} \newcommand{\mathfr}{\mathfrak} \newcommand{\statusline}[2]{#2} \newcommand{\tooltip}[2]{#2} \newcommand{\toggle}[2]{#2} % Theorem Environments \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma} \newtheorem{prop}{Proposition} \newtheorem{cor}{Corollary} \newtheorem*{utheorem}{Theorem} \newtheorem*{ulemma}{Lemma} \newtheorem*{uprop}{Proposition} \newtheorem*{ucor}{Corollary} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{example}{Example} \newtheorem*{udefn}{Definition} \newtheorem*{uexample}{Example} \theoremstyle{remark} \newtheorem{remark}{Remark} \newtheorem{note}{Note} \newtheorem*{uremark}{Remark} \newtheorem*{unote}{Note} %------------------------------------------------------------------- \begin{document} %------------------------------------------------------------------- \section*{natural numbers object} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{topos_theory}{}\paragraph*{{Topos Theory}}\label{topos_theory} [[!include topos theory - contents]] \hypertarget{induction}{}\paragraph*{{Induction}}\label{induction} [[!include induction - contents]] \hypertarget{natural_numbers_object}{}\section*{{Natural numbers object}}\label{natural_numbers_object} \noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak \noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak \noindent\hyperlink{CCC}{In a topos or cartesian closed category}\dotfill \pageref*{CCC} \linebreak \noindent\hyperlink{withparams}{In a general category with finite products}\dotfill \pageref*{withparams} \linebreak \noindent\hyperlink{in_type_theory}{In type theory}\dotfill \pageref*{in_type_theory} \linebreak \noindent\hyperlink{finite_colimit_characterization}{Finite colimit characterization}\dotfill \pageref*{finite_colimit_characterization} \linebreak \noindent\hyperlink{free_constructions_in_a_topos}{Free constructions in a topos}\dotfill \pageref*{free_constructions_in_a_topos} \linebreak \noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak \noindent\hyperlink{ExamplesInASheafTopos}{In a sheaf topos}\dotfill \pageref*{ExamplesInASheafTopos} \linebreak \noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak \noindent\hyperlink{Transfer}{Transfer along inverse images}\dotfill \pageref*{Transfer} \linebreak \noindent\hyperlink{relation_to_object_of_integers}{Relation to object of integers}\dotfill \pageref*{relation_to_object_of_integers} \linebreak \noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{idea} Recall that a [[topos]] is a [[category]] that behaves likes the category [[Set]] of [[set|sets]]. A \textbf{natural numbers object} (NNO) in a topos is an [[object]] that behaves in that topos like the set $\mathbb{N}$ of [[natural number|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]] (\hyperlink{Law63}{1963}). \hypertarget{definition}{}\subsection*{{Definition}}\label{definition} \hypertarget{CCC}{}\subsubsection*{{In a topos or cartesian closed category}}\label{CCC} A \textbf{natural numbers object} in a [[topos]] (or any [[cartesian closed category]]) $E$ with [[terminal object]] $1$ is \begin{itemize}% \item an [[object]] $\mathbb{N}$ in $E$ \item equipped with \begin{itemize}% \item a [[morphism]] $z :1 \to \mathbb{N}$ from the [[terminal object]] $1$; \item a [[morphism]] $s : \mathbb{N} \to \mathbb{N}$ (successor); \end{itemize} \item such that for every other [[diagram]] $1 \stackrel{q}{\to}A \stackrel{f}{\to} A$ there is a unique morphism $u : \mathbb{N} \to A$ such that \end{itemize} \begin{displaymath} \itexarray{ 1 &\stackrel{z}{\to}& \mathbb{N} &\stackrel{s}{\to}& \mathbb{N} \\ & {}_q\searrow & \downarrow^{u} && \downarrow^{u} \\ && A &\stackrel{f}{\to} & A } \end{displaymath} All this may be summed up by saying that a natural numbers object is an [[initial algebra|initial]] [[algebra for an endofunctor|algebra for the endofunctor]] $X \mapsto 1 + X$ (the functor underlying the ``[[maybe monad]]''). Equivalently, it is an initial [[algebra for an endo-profunctor|algebra for the endo-profunctor]] $Hom_E(1,=) \times Hom_E(-,=)$. By the universal property, the natural numbers object is unique up to [[isomorphism]]. \begin{prop} \label{}\hypertarget{}{} Let $C, D$ be cartesian closed categories, and suppose $D$ has a natural numbers object $(\mathbb{N}, z: 1 \to \mathbb{N}, s: \mathbb{N} \to \mathbb{N})$. If $L: D \to C$ is a [[left adjoint]] that preserves the terminal object, then $(L \mathbb{N}, L z, L s)$ is a natural numbers object in $C$. \end{prop} The proof is straightforward. It follows for example that the left adjoint part $f^\ast$ of a geometric morphism $f^\ast \dashv f_\ast: E \to F$ between toposes with natural numbers objects preserves the natural numbers object, and also that a [[Grothendieck quasitopos]] $Q$ presented by a [[site]] $(C, J)$ has a natural numbers object, since the [[reflective subcategory|reflection functor]] $L: Set^{C^{op}} \to Q$ preserves finite products and the terminal object in particular. \hypertarget{withparams}{}\subsubsection*{{In a general category with finite products}}\label{withparams} Note that this definition actually makes sense in any category $E$ having finite [[product]]s. However, if $E$ is not [[cartesian closed category|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 $(\mathbb{N}, 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 cofree coalgebra functor into the [[Kleisli category]] of the [[comonad]] $X \mapsto A \times 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$). To be explicit: \begin{defn} \label{}\hypertarget{}{} In a category with finite products, a \emph{parametrized natural numbers object} is an object $N$ together with maps $z: 1 \to N$, $s: N \to N$ such that given any objects $A$, $X$ and maps $f: A \to X$, $g: X \to X$, there is a unique map $\phi_{f, g}: A \times N \to X$ making the following diagram commute: \begin{displaymath} \itexarray{ A & \stackrel{\langle z \circ !, 1_A\rangle}{\to} & N \times A & \stackrel{s \times 1_A}{\leftarrow} & N \times A \\ & \mathllap{f} \searrow & \downarrow \mathrlap{\phi_{f, g}} & & \downarrow \mathrlap{\phi_{f, g}} \\ & & X & \underset{g}{\leftarrow} & X } \end{displaymath} \end{defn} The functions which are constructible out of the structure of a category with finite products and such a ``parametrized NNO'' are precisely the [[partial recursive function|primitive recursive]] ones. Specifically, the unique structure-preserving functor from the free such category $F$ into [[Set]] yields a bijection between $Hom_F(1, \mathbb{N})$ and the actual natural numbers, as well as surjections from $Hom_F(\mathbb{N}^m, \mathbb{N})$ 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 [[partial recursive function|Ackermann function]]) become definable as well. In this context an important class is the class of [[pretopos|pretoposes]] with a parametrized NNO - the so called [[arithmetic pretopos|arithmetic pretoposes]]. \hypertarget{in_type_theory}{}\subsubsection*{{In type theory}}\label{in_type_theory} For the moment see at \emph{[[inductive type]]} the section \emph{\href{inductive+type#NaturalNumbers}{Examples - Natural numbers}} \hypertarget{finite_colimit_characterization}{}\subsection*{{Finite colimit characterization}}\label{finite_colimit_characterization} In a topos, the natural numbers object $\mathbb{N}$ is uniquely characterized by the following [[colimit]] conditions due to [[Peter Freyd]]: \begin{theorem} \label{Freyd}\hypertarget{Freyd}{} In a topos, a triple $(\mathbb{N}, 0: 1 \to \mathbb{N}, s: \mathbb{N} \to \mathbb{N})$ is a natural numbers object if and only if \begin{enumerate}% \item The morphism $(0, s): 1 + \mathbb{N} \to \mathbb{N}$ is an [[isomorphism]]; \item The diagram \begin{displaymath} \mathbb{N} \stackrel{\overset{s}{\to}}{\underset{1}{\to}} \mathbb{N} \to 1 \end{displaymath} is a [[coequalizer]]. \end{enumerate} \end{theorem} 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. \begin{proof} 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 + \mathbb{N} \to \mathbb{N}$ for the endofunctor $F(c) = 1 + c$ defined on $C$. Then condition 1 is a special case of [[initial algebra of an endofunctor|Lambek's theorem]], that the algebra structure map of an initial algebra is an isomorphism. As for condition 2, given $f: \mathbb{N} \to X$ such that $f = f \circ s$, the claim is that $f$ factors as \begin{displaymath} \mathbb{N} \overset{!}{\to} 1 \overset{x}{\to} X \end{displaymath} for some unique $x$, in fact for $x = f(0)$. Uniqueness is clear since $!: \mathbb{N} \to 1$, being a retraction for $0: 1 \to \mathbb{N}$, is epic. On the other hand, substituting either $f$ or $f(0) \circ !$ for $g$ in the diagram \begin{displaymath} \itexarray{ 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 } \end{displaymath} this diagram commutes, so that $f = f(0) \circ !$ by the uniqueness clause in the universal property for $\mathbb{N}$. \end{proof} \begin{proof} Here we just give an outline, referring to \hyperlink{Johnstone}{(Johnstone)}, section D.5.1, for full details. Let $N$ be an object satisfying the two colimit conditions of Freyd. First one shows (see the lemma \ref{Peano} below) that $N$ has no nontrivial $F$-subalgebras. Next, let $A$ be any $F$-algebra, and let $i: B \to N \times A$ be the intersection of all $F$-subalgebras of $N \times A$. One shows that $\pi_1 \circ i: B \to N$ is an ($F$-algebra) isomorphism. Thus we have an $F$-algebra map $f: N \to A$. If $g: N \to A$ 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$. \end{proof} \begin{lemma} \label{Peano}\hypertarget{Peano}{} Let $F$ be the endofunctor $F(X) = 1+X$. If $N$ satisfies Freyd's colimit conditions, then any $F$-subalgebra of $N$ is the entirety of $N$. \end{lemma} \begin{proof} Following \hyperlink{Johnstone}{(Johnstone)}, we may as well show that the smallest $F$-subalgebra $N'$ of $N$ (the internal intersection of all $F$-subalgebras) is all of $N$. Let $S \hookrightarrow N \times N$ be the union of the relation $R = \langle 1, s \rangle: N \to N \times N$ and its opposite, so that $S$ is a symmetric relation. Working in the Mitchell-B\'e{}nabou language, one may check directly that the following formula is satisfied: \begin{displaymath} \forall x, y: N (\langle x, y \rangle \in S) \Rightarrow ((x \in N') \Leftrightarrow (y \in N')) \end{displaymath} Let us say a term $w$ of type $P N$ is $S$-\textbf{closed} if the formula \begin{displaymath} \forall x, y: N (\langle x, y \rangle \in S) \Rightarrow ((x \in [w]) \Leftrightarrow (y \in [w])) \end{displaymath} is satisfied. Now define a relation $T$ on $N$ by the subobject \begin{displaymath} \{\langle x, y \rangle \in N \times N: \forall w: P N (w \; is \; S closed) \Rightarrow ((x \in [w]) \Leftrightarrow (y \in [w])). \end{displaymath} Observe that $T$ is an equivalence relation that contains $S$ and therefore $R$. It therefore contains the kernel pair of the coequalizer of $1$ and $s$; since this coequalizer is by assumption $N \to 1$, the kernel pair is all of $N \times N$. Also observe that since $N'$ is $S$-closed by definition, it is $T$-closed as well, and we now conclude \begin{displaymath} \forall x, y \in N: (x \in N') \Leftrightarrow (y \in N') \end{displaymath} so that, putting $y = 0: 1 \to N'$, we conclude that $x \in N \Rightarrow x \in N'$, i.e., that $N'$ is all of $N$. \end{proof} \begin{uremark} A slightly alternative proof of sufficiency uses the theory of well-founded coalgebras, as given \href{http://ncatlab.org/toddtrimble/published/Initial+algebras+and+terminal+coalgebras}{here}. If $N$ is a fixpoint of the functor $F(X) = 1+X$, regarded as an $F$-[[coalgebra for an endofunctor|coalgebra]], then the internal union of well-founded subcoalgebras of $N$ is a natural numbers object $\mathbb{N}$. Then the subobject $\mathbb{N} \hookrightarrow N$ can also be regarded as a subalgebra; by the lemma, it is all of $N$. Thus $N$ is a natural numbers object. \end{uremark} \hypertarget{free_constructions_in_a_topos}{}\subsection*{{Free constructions in a topos}}\label{free_constructions_in_a_topos} In [[topos theory]] the existence of a natural numbers object (NNO) has a couple of far-reaching consequences. Firstly, it is a theorem is due to C. J. Mikkelsen that the existence of a NNO in a topos $\mathcal{S}$ is equivalent to the existence of [[free monoid|free monoids]] in $\mathcal{S}$: \begin{prop} \label{free_monoids_in_topos}\hypertarget{free_monoids_in_topos}{} Let $\mathcal{S}$ be a topos and $\mathbf{mon}(\mathcal{S})$ its category of internal monoids. Then $\mathcal{S}$ has a NNO precisely if the forgetful functor $U:\mathbf{mon}(\mathcal{S})\to \mathcal{S}$ has a left adjoint. \end{prop} For a proof see Johnstone (\hyperlink{JT77}{1977},p.190). Secondly, it then is a theorem due to [[Andreas Blass]] (\hyperlink{Blass}{1989}) that $\mathcal{S}$ has a NNO precisely if $\mathcal{S}$ has an [[classifying topos for the theory of objects|object classifier]] $\mathcal{S}[\mathbb{O}]$. A consequence of this, discussed in sec. B4.2 of (Johnstone 2002,I p.431), is that [[classifying topos|classifying toposes]] for [[geometric theories]] over $\mathcal{S}$ exist precisely if $\mathcal{S}$ has a NNO. So from a different perspective, in a topos the existence of free objects over various gadgets like e.g. [[algebraic theory|algebraic theories]] or [[geometric theory|geometric theories]] (often) hinge on the existence of free monoids, the intuition being that the free monoids permit to construct a free model \emph{syntactically} by providing for the (syntactic) building blocks needed for this process. Notice that algebraic theories can nevertheless have free algebras even if the ambient topos lacks a NNO. This may happen for algebraic theories that have the property that the free algebra on a finite set of generators has a finite carrier e.g. in the topos $FinSet$ of finite sets [[graphic category|free graphic monoids]] exist. \hypertarget{examples}{}\subsection*{{Examples}}\label{examples} \hypertarget{ExamplesInASheafTopos}{}\subsubsection*{{In a sheaf topos}}\label{ExamplesInASheafTopos} 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^{op} \to Set$ that is constant on the set $\mathbb{N}$. 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 \textbf{[[smooth natural numbers]]} that has [[generalized element]]s which are ``infinite natural numbers'' in the sense of [[nonstandard analysis]]. \hypertarget{properties}{}\subsection*{{Properties}}\label{properties} \hypertarget{Transfer}{}\subsubsection*{{Transfer along inverse images}}\label{Transfer} \begin{prop} \label{}\hypertarget{}{} Natural number objects are preserved by [[inverse images]]: let $f = (f^* \dashv f_*) : \mathcal{E} \underoverset{f_*}{f^*}{\leftrightarrows} \mathcal{F}$ be a [[geometric morphism]] of toposes. If $\mathbb{N} \in \mathcal{F}$ is a natural numbers object, then its [[inverse image]] $f^* \mathbb{N}$ is a natural numbers object in $\mathcal{E}$. \end{prop} (\hyperlink{Johnstone}{Johnstone, lemma A.4.1.14}). Of course, by the \href{http://ncatlab.org/nlab/show/natural+numbers+object#finite_colimit_characterization_24}{finite colimit characterization}, we need only the fact that inverse images preserve finite colimits and the terminal object. \begin{example} \label{}\hypertarget{}{} If $\mathcal{E}$ is a [[sheaf topos]], then there is a unique [[geometric morphism]] $(\Delta \dashv \Gamma): \mathcal{E} \underoverset{\Gamma}{\Delta}{\leftrightarrows} Set$, the [[global section]] geometric morphism, with the [[inverse image]] being the [[locally constant sheaf]] functor, it follows that \begin{displaymath} \Delta(\mathbb{N}) \cong \Delta(\sum_{n: \mathbb{N}} 1) \cong \sum_{n: N} \Delta 1 \cong \sum_{n: \mathbb{N}} 1, \end{displaymath} with the evident successor and constant $0$, is the natural nunbers object in $\mathcal{E}$. \end{example} \begin{example} \label{}\hypertarget{}{} If $\mathcal{E}$ is a topos and $X \in \mathcal{E}$ an object, then the [[slice topos]] sits by an [[etale geometric morphism]] over $\mathcal{E}$ \begin{displaymath} \mathcal{E}_{/X} \stackrel{\overset{X^*}{\leftarrow}}{\underset{X_*}{\to}} \mathcal{E} \,, \end{displaymath} where the [[inverse image]] form the [[product]] with $X$. Hence for $\mathbb{N} \in \mathcal{E}$ a natural numbers object, the projection $(X \times \mathbb{N} \to X)$ is a natural numbers object in $\mathcal{E}_{/X}$. \end{example} \hypertarget{relation_to_object_of_integers}{}\subsubsection*{{Relation to object of integers}}\label{relation_to_object_of_integers} Given a natural numbers object $\mathbb{N}$ in a [[pretopos]], we can construct an [[integers]] object as follows. Let $a, b\colon E \to \mathbb{N} \times \mathbb{N}$ be the [[kernel pair]] of the addition map ${+}\colon \mathbb{N} \times \mathbb{N} \to \mathbb{N}$, and let $\pi_1, \pi_2\colon \mathbb{N} \times \mathbb{N} \to \mathbb{N}$ be the [[product]] projections. We define $\mathbb{Z}$ to be the [[coequalizer]] of the [[congruence]] $(\pi_1 \circ a, \pi_2 \circ b), (\pi_2 \circ a, \pi_1 \circ b)\colon E \to \mathbb{N} \times \mathbb{N}$. A similar construction yields a [[rational numbers]] object $\mathbb{Q}$. For a [[real numbers]] object, rather more care is needed; see [[real numbers object]]. \hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts} \begin{itemize}% \item [[natural numbers]] \item [[natural numbers type]] \item [[Peano arithmetic]] \item [[free monoid]] \item [[arithmetic pretopos]] \end{itemize} \hypertarget{references}{}\subsection*{{References}}\label{references} \begin{itemize}% \item [[F. William Lawvere]], \emph{[[Functorial Semantics of Algebraic Theories]]} , Ph.D. thesis Columbia University 1963. (Published with an author's comment as TAC Reprint no.5 (2004) pp 1-121. (\href{http://www.tac.mta.ca/tac/reprints/articles/5/tr5abs.html}{abstract}) \item [[Jean Bénabou]], \emph{Some Remarks on Free Monoids in a Topos} , pp.20-29 in LNM \textbf{1488} Springer Heidelberg 1991. \item [[Andreas Blass]], \emph{Classifying topoi and the axiom of infinity} , Algebra Universalis \textbf{26} (1989) pp.341-345. \item [[Peter Johnstone]], \emph{Topos Theory} , Academic Press New York 1977. (Dover reprint Minneola 2014, chap. 6) \item [[Peter Johnstone]], \emph{[[Sketches of an Elephant]]} , Oxford UP 2002. \end{itemize} [[!redirects natural numbers object]] [[!redirects natural numbers objects]] [[!redirects natural number object]] [[!redirects natural number objects]] [[!redirects natural-numbers object]] [[!redirects natural-numbers objects]] [[!redirects natural-number object]] [[!redirects natural-number objects]] [[!redirects NNO]] [[!redirects NNOs]] \end{document}