Categoría cerrada cartesiana

En teoría de categorías , una categoría es cartesiana cerrada si, en términos generales, cualquier morfismo definido en un producto de dos objetos puede identificarse naturalmente con un morfismo definido en uno de los factores. Estas categorías son particularmente importantes en lógica matemática y teoría de la programación, ya que su lenguaje interno es el cálculo lambda simplemente tipado . Se generalizan mediante categorías monoidales cerradas , cuyo lenguaje interno, los sistemas de tipos lineales , son adecuados tanto para la computación cuántica como para la clásica. ^{[ 1 ]}

Etimología

Recibe su nombre de René Descartes (1596-1650), filósofo, matemático y científico francés, cuya formulación de la geometría analítica dio origen al concepto de producto cartesiano , que posteriormente se generalizó a la noción de producto categórico .

Definición

La categoría C se denomina cartesiana cerrada ^{[ 2 ]} si satisface las siguientes tres propiedades:

Tiene un objeto terminal .
Cualquier par de objetos X e Y de C tienen un producto X × Y en C.
Cualquier par de objetos Y y Z de C tienen una función exponencial Z ^Y en C.

Las dos primeras condiciones se pueden combinar en el único requisito de que cualquier familia finita (posiblemente vacía) de objetos de C admita un producto en C , debido a la asociatividad natural del producto categórico y porque el producto vacío en una categoría es el objeto terminal de esa categoría.

La tercera condición es equivalente al requisito de que el functor –× Y (es decir, el functor de C a C que mapea objetos X a X × Y y morfismos φ a φ × id _Y ) tenga un adjunto derecho , usualmente denotado – ^Y , para todos los objetos Y en C. Para categorías localmente pequeñas , esto puede expresarse por la existencia de una biyección entre los conjuntos hom. $\mathrm {Hom} (X\times Y,Z)\cong \mathrm {Hom} (X,Z^{Y})$ ^lo cual es natural en X , Y y Z. ^[³ ]

Tenga en cuenta que una categoría cartesiana cerrada no tiene por qué tener límites finitos ; solo se garantizan productos finitos.

Si una categoría tiene la propiedad de que todas sus categorías de rebanadas son cartesianas cerradas, entonces se dice que es localmente cartesiana cerrada . ^{[ 4 ]} Nótese que si C es localmente cartesiana cerrada, no tiene por qué ser realmente cartesiana cerrada; eso ocurre si y solo si C tiene un objeto terminal.

Construcciones básicas

Evaluación

Para cada objeto Y , la counidad de la adjunción exponencial es una transformación natural. $\mathrm {ev} _{Y,Z}:Z^{Y}\times Y\to Z$ denominado mapa de evaluación (interno) . De forma más general, podemos construir el mapa de aplicación parcial como el compuesto $\mathrm {papply} _{X,Y,Z}:Z^{X\times Y}\times X\cong (Z^{Y})^{X}\times X\,\xrightarrow {\overset {}{\mathrm {ev} _{X,Z^{Y}}}} \,Z^{Y}.$

En el caso particular de la categoría Conjunto , estas se reducen a las operaciones ordinarias: $\mathrm {ev} _ {Y,Z}(f,y)=f(y).$

Composición

Evaluar la exponencial en un argumento en un morfismo p : X → Y da morfismos ${\begin{aligned}p^{Z}:X^{Z}\to Y^{Z},\\Z^{p}&:Z^{Y}\to Z^{X},\end{aligned}}$ correspondiente a la operación de composición con p . Las notaciones alternativas para la operación p ^Z incluyen p _* y p ∘-. Las notaciones alternativas para la operación Z ^p incluyen p ^* y -∘ p .

Los mapas de evaluación se pueden encadenar como $Z^{Y}\times Y^{X}\times X\,\xrightarrow {\mathrm {id} \times \mathrm {ev} _{X,Y}} \,Z^{Y}\times Y\,\xrightarrow {\mathrm {ev} _{Y,Z}} \,Z$ la flecha correspondiente bajo la adjunción exponencial $c_{X,Y,Z}:Z^{Y}\times Y^{X}\to Z^{X}$ Se denomina mapa de composición (interno) .

