En la teoría de categorías , un objeto de números naturales ( NNO ) es un objeto dotado de una estructura recursiva similar a los números naturales . Más precisamente, en una categoría E con un objeto terminal 1, un NNO N viene dado por:
- un elemento global z : 1 → N , y
- una flecha s : N → N ,
tal que para cualquier objeto A de E , elemento global q : 1 → A , y flecha f : A → A , existe una flecha única u : N → A tal que:
En otras palabras, el triángulo y el cuadrado en el siguiente diagrama se desplazan.
El par ( q , f ) a veces se denomina datos de recursividad para u , dado en forma de definición recursiva :
- ⊢ u ( z ) = q
- y ∈ E N ⊢ u ( s y ) = f ( u ( y ))
La definición anterior es propiedad universal de los NNO, lo que significa que se definen hasta el isomorfismo canónico . Si la flecha u , tal como se definió anteriormente, simplemente tiene que existir, es decir, no se requiere la unicidad, entonces N se denomina NNO débil .
Definiciones equivalentes
NNOS en categorías cerradas cartesianas (CCCs) o topoi a veces se definen de la siguiente manera equivalente (debido a Lawvere ): para cada par de flechas g : A → B y f : B → B , hay un único h : N × A → B de manera que los cuadrados del siguiente diagrama se conmuten. [4]
Esta misma construcción define NNO débiles en categorías cartesianas que no son cartesianas cerradas.
En una categoría con un objeto terminal 1 y coproductos binarios (denotado por +), un NNO se puede definir como el álgebra inicial del endofunctor que actúa sobre los objetos por X ↦ 1 + X y sobre las flechas por f ↦ [id 1 , f ] . [5]
Propiedades
- Cada NNO es un objeto inicial de la categoría de diagramas de la forma
- Si una categoría cerrada cartesiana tiene NNO débiles, entonces cada porción de ella también tiene un NNO débil.
- Los NNO se pueden utilizar para modelos no estándar de teoría de tipos de manera análoga a los modelos de análisis no estándar. Tales categorías (o topoi) tienden a tener "infinitos" números naturales no estándar. [ aclaración necesaria ] (Como siempre, hay formas sencillas de obtener NNO no estándar; por ejemplo, si z = sz , en cuyo caso la categoría o el topos E es trivial).
- Freyd mostró que z y s forman un coproducto diagrama para nNOS; además, ! N : N → 1 es un coecualizador de sy 1 N , es decir , cada par de elementos globales de N están conectados por medio de s ; además, este par de hechos caracteriza a todos los NNO.
Ejemplos de
- En Conjunto , la categoría de conjuntos , los números naturales estándar son un NNO. [6] Un objeto terminal en Set es un singleton , y una función de un singleton selecciona un solo elemento de un conjunto. Los números naturales 𝐍 son un NNO donde z es una función de un singleton a 𝐍 cuya imagen es cero, y s es la función sucesora . (De hecho, podríamos permitir que z seleccionara cualquier elemento de 𝐍, y el NNO resultante sería isomorfo a éste.) Se puede probar que el diagrama en la definición conmuta usando inducción matemática .
- En la categoría de tipos de la teoría de tipos de Martin-Löf (con tipos como objetos y funciones como flechas), el tipo de números naturales estándar nat es un NNO. Se puede usar el recursor para nat para mostrar que el diagrama apropiado conmuta.
- Asumir que es un topos de Grothendieck con objeto terminal y eso para alguna topología de Grothendieck en la categoría . Entonces sí es la gavilla constante en , luego el NNO en es la gavilla de y puede mostrarse que toma la forma
Ver también
- Los axiomas de la aritmética de Peano
- Lógica categórica
Referencias
- ^ Johnstone 2002 , A2.5.1.
- ^ Lawvere 2005 , p. 14.
- ^ Leinster, Tom (2014). "Repensar la teoría de conjuntos". American Mathematical Monthly . 121 (5): 403–415. arXiv : 1212.6543 . Código Bib : 2012arXiv1212.6543L . doi : 10.4169 / amer.math.monthly.121.05.403 .
- ^ Johnstone 2002 , A2.5.2.
- ^ Barr, Michael; Wells, Charles (1990). Teoría de categorías para ciencias de la computación . Nueva York: Prentice Hall. pag. 358. ISBN 0131204866. OCLC 19126000 .
- ^ Johnstone 2005 , p. 108.
- Johnstone, Peter T. (2002). Bocetos de un elefante: un compendio de teoría de Topos . Oxford: Prensa de la Universidad de Oxford. ISBN 0198534256. OCLC 50164783 .
- Lawvere, William (2005) [1964]. "Una teoría elemental de la categoría de conjuntos (versión larga) con comentario" . Reimpresiones en teoría y aplicaciones de categorías . 11 : 1–35.
enlaces externos
- Notas de la conferencia de Robert Harper que discuten los NNO en la Sección 2.2: https://www.cs.cmu.edu/~rwh/courses/hott/notes/notes_week3.pdf
- Una publicación de blog de Clive Newstead en n -Category Cafe: https://golem.ph.utexas.edu/category/2014/01/an_elementary_theory_of_the_ca.html
- Notas sobre tipos de datos como álgebras para endofunctores por el científico informático Philip Wadler : http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt
- Notas sobre nLab : https://ncatlab.org/nlab/show/ETCS