自然数オブジェクト

数学の圏論において、自然数オブジェクト（NNO ）とは、自然数と同様の再帰構造を持つオブジェクトのことである。より正確には、終端オブジェクト1を持つ圏Eにおいて、NNO Nは次のように定義される。

1. グローバル要素z  : 1 → N、
2. 矢印s : N → N、​ 

Eの任意のオブジェクトA、グローバル要素q : 1 → A、および矢印f : A → Aに対して、次のような一意の矢印u : N → Aが存在する。   

1. u ∘ z = q、そして
2. u ∘ s = f ∘ u。^{[ 1 ] [ 2 ] [ 3 ]}

つまり、次の図の三角形と四角形は可換である。

ペア ( q , f ) は、uの再帰データと呼ばれることもあり、再帰的な定義の形で与えられます。

1. ⊢ u ( z ) = q
2. y ∈ _E N ⊢ u ( s y ) = f ( u ( y ))

上記の定義はNNOの普遍的な性質であり、正準同型を除いて 定義されていることを意味します。上記のように定義された矢印uが存在するだけでよく、一意性が要求されない場合、Nは弱いNNOと呼ばれます。

デカルト閉圏(CCC)における NNO は、次のような同等な方法で定義されることがあります ( Lawvereによる)。任意の矢印のペアg  : A → Bとf  : B → Bに対して、次の図の正方形が可換となるような一意のh  : N × A → Bが存在します。 ^{[ 4 ]}

この同じ構成により、デカルト的に閉じていないデカルト圏における弱いNNOが定義される。

終端オブジェクト 1 と二項積(+ で表される)を持つ圏では、NNO は、オブジェクトに対してX ↦ 1 + Xで作用し、矢印に対してf ↦ id ₁ + fで作用する自己関手の初期代数として定義できる。^{[ 5 ]}

• すべての NNO は、次の形式の図のカテゴリの初期オブジェクトです。

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

• 直交閉圏に弱いNNOが存在する場合、その圏のすべてのスライスにも弱いNNOが存在する。
• NNOは、解析学の非標準モデルと同様の方法で、型理論の非標準モデルにも使用できます。このような圏（またはトポス）は、「無限に多くの」非標準自然数を持つ傾向があります。 （いつものように、非標準NNOを得る簡単な方法があります。たとえば、z = szの場合、圏またはトポスEは自明です。）
• フレイドは、 zとsがNNOのコプロダクト図を形成することを示した。また、  ! _N  : N → 1はsと1N_のコイコライザーであり、つまりNのグローバル要素の任意のペアはsによって結び付けられる。さらに、この2つの事実はすべてのNNOを特徴づける。

• 集合の圏Setにおいて、標準自然数は NNO です。^{[ 6 ]} Setの終端オブジェクトはシングルトンであり、シングルトンからの関数は集合の単一の要素を選び出します。自然数 𝐍 は NNO であり、 zはシングルトンから 𝐍 への関数で、その像はゼロであり、sは後継関数です。（実際には、 z が𝐍 の任意の要素を選び出すことを許可しても、結果として得られる NNO はこの NNO と同型になります。）定義の図式が可換であることは、数学的帰納法を用いて証明できます。
• マルティン＝レーフ型理論の型（型を対象、関数を矢印とする）のカテゴリーにおいて、標準的な自然数型natは NNO である。nat の再帰関数を用いることで、適切な図式が可換であることを示すことができる。
• と仮定する${\displaystyle {\mathcal {E}}}$終端オブジェクトを持つグロタンディーク・トポスである${\displaystyle \top }$そしてそれは${\displaystyle {\mathcal {E}}\simeq \mathbf {Shv} ({\mathfrak {C}},J)}$グロタンディーク位相の場合${\displaystyle J}$カテゴリーについて${\displaystyle {\mathfrak {C}}}$ならば$\displaystyle \Gamma _{\mathbb {N}}$定数前層は${\displaystyle {\mathfrak {C}}}$するとNNOは${\displaystyle {\mathcal {E}}}$は、$\displaystyle \Gamma _{\mathbb {N}}$そして、次のような形をとることが示されるかもしれない$${\displaystyle \mathbb {N} _{\mathcal {E}}\cong \left(\Gamma _{\mathbb {N} }\right)^{++}\cong \coprod _{n\in \mathbb {N} }\top .}$$

• ペアノの算術の公理
• カテゴリー論理

• ジョンストン、ピーター・T. (2002). 『象のスケッチ：トポス理論概説』 オックスフォード：オックスフォード大学出版局。ISBN 0198534256OCLC 50164783​​ 
• Lawvere, William (2005) [1964]. 「集合の圏の初等理論（長編版）解説付き」 . Theory and Applications of Categories 再録. 11 : 1– 35.

• ロバート・ハーパーによる講義ノート（第2.2節でNNOについて解説）：https://www.cs.cmu.edu/~rwh/courses/hott/notes/notes_week3.pdf
• Clive Newstead氏によるn -Category Cafeのブログ記事：https://golem.ph.utexas.edu/category/2014/01/an_elementary_theory_of_the_ca.html
• コンピュータ科学者フィリップ・ワドラーによる、自己関手の代数としてのデータ型に関する注記：http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt
• nLabに関する注記：https://ncatlab.org/nlab/show/ETCS