Categoría cerrada cartesiana

format_list_bulleted Contenido keyboard_arrow_down

ImprimirCitar

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

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 escrito. Se generalizan por categorías monoidales cerradas, cuyo lenguaje interno, sistemas de tipo lineal, son aptos tanto para la computación cuántica como para la clásica.

Etimología

Nombrado en honor a 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 denomina cerrada cartesiana si y solo si cumple las siguientes tres propiedades:

Tiene un objeto terminal.
Dos objetos X y Y de C tener un producto X×Y dentro C.
Dos objetos Y y Z de C tienen un exponencial Z^Y dentro C.

Las dos primeras condiciones se pueden combinar con el único requisito de que cualquier familia finita (posiblemente vacía) de objetos de C admita un producto en C, debido a la naturaleza asociatividad 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 asigna objetos X a X ×Y y morfismos φ a φ × id_Y) tiene un adjunto derecho, generalmente 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-sets

mathrm{Hom}(Xtimes Y,Z) cong mathrm{Hom}(X,Z^Y)

que es natural en X, Y y Z.

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

Si una categoría tiene la propiedad de que todas sus categorías de corte son cartesianas cerradas, entonces se denomina localmente cartesiana cerrada. Tenga en cuenta que si C es cerrado cartesiano localmente, no necesita ser cerrado cartesiano en realidad; eso sucede si y solo si C tiene un objeto terminal.

Construcciones básicas

Evaluación

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

{displaystyle mathrm {ev} _{Y,Z}:Z^{Y}times Yto Z}

llamado mapa (interno) de evaluación. En términos más generales, podemos construir el mapa de aplicación parcial como el mapa compuesto

{displaystyle mathrm {papply} _{X,Y,Z}:Z^{Xtimes Y}times Xcong (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 el mapa de composición (interno).

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

{displaystyle c_{X,Y,Z}(g,f)=gcirc f.}

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:

{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 abajo corresponde 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 todo morfismo p con codominio Y, entonces se puede ensamblar en un funtor Γ_Y: C/Y → C en la categoría de corte, que está justo al lado de una variante del funtor de producto:

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

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

{displaystyle Z^{Y}cong Gamma _{Y}(Ztimes Y{xrightarrow {pi _{2}}}Y).}

Ejemplos

Los ejemplos de categorías cerradas cartesianas incluyen:

La categoría Set de todos los conjuntos, con funciones como morfismos, está cerrado cartesiano. 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 unión se expresa por el siguiente hecho: la función f: X×Y → Z se identifica naturalmente con la función curried g: X → Z^Y definidas por g()x)Sí.) f()x,Sí.) para todos x dentro X y Sí. dentro Y.
La categoría de conjuntos finitos, con funciones como morfismos, es cartesiano cerrado por la misma razón.
Si G es un grupo, entonces la categoría de todos los conjuntos G es Cartesian cerrado. Si Y y Z dos G-sets, entonces Z^Y es el conjunto de todas las funciones de Y a Z con G acción definida por (g.F)Sí.) g.F(g⁻¹.y) para todos g dentro G, F:Y → Z y Sí. dentro Y.
La categoría de finito G-sets también está cerrado cartesiano.
La categoría Gato de todas las categorías pequeñas (con functores como morfismos) es Cartesiano cerrado; el exponencial C^D es dado por la categoría de functor que consiste de todos los functores de D a C, con transformaciones naturales como morfismos.
Si C es una pequeña categoría, entonces la categoría de functor Set^C que consiste en todos los funerarios covariantes de C en la categoría de conjuntos, con transformaciones naturales como morfismos, está cerrado cartesiano. Si F y G son dos functores de C a Set, entonces el exponencial F^G es el functor cuyo valor en el objeto X de C es dado por el conjunto de todas las transformaciones naturales de ()X,−) ×G a F.
- El ejemplo anterior G-sets se puede ver como un caso especial de categorías de functor: cada grupo puede ser considerado como una categoría de un objeto, y G-sets no son más que functores de esta categoría a Set
- La categoría de todos los gráficos dirigidos es Cartesian cerrado; 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: Δ^operaciones → Set) es Cartesian cerrado.
Más generalmente, cada topos elementales está cerrado.
En topología algebraica, las categorías cerradas cartesianas son particularmente fáciles de trabajar con. Ni la categoría de espacios topológicos con mapas continuos ni la categoría de andamios suaves con mapas suaves es Cartesiano cerrado. Por lo tanto, se han considerado categorías substitutas: la categoría de espacios Hausdorff generados compactamente es Cartesian cerrado, como es la categoría de espacios Frölicher.
En teoría del orden, órdenes parciales completas (cpos) 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 curry como aplicación son funciones continuas en la topología de Scott, y currying, junto con la aplicación, proporcionan la unión.
Un álgebra Heyting es un cartesiano cerrado (limitado) lattice. Un ejemplo importante surge de los espacios topológicos. Si X es un espacio topológico, entonces el abierto se pone en X formar los objetos de una categoría O(X) para el cual hay un morfismo único U a V si U es un subconjunto de V y no morfismo de otra manera. Esta pose es una categoría cerrada cartesiana: el "producto" de U y V es la intersección de U y V y el exponencial U^V es el interior de $U \cup X V)$ .
Una categoría con un objeto cero es Cartesiano cerrado si y sólo si es equivalente a una categoría con sólo un objeto y un morfismo de identidad. De hecho, si 0 es un objeto inicial y 1 es un objeto final y tenemos 0.. 1{displaystyle 0cong 1} ${displaystyle 0cong 1}$ , entonces Hom()X,Y).. Hom()1,YX).. Hom()0,YX).. 1{displaystyle mathrm {Hom} (X,Y)cong mathrm {Hom} (1,Y^{X})cong mathrm {Hom} (0,Y^{X})cong 1} ${displaystyle mathrm {Hom} (X,Y)cong mathrm {Hom} (1,Y^{X})cong mathrm {Hom} (0,Y^{X})cong 1}$ que tiene sólo un elemento.
- En particular, cualquier categoría no-trivial con un objeto cero, como una categoría abeliana, no es cartesiana cerrada. Así que la categoría de módulos sobre un anillo no es Cartesiano cerrado. Sin embargo, el producto tensor del functor ${displaystyle -otimes M}$ con un módulo fijo tiene una unión derecha. El producto tensor 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 cerrado.

