Teoria kategorii dla informatyków/Wykład 14: Teoria dziedzin III: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
 
Linia 6: Linia 6:
 
{{twierdzenie||mod14:thm:grodwr| W <math>\mathbf{Dcpo}</math> istnieją granice dowolnych diagramów. }}
 
{{twierdzenie||mod14:thm:grodwr| W <math>\mathbf{Dcpo}</math> 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.
+
{{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.
 
}}
 
}}
  
Linia 45: Linia 45:
  
 
Pokażmy teraz, że funkcje <math>e_m</math> są dobrze zdefiniowane, tj. że <math>y = e_m(x)</math> należy do <math>D</math> dla dowolnego <math>m\in \omega</math>. Niech <math>m</math> będzie dowolne i załóżmy, że <math>n\leq n'</math>. Mamy:
 
Pokażmy teraz, że funkcje <math>e_m</math> są dobrze zdefiniowane, tj. że <math>y = e_m(x)</math> należy do <math>D</math> dla dowolnego <math>m\in \omega</math>. Niech <math>m</math> będzie dowolne i załóżmy, że <math>n\leq n'</math>. Mamy:
\begin{eqnarray*}
+
 
p_{nn'}(y_{n'})  & = & p_{nn'}(\bigvee{}^\downarrow_{k\geq n',m}  
+
<center><math>
p_{n'k}\circ  e_{km}(x))\\ & = & \bigvee{}^\downarrow_{k\geq  
+
p_{nn'}(y_{n'})  & = & p_{nn'}(\bigvee{}^\downarrow_{k\geq n',m} p_{n'k}\circ  e_{km}(x)) = \bigvee{}^\downarrow_{k\geq n',m} p_{nn'}\circ p_{n'k}\circ e_{km}(x) = \bigvee{}^\downarrow_{k\geq n',m} p_{nk}\circ e_{km}(x)=y_n.
n',m} p_{nn'}\circ p_{n'k}\circ e_{km}(x)\\ & = &
+
</math></center>
\bigvee{}^\downarrow_{k\geq n',m} p_{nk}\circ e_{km}(x)\\ & = &
+
 
y_n.
+
W dowodzie korzystaliśmy kolejno z: definicji <math>y_{n'}</math>, ciągłości <math>p_{nn'}</math> i definicji <math>y_n</math>. A zatem <math>y = (y_0, y_1, ...)\in D</math>. Co więcej, funkcje <math>e_m</math> są ciągłe, gdyż tylko funkcje ciągłe zostały
\end{eqnarray*}
 
W dowodzie korzystaliśmy kolejno z: definicji <math>y_{n'}</math>,
 
ciągłości <math>p_{nn'}</math> i definicji <math>y_n</math>. A
 
zatem <math>y = (y_0, y_1, ...)\in D</math>. Co więcej, funkcje
 
<math>e_m</math> są ciągłe, gdyż tylko funkcje ciągłe zostały
 
 
użyte w ich definicji.
 
użyte w ich definicji.
  
 
Przejdźmy do dowodu (5). Niech <math>m\in \omega</math>. Mamy:
 
Przejdźmy do dowodu (5). Niech <math>m\in \omega</math>. Mamy:
\begin{eqnarray*}
+
 
e_m\circ p_m (x_n\mid n\in \omega) & = & e_m(x_m)\\ & = &
+
 
(\bigvee{}^\downarrow_{k\geq n,m} p_{nk}\circ e_{km} (x_m)\mid  
+
<center><math> e_m\circ p_m (x_n\mid n\in \omega)=e_m(x_m)= (\bigvee{}^\downarrow_{k\geq n,m} p_{nk}\circ e_{km} (x_m)\mid n\in\omega)=(\bigvee{}^\downarrow_{k\geq n,m} p_{nk}\circ  
n\in\omega)\\ & = & (\bigvee{}^\downarrow_{k\geq n,m} p_{nk}\circ  
+
e_{km} \circ p_{mk} (x_k)\mid n\in\omega)\sqsubseteq (\bigvee{}^\downarrow_{k\geq n,m} p_{nk} (x_k)\mid n\in\omega)=(\bigvee{}^\downarrow_{k\geq n} p_{nk} (x_k)\mid n\in\omega)=(x_n\mid n\in\omega). </math></center>
e_{km} \circ p_{mk} (x_k)\mid n\in\omega)\\ & \sqsubseteq &
+
 
(\bigvee{}^\downarrow_{k\geq n,m} p_{nk} (x_k)\mid n\in\omega)\\
 
& = & (\bigvee{}^\downarrow_{k\geq n} p_{nk} (x_k)\mid  
 
n\in\omega)\\ & = & (x_n\mid n\in\omega).
 
\end{eqnarray*}
 
 
Ponadto,
 
Ponadto,
  
<center><math>p_m\circ e_m (x) = p_m (\bigvee{}^\downarrow_{k\geq  
+
<center><math>p_m\circ e_m (x) = p_m (\bigvee{}^\downarrow_{k\geq n,m} p_{nk}\circ e_{km}(x)\mid n\in\omega ) = \bigvee{}^\downarrow_{k\geq m} p_{mk}\circ e_{km}(x) =  
n,m} p_{nk}\circ e_{km}(x)\mid n\in\omega ) =  
 
\bigvee{}^\downarrow_{k\geq m} p_{mk}\circ e_{km}(x) =  
 
 
x.</math></center>
 
x.</math></center>
  
  
Bliższa analiza pokazuje, że <math>e_m\circ p_m</math> pozostawi
+
Bliższa analiza pokazuje, że <math>e_m\circ p_m</math> pozostawi niezmienione te elementy ciągu <math>(x_n\mid n\in\omega)</math>, gdzie <math>n\leq m</math>.
niezmienione te elementy ciągu <math>(x_n\mid n\in\omega)</math>,
+
 
gdzie <math>n\leq m</math>.
+
<center><math>p_n(e_m\circ p_m (x_n\mid n\in \omega))= ... = p_n(\bigvee{}^\downarrow_{k\geq n,m} p_{nk}\circ e_{km} \circ p_{mk} (x_k)\mid n\in\omega)= p_n(\bigvee{}^\downarrow_{k\geq n,m} p_{nm}\circ p_{mk} \circ e_{km} \circ p_{mk} (x_k)\mid n\in\omega)= p_n(\bigvee{}^\downarrow_{k\geq n,m} p_{nm}\circ  p_{mk} (x_k)\mid n\in\omega)= p_n(\bigvee{}^\downarrow_{k\geq n} p_{nk} (x_k)\mid n\in\omega)= p_n(\bigvee{}^\downarrow_{k\geq n} x_n\mid n\in\omega)= p_n(x_n\mid n\in\omega)\\ & = & x_n.
\begin{eqnarray*}
+
</math></center>
p_n(e_m\circ p_m (x_n\mid n\in \omega)) & = & ...\\ & = &
+
 
p_n(\bigvee{}^\downarrow_{k\geq n,m} p_{nk}\circ e_{km} \circ  
+
To dowodzi, że <math>\bigvee{}^\downarrow_n e_n\circ p_n = 1_{D}</math>, czyli (5).
p_{mk} (x_k)\mid n\in\omega)\\ & = &
 
p_n(\bigvee{}^\downarrow_{k\geq n,m} p_{nm}\circ p_{mk} \circ  
 
e_{km} \circ p_{mk} (x_k)\mid n\in\omega)\\ & = &
 
p_n(\bigvee{}^\downarrow_{k\geq n,m} p_{nm}\circ  p_{mk}  
 
(x_k)\mid n\in\omega)\\ & = & p_n(\bigvee{}^\downarrow_{k\geq n}  
 
p_{nk} (x_k)\mid n\in\omega)\\ & = &
 
p_n(\bigvee{}^\downarrow_{k\geq n} x_n\mid n\in\omega)\\ & = &
 
p_n(x_n\mid n\in\omega)\\ & = & x_n.
 
\end{eqnarray*}
 
To dowodzi, że <math>\bigvee{}^\downarrow_n e_n\circ p_n =  
 
1_{D}</math>, czyli (5).
 
  
 
Korzystając z powyższego mamy też natychmiast
 
Korzystając z powyższego mamy też natychmiast
  
<center><math>h = 1_D\circ h = \bigvee{}^\downarrow_n E_n\circ  
+
<center><math>h = 1_D\circ h = \bigvee{}^\downarrow_n E_n\circ p_n\circ h = \bigvee{}^\downarrow e_m \circ g_n,</math></center>
p_n\circ h = \bigvee{}^\downarrow e_m \circ g_n,</math></center>
 
  
 
co kończy dowód (6).
 
co kończy dowód (6).
  
Do pokazania pozostała nam (7), czyli fakt, że <math>\{e_n\colon
+
Do pokazania pozostała nam (7), czyli fakt, że <math>\{e_n\colon D_n\to D\}</math> jest granicą odwrotną diagramu <math>F</math>. Jeśli <math>\{f_n\colon E\to D_n\}</math> jest dowolną inną
D_n\to D\}</math> jest granicą odwrotną diagramu <math>F</math>.
+
granicą, to sprawdźmy najpierw czy funkcja <math>f = \bigvee{}^\downarrow_n f_n\circ p_n</math> jest dobrze zdefiniowana, tj. czy supremum jest nad zbiorem skierowanym. Ale tak jest, ponieważ dla <math>n\leq m</math>
Jeśli <math>\{f_n\colon E\to D_n\}</math> jest dowolną inną
 
granicą, to sprawdźmy najpierw czy funkcja <math>f =  
 
\bigvee{}^\downarrow_n f_n\circ p_n</math> jest dobrze  
 
zdefiniowana, tj. czy supremum jest nad zbiorem skierowanym. Ale  
 
tak jest, ponieważ dla <math>n\leq m</math>
 
  
<center><math>f_n \circ p_n = f_m \circ e_{mn}\circ p_{nm}\circ  
+
<center><math>f_n \circ p_n = f_m \circ e_{mn}\circ p_{nm}\circ p_m\sqsubseteq f_m\circ p_m.</math></center>
p_m\sqsubseteq f_m\circ p_m.</math></center>
 
  
 +
Co więcej,
  
Co więcej,
+
<center><math>
\begin{eqnarray*}
+
f\circ e_m=\bigvee{}^\downarrow_{n\leq m} f_n\circ p_n\circ e_m= \bigvee{}^\downarrow_{n\leq m} f_n\circ p_n\circ e_n\circ e_{nm}=\bigvee{}^\downarrow_{n\leq m} f_n\circ e_{nm}=\bigvee{}^\downarrow_{n\leq m} f_m=f_m.</math></center>
f\circ e_m & = & \bigvee{}^\downarrow_{n\leq m} f_n\circ p_n\circ  
+
 
e_m\\ & = & \bigvee{}^\downarrow_{n\leq m} f_n\circ p_n\circ  
+
W końcu, pokażemy, że funkcja <math>f</math> o podanych własnościach jest tylko jedna. Jeśli dla <math>f'\colon D\to E</math> zachodzi <math>f'\circ e_m = f_m</math>, to <math>f'\circ
e_n\circ e_{nm}\\ & = & \bigvee{}^\downarrow_{n\leq m} f_n\circ  
 
e_{nm}\\ & = & \bigvee{}^\downarrow_{n\leq m} f_m\\ & = & f_m.
 
\end{eqnarray*}
 
W końcu, pokażemy, że funkcja <math>f</math> o podanych
 
własnościach jest tylko jedna. Jeśli dla <math>f'\colon D\to
 
E</math> zachodzi <math>f'\circ e_m = f_m</math>, to <math>f'\circ
 
 
e_m \circ p_m = f_m\circ p_m</math>, a zatem
 
e_m \circ p_m = f_m\circ p_m</math>, a zatem
  
<center><math>\bigvee{}^\downarrow_m f'\circ e_m \circ p_m =  
+
<center><math>\bigvee{}^\downarrow_m f'\circ e_m \circ p_m = \bigvee{}^\downarrow_m f_m\circ p_m,</math></center>
\bigvee{}^\downarrow_m f_m\circ p_m,</math></center>
 
  
 
czyli z ciągłości <math>f'</math>:
 
czyli z ciągłości <math>f'</math>:
  
<center><math>f'(\bigvee{}^\downarrow_m \circ e_m \circ p_m) =  
+
<center><math>f'(\bigvee{}^\downarrow_m \circ e_m \circ p_m) = \bigvee{}^\downarrow_m f_m\circ p_m.</math></center>
\bigvee{}^\downarrow_m f_m\circ p_m.</math></center>
+
 
 +
Ale <math>\bigvee{}^\downarrow_m \circ e_m \circ p_m = 1_D</math>  oraz <math>\bigvee{}^\downarrow_m f_m\circ p_m = f</math>, co daje <math>f'\circ 1_D = f</math>, czyli <math>f'=f</math>.}}
  
Ale <math>\bigvee{}^\downarrow_m \circ e_m \circ p_m = 1_D</math>
 
oraz <math>\bigvee{}^\downarrow_m f_m\circ p_m = f</math>, co
 
daje <math>f'\circ 1_D = f</math>, czyli <math>f'=f</math>. }}
 
  
 
