En la 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 la lógica matemática y la teoría de la programación, ya que su lenguaje interno es el cálculo lambda simplemente tipeado . Se generalizan mediante categorías monoidales cerradas , cuyo lenguaje interno, los sistemas de tipo lineal , son adecuados tanto para la computación cuántica como para la clásica. [1]
Etimología
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 luego se generalizó a la noción de producto categórico .
Definición
La categoría C se llama cerrada cartesiana [2] si y solo si satisface las siguientes tres propiedades:
- Tiene un objeto terminal .
- Dos objetos X y Y de C tienen un producto X × Y en C .
- Dos objetos Y y Z de C tienen un exponencial Z Y en C .
Las dos primeras condiciones pueden combinarse con 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 funtor - × Y (es decir, el funtor de C a C que mapea los objetos X a X × Y y los morfismos φ a φ × id Y ) tiene un adjunto derecho , generalmente denotado - Y , para todos los objetos de Y en C . Para categorías localmente pequeñas , esto puede expresarse por la existencia de una biyección entre los hom-sets
que es natural, tanto en X y Z . [3]
Tenga cuidado de tener en cuenta que una categoría cerrada cartesiana 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 cerradas cartesianas, entonces se denomina cerradas cartesianas localmente . [4] Tenga en cuenta que si C es localmente cerrado cartesiano, en realidad no necesita ser cartesiano cerrado; eso sucede si y solo si C tiene un objeto terminal.
Construcciones basicas
Evaluación
Para cada objeto Y , el recuento de la adjunción exponencial es una transformación natural
llamado mapa de evaluación (interna) . De manera más general, podemos construir el mapa de aplicación parcial como el compuesto
En el caso particular de la categoría Conjunto , estos se reducen a las operaciones ordinarias:
Composición
Evaluar el exponencial en un argumento en un morfismo p : X → Y da morfismos
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
la flecha correspondiente debajo del adjunto exponencial
se llama mapa de composición (interno) .
En el caso particular de la categoría Set , esta es la operación de composición ordinaria:
Secciones
Para un morfismo p : X → Y , suponga que existe el siguiente cuadrado de retroceso, que define el subobjeto de X Y correspondiente a mapas cuyo compuesto con p es la identidad:
donde la flecha de la derecha es P Y y la flecha de la corresponde inferiores a la identidad en Y . Entonces Γ Y ( p ) se llama 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 funtor Γ Y : C / Y → C en la categoría de corte, que es adyacente a una variante del functor de producto:
La exponencial por Y se puede expresar en términos de secciones:
Ejemplos de
Ejemplos de categorías cerradas cartesianas incluyen:
- 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 y Y , y Z Y es el conjunto de todas las funciones de Y a Z . La contigüidad se expresa mediante el siguiente hecho: la función f : X × Y → Z se identifica naturalmente con la función de curry g : X → Z Y definida por g ( x ) ( y ) = f ( x , y ) para todo x en X y y en y .
- La categoría de conjuntos finitos , con funciones como morfismos, es cartesiana cerrada por la misma razón.
- Si G es un grupo , entonces la categoría de todos los G conjuntos- es cartesiano cerrada. Si Y y Z son dos conjuntos G , entonces Z Y es el conjunto de todas las funciones de Y a Z con la acción G definida por ( g . F ) ( y ) = g . (F ( g −1 .y)) para todo g en g , F : y → Z y y en y .
- La categoría de conjuntos G finitos también es cartesiana cerrada.
- La categoría Gato de todas las categorías pequeñas (con functores como morfismos) es cartesiana cerrada; el C D exponencial viene dado por la categoría de functor que consta de todos los functores de D a C , con transformaciones naturales como morfismos.
- Si C es una categoría pequeña , entonces el conjunto de categorías de functores C que consta de todos los functores covariantes de C en la categoría de conjuntos, con transformaciones naturales como morfismos, es cartesiano cerrado. Si F y G son dos funtores desde C a Set , a continuación, la exponencial F G es el funtor cuyo valor en el objeto X de C está dada por el conjunto de todas las transformaciones naturales de ( X , -) × G a F .
- El ejemplo anterior de G -sets puede verse como un caso especial de categorías de functor: cada grupo puede considerarse como una categoría de un objeto, y G -sets no son más que functors de esta categoría a Set
- La categoría de todos los gráficos dirigidos es cartesiana cerrada; esta es una categoría de functor como se explica en la categoría de functor.
- En particular, la categoría de conjuntos simpliciales (que son functores X : Δ op → Conjunto ) es cartesiana cerrada.
- Incluso de manera más general, cada topos elemental es cartesiano cerrado.
- En topología algebraica , es particularmente fácil trabajar con categorías cerradas cartesianas. Ni la categoría de espacios topológicos con mapas continuos ni la categoría de variedades suaves con mapas suaves es cartesiana cerrada. 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 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 cerrada cartesiana (es decir, los objetos son los cpos y los morfismos son los mapas continuos de Scott ). Tanto el curado como la aplicación son funciones continuas en la topología de Scott, y el curado, junto con la 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 los cuales hay un morfismo único de U a V si U es un subconjunto de V y no hay morfismo en caso contrario. Este poset es una categoría cerrada cartesiana: 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 de identidad. De hecho, si 0 es un objeto inicial y 1 es un objeto final y tenemos, luego 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. Entonces, la categoría de módulos sobre un anillo no es cartesiana cerrada. Sin embargo, el producto del tensor de functor con un módulo fijo tiene un derecho adjunto . El producto tensorial no es un producto categórico, por lo que esto no contradice lo anterior. En cambio, obtenemos que la categoría de módulos es monoidal cerrada .
Ejemplos de categorías cerradas cartesianas locales incluyen:
- Cada topos elemental es localmente cartesiano cerrado. Este ejemplo incluye Set , FINSET , G : establece para un grupo G , así como Set C para las pequeñas categorí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 poleas.. Sin embargo, LH no tiene un objeto terminal y, por lo tanto, no es cartesiano cerrado.
- Si C tiene pullbacks y para cada flecha p : X → Y , el funtor p * : C / Y → C / X dado al tomar pullbacks tiene un adjunto derecho, entonces C es localmente cartesiano cerrado.
- Si C es localmente cerrado cartesiano, entonces todas sus categorías de corte C / X también están localmente cerradas cartesianas.
Los no ejemplos de categorías cerradas cartesianas locales incluyen:
- Cat no es localmente cartesiano cerrado.
Aplicaciones
En categorías cerradas cartesianas, 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 las aplicaciones informáticas , esto se conoce como currying ; ha llevado a la comprensión de que el cálculo lambda de tipo simple se puede interpretar en cualquier categoría cerrada cartesiana.
La correspondencia Curry-Howard-Lambek proporciona un isomorfismo profundo entre la lógica intuicionista, el cálculo lambda simple y las categorías cerradas cartesianas.
Ciertas categorías cerradas cartesianas, los topoi , se han propuesto como un escenario general para las matemáticas, en lugar de la teoría de conjuntos tradicional .
El renombrado informático John Backus ha abogado por 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 cerradas cartesianas. CAML se modela más conscientemente en categorías cerradas cartesianas.
Suma y producto dependientes
Sea C una categoría cerrada localmente cartesiana. Entonces C tiene todos los retrocesos, debido a que la retirada de dos flechas con codomain Z está dada por el producto en C / Z .
Por cada flecha p : X → Y , deja P denotan el objeto correspondiente de C / Y . Tomando pullbacks a lo largo de p se obtiene un funtor p * : C / Y → C / X que tiene un adjunto tanto izquierdo como derecho.
El adjunto izquierdo se llama suma dependiente y viene dada por composición con p .
El adjunto correcto se llama producto dependiente .
El exponencial por P en C / Y se puede expresar en términos del producto dependiente mediante la fórmula.
La razón de estos nombres es porque, al interpretar P como un tipo dependiente , los functors y corresponden a las formaciones tipo y respectivamente.
Teoría ecuacional
En cada categoría cerrada cartesiana (usando la 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 .
Uno puede preguntarse qué otras ecuaciones de este tipo son válidas en todas las categorías cerradas cartesianas. Resulta que todos se siguen lógicamente de los siguientes axiomas: [7]
- x × ( y × z ) = ( x × y ) × z
- x × y = y × x
- x × 1 = x (aquí 1 denota el objeto terminal de C )
- 1 x = 1
- x 1 = 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 distribuidos sobre coproductos. Su teoría de las ecuaciones se amplía con los siguientes axiomas, lo que produce algo similar a los axiomas de la escuela secundaria de Tarski pero con inversos aditivos:
- 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
- x 0 = 1
Sin embargo, tenga en cuenta que la lista anterior no está completa; El isomorfismo de tipo en el BCCC libre no es finitamente axiomatizable, y su decidibilidad sigue siendo un problema abierto. [8]
Referencias
- ^ John C. Baez y Mike Stay, " Física, topología, lógica y computación: una piedra de Rosetta ", (2009) ArXiv 0903.0340 en Nuevas estructuras para la física , ed. Bob Coecke, Lecture Notes in Physics vol. 813 , Springer, Berlín, 2011, págs. 95-174.
- ^ Saunders., Mac Lane (1978). Categorías para el matemático que trabaja (Segunda ed.). Nueva York, NY: Springer New York. ISBN 1441931236. OCLC 851741862 .
- ^ "categoría cerrada cartesiana en nLab" . ncatlab.org . Consultado el 17 de septiembre de 2017 .
- ^ Categoría cerrada localmente cartesiana en nLab
- ^ HP Barendregt, El cálculo Lambda , (1984) Holanda Septentrional ISBN 0-444-87508-5 (Ver teorema 1.2.16)
- ^ "Ct. Teoría de la categoría: ¿la categoría monoides conmutativos cartesianos está cerrada?" .
- ^ S. Soloviev. "Categoría de conjuntos finitos y categorías cerradas cartesianas", Journal of Soviet Mathematics, 22, 3 (1983)
- ^ Fiore, Cosmo y Balat. Comentarios sobre isomorfismos en cálculos lambda tipificados con tipos de suma y vacío [1]
- Seely, RAG (1984). "Categorías cerradas cartesianas localmente y teoría de tipos". Procedimientos matemáticos de la Sociedad Filosófica de Cambridge . 95 (1): 33–48. doi : 10.1017 / S0305004100061284 . ISSN 1469-8064 .
enlaces externos
- Categoría cerrada cartesiana en nLab
- Una publicación de blog sobre la relación entre los CCC y el cálculo lambda : https://golem.ph.utexas.edu/category/2006/08/cartesian_closed_categories_an_1.html