Ejemplos de categorías cerradas localmente cartesianas incluyen:

Cada topos elementales es localmente cartesiano cerrado. Este ejemplo incluye Set, FinSet, G-sets for a group G, así como Set^C para las categorías pequeñas C.
La categoría LH cuyos objetos son espacios topológicos y cuyos morfismos son homeomorfismos locales está cerrado localmente cartesiano, ya que LH/X es equivalente a la categoría de cuchillas ${displaystyle 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 por tomar retrocesos tiene una unión derecha, entonces C es localmente Cartesiano cerrado.
Si C es localmente Cartesiano cerrado, entonces todas sus categorías de rebanadas C/X son también localmente Cartesian cerrado.

Los no ejemplos de categorías cerradas localmente cartesianas incluyen:

Gato 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 curry; 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 profundo isomorfismo entre la lógica intuicionista, el cálculo lambda de tipo simple y las categorías cerradas cartesianas.

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

El renombrado 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 cerradas cartesianas. CAML está más conscientemente modelado en categorías cerradas cartesianas.

Suma y producto dependientes

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

Para cada flecha p: X → Y, sea P el objeto correspondiente de C/Y. Tomar retrocesos a lo largo de p da un funtor p^*: C/Y → C/X que tiene un lado izquierdo y otro derecho.

El adjoint izquierdo ${displaystyle Sigma _{p}:C/Xto C/Y}$ se llama suma dependiente y se da por composición ${displaystyle pcirc (-)}$ .

The right adjoint ${displaystyle Pi _{p}:C/Xto C/Y}$ se llama producto dependiente.

El exponencial P dentro 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 tipo dependiente ${displaystyle y:Yvdash P(y):mathrm {Type} }$ , los functores ${displaystyle Sigma _{p}}$ y ${displaystyle Pi _{p}}$ corresponde a las formaciones tipo ${displaystyle Sigma _{x:P(y)}}$ y ${displaystyle Pi _{x:P(y)}}$ respectivamente.

Teoría Ecuacional

En cada categoría cerrada cartesiana (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^Sí.)^z =x^z)^Sí..

Uno puede preguntarse qué otras ecuaciones similares son válidas en todas las categorías cerradas cartesianas. Resulta que todos ellos se siguen lógicamente de los siguientes axiomas:

x×Sí.×z) =x×Sí.)×z
x×Sí. = Sí.×x
x× 1 = x (aquí 1 denota el objeto terminal de C)
1^x = 1
x¹ = x
()x×Sí.)^z = x^z×Sí.^z
()x^Sí.)^z = x^()Sí.×z)

Categorías cerradas bicartesianas

Las categorías cerradas bicartesianas amplían las categorías cerradas cartesianas con coproductos binarios y un objeto inicial, con productos que se distribuyen sobre coproductos. Su teoría ecuacional se amplía con los siguientes axiomas, produciendo algo similar a los axiomas de la escuela secundaria de Tarski pero con un cero:

x + Sí. = Sí. + x
()x + Sí.) + z = x +Sí. + z)
x×Sí. + z) x×Sí. + x×z
x^{()Sí. + z)} = x^Sí.×^z
0 + x = x
x×0 = 0
x⁰ = 1

No obstante, 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.

Contenido relacionado

Más resultados...