En el caso particular de la categoría Conjunto , esta es la operación de composición ordinaria: $c_{X,Y,Z}(g,f)=g\circ f.$

Secciones

Para un morfismo p : X → Y , supongamos que existe el siguiente cuadrado de retroceso , que define el subobjeto de X ^Y correspondiente a las aplicaciones cuya composición con p es la identidad: ${\begin{array}{ccc}\Gamma _{Y}(p)&\to &X^{Y}\\\downarrow &&\downarrow \\1&\to &Y^{Y}\end{array}}$ donde la flecha de la derecha es p ^Y y la flecha de abajo corresponde a la identidad en Y. Entonces Γ _Y ( p ) se llama el objeto de secciones de p . A menudo se abrevia como Γ _Y ( X ).

Si Γ _Y ( p ) existe para cada morfismo p con codominio Y , entonces se puede ensamblar en un functor Γ _Y : C / Y → C en la categoría de rebanadas, que es adjunto derecho a una variante del functor producto: $\hom _{C/Y}(X\times Y\,\xrightarrow {\overset {}{\pi _{2}}} \,Y,Z\,\xrightarrow {\overset {}{p}} \,Y)\cong \hom _{C}(X,\Gamma _{Y}(p)).$ La exponencial por Y se puede expresar en términos de secciones: $Z^{Y}\cong \Gamma _ {Y}(Z\times Y\,\xrightarrow {\overset {}{\pi _{2}}} \,Y).$

Ejemplos

Algunos ejemplos de categorías cartesianas cerradas son:

La categoría Conjunto de todos los conjuntos , con funciones como morfismos, es cartesiana cerrada. El producto X × Y es el producto cartesiano de X e Y , y Z ^Y es el conjunto de todas las funciones de Y a Z. La adjunción se expresa mediante el siguiente hecho: la función f : X × Y → Z se identifica naturalmente con la función currificada g : X → Z ^Y definida por g ( x )( y ) = f ( x , y ) para todo x en X e y en Y.
La subcategoría de conjuntos finitos , con funciones como morfismos, también es cartesiana cerrada por la misma razón.
Si G es un grupo , entonces la categoría de todos los G -conjuntos es cartesiana cerrada. Si Y y Z son dos G -conjuntos, entonces Z ^Y es el conjunto de todas las funciones de Y a Z con acción G definida por ( g . F )( y ) = g .F( g ⁻¹ . y ) para todo g en G , F : Y → Z e y en Y .
La subcategoría de conjuntos G finitos también es cartesiana cerrada.
La categoría Cat de todas las categorías pequeñas (con functores como morfismos) es cartesiana cerrada; la exponencial C ^D viene dada por la categoría de functores que consiste en todos los functores de D a C , con transformaciones naturales como morfismos.
Si C es una categoría pequeña , entonces la categoría de funtores Set ^C que consta de todos los funtores covariantes de C en la categoría de conjuntos, con transformaciones naturales como morfismos, es cartesiana cerrada. Si F y G son dos funtores de C a Set , entonces el exponencial F ^G es el funtor cuyo valor en el objeto X de C está dado por el conjunto de todas las transformaciones naturales de ( X , −) × G a F .
- El ejemplo anterior de G -conjuntos puede verse como un caso especial de categorías de funtores: cada grupo puede considerarse como una categoría de un solo objeto, y los G- conjuntos no son más que funtores de esta categoría a Conjunto
- La categoría de todos los grafos dirigidos es cartesiana cerrada; esta es una categoría de funtores, como se explica en la sección de categorías de funtores.
- En particular, la categoría de conjuntos simpliciales (que son functores X : Δ ^op → Set ) es cartesiana cerrada.
De forma aún más general, todo topos elemental es cartesiano cerrado.
En topología algebraica , las categorías cartesianas cerradas son particularmente fáciles de manejar. Ni la categoría de espacios topológicos con aplicaciones continuas ni la categoría de variedades diferenciables con aplicaciones diferenciables son cartesianas cerradas. Por lo tanto, se han considerado categorías sustitutas: la categoría de espacios de Hausdorff generados de forma compacta es cartesiana cerrada, al igual que la categoría de espacios de Frölicher .
En la teoría del orden , los órdenes parciales completos ( CPO ) tienen una topología natural , la topología de Scott , cuyos mapas continuos forman una categoría cartesiana cerrada (es decir, los objetos son los CPO y los morfismos son los mapas continuos de Scott ). Tanto la función de currificación como la de aplicación son funciones continuas en la topología de Scott, y la función de currificación, junto con la de aplicación, proporcionan el adjunto. ^{[ 5 ]}
Un álgebra de Heyting es un retículo cartesiano cerrado (acotado) . Un ejemplo importante surge de los espacios topológicos. Si X es un espacio topológico, entonces los conjuntos abiertos en X forman los objetos de una categoría O( X ) para la cual existe un único morfismo de U a V si U es un subconjunto de V y ningún morfismo en caso contrario. Este poset es una categoría cartesiana cerrada: el "producto" de U y V es la intersección de U y V y la exponencial U ^V es el interior de $U ∪( X \ V )$ .
Una categoría con un objeto cero es cartesiana cerrada si y solo si es equivalente a una categoría con un solo objeto y un morfismo identidad. En efecto, si 0 es un objeto inicial y 1 es un objeto final y tenemos $0\cong 1$ $0\cong 1$ , entonces $\mathrm {Hom} (X,Y)\cong \mathrm {Hom} (1,Y^{X})\cong \mathrm {Hom} (0,Y^{X})\cong 1$ $\mathrm {Hom} (X,Y)\cong \mathrm {Hom} (1,Y^{X})\cong \mathrm {Hom} (0,Y^{X})\cong 1$ que tiene un solo elemento. ^{[ 6 ]}
- En particular, cualquier categoría no trivial con un objeto cero, como una categoría abeliana , no es cartesiana cerrada. Por lo tanto, la categoría de módulos sobre un anillo no es cartesiana cerrada. Sin embargo, el producto tensorial functor sí lo es. $-\otimes M$ con un módulo fijo sí tiene un adjunto derecho . El producto tensorial no es un producto categórico, por lo que esto no contradice lo anterior. Obtenemos en cambio que la categoría de módulos es monoidal cerrada .

