Teoria kategorii dla informatyków/Wykład 14: Teoria dziedzin III

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Z poprzedniego wykładu wiemy, że - kategoria wszystkich dcpo wraz z funkcjami ciągłymi w sensie Scotta - patrz Wykład 12. - jest kartezjańsko zamknięta. Kategoria ta jest również zupełna. Dowód poniższego twierdzenia znajdziemy w rozwiązaniu Zadania 14.1.


Twierdzenie 14.1

W istnieją granice dowolnych diagramów.
Uwaga
Powyższe twierdzenie nie zachodzi dla klas dziedzin ciągłych i algebraicznych w ogólności. Aby granica była również posetem odpowiedniej klasy, musimy nałożyć pewne restrykcje zarówno na kształt diagramów, jak i na własności funkcji tworzących diagram.


Twierdzenie o zgodności granicy prostej i odwrotnej

Przedstawimy teraz twierdzenie o zgodności granicy prostej i odwrotnej pewnych szczególnych diagramów w kategorii . Wynik ten jest znany w literaturze angielskojęzycznej jako limit-colimt coincidence i jest jednym z kamieni milowych w teorii dziedzin. Twierdzenie to wykorzystuje się przede wszystkim przy rozwiązywaniu tak zwanych rekursywnych równań dziedzinowych (ang. recursive domain equations).

Ilustracja2.png

Przykładem takiego równania jest . Okazuje się, że jego nietrywialne rozwiązania istnieją! Tak więc istnieją posety więcej niż jednoelementowe, które są izomorficzne z przestrzenią swoich ciągłych endofunkcji! Wynik jest o tyle zaskakujący, że w taka sytuacja, zgodnie z twierdzeniem Cantora nie może mieć miejsca.


Twierdzenie 14.2

Rozważmy diagram w kategorii taki, że:
  • Wierzchołkami są posety
  • Dla istnieją funkcje , i tworzące parę e-p.
  • Dla każdego mamy .
  • Dla mamy oraz

.

Zdefiniujmy:

Wtedy:

  • Para jest parą e-p i zachodzi .
  • jest granicą diagramu . Jeśli jest dowolną inną granicą, to izmorfizm jest dany jako lub .
  • jest granicą odwrotną diagramu . Jeśli jest dowolną inną granicą, to izmorfizm jest dany jako lub .

Dowód

W dowodzie Twierdzenia 14.1 podanym w Zadaniu 14.1

pokazaliśmy już, że granicą diagramu jest i że izomorfizm ma (pierwszą z) postulowanych postaci.

Pokażmy teraz, że funkcje są dobrze zdefiniowane, tj. że należy do dla dowolnego . Niech będzie dowolne i załóżmy, że . Mamy:

W dowodzie korzystaliśmy kolejno z: definicji , ciągłości i definicji . A zatem . Co więcej, funkcje są ciągłe, gdyż tylko funkcje ciągłe zostały użyte w ich definicji.

Przejdźmy do dowodu (5). Niech . Mamy:


Ponadto:


Bliższa analiza pokazuje, że pozostawi niezmienione te elementy ciągu , gdzie .


To dowodzi, że , czyli (5).

Korzystając z powyższego, mamy też natychmiast:

co kończy dowód (6).

Do pokazania pozostała nam (7), czyli fakt, że jest granicą odwrotną diagramu . Jeśli jest dowolną inną granicą, to sprawdźmy najpierw, czy funkcja jest dobrze zdefiniowana, tj., czy supremum jest nad zbiorem skierowanym. Ale tak jest, ponieważ dla :

Co więcej:

W końcu, pokażemy, że funkcja o podanych własnościach jest tylko jedna. Jeśli dla zachodzi , to , a zatem:

czyli z ciągłości :

Ale oraz , co daje , czyli . End of proof.gif

Kategoria dcpo i par e-p

W tej kategorii obiektami są dcpo posiadające element najmniejszy, zaś morfizmami są pary e-p, o których była mowa podczas Wykładu 2. Złożenie morfizmów

Tk-14.1.png

definiujemy w naturalny sposób jako morfizm

Tk-14.2.png

Czy jest parą e-p? Tak, ponieważ:

oraz

A zatem złożenie par e-p jest dobrze zdefiniowane, a co za tym idzie, i co łatwo już teraz pokazać, jest kategorią.


Definicja 14.3 [Omega-kategoria]

Nazwijmy -kategorią każdą kategorię, w której diagram postaci:
Tk-14.3.png
posiada granicę odwrotną.

Zauważmy, że twierdzenie o zgodności granicy prostej i odwrotnej - Twierdzenie 14.2 - mówi, że jest -kategorią!


