Jaka jest różnica między strzałkami a obiektami wykładniczymi w kartezjańskiej kategorii zamkniętej?

21

W kategorii kartezjański Zamknięty ( CCC ), istnieją tzw wykładnicze obiektów , napisane . Gdy CCC uważane za modelem prostu wpisany -calculus , wykładniczy przedmiot jak B ^ A charakteryzuje miejsca funkcyjnego od typu A do typu B . Obiekt wykładniczy jest wprowadzany za pomocą strzałki zwanej curry: (A \ times B \ rightarrow C) \ rightarrow (A \ rightarrow C ^ B) i eliminowany przez strzałkę o nazwie zastosowanie: C ^ B \ times B \ rightarrow C (co niestety nazywany evalλBAλ A BBAABa p p l y : C B × B C e v a lcurry:(A×BC)(ACB)apply:CB×BCevalw większości tekstów dotyczących teorii kategorii). Moje pytania tutaj: czy jest jakaś różnica między wykładniczym obiektem CB , a strzałką BC ?

dzień
źródło
3
W kategorii jest to obiekt wykładniczy , ale w teorii typów można go nazwać typem wykładniczym .
Andrej Bauer,
To nie jest pytanie na poziomie badawczym. Przenieś się na cs-exchange?
Andrea Asperti

Odpowiedzi:

34

Jeden jest wewnętrzny, a drugi zewnętrzny .

Kategoria składa się z przedmiotów i morfizmów. Kiedy piszemy rozumiemy, że jest morfizmem od obiektu do obiektu . Możemy zebrać wszystkie morfizmy od do w zbiór morfizmów , zwany „hom-set”. Ten zestaw nie jest obiektem , ale raczej obiektem kategorii zbiorów. f : A B f A B A BCf:ABfABAB HomC(A,B)C

Natomiast wykładniczy jest obiektem w . Oto jak „ myśli o swoich zestawach hom”. Zatem musi być wyposażony w dowolną strukturę obiektów .BAC B A CCCBAC

Jako przykład rozważmy kategorię przestrzeni topologicznych. Zatem jest ciągłą mapą od do , a jest zbiorem wszystkich takich ciągłych map. Ale , jeśli istnieje, jest przestrzenią topologiczną! Można udowodnić, że punkty są (w bijective korespondencji z) ciągłych map z do . W rzeczywistości dotyczy to w ogólności: morfizmy (które są „punktami globalnymi ”) są w bijectywnej korespondencji z morfizmami , ponieważ X Y H o m T o p ( X , Y ) Y X Y X X Y 1 B A B A A B H o m ( 1 , B A )f:XYXYHomTop(X,Y)YXYXXY1BABAAB

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

Czasami mamy niechlujstwa o pisaniu w przeciwieństwie do . W rzeczywistości często te dwa są synonimami, przy założeniu, że może oznaczać „och, tak przy okazji, miałem na myśli inną notację, więc oznacza to, że jest morfizmem od do ”. Na przykład, kiedy zapisałeś morfizm , naprawdę powinieneś był napisać Tak więc nie możemy tak naprawdę winić nikogo za zamieszanie. Wewnętrzna jest stosowane w sensie wewnętrznej i zewnętrznej w zewnętrznych. A B f : A B f A B curry : ( A × B C ) ( A C B ) curry : CBAABf:ABfAB

curry:(A×BC)(ACB)
curry:CA×B(CB)A.

Jeśli pracujemy po prostu wpisując -calculus, wtedy wszystko jest wewnętrzne, że tak powiem. Mamy tylko podstawowe orzeczenia wpisując „ ma typ ”, napisany jako . Ponieważ tutaj jest typem, a typy odpowiadają obiektom, wówczas wyraźnie interpretujemy wykładnicze i strzałki w w sensie wewnętrznym. Tak więc, jeśli rozumiemy jako osąd pisania w -calculus, wszystkie strzałki są wewnętrzne, więc jest to to samo co Mam nadzieję, że już teraz jest jasne, dlaczego ludzie używająT B T : B B B curry : ( x B C ) ( C B ) λ curry : ( ( C, B ) ) C x B . B A A BλtBt:BBB

curry:(A×BC)(ACB)
λ
curry:((CB)A)CA×B.
BAi jako synonimy.AB
Andrej Bauer
źródło
Dzięki za świetną odpowiedź, całkowicie rozwiewającą tajemnicę.
dzień
W rzeczy samej! Świetne wyjaśnienie!
Uday Reddy
Więc co jest wewnętrzne, a które zewnętrzne?
CMCDragonkai