[1] 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 tipado . Están generalizados por categorías monoidales cerradas , cuyo lenguaje interno, los sistemas de tipo lineal , son adecuados tanto parala computación cuántica como para la clásica.[2]
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 .
La categoría C se denomina cerrada cartesiana [3] si y solo si satisface las siguientes tres propiedades:
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
Tenga cuidado de notar que una categoría cerrada cartesiana no necesita tener límites finitos; solo se garantizan productos finitos.