En théorie des catégories, une branche des mathématiques, un objet nombres naturels (ONN) est un objet muni d'une structure récursive semblable à celle des nombres naturels. Plus précisément, dans une catégorie E avec objet terminal 1, un ONN N est défini par :
un élément global z : 1 → N, et une flèche s : N → N ,
tels que pour tout objet A de E, élément global q : 1 → A, et flèche f : A → A, il existe une unique flèche u : N → A telle que :
u ∘ z = q, et u ∘ s = f ∘ u.
Dit autrement, le triangle et le carré du diagramme suivant commutent.250x250px|A commutative diagram expressing the equations in the definition of an NNOLa paire (q, f) est parfois appelée donnée de récursion pour u, sous la forme d'une définition récursive :
⊢ u ( z ) = q y ∈ E N ⊢ u ( s y ) = f ( u ( y ))
Cette définition est la propriété universelle des ONN, c'est-à-dire qu'ils sont définis à isomorphisme canonique près. Si l'existence de la flèche u telle que définie ci-dessus est la seule condition requise, c'est-à-dire si l'unicité n'est pas nécessaire, alors N est appelé un NNO faible.
Définitions équivalentes Les OON dans les catégories cartésiennes fermées ou topos sont parfois définis de la manière équivalente suivante (que l'on doit à Lawvere ) : pour toute paire de flèches g : A → B et f : B → B, il existe un unique h: N × A → B tel que les carrés du diagramme suivant commutent. alternate NNO definitionCette même construction définit des OON faibles dans des catégories cartésiennes qui ne sont pas fermées-cartésiennes.
Dans une catégorie avec objet terminal 1 et avec coproduits notés +, un OON peut être défini comme l'algèbre initiale de l'endofoncteur qui agit sur les objets par et qui agit sur les flèches par .
Propriétés
Tout OON est un objet initial de la catégorie des diagrammes de la forme
Si une catégorie cartésienne fermée possède des OON faibles, alors chaque tranche (slice) de celle-ci possède également un OON faible. Les OON peuvent être utilisés pour des modèles non standards de la théorie des types, de manière analogue aux modèles non standards de l'analyse. Des catégories telles (ou topos) tendent à posséder une "infinité" de nombres naturels non standards. (Comme toujours, il existe des moyens simples d'obtenir des OON non standards ; par exemple, si z = sz, auquel cas la catégorie ou le topoi E est trivial.) Freyd a montré que z et s forment un diagramme de coproduits pour les OON; de plus, ! N : N → 1 est un coégalisateur de s et 1 N, c'est-à-dire que chaque paire d'éléments globaux de N est connectée au moyen de s ; de plus, ces deux faits caractérisent tous les OON.
Exemples
Dans la catégorie des ensembles, l'ensemble des nombres naturels usuels est un OON. Un objet terminal de Ens, et une fonction d'un singleton sélectionne un unique élément de l'ensemble. L'ensemble des nombres naturels 𝐍 est un OONoù est une fonction d'un singleton vers 𝐍 dont l'image est nulle, et est la fonction successeur. (On pourrait en fait autoriser à sélectionner n'importe quel élément de 𝐍, et le OON résultant serait isomorphe à celui-ci.) On peut démontrer que le diagramme de la définition commute par récurrence. Dans la catégorie des types de la théorie des types de Martin-Löf (où les types sont des objets et les fonctions des flèches), le type standard des nombres naturels `nat` est un OON. On peut utiliser le récurseur de `nat` pour montrer que le diagramme correspondant commute. Supposons que est un topos de Grothendieck avec objet terminal et que pour une certaine topologie de Grothendieck dans la catégorie . Alors si est le préfaisceau constant sur , alors le OON dans est la sheafification de et on peut montrer que cela se présente sous la forme
Voir aussi
Les axiomes arithmétiques de Peano Logique catégorique
Références
Liens externes
Notes de cours de Robert Harper traitant des OON dans la section 2.2 : https://www.cs.cmu.edu/~rwh/courses/hott/notes/notes_week3.pdf Un article de blog de Clive Newstead sur le -Category Cafe : https://golem.ph.utexas.edu/category/2014/01/an_elementary_theory_of_the_ca.html Notes sur les types de données en tant qu'algèbres pour endofoncteurs par l'informaticien Philip Wadler : http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt Notes sur nLab : https://ncatlab.org/nlab/show/ETCS
Catégorie:Théorie des catégories