Algunos ejemplos de categorías cerradas cartesianas locales son:

Todo topos elemental es localmente cartesiano cerrado. Este ejemplo incluye Set , FinSet , G -conjuntos para un grupo G , así como Set ^C para categorías pequeñas C.
La categoría LH cuyos objetos son espacios topológicos y cuyos morfismos son homeomorfismos locales es localmente cartesiana cerrada, ya que LH / X es equivalente a la categoría de haces . $Sh(X)$ Sin embargo, LH no tiene un objeto terminal y, por lo tanto, no es cartesiano cerrado.
Si C tiene retrocesos y para cada flecha p : X → Y , el functor p ^* : C/Y → C/X dado al tomar retrocesos tiene un adjunto derecho, entonces C es localmente cartesiano cerrado.
Si C es localmente cartesiana cerrada, entonces todas sus categorías de rebanadas C / X también son localmente cartesianas cerradas.

Algunos ejemplos de categorías cerradas localmente cartesianas son:

El gato no está cerrado cartesiano localmente.

Aplicaciones

En las categorías cartesianas cerradas, una "función de dos variables" (un morfismo f : X × Y → Z ) siempre puede representarse como una "función de una variable" (el morfismo λ f : X → Z ^Y ). En aplicaciones informáticas , esto se conoce como currificación ; ha llevado a la constatación de que el cálculo lambda de tipo simple puede interpretarse en cualquier categoría cartesiana cerrada.

La correspondencia de Curry-Howard-Lambek proporciona un isomorfismo profundo entre la lógica intuicionista , el cálculo lambda de tipos simples y las categorías cartesianas cerradas.

Ciertas categorías cartesianas cerradas, los topoi , se han propuesto como un marco general para las matemáticas, en lugar de la teoría de conjuntos tradicional .

El científico informático John Backus ha defendido una notación sin variables, o programación a nivel de función , que en retrospectiva guarda cierta similitud con el lenguaje interno de las categorías cerradas cartesianas. ^{[ 7 ]} CAML se modela de forma más consciente a partir de categorías cerradas cartesianas.