Definicja 14.4 [Funktor ciągły]

Funktor między -kategoriami nazywamy ciągłym, jeśli zachowuje granice odwrotne, tj.: jeśli jest kogranicą powyższego diagramu, to jest kogranicą diagramu:
Tk-14.4.png
Uwaga
Tak naprawdę, aby być w zgodzie z definicją funktora ciągłego podaną przed Zadaniem Zadaniem 3.3, powinniśmy powyższą własność nazwać nie: ciągłością, ale ciągłością dualną, a funktor - funktorem dualnie ciągłym. Dla potrzeb tego wykładu przyjmijmy jednak powyższą nomenklaturę.


Lemat 14.5

Niech będzie -kategorią, funktorem ciągłym, morfizmem w oraz niech diagram:
Tk-14.7.png
posiada granicę odwrotną . Wówczas .


Zauważmy, że przekątna , , dla , jest ciągłym funktorem.

Lokalna ciągłość funktorów

Ciągłość funktora jest często niełatwa do sprawdzenia. Na szczęście istnieje własność mocniejsza, która jest łatwiej weryfikowalna: lokalna ciągłość.


Definicja 14.6

Funktor pomiędzy kategoriami posetów jest lokalnie ciągły jeśli przekształcenia typu są ciągłe w sensie Scotta dla każdej pary obiektów .


Dla przykładu przeczytajmy tę definicję dla bifunktora : funktor jest lokalnie ciągły, jeśli dla dowolnych zbiorów skierowanych i , gdzie , mamy:

Zauważmy, że supremum po prawej stronie istnieje w .

Dla przykładu, eksponent jest lokalnie ciągły, ponieważ jest złożeniem funkcji ciągłych w sensie Scotta.


Lemat 14.7 [istnienie funktorów ciągłych]

Niech funktor będzie lokalnie ciągły. Wtedy istnieje ciągły funktor , którego działanie na obiekty jest takie samo, jak funktora .


Dowód

Połóżmy , gdzie są dcpo z elementami najmniejszymi. Rozważmy pary e-p:
Tk-14.5.png

Możemy wówczas stworzyć diagram:

Tk-14.6.png

i para morfizmów powyżej jest parą e-p. Rzeczywiście:

Wykorzystaliśmy kolejno: kontrawariantność dla pierwszego argumentu, własności par e-p i definicję funktora. Ponadto:

Wykorzystaliśmy kolejno: definicję funktora, monotoniczność , która wynika z lokalnej ciągłości i w końcu definicję jeszcze raz.

Zdefiniujmy zatem:

Oczywiście, jest funktorem. Aby pokazać ciągłość, załóżmy, że mamy w diagram:

który ma granicę odwrotną . A to znaczy, że w mamy dwa diagramy:

i

których granicami są odpowiednio i . Z twierdzenia o koincydencji granicy prostej i odwrotnej (Twierdzenie 14.2) wiemy, że zachodzi oraz , a więc . Aplikując lokalną ciągłość do ostatniej równości, mamy:

Ale Twierdzenie 14.2 mówi, że ostatnia równość charakteryzuje granicę odwrotną diagramu w

a zatem jest tą szukaną granicą odwrotną, co należało pokazać. End of proof.gif


Dana S. Scott ur. 1932
Zobacz biografię

Twierdzenie Scotta

Zgodnie z poprzednim twierdzeniem możemy zdefiniować Eksponent jako , który jest ciągły (ponieważ eksponent jest lokalnie ciągły). Rozważmy złożenie Definiuje ono funktor ciągły (jako złożenie dwóch funktorów ciągłych). Jak on działa? Rozważmy parę:

Tk-14.8.png

Mamy . Podobnie . Działanie na morfizmach:

A zatem otrzymujemy:

Tk-14.9.png

Wiemy już, że para funkcji powyżej tworzy parę e-p! Przypomnijmy jeszcze raz, jak działają funkcje i na elementy z odpowiednio i . Przykładowo, dla mamy dla :

to znaczy . Podobnie dla .

Zauważmy w końcu, że dla dowolnego dcpo , jeśli jako weźmiemy funkcję , zaś jako weźmiemy funkcję , to para jest parą e-p typu .

A zatem otrzymujemy końcowy wniosek:

Twierdzenie 14.8 [Scott]

Niech będzie dcpo z elementem najmniejszym . Zdefiniujmy diagram w , jak następuje:
Tk-14.10.png

gdzie:

  • , ,
  • jest funkcją .

jest funkcją .

  • jest funkcją . jest funkcją .

Niech będzie granicą diagramu:

Tk-14.11.png

w . Wówczas: