¿Cuál es la diferencia entre flechas y objetos exponenciales en una categoría cerrada cartesiana?

21

En una categoría cartesiana cerrada ( CCC ), existen los llamados objetos exponenciales , escritas . Cuando un CCC es considerado como un modelo de la simplemente-mecanografiada λ -calculus , un objeto exponencial como B A caracteriza el espacio de la función de tipo A a tipo B . Un objeto exponencial es introducido por una flecha llamada c u r r y : ( A × B C ) ( A C BBAλBAAB Y eliminado por una flecha llama un p p l y : C B × B C (que por desgracia llama e v un l en la mayoría de textos sobre teoría de la categoría). Mi pregunta aquí es: ¿hay alguna diferencia entre el objeto exponencial C B y la flecha B C ?curry:(A×BC)(ACB)apply:CB×BCevalCBBC

día
fuente
3
En una categoría es el objeto exponencial , pero en la teoría de tipos podría llamarse el tipo exponencial .
Andrej Bauer
Esta no es una pregunta de nivel de investigación. ¿Pasar a cs-exchange?
Andrea Asperti

Respuestas:

34

Uno es interno y el otro es externo .

Una categoría consta de objetos y morfismos. Cuando escribimos f : A B queremos decir que f es un morfismo de un objeto A al objeto B . Podemos recopilar todos los morfismos de A a B en un conjunto de morfismos H o m C ( A , B ) , llamado "conjunto hom". Este conjunto no es un objeto de C , sino un objeto de la categoría de conjuntos.Cf:ABfABAB HomC(A,B)C

En contraste, una exponencial es un objeto en C . Es cómo " C piensa en sus hom-sets". Por lo tanto, B A debe estar equipado con cualquier estructura los objetos de C tienen.BACCBAC

Como ejemplo, consideremos la categoría de espacios topológicos. Entonces es un mapa continuo de X a Y , y H o m T o p ( X , Y ) es el conjunto de todos estos mapas continuos. ¡Pero Y X , si existe, es un espacio topológico! Se puede demostrar que los puntos de Y X son (en correspondencia biyectiva con) los mapas continuos de X a Y . De hecho, esto se cumple en general: los morfismos 1 B Af:XYXYHomTop(X,Y)YXYXXY1BA(que son "los puntos globales de ") están en correspondencia biyectiva con morfismos A B , porque H o m ( 1 , B A ) H o m ( 1 × A , B ) H o m ( A , B ) .BAAB

Hom(1,BA)Hom(1×A,B)Hom(A,B).

A veces tenemos descuidado acerca de la escritura en lugar de un B . De hecho, a menudo estos dos son sinónimos, con el entendimiento de que f : A B podría significar "oh, por cierto, quise decir la otra notación, por lo que esto significa que f es un morfismo de A a B ". Por ejemplo, cuando escribió el curry de morfismo curry : ( A × B C ) ( A C B ) realmente debería haber escrito curry :BAABf:ABfAB

curry:(A×BC)(ACB)
Así que no podemos culpar a nadie por confundirse aquí. El internose usa en el sentido interno y el externo en el externo.
curry:CA×B(CB)A.

λtBt:BBB

curry:(A×BC)(ACB)
λ
curry:((CB)A)CA×B.
BAAB
Andrej Bauer
fuente
Gracias por la gran respuesta, disipando completamente el misterio.
día
¡En efecto! ¡Gran explicación!
Uday Reddy
Entonces, ¿cuál es interno y cuál es externo?
CMCDragonkai