Suma y producto dependientes

Sea C una categoría localmente cartesiana cerrada. Entonces C tiene todas las retrotracciones, porque la retrotracción de dos flechas con codominio Z viene dada por el producto en C / Z.

Para cada flecha p : X → Y , sea P el objeto correspondiente de C/Y . Tomando retrocesos a lo largo de p se obtiene un functor p ^* : C / Y → C / X que tiene un adjunto izquierdo y un adjunto derecho.

El adjunto izquierdo $\Sigma _{p}:C/X\to C/Y$ se denomina suma dependiente y se obtiene mediante composición $p\circ (-)$ .

El adjunto derecho $\Pi _{p}:C/X\to C/Y$ se denomina producto dependiente .

La exponencial de P en C / Y se puede expresar en términos del producto dependiente mediante la fórmula $Q^{P}\cong \Pi _{p}(p^{*}(Q))$ .

La razón de estos nombres es porque, al interpretar P como un tipo dependiente $y:Y\vdash P(y):\mathrm {Tipo}$ , los functores $\Sigma _{p}$ y $\Pi _{p}$ corresponden a las formaciones tipo $\Sigma _{x:P(y)}$ y $\Pi _{x:P(y)}$ respectivamente.

Teoría de ecuaciones

En toda categoría cartesiana cerrada (usando notación exponencial), ( X ^Y ) ^Z y ( X ^Z ) ^Y son isomorfos para todos los objetos X , Y y Z . Escribimos esto como la "ecuación"

$(x^{y})^{z}=(x^{z})^{y}.$

Cabe preguntarse qué otras ecuaciones de este tipo son válidas en todas las categorías cartesianas cerradas. Resulta que todas ellas se derivan lógicamente de los siguientes axiomas (donde $1$ denota el objeto terminal de $C$ : ^{[ 8 ]}

El producto es asociativo: $x\times (y\times z)=(x\times y)\times z$
El producto es conmutativo: $x\times y=y\times x$
El objeto terminal es la identidad del producto: $x\times 1=x$
El objeto terminal es el cero izquierdo (algebraico) para la exponenciación: $1^{x}=1$
El objeto terminal es la identidad correcta para la exponenciación: $x^{1}=x$
La exponenciación se distribuye a la derecha sobre los productos: $(x\times y)^{z}=x^{z}\times y^{z}$
zurra: $(x^{y})^{z}=x^{y\times z}$

Categorías cerradas bicartesianas

Las categorías cerradas bicartesianas extienden las categorías cerradas cartesianas con coproductos binarios y un objeto inicial , con productos que se distribuyen sobre los coproductos. Su teoría ecuacional se extiende con los siguientes axiomas, dando como resultado algo similar a los axiomas de Tarski de nivel de secundaria , pero con un cero:

Los coproductos son conmutativos: $x+y=y+x$
Los coproductos son asociativos: $(x+y)+z=x+(y+z)$
Los productos se distribuyen entre los coproductos: $x\times (y+z)=x\times y+x\times z$
La exponenciación mediante coproductos es lo mismo que un producto de exponentes: $x^{y+z}=x^{y}\times x^{z}$
El objeto inicial es la identidad del coproducto: $0+x=x$
El objeto inicial es el producto cero: $x\times 0=0$
La exponenciación por el objeto inicial es el objeto terminal: $x^{0}=1$

Sin embargo, cabe señalar que la lista anterior no es exhaustiva; el isomorfismo de tipos en el BCCC libre no es finitamente axiomatizable, y su decidibilidad sigue siendo un problema abierto . ^{[ 9 ]}

Referencias

↑ Baez, John C. ; Stay, Mike (2011). "Física, topología, lógica y computación: una piedra Rosetta" (PDF) . En Coecke, Bob (ed.). Nuevas estructuras para la física . Lecture Notes in Physics. Vol. 813. Springer. pp. 95–174 . arXiv : 0903.0340 . CiteSeerX 10.1.1.296.1044 . doi : 10.1007/978-3-642-12821-9_2 . ISBN 978-3-642-12821-9. S2CID 115169297 .
↑ Saunders, Mac Lane (1978). Categorías para el matemático práctico (2.ª ed.). Springer. ISBN 1441931236OCLC 851741862
↑ "categoría cerrada cartesiana en nLab" . ncatlab.org . Consultado el 17 de septiembre de 2017 .
↑ Categoría localmente cartesiana cerrada en el n Lab
^ Barendregt, HP (1984). "Teorema 1.2.16". El cálculo Lambda . Holanda del Norte. ISBN 0-444-87508-5.
↑ "Teoría de la categoría Ct: ¿es cartesiana cerrada la categoría de monoides conmutativos?" .
↑ Backus, John (1981). «Programas a nivel de función como objetos matemáticos». Actas de la conferencia de 1981 sobre lenguajes de programación funcional y arquitectura de computadoras - FPCA '81 . Nueva York, Nueva York, EE. UU.: ACM Press. págs. 1–10 . doi : 10.1145/800223.806757 . ISBN 0-89791-060-5.
↑ Solov'ev, SV (1983). "La categoría de conjuntos finitos y categorías cartesianas cerradas". Journal of Mathematical Sciences . 22 (3): 1387– 1400. doi : 10.1007/BF01084396 . S2CID 122693163 .
↑ Fiore, M.; Di Cosmo, R.; Balat, V. (2006). "Observaciones sobre isomorfismos en cálculos lambda tipados con tipos vacíos y suma" (PDF) . Annals of Pure and Applied Logic . 141 ( 1–2 ): 35–50 . doi : 10.1016/j.apal.2005.09.001 .

Seely, RAG (1984). "Categorías cerradas localmente cartesianas y teoría de tipos". Mathematical Proceedings of the Cambridge Philosophical Society . 95 (1): 33– 48. doi : 10.1017/S0305004100061284 . ISSN 1469-8064 . S2CID 15115721 .

Enlaces externos

Categoría cartesiana cerrada en el Laboratorio n
Baez, John (2006). "CCC y el cálculo λ" . The n-Category Café: Un blog grupal sobre matemáticas, física y filosofía . Universidad de Texas.

[1] Baez, John C. ; Stay, Mike (2011). "Física, topología, lógica y computación: una piedra Rosetta" (PDF) . En Coecke, Bob (ed.). Nuevas estructuras para la física . Lecture Notes in Physics. Vol. 813. Springer. pp. 95–174 . arXiv : 0903.0340 . CiteSeerX 10.1.1.296.1044 . doi : 10.1007/978-3-642-12821-9_2 . ISBN 978-3-642-12821-9. S2CID 115169297 .

[2] Saunders, Mac Lane (1978). Categorías para el matemático práctico (2.ª ed.). Springer. ISBN 1441931236OCLC 851741862

[3] "categoría cerrada cartesiana en nLab" . ncatlab.org . Consultado el 17 de septiembre de 2017 .

[4] Categoría localmente cartesiana cerrada en el n Lab

[5] Barendregt, HP (1984). "Teorema 1.2.16". El cálculo Lambda . Holanda del Norte. ISBN 0-444-87508-5.

[6] "Teoría de la categoría Ct: ¿es cartesiana cerrada la categoría de monoides conmutativos?" .

[Backus_1981_p.-7] Backus, John (1981). «Programas a nivel de función como objetos matemáticos». Actas de la conferencia de 1981 sobre lenguajes de programación funcional y arquitectura de computadoras - FPCA '81 . Nueva York, Nueva York, EE. UU.: ACM Press. págs. 1–10 . doi : 10.1145/800223.806757 . ISBN 0-89791-060-5.

[8] Solov'ev, SV (1983). "La categoría de conjuntos finitos y categorías cartesianas cerradas". Journal of Mathematical Sciences . 22 (3): 1387– 1400. doi : 10.1007/BF01084396 . S2CID 122693163 .

[9] Fiore, M.; Di Cosmo, R.; Balat, V. (2006). "Observaciones sobre isomorfismos en cálculos lambda tipados con tipos vacíos y suma" (PDF) . Annals of Pure and Applied Logic . 141 ( 1–2 ): 35–50 . doi : 10.1016/j.apal.2005.09.001 .

[ 1 ]

[ 2 ]

lo

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]