Categoría cartesiana cerrada

Tipo de categoría en la teoría de categorías

En teoría de categorías , una categoría es cartesianamente 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 en la teoría de la programación, ya que su lenguaje interno es el cálculo lambda de tipos simples . 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

Lleva el 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 lugar al concepto de producto cartesiano , que más tarde se generalizó a la noción de producto categórico .

Definición

La categoría C se llama cartesiana cerrada ^[2] si y sólo si satisface las tres propiedades siguientes:

• Tiene un objeto terminal .
• Dos objetos cualesquiera X e Y de C tienen un producto X  × Y en C.
• Cualesquiera dos objetos Y y Z de C tienen una Z ^Y exponencial en C.

Las dos primeras condiciones pueden combinarse con el requisito único 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 funtor – × Y (es decir, el funtor de C a C que mapea los objetos X a X  × Y y los 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 hom-conjuntos

${\displaystyle \mathrm {Hom} (X\times Y,Z)\cong \mathrm {Hom} (X,Z^{Y})}$

lo cual es natural en X , Y y Z. ^[3 ]

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

Si una categoría tiene la propiedad de que todas sus categorías de corte son cartesianamente cerradas, entonces se denomina cartesianamente cerrada localmente . ^[4] Nótese que si C es cartesianamente cerrada localmente, en realidad no necesita ser cartesianamente cerrada; eso sucede si y solo si C tiene un objeto terminal.

Construcciones básicas

Evaluación

Para cada objeto Y , el cociente de la adjunción exponencial es una transformación natural

${\displaystyle \mathrm {ev} _{Y,Z}:Z^{Y}\times Y\to Z}$

llamado mapa de evaluación (interno) . De manera más general, podemos construir el mapa de aplicación parcial como el mapa compuesto

${\displaystyle \mathrm {papply} _{X,Y,Z}:Z^{X\times Y}\times X\cong (Z^{Y})^{X}\times X{\xrightarrow {\mathrm {ev} _{X,Z^{Y}}}}Z^{Y}.}$

En el caso particular de la categoría Conjunto , estas se reducen a las operaciones ordinarias:

${\displaystyle \mathrm {ev} _{Y,Z}(f,y)=f(y).}$

Composición

Evaluar la exponencial en un argumento en un morfismo p  : X → Y da morfismos

${\displaystyle p^{Z}:X^{Z}\to Y^{Z},}$

${\displaystyle Z^{p}:Z^{Y}\to Z^{X},}$

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

${\displaystyle 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 debajo de la adjunción exponencial

${\displaystyle c_{X,Y,Z}:Z^{Y}\times Y^{X}\to Z^{X}}$

se llama mapa de composición (interna) .

En el caso particular de la categoría Conjunto , ésta es la operación de composición ordinaria:

${\displaystyle 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 los mapas cuyo compuesto con p es la identidad:

${\displaystyle {\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 la parte inferior 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 puede ensamblarse en un funtor Γ _Y  : C / Y → C en la categoría de porción, que es adjunto derecho a una variante del funtor producto:

${\displaystyle \hom _{C/Y}(X\times Y{\xrightarrow {\pi _{2}}}Y,Z{\xrightarrow {p}}Y)\cong \hom _{C}(X,\Gamma _{Y}(p)).}$

La exponencial de Y se puede expresar en términos de secciones:

${\displaystyle Z^{Y}\cong \Gamma _{Y}(Z\times Y{\xrightarrow {\pi _{2}}}Y).}$

Ejemplos

Algunos ejemplos de categorías cartesianas cerradas incluyen:

• El conjunto de categorías de todos los conjuntos , con funciones como morfismos, es cartesianamente cerrado. El producto X × Y es el producto cartesiano de X e Y , y Z ^Y es el conjunto de todas las funciones desde Y hasta Z . La adjunción se expresa por 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 y en Y .
• La categoría de conjuntos finitos , con funciones como morfismos, es cartesianamente cerrada por la misma razón.
• Si G es un grupo , entonces la categoría de todos los conjuntos G es cartesianamente cerrada. Si Y y Z son dos conjuntos G , entonces Z ^Y es el conjunto de todas las funciones desde Y hasta 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 categoría de conjuntos G finitos también es cartesianamente cerrada.
• La categoría Cat de todas las categorías pequeñas (con funtores como morfismos) es cartesianamente cerrada; la exponencial C ^D está dada por la categoría de funtores que consiste en todos los funtores desde D hasta C , con transformaciones naturales como morfismos.
• Si C es una categoría pequeña , entonces la categoría de funtores Conjunto ^C que consiste en todos los funtores covariantes de C en la categoría de conjuntos, con transformaciones naturales como morfismos, es cartesianamente cerrada. Si F y G son dos funtores de C en Conjunto , entonces la 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 en 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 objeto, y los G -conjuntos no son nada más que funtores de esta categoría a Conjunto.
  • La categoría de todos los gráficos dirigidos es cartesianamente cerrada; esta es una categoría de functor como se explica en categoría de functor.
  • En particular, la categoría de conjuntos simpliciales (que son funtores X  : Δ ^op → Set ) es cartesianamente cerrada.
• De manera más general, todo topos elemental es cartesianamente 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 suaves con aplicaciones suaves son cartesianas cerradas. Por lo tanto, se han considerado categorías sustitutivas: 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 de órdenes , 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 currying como apply son funciones continuas en la topología de Scott, y currying, junto con apply, proporcionan el adjunto. ^[5]
• Un álgebra de Heyting es una red cartesiana cerrada (acotada) . 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 hay un morfismo único de U a V si U es un subconjunto de V y ningún morfismo en caso contrario. Este conjunto parcial 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 cartesianamente 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 , entonces que tiene un solo elemento. ^[6] ${\displaystyle 0\cong 1}$ ${\displaystyle \mathrm {Hom} (X,Y)\cong \mathrm {Hom} (1,Y^{X})\cong \mathrm {Hom} (0,Y^{X})\cong 1}$
  • En particular, cualquier categoría no trivial con un objeto cero, como una categoría abeliana , no es cartesianamente cerrada. Por lo tanto, la categoría de módulos sobre un anillo no es cartesianamente cerrada. Sin embargo, el producto tensorial functor 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 monoidalmente cerrada . ${\displaystyle -\otimes M}$

Algunos ejemplos de categorías cartesianas cerradas localmente incluyen:

• Todo topos elemental es cartesiano cerrado localmente. Este ejemplo incluye los conjuntos Set , FinSet , G para un grupo G , así como el conjunto ^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 cartesianamente cerrada, ya que LH/X es equivalente a la categoría de haces ⁠ ⁠ ${\displaystyle Sh(X)}$ . Sin embargo, LH no tiene un objeto terminal y, por lo tanto, no es cartesianamente cerrada.
• Si C tiene retrocesos y para cada flecha p  : X → Y , el funtor p ^*  : C/Y → C/X dado al tomar retrocesos tiene un adjunto derecho, entonces C es localmente cartesiano cerrado.
• Si C es localmente cartesianamente cerrado, entonces todas sus categorías de porción C/X también son localmente cartesianamente cerradas.

Los ejemplos no convencionales de categorías cerradas cartesianas locales incluyen:

• El gato no es cartesiano localmente cerrado.

Aplicaciones

En las categorías cartesianas cerradas, una "función de dos variables" (un morfismo f  : X × Y → Z ) siempre se puede representar 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 conclusión de que el cálculo lambda de tipos simples se puede interpretar en cualquier categoría cartesiana cerrada.

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

Se han propuesto ciertas categorías cartesianas cerradas, los topoi , 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 libre de variables, o programación a nivel de función , que en retrospectiva tiene cierta similitud con el lenguaje interno de las categorías cartesianas cerradas. ^[7] CAML está modelado de manera más consciente sobre las categorías cartesianas cerradas.

Suma y producto dependientes

Sea C una categoría localmente cartesiana cerrada. Entonces C tiene todos los pullbacks, porque el pullback de dos flechas con codominio Z está dado por el producto en C/Z .

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

El adjunto izquierdo se llama suma dependiente y está dado por la composición . ${\displaystyle \Sigma _{p}:C/X\to C/Y}$ ${\displaystyle p\circ (-)}$

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

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

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

Teoría de ecuaciones

En cada 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 deducen lógicamente de los siguientes axiomas: ^[8]

• x ×( y × z ) = ( x × y )× z
• x × y = y × x
• x ×1 = x (aquí 1 denota el objeto terminal de C )
• 1x ⁼ 1
• x1 = x^​
• ( x × y ) ^z = x ^z × y ^z
• ( x ^y ) ^z = x ^{( y × 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 entre los coproductos. Su teoría ecuacional se extiende con los siguientes axiomas, lo que produce algo similar a los axiomas de secundaria de Tarski pero con un cero:

• x + y = y + x
• ( x + y ) + z = x + ( y + z )
• x ×( y + z ) = x × y + x × z
• x ^{( y + z )} = x ^y × x ^z
• 0 + x = x
• x ×0 = 0
• x0 = ¹

Sin embargo, hay que tener en cuenta que la lista anterior no está completa; el isomorfismo de tipos en el BCCC libre no es finitamente axiomatizable y su decidibilidad sigue siendo un problema abierto. ^[9]

Referencias

1. Baez, John C. ; Stay, Mike (2011). "Física, topología, lógica y computación: una piedra de Rosetta" (PDF) . En Coecke, Bob (ed.). Nuevas estructuras para la física . Apuntes de clase en física. Vol. 813. Springer. págs. 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.S2CID115169297  .​
2. Saunders, Mac Lane (1978). Categorías para el matemático en activo (2.ª ed.). Springer. ISBN 1441931236.OCLC 851741862  .
3. "categoría cartesiana cerrada en nLab". ncatlab.org . Consultado el 17 de septiembre de 2017 .
4. Categoría cartesiana cerrada localmente en el laboratorio n
5. Barendregt, HP (1984). "Teorema 1.2.16". El cálculo lambda . Holanda Septentrional. ISBN 0-444-87508-5.
6. "Teoría de categorías Ct.: ¿la categoría de monoides conmutativos es cartesiana cerrada?".
7. Backus, John (1981). Programas de nivel de función como objetos matemáticos . Nueva York, Nueva York, EE. UU.: ACM Press. doi :10.1145/800223.806757.
8. Solov'ev, SV (1983). "La categoría de conjuntos finitos y categorías cartesianas cerradas". J Math Sci . 22 (3): 1387–1400. doi :10.1007/BF01084396. S2CID  122693163.
9. Fiore, M.; Cosmo, R. Di; Balat, V. (2006). "Observaciones sobre isomorfismos en cálculos lambda tipados con tipos vacíos y suma" (PDF) . Anales de lógica pura y aplicada . 141 (1–2): 35–50. doi :10.1016/j.apal.2005.09.001.

• Seely, RAG (1984). "Categorías cerradas cartesianas locales y teoría de tipos". Actas matemáticas de la 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). "CCCs and the λ-calculus". The n-Category Café: Un blog grupal sobre matemáticas, física y filosofía . Universidad de Texas.