==Kategoria dcpo i par e-p==
 
==Kategoria dcpo i par e-p==
  
W tej kategorii obiektami są dcpo  posiadające element
+
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 [[Teoria_kategorii_dla_informatyków/TKI_Moduł_2#wyklad2| 2]]. Złożenie morfizmów
najmniejszy, zaś morfizmami są pary e-p, o których była mowa
 
podczas Wykładu
 
[[Teoria_kategorii_dla_informatyków/TKI_Moduł_?#wyklad2| ?]].
 
Złożenie morfizmów
 
  
 
[[Grafika:tk_14_1.png]]
 
[[Grafika:tk_14_1.png]]
Linia 151: Linia 110:
 
[[Grafika:tk_14_2.png]]
 
[[Grafika:tk_14_2.png]]
  
Czy <math>(e_2\circ e_1, p_1\circ p_2)</math> jest parą e-p? Tak,
+
Czy <math>(e_2\circ e_1, p_1\circ p_2)</math> jest parą e-p? Tak, ponieważ:
ponieważ:
 
  
 
<center><math>e_2\circ e_1\circ p_1\circ p_2 \sqsubseteq e_2\circ  
 
<center><math>e_2\circ e_1\circ p_1\circ p_2 \sqsubseteq e_2\circ  
Linia 182: Linia 140:
 
[[Grafika:tk_14_4.png]] }}
 
[[Grafika:tk_14_4.png]] }}
  
{{uwaga|| Tak naprawdę, aby być w zgodzie z definicją funktora
+
{{uwaga|||Tak naprawdę, aby być w zgodzie z definicją funktora ciągłego podaną przed Zadaniem
ciągłego podaną przed Zadaniem
+
[[Teoria_kategorii_dla_informatyków/TKI_Moduł_?#mod3:zad3| ?]], 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''.  
[[Teoria_kategorii_dla_informatyków/TKI_Moduł_?#mod3:zad3| ?]],
 
powinniśmy powyższą własność nazwać nie ciągłością, ale {\it
 
ciągłością dualną}, a funktor - ''funktorem dualnie ciągłym''.  
 
 
Dla potrzeb tego wykładu przyjmijmy jednak powyższą nomenklaturę.}}
 
Dla potrzeb tego wykładu przyjmijmy jednak powyższą nomenklaturę.}}
  
  
{{lemat||mod14:lemma:iso1| Niech <math>\mathbf{A}</math> będzie
+
{{lemat||mod14:lemma:iso1| Niech <math>\mathbf{A}</math> będzie <math>\omega</math>-kategorią, <math>F\colon \mathbf{A}\to \mathbf{A}</math> funktorem ciągłym, <math>f\colon A\to F(A)</math> morfizmem w <math>\mathbf{A}</math> oraz niech diagram
<math>\omega</math>-kategorią, <math>F\colon \mathbf{A}\to \mathbf{A}</math> funktorem ciągłym, <math>f\colon A\to F(A)</math> morfizmem w <math>\mathbf{A}</math> oraz niech diagram
 
  
 
[[Grafika:tk_14_7.png]]
 
[[Grafika:tk_14_7.png]]
Linia 197: Linia 151:
 
posiada granicę odwrotną <math>D_{\infty}</math>. Wówczas <math>D_{\infty}\cong F(D_{\infty})</math>. }}
 
posiada granicę odwrotną <math>D_{\infty}</math>. Wówczas <math>D_{\infty}\cong F(D_{\infty})</math>. }}
  
Zauważmy, że przekątna <math>\Delta\colon \mathbf{Dcpo}\to  
+
 
\mathbf{Dcpo}\times \mathbf{Dcpo}</math>, <math>a\mapsto  
+
Zauważmy, że przekątna <math>\Delta\colon \mathbf{Dcpo}\to \mathbf{Dcpo}\times \mathbf{Dcpo}</math>, <math>a\mapsto (a,a)</math>, <math>f\mapsto (f,f)</math> dla <math>a\in  
(a,a)</math>, <math>f\mapsto (f,f)</math> dla <math>a\in  
+
\mathbf{Dcpo}_0</math>, <math>f\in \mathbf{Dcpo}_1</math> jest ciągłym funktorem.
\mathbf{Dcpo}_0</math>, <math>f\in \mathbf{Dcpo}_1</math> jest  
+
 
ciągłym funktorem.
 
  
 
==Lokalna ciągłość funktorów==  
 
==Lokalna ciągłość funktorów==  

Wersja z 07:50, 3 sie 2006

{{kotwica|wyklad14|} 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  ?.


Twierdzenie

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). 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||mod14:thm:limitcolimit| 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 ? podanym w Zadaniu  ?

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:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle p_{nn'}(y_{n'}) & = & p_{nn'}(\bigvee{}^\downarrow_{k\geq n',m} p_{n'k}\circ e_{km}(x)) = \bigvee{}^\downarrow_{k\geq n',m} p_{nn'}\circ p_{n'k}\circ e_{km}(x) = \bigvee{}^\downarrow_{k\geq n',m} p_{nk}\circ e_{km}(x)=y_n. }

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 .

Parser nie mógł rozpoznać (błąd składni): {\displaystyle p_n(e_m\circ p_m (x_n\mid n\in \omega))= ... = p_n(\bigvee{}^\downarrow_{k\geq n,m} p_{nk}\circ e_{km} \circ p_{mk} (x_k)\mid n\in\omega)= p_n(\bigvee{}^\downarrow_{k\geq n,m} p_{nm}\circ p_{mk} \circ e_{km} \circ p_{mk} (x_k)\mid n\in\omega)= p_n(\bigvee{}^\downarrow_{k\geq n,m} p_{nm}\circ p_{mk} (x_k)\mid n\in\omega)= p_n(\bigvee{}^\downarrow_{k\geq n} p_{nk} (x_k)\mid n\in\omega)= p_n(\bigvee{}^\downarrow_{k\geq n} x_n\mid n\in\omega)= p_n(x_n\mid n\in\omega)\\ & = & x_n. }

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

Plik:Tk 14 1.png

definiujemy w naturalny sposób jako morfizm

Plik: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 [Omega-kategoria]

Nazwijmy {\bf

-kategorią} każdą kategorię, w której diagram

postaci Plik:Tk 14 3.png posiada granicę odwrotną.

Zauważmy, że twierdzenie o zgodności granicy prostej i odwrotnej - Twierdzenie ? - mówi, że Parser nie mógł rozpoznać (Błąd konwersji. Serwer („https://wazniak.mimuw.edu.pl/api/rest_”) zgłosił: „Cannot get mml. TeX parse error: Double exponent: use braces to clarify”): {\displaystyle \mathrm {'} ''Dcpo'''_{\bot }^{EP}} jest -kategorią!

Definicja

Funktor między

-kategoriami nazywamy ciągłym, jeśli zachowuje granice odwrotne, t.j. jeśli jest kogranicą powyższego diagramu, to jest kogranicą diagramu

Plik:Tk 14 4.png
Uwaga
Tak naprawdę, aby być w zgodzie z definicją funktora ciągłego podaną przed Zadaniem

 ?, 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

Niech będzie -kategorią, funktorem ciągłym, morfizmem w oraz niech diagram

Plik: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ść {\it mocniejsza}, która jest łatwiej weryfikowalna: lokalna ciągłość.

Definicja

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 [istnienie funktorów ciągłych]

Niech

funktor będzie lokalnie ciągły. Wtedy istnieje ciągły funktor Parser nie mógł rozpoznać (Błąd konwersji. Serwer („https://wazniak.mimuw.edu.pl/api/rest_”) zgłosił: „Cannot get mml. TeX parse error: Double exponent: use braces to clarify”): {\displaystyle {\widehat {F}}\colon \mathrm {'} ''Dcpo'''_{\bot }^{EP}\times \mathrm {'} ''Dcpo'''_{\bot }^{EP}\to \mathrm {\bf {Dcpo}} _{\bot }^{EP}} , którego działanie na obiekty jest takie

samo, jak funktora .

Dowód

{{{3}}} End of proof.gif


Twierdzenie Scotta

Zgodnie z poprzednim twierdzeniem możemy zdefiniować Eksponent Parser nie mógł rozpoznać (Błąd konwersji. Serwer („https://wazniak.mimuw.edu.pl/api/rest_”) zgłosił: „Cannot get mml. TeX parse error: Double exponent: use braces to clarify”): {\displaystyle Exp\colon \mathrm {\bf {Dcpo}} _{\bot }^{EP}\times \mathrm {'} ''Dcpo'''_{\bot }^{EP}\to \mathrm {'} ''Dcpo'''_{\bot }^{EP}} jako , który jest ciągły (ponieważ eksponent jest lokalnie ciągły). Rozważmy złożenie

Parser nie mógł rozpoznać (Błąd konwersji. Serwer („https://wazniak.mimuw.edu.pl/api/rest_”) zgłosił: „Cannot get mml. TeX parse error: Double exponent: use braces to clarify”): {\displaystyle \mathrm {'} ''Dcpo'''_{\bot }^{EP}{\stackrel {\Delta }{\rightarrow }}\mathrm {\bf {Dcpo}} _{\bot }^{EP}\times \mathrm {'} ''Dcpo'''_{\bot }^{EP}{\stackrel {Exp}{\rightarrow }}\mathrm {'} ''Dcpo'''_{\bot }^{EP}.}

Definiuje ono funktor ciągły (jako złożenie dwóch funktorów ciągłych). Jak on działa? Rozważmy parę:

Plik:Tk 14 8.png

Mamy . Podobnie . Działanie na morfizmach: \begin{eqnarray*} F(e,p) & = & Exp((e,p),(e,p))\\

      & = & ([-,-](p,e), [-,-](e,p))\\
      & = & ([p,e], [e,p]).

\end{eqnarray*} A zatem otrzymujemy

Plik: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 \begin{eqnarray*} [p\to e](f)(q) & = & curry(e\circ ev\circ (1\times p))(f)(q)\\

           & = & (e\circ ev\circ (1\times p))(f,q)\\
           & = & e(ev((f,p(q))))\\
           & = & e(f(p(q)))\\
           & = & e\circ f\circ p (q),

\end{eqnarray*} 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 [Scott]

Niech będzie dcpo z elementem najmniejszym . Zdefiniujmy diagram w jak następuje:

Plik:Tk 14 10.png

gdzie

  • , ,
  • jest funkcją .

jest funkcją .

  • jest funkcją . jest funkcją .

Niech będzie granicą diagramu

Plik:Tk 14 11.png

w . Wówczas