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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
 
(Nie pokazano 22 wersji utworzonych przez 3 użytkowników)
Linia 1: Linia 1:
{{kotwica|wyklad14|} Z poprzedniego wykładu wiemy, że <math>\mathbf{Dcpo}</math> -  
+
{{kotwica|wyklad14|}} Z poprzedniego wykładu wiemy, że <math>\mathbf{Dcpo}</math> - kategoria wszystkich dcpo wraz z funkcjami ciągłymi w sensie Scotta - patrz [[Teoria_kategorii_dla_informatyków/Wykład_12:_Teoria_dziedzin_I#wyklad12|Wykład 12]]. - jest kartezjańsko zamknięta. Kategoria ta jest również zupełna.  Dowód poniższego twierdzenia znajdziemy w rozwiązaniu  [[Teoria_kategorii_dla_informatyków/Ćwiczenia_14:_Teoria_dziedzin_III#mod14:zad1|Zadania 14.1]].
kategoria wszystkich dcpo wraz z funkcjami ciągłymi w sensie Scotta - patrz Wykład
 
[[Teoria_kategorii_dla_informatyków/TKI_Moduł_12#wyklad12|12]] - jest kartezjańsko zamknięta. Kategoria ta jest również zupełna.  Dowód poniższego twierdzenia znajdziemy w rozwiązaniu Zadania [[Teoria_kategorii_dla_informatyków/TKI_Moduł_?#mod14:zad1| ?]].
 
  
  
{{twierdzenie||mod14:thm:grodwr| W <math>\mathbf{Dcpo}</math> istnieją granice dowolnych diagramów. }}
+
{{twierdzenie|14.1|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.
 
}}
 
}}
 +
  
 
==Twierdzenie o zgodności granicy prostej i odwrotnej==
 
==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 <math>\mathbf{Dcpo}</math>. Wynik ten jest znany w literaturze
+
Przedstawimy teraz twierdzenie o zgodności granicy prostej i odwrotnej pewnych szczególnych diagramów w kategorii <math>\mathbf{Dcpo}</math>. 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'').  
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 <math>D\cong [D\to D]</math>. 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 <math>\mathbf{Set}</math> taka sytuacja, zgodnie z twierdzeniem Cantora nie może mieć miejsca.
+
<center>[[Grafika:ilustracja2.png]]</center>
 +
 
 +
Przykładem takiego równania jest <math>D\cong [D,D]</math>. 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 <math>\mathbf{Set}</math> taka sytuacja, zgodnie z twierdzeniem Cantora nie może mieć miejsca.
  
  
{{twierdzenie||mod14:thm:limitcolimit| Rozważmy diagram <math>F</math> w kategorii <math>\mathbf{Dcpo}</math> taki, że
+
{{twierdzenie|14.2|mod14:thm:limitcolimit| Rozważmy diagram <math>F</math> w kategorii <math>\mathbf{Dcpo}</math> taki, że:
* Wierzchołkami <math>F</math> są posety <math>D_0, D_1, D_2, ...</math>.
+
* Wierzchołkami <math>F</math> są posety <math>D_0, D_1, D_2, ...</math>
* Dla <math>n\leq m</math> istnieją funkcje <math>e_{mn}\colon D_n\to D_m</math>,
+
* Dla <math>n\leq m</math> istnieją funkcje <math>e_{mn}\colon D_n\to D_m</math>, i  <math>p_{nm}\colon D_m\to D_n</math> tworzące parę e-p.
      i  <math>p_{nm}\colon D_m\to D_n</math> tworzące parę e-p.
 
 
* Dla każdego <math>n\in \omega</math> mamy <math>e_{nn} = 1_{D_n}</math>.
 
* Dla każdego <math>n\in \omega</math> mamy <math>e_{nn} = 1_{D_n}</math>.
 
* Dla <math>n\leq m\leq k</math> mamy <math>e_{kn} = e_{km}\circ e_{mn}</math> oraz
 
* Dla <math>n\leq m\leq k</math> mamy <math>e_{kn} = e_{km}\circ e_{mn}</math> oraz
 
<math>p_{nk} = p_{nm}\circ p_{mk}</math>.
 
<math>p_{nk} = p_{nm}\circ p_{mk}</math>.
  
Zdefiniujmy
+
Zdefiniujmy:
  
<center><math>D = \{ (x_0, x_1, ...)\mid (\forall n\leq  
+
<center><math>D = \{ (x_0, x_1, ...)\mid (\forall n\leq m)(x_n=p_{nm}(x_m)) \},</math></center>
m)(x_n=p_{nm}(x_m)) \},</math></center>
 
  
<center><math>p_m\colon D\to D_m, \qquad (x_0, x_1, ...)\mapsto x_m, \ m\in \omega</math></center>
+
<center><math>p_m\colon D\to D_m, \qquad (x_0, x_1, ...)\mapsto x_m, \ m\in \omega,</math></center>
  
<center><math>e_m\colon D_m\to D, \ x\mapsto  
+
<center><math>e_m\colon D_m\to D, \ x\mapsto (\bigvee{}^\downarrow_{k\geq n,m} p_{nk}\circ e_{km}(x)\mid n\in \omega).</math></center>
(\bigvee{}^\downarrow_{k\geq n,m} p_{nk}\circ e_{km}(x)\mid n\in  
 
\omega).</math></center>
 
  
 
Wtedy:
 
Wtedy:
Linia 39: Linia 36:
 
* <math>\{p_n\colon D\to D_n\}</math> jest granicą diagramu <math>F</math>. Jeśli <math>\{g_n\colon C\to D_n\}</math> jest dowolną inną granicą, to izmorfizm <math>h\colon C\to D</math> jest dany jako <math>h(x) = (g_n(x)\mid n\in \omega)</math> lub <math>h = \bigvee{}^\downarrow_n e_n\circ g_n</math>.
 
* <math>\{p_n\colon D\to D_n\}</math> jest granicą diagramu <math>F</math>. Jeśli <math>\{g_n\colon C\to D_n\}</math> jest dowolną inną granicą, to izmorfizm <math>h\colon C\to D</math> jest dany jako <math>h(x) = (g_n(x)\mid n\in \omega)</math> lub <math>h = \bigvee{}^\downarrow_n e_n\circ g_n</math>.
 
* <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ą granicą, to izmorfizm <math>f\colon D\to E</math> jest dany jako <math>f(x_n\mid n\in \omega) = \bigvee{}^\downarrow_n f_n(x_n)</math> lub <math>f = \bigvee{}^\downarrow_n f_n\circ p_n</math>.
 
* <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ą granicą, to izmorfizm <math>f\colon D\to E</math> jest dany jako <math>f(x_n\mid n\in \omega) = \bigvee{}^\downarrow_n f_n(x_n)</math> lub <math>f = \bigvee{}^\downarrow_n f_n\circ p_n</math>.
 +
}}
  
{{dowod||| W dowodzie Twierdzenia [[Teoria_kategorii_dla_informatyków/TKI_Moduł_?#mod14:thm:grodwr|
+
{{dowod||| W dowodzie [[Teoria_kategorii_dla_informatyków/Wykład_14:_Teoria_dziedzin_III#mod14:thm:grodwr|Twierdzenia 14.1]] podanym w [[Teoria_kategorii_dla_informatyków/Ćwiczenia_14:_Teoria_dziedzin_III#mod14:zad1|Zadaniu 14.1]]
?]] podanym w Zadaniu [[Teoria_kategorii_dla_informatyków/TKI_Moduł_?#mod14:zad1| ?]]
 
 
pokazaliśmy już, że granicą diagramu jest <math>\{p_n\colon D\to D_n\}</math> i że izomorfizm <math>h\colon C\to D</math> ma (pierwszą z) postulowanych postaci.
 
pokazaliśmy już, że granicą diagramu jest <math>\{p_n\colon D\to D_n\}</math> i że izomorfizm <math>h\colon C\to D</math> ma (pierwszą z) postulowanych postaci.
  
Linia 47: Linia 44:
  
 
<center><math>
 
<center><math>
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.
+
\begin{align}
 +
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.
 +
\end{align}
 
</math></center>
 
</math></center>
  
Linia 56: Linia 55:
  
  
<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  
+
<center><math>\begin{align} 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 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{align} </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). </math></center>
 
  
Ponadto,
+
Ponadto:
  
<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) =  
+
<center><math>\begin{align} 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)\\ &=&
x.</math></center>
+
x.\end{align}</math></center>
  
  
 
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>.
 
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>.
  
<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.
+
<center><math>\begin{align} 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.\end{align}
 
</math></center>
 
</math></center>
 +
  
 
To dowodzi, że <math>\bigvee{}^\downarrow_n e_n\circ p_n = 1_{D}</math>, czyli (5).
 
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 p_n\circ h = \bigvee{}^\downarrow e_m \circ g_n,</math></center>
 
<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>
Linia 79: Linia 78:
  
 
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ą
 
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ą
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>
+
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 p_m\sqsubseteq f_m\circ p_m.</math></center>
 
<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>
  
Co więcej,
+
Co więcej:
  
 
<center><math>
 
<center><math>
Linia 89: Linia 88:
  
 
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
 
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 =  \bigvee{}^\downarrow_m f_m\circ p_m,</math></center>
 
<center><math>\bigvee{}^\downarrow_m f'\circ e_m \circ p_m =  \bigvee{}^\downarrow_m f_m\circ p_m,</math></center>
Linia 98: Linia 97:
  
 
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 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
+
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/Wykład_2:_Morfizmy_specjalne#wyklad2| 2]]. Złożenie morfizmów
  
[[Grafika:tk_14_1.png]]
+
<center>[[Grafika:tk-14.1.png]]</center>
  
 
definiujemy w naturalny sposób jako morfizm
 
definiujemy w naturalny sposób jako morfizm
  
[[Grafika:tk_14_2.png]]
+
<center>[[Grafika:tk-14.2.png]]</center>
  
 
Czy <math>(e_2\circ e_1, p_1\circ p_2)</math> jest parą e-p? Tak, ponieważ:
 
Czy <math>(e_2\circ e_1, p_1\circ p_2)</math> jest parą e-p? Tak, 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 1_E\circ p_2 = e_2\circ p_2\sqsubseteq 1_F</math></center>
1_E\circ p_2 = e_2\circ p_2\sqsubseteq 1_F</math></center>
 
  
 
oraz
 
oraz
Linia 119: Linia 116:
 
<center><math>p_1\circ p_2\circ e_2\circ e_1 = p_1\circ 1_E\circ e_1 = p_1\circ e_1 = 1_D.</math></center>
 
<center><math>p_1\circ p_2\circ e_2\circ e_1 = p_1\circ 1_E\circ e_1 = p_1\circ e_1 = 1_D.</math></center>
  
A zatem złożenie par e-p jest dobrze zdefiniowane, a co za tym
+
A zatem złożenie par e-p jest dobrze zdefiniowane, a co za tym idzie, i co łatwo już teraz pokazać, <math>\mathbf{Dcpo}^{EP}_{\bot}</math> jest kategorią.
idzie, i co łatwo już teraz pokazać, <math>\mathrm{\bf
 
Dcpo}^{EP}_{\bot}</math> jest kategorią.
 
  
{{definicja|[Omega-kategoria]|def:omegacat| Nazwijmy {\bf
 
<math>\omega</math>-kategorią} każdą kategorię, w której diagram
 
postaci [[Grafika:tk_14_3.png]] posiada granicę odwrotną. }}
 
Zauważmy, że twierdzenie o zgodności granicy prostej i odwrotnej
 
- Twierdzenie
 
[[Teoria_kategorii_dla_informatyków/TKI_Moduł_?#mod14:thm:limitcolimit|
 
?]] - mówi, że <math>\mathrm'''Dcpo'''^{EP}_{\bot}</math> jest
 
<math>\omega</math>-kategorią!
 
  
{{definicja ||| Funktor <math>F</math> między
+
{{definicja|14.3 [Omega-kategoria]|def:omegacat| Nazwijmy <math>\omega</math>-'''kategorią''' każdą kategorię, w której diagram postaci:
<math>\omega</math>-kategoriami nazywamy '''ciągłym''', jeśli
 
zachowuje granice odwrotne, t.j. jeśli <math>D_{\infty}</math>
 
jest kogranicą powyższego diagramu, to <math>F(D_{\infty})</math>
 
jest kogranicą diagramu
 
  
[[Grafika:tk_14_4.png]] }}
+
<center>[[Grafika:tk-14.3.png]]</center>
  
{{uwaga|||Tak naprawdę, aby być w zgodzie z definicją funktora ciągłego podaną przed Zadaniem
+
posiada granicę odwrotną. }} Zauważmy, że twierdzenie o zgodności granicy prostej i odwrotnej  - [[Teoria_kategorii_dla_informatyków/Wykład_14:_Teoria_dziedzin_III#mod14:thm:limitcolimit| Twierdzenie 14.2]] - mówi, że <math>\mathbb{Dcpo}^{EP}_{\bot}</math> jest  <math>\omega</math>-kategorią!
[[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''.
 
Dla potrzeb tego wykładu przyjmijmy jednak powyższą nomenklaturę.}}
 
  
  
{{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
+
{{definicja |14.4 [Funktor ciągły]|| Funktor <math>F</math> między <math>\omega</math>-kategoriami nazywamy '''ciągłym''', jeśli zachowuje granice odwrotne, tj.: jeśli <math>D_{\infty}</math> jest kogranicą powyższego diagramu, to <math>F(D_{\infty})</math> jest kogranicą diagramu:
  
[[Grafika:tk_14_7.png]]
+
<center>[[Grafika:tk-14.4.png]]</center> }}
 +
 
 +
{{uwaga|||Tak naprawdę, aby być w zgodzie z definicją funktora ciągłego podaną przed Zadaniem [[Teoria_kategorii_dla_informatyków/Ćwiczenia_3:_Zasada_dualności_i_proste_konstrukcje_uniwersalne#mod3:zad3|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|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:
 +
 
 +
<center>[[Grafika:tk-14.7.png]]</center>
  
 
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 (a,a)</math>, <math>f\mapsto (f,f)</math> dla <math>a\in  
+
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 \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==
+
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 <math>F\colon \mathbf{D}\to \mathbf{E}</math> pomiędzy kategoriami posetów <math>\mathbf{D}, \mathbf{E}</math> jest '''lokalnie ciągły''' jeśli przekształcenia <math>f\mapsto F(f)</math> typu <math>\mathrm{Hom}(D,D')\to \mathrm{Hom}(F(D),F(D'))</math> są ciągłe w sensie Scotta dla każdej pary obiektów <math>D,D'\in \mathbf{D}_0</math>.}}
  
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 <math>F\colon \mathbf{D}\to
+
Dla przykładu przeczytajmy tę definicję dla bifunktora <math>F\colon \mathbf{Dcpo}^{op}\times \mathbf{Dcpo}\to \mathbf{Dcpo}</math>: funktor <math>F</math> jest lokalnie ciągły, jeśli dla dowolnych zbiorów skierowanych <math>A\subseteq^{\uparrow} [D_2, D_1]</math> i <math>B\subseteq^{\uparrow} [D_3, D_4]</math>, gdzie <math>D_1, ..., D_4\in \mathbf{Dcpo}_0</math>, mamy:
\mathbf{E}</math> pomiędzy kategoriami posetów <math>\mathbf{D},
 
\mathbf{E}</math> jest '''lokalnie ciągły''' jeśli przekształcenia
 
<math>f\mapsto F(f)</math> typu <math>\mathrm{Hom}(D,D')\to
 
\mathrm{Hom}(F(D),F(D'))</math> są ciągłe w sensie Scotta dla
 
każdej pary obiektów <math>D,D'\in \mathbf{D}_0</math>. }}
 
  
Dla przykładu przeczytajmy tę definicję dla bifunktora
+
<center><math>F(\bigvee{}^\downarrow A, \bigvee{}^\downarrow B) = \bigvee{}^\downarrow_{f\in A, g\in G} F(f,g).</math></center>
<math>F\colon \mathbf{Dcpo}^{op}\times \mathbf{Dcpo}\to
 
\mathbf{Dcpo}</math>: funktor <math>F</math> jest lokalnie
 
ciągły, jeśli dla dowolnych zbiorów skierowanych
 
<math>A\subseteq^{\uparrow} [D_2, D_1]</math> i
 
<math>B\subseteq^{\uparrow} [D_3, D_4]</math>, gdzie <math>D_1,
 
..., D_4\in \mathbf{Dcpo}_0</math>, mamy
 
  
<center><math>F(\bigvee{}^\downarrow A, \bigvee{}^\downarrow B) =
+
Zauważmy, że supremum po prawej stronie istnieje w <math>[F(D_1,D_3), F(D_2, D_4)]</math>.
\bigvee{}^\downarrow_{f\in A, g\in G} F(f,g).</math></center>
 
  
Zauważmy, że supremum po prawej stronie istnieje w
+
Dla przykładu, eksponent <math>[-,-]\colon\mathbf{Dcpo}^{op}\times \mathbf{Dcpo}\to  \mathbf{Dcpo}</math> jest lokalnie ciągły, ponieważ <math>[f\to g] = curry(g\circ ev\circ (1\times f))</math> jest złożeniem  funkcji ciągłych w sensie Scotta.
<math>[F(D_1,D_3), F(D_2, D_4)]</math>.
 
  
Dla przykładu, eksponent
 
<math>[\_,\_]\colon\mathbf{Dcpo}^{op}\times \mathbf{Dcpo}\to
 
\mathbf{Dcpo}</math> jest lokalnie ciągły, ponieważ <math>[f\to
 
g] = curry(g\circ ev\circ (1\times f))</math> jest złożeniem
 
funkcji ciągłych w sensie Scotta.
 
  
 +
{{lemat|14.7 [istnienie funktorów ciągłych]|mod14:lemma:lokci| Niech funktor <math>F\colon \mathbf{Dcpo}^{op}_{\bot}\times \mathbf{Dcpo}_{\bot}\to \mathbf{Dcpo}_{\bot}</math> będzie  lokalnie ciągły. Wtedy istnieje ciągły funktor <math>\widehat{F}\colon \mathbf{Dcpo}^{EP}_{\bot}\times \mathbf{Dcpo}^{EP}_{\bot}\to \mathbf{Dcpo}^{EP}_{\bot}</math>, którego działanie na obiekty jest takie samo, jak funktora <math>F</math>.}}
  
{{lemat|[istnienie funktorów ciągłych]|mod14:lemma:lokci| Niech
 
funktor <math>F\colon \mathbf{Dcpo}^{op}_{\bot}\times
 
\mathbf{Dcpo}_{\bot}\to \mathbf{Dcpo}_{\bot}</math> będzie
 
lokalnie ciągły. Wtedy istnieje ciągły funktor
 
<math>\widehat{F}\colon \mathrm'''Dcpo'''^{EP}_{\bot}\times
 
\mathrm'''Dcpo'''^{EP}_{\bot}\to \mathrm{\bf
 
Dcpo}^{EP}_{\bot}</math>, którego działanie na obiekty jest takie
 
samo, jak funktora <math>F</math>.}}
 
  
{{dowod||| Połóżmy <math>\widehat{F}(A,B) = F(A,B)</math>, gdzie
+
{{dowod||| Połóżmy <math>\widehat{F}(A,B) = F(A,B)</math>, gdzie <math>A,B</math> są dcpo z elementami najmniejszymi. Rozważmy pary e-p:
<math>A,B</math> są dcpo z elementami najmniejszymi. Rozważmy pary
 
e-p:
 
  
[[Grafika:tk_14_5.png]]
+
<center>[[Grafika:tk-14.5.png]]</center>
  
Możemy wówczas stworzyć diagram
+
Możemy wówczas stworzyć diagram:
  
[[Grafika:tk_14_6.png]]
+
<center>[[Grafika:tk-14.6.png]]</center>
  
 
i para morfizmów powyżej jest parą e-p. Rzeczywiście:
 
i para morfizmów powyżej jest parą e-p. Rzeczywiście:
  
<center><math>F(e,s)\circ F(p,j) = F(p\circ e, s\circ j) = F(1_A, 1_B) = 1_{F(A,B))}.</math></center>
+
<center><math>F(e,s)\circ F(p,j) = F(p\circ e, s\circ j) = F(1_A, 1_B) =1_{F(A,B))}.</math></center>
  
Wykorzystaliśmy kolejno: kontrawariantność <math>F</math> dla
+
Wykorzystaliśmy kolejno: kontrawariantność <math>F</math> dla pierwszego argumentu, własności par e-p i definicję funktora. Ponadto:
pierwszego argumentu, własności par e-p i definicję funktora.
 
Ponadto,
 
  
<center><math>F(p,j)\circ F(e,s)  = F(e\circ p, j\circ s)  
+
<center><math>F(p,j)\circ F(e,s)  = F(e\circ p, j\circ s) \sqsubseteq F(1_{A'}, 1_{B'}) = 1_{F(A',B')}.</math></center>
\sqsubseteq F(1_{A'}, 1_{B'}) = 1_{F(A',B')}.</math></center>
 
  
Wykorzystaliśmy kolejno: definicję funktora, monotoniczność
+
Wykorzystaliśmy kolejno: definicję funktora, monotoniczność <math>F</math>, która wynika z lokalnej ciągłości i w końcu definicję <math>F</math> jeszcze raz.
<math>F</math>, która wynika z lokalnej ciągłości i w końcu
 
definicję <math>F</math> jeszcze raz.
 
  
Zdefiniujmy zatem
+
Zdefiniujmy zatem:
  
 
<center><math>\widehat{F}((e,p),(j,s)) = (F(p,j),F(e,s)).</math></center>
 
<center><math>\widehat{F}((e,p),(j,s)) = (F(p,j),F(e,s)).</math></center>
  
Oczywiście, <math>\widehat{F}</math> jest funktorem. Aby pokazać
+
Oczywiście, <math>\widehat{F}</math> jest funktorem. Aby pokazać ciągłość, załóżmy, że mamy w <math>\mathbf{Dcpo}^{EP}_{\bot}\times \mathbf{Dcpo}^{EP}_{\bot}</math> diagram:
ciągłość, załóżmy, że mamy w <math>\mathrm{\bf
 
Dcpo}^{EP}_{\bot}\times \mathrm'''Dcpo'''^{EP}_{\bot}</math>  
 
diagram
 
  
 
<center><math>(A_1,B_1)\to  (A_2,B_2)\to (A_3,B_3)\to...,</math></center>
 
<center><math>(A_1,B_1)\to  (A_2,B_2)\to (A_3,B_3)\to...,</math></center>
  
który ma granicę odwrotną <math>(D,E)</math>. A to znaczy, że w
+
który ma granicę odwrotną <math>(D,E)</math>. A to znaczy, że w <math>\mathbf{Dcpo}</math> mamy dwa diagramy:
<math>\mathbf{Dcpo}</math> mamy dwa diagramy
 
  
 
<center><math>A_1\to A_2\to A_3\to...</math></center>
 
<center><math>A_1\to A_2\to A_3\to...</math></center>
Linia 243: Linia 196:
 
<center><math>B_1\to B_2\to B_3\to...,</math></center>
 
<center><math>B_1\to B_2\to B_3\to...,</math></center>
  
których granicami są odpowiednio <math>D</math> i <math>E</math>.
+
których granicami są odpowiednio <math>D</math> i <math>E</math>. Z twierdzenia o koincydencji granicy prostej i odwrotnej ([[Teoria_kategorii_dla_informatyków/Wykład_14:_Teoria_dziedzin_III#mod14:thm:limitcolimit|Twierdzenie 14.2]]) wiemy, że zachodzi <math>1_D = \bigvee{}^\downarrow_n e_n\circ p_n</math> oraz <math>1_E = \bigvee{}^\downarrow_n j_n\circ s_n</math>, a więc <math>1_{(D,E)} = \bigvee{}^\downarrow (e_n\circ p_n, j_n\circ s_n)</math>. Aplikując lokalną ciągłość <math>F</math> do ostatniej równości, mamy:
Z twierdzenia o koincydencji granicy prostej i odwrotnej
+
 
(Twierdzenie [[Teoria_kategorii_dla_informatyków/TKI_Moduł_?#mod14:thm:limitcolimit|
+
<center><math>1_{\widehat{F}(D,E)} = \widehat{F}(1_{(D,e)})=(F(1_D,1_E),F(1_D,1_E))= \bigvee{}^\downarrow (F(e_n\circ p_n, j_n\circ s_n),F(e_n\circ p_n, j_n\circ s_n)).</math></center>
?]]) wiemy, że zachodzi <math>1_D = \bigvee{}^\downarrow_n  
+
 
e_n\circ p_n</math> oraz <math>1_E = \bigvee{}^\downarrow_n  
+
Ale [[Teoria_kategorii_dla_informatyków/Wykład_14:_Teoria_dziedzin_III#mod14:thm:limitcolimit|Twierdzenie 14.2]] mówi, że ostatnia równość charakteryzuje granicę odwrotną diagramu w <math>\mathbf{Dcpo}^{EP}_{\bot}</math>
j_n\circ s_n</math>, a więc <math>1_{(D,E)} =  
 
\bigvee{}^\downarrow (e_n\circ p_n, j_n\circ s_n)</math>.  
 
Aplikując lokalną ciągłość <math>F</math> do ostatniej równości  
 
mamy
 
\begin{eqnarray*}
 
1_{\widehat{F}(D,E)} & = & \widehat{F}(1_{(D,e)})\\
 
                    & = & (F(1_D,1_E),F(1_D,1_E))\\
 
                    & = & \bigvee{}^\downarrow (F(e_n\circ p_n, j_n\circ s_n),F(e_n\circ p_n, j_n\circ s_n)).
 
\end{eqnarray*}
 
Ale Twierdzenie
 
[[Teoria_kategorii_dla_informatyków/TKI_Moduł_?#mod14:thm:limitcolimit|
 
?]] mówi, że ostatnia równość charakteryzuje granicę odwrotną
 
diagramu w <math>\mathrm'''Dcpo'''^{EP}_{\bot}</math>
 
  
 
<center><math>\widehat{F}(A_1,B_1)\to \widehat{F}(A_2,B_2)\to \widehat{F}(A_3,B_3)\to ...</math></center>
 
<center><math>\widehat{F}(A_1,B_1)\to \widehat{F}(A_2,B_2)\to \widehat{F}(A_3,B_3)\to ...</math></center>
  
a zatem <math>\widehat{F}(D,E)=F(D,E)</math> jest tą szukaną
+
a zatem <math>\widehat{F}(D,E)=F(D,E)</math> jest tą szukaną granicą odwrotną, co należało pokazać.}}
granicą odwrotną, co należało pokazać. }}
+
 
  
 +
[[grafika:Scott-portret.gif|thumb|right||Dana S. Scott ur. 1932<br>[[Biografia Scotta|Zobacz biografię]]]]
  
 
==Twierdzenie Scotta==  
 
==Twierdzenie Scotta==  
  
Zgodnie z poprzednim twierdzeniem możemy zdefiniować Eksponent <math>Exp\colon \mathrm{\bf
+
Zgodnie z poprzednim twierdzeniem możemy zdefiniować Eksponent <math>Exp\colon \mathbf{Dcpo}^{EP}_{\bot}\times \mathbf{Dcpo}^{EP}_{\bot} \to \mathbf{Dcpo}^{EP}_{\bot}</math> jako <math>\widehat{[-,-]}</math>, który jest ciągły (ponieważ eksponent <math>[-,-]</math> jest lokalnie ciągły). Rozważmy złożenie <math>\mathbf{Dcpo}^{EP}_{\bot}  \stackrel{\Delta}{\rightarrow} \mathbf{Dcpo}^{EP}_{\bot}\times\mathbf{Dcpo}^{EP}_{\bot} \stackrel{Exp}{\rightarrow} \mathbf{Dcpo}^{EP}_{\bot} .</math> Definiuje ono funktor ciągły <math>F</math> (jako złożenie dwóch funktorów ciągłych). Jak on działa? Rozważmy parę:
Dcpo}^{EP}_{\bot}\times \mathrm'''Dcpo'''^{EP}_{\bot} \to  
 
\mathrm'''Dcpo'''^{EP}_{\bot}</math> jako  
 
<math>\widehat{[-,-]}</math>, który jest ciągły (ponieważ  
 
eksponent <math>[-,-]</math> jest lokalnie ciągły). Rozważmy  
 
złożenie
 
  
<center><math>\mathrm'''Dcpo'''^{EP}_{\bot}
+
<center>[[Grafika:tk-14.8.png]]</center>  
\stackrel{\Delta}{\rightarrow} \mathrm{\bf
 
Dcpo}^{EP}_{\bot}\times\mathrm'''Dcpo'''^{EP}_{\bot}
 
\stackrel{Exp}{\rightarrow} \mathrm'''Dcpo'''^{EP}_{\bot}
 
.</math></center>
 
  
Definiuje ono funktor ciągły <math>F</math> (jako złożenie dwóch
+
Mamy <math>F(P) = Exp\circ \Delta(P) = Exp(P,P) = [-,-](P,P) =[P,P]</math>. Podobnie <math>F(Q) = [Q,Q]</math>. Działanie na morfizmach:
funktorów ciągłych). Jak on działa? Rozważmy parę:
 
  
[[Grafika:tk_14_8.png]]
+
<center><math> F(e,p) = Exp((e,p),(e,p))= ([-,-](p,e), [-,-](e,p)) = ([p,e], [e,p]).</math></center>
  
Mamy <math>F(P) = Exp\circ \Delta(P) = Exp(P,P) = [-,-](P,P) =
+
A zatem otrzymujemy:
[P,P]</math>. Podobnie <math>F(Q) = [Q,Q]</math>. 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
 
  
[[Grafika:tk_14_9.png]]
+
<center>[[Grafika:tk-14.9.png]]</center>
  
Wiemy już, że para funkcji powyżej tworzy parę e-p! Przypomnijmy
+
Wiemy już, że para funkcji powyżej tworzy parę e-p! Przypomnijmy jeszcze raz, jak działają funkcje <math>[p,e]</math> i <math>[e,p]</math> na elementy z odpowiednio <math>[P,P]</math> i <math>[Q,Q]</math>. Przykładowo, dla <math>f\in [P,P]</math> mamy dla <math>q\in Q</math>:
jeszcze raz jak działają funkcje <math>[p,e]</math> i
 
<math>[e,p]</math> na elementy z odpowiednio <math>[P,P]</math> i
 
<math>[Q,Q]</math>: przykładowo, dla <math>f\in [P,P]</math> mamy
 
dla <math>q\in Q</math>
 
\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 <math>[p,e](f) = e\circ f\circ p</math>. Podobnie
 
<math>[e,p](g) = p\circ g\circ e</math> dla <math>g\in
 
[Q,Q]</math>.
 
  
Zauważmy w końcu, że dla dowolnego dcpo <math>P</math>, jeśli jako
+
<center><math> [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),</math></center>
<math>e\colon P\to F(P)</math> weźmiemy funkcję <math>y\mapsto
+
 
\lambda x.y</math>, zaś jako <math>p\colon F(P)\to P</math>
+
to znaczy <math>[p,e](f) = e\circ f\circ p</math>. Podobnie <math>[e,p](g) = p\circ g\circ e</math> dla <math>g\in [Q,Q]</math>.
weźmiemy funkcję <math>f\mapsto f(\bot)</math>, to para
+
 
<math>(e,p)</math> jest parą e-p typu <math>P\to F(P)</math>.
+
Zauważmy w końcu, że dla dowolnego dcpo <math>P</math>, jeśli jako <math>e\colon P\to F(P)</math> weźmiemy funkcję <math>y\mapsto \lambda x.y</math>, zaś jako <math>p\colon F(P)\to P</math> weźmiemy funkcję <math>f\mapsto f(\bot)</math>, to para <math>(e,p)</math> jest parą e-p typu <math>P\to F(P)</math>.
  
 
A zatem otrzymujemy końcowy wniosek:
 
A zatem otrzymujemy końcowy wniosek:
  
 +
{{twierdzenie|14.8 [Scott]|mod14:thm:Scotta| Niech <math>P</math> będzie dcpo z elementem najmniejszym <math>\bot</math>. Zdefiniujmy diagram w <math>\mathbf{Dcpo}</math>, jak następuje:
  
{{twierdzenie|[Scott]|mod14:thm:Scotta| Niech <math>P</math> będzie dcpo z elementem najmniejszym <math>\bot</math>. Zdefiniujmy diagram w <math>\mathbf{Dcpo}</math> jak następuje:
+
<center>[[Grafika:tk-14.10.png]]</center>
  
[[Grafika:tk_14_10.png]]
+
gdzie:
 
 
gdzie
 
  
 
* <math>D_0 = P</math>, <math>D_{n+1} = [D_n,D_n]</math>,
 
* <math>D_0 = P</math>, <math>D_{n+1} = [D_n,D_n]</math>,
Linia 336: Linia 244:
 
* <math>e_{n+1}\colon [D_n,D_n] = D_{n+1} \to [D_{n+1},D_{n+1}]</math> jest funkcją <math>\lambda f.e_n\circ f\circ p_n</math>. <math>p_{n+1}\colon [D_{n+1},D_{n+1}]\to [D_n,D_n]</math> jest funkcją <math>\lambda g.p_n \circ g\circ e_n</math>.
 
* <math>e_{n+1}\colon [D_n,D_n] = D_{n+1} \to [D_{n+1},D_{n+1}]</math> jest funkcją <math>\lambda f.e_n\circ f\circ p_n</math>. <math>p_{n+1}\colon [D_{n+1},D_{n+1}]\to [D_n,D_n]</math> jest funkcją <math>\lambda g.p_n \circ g\circ e_n</math>.
  
Niech <math>D_{\infty}</math> będzie granicą diagramu
+
Niech <math>D_{\infty}</math> będzie granicą diagramu:
  
[[Grafika:tk_14_11.png]]
+
<center>[[Grafika:tk-14.11.png]]</center>
  
w <math>\mathbf{Dcpo}</math>. Wówczas
+
w <math>\mathbf{Dcpo}</math>. Wówczas:
  
 
<center><math>D_{\infty}\cong [D_{\infty},D_{\infty}].</math></center>
 
<center><math>D_{\infty}\cong [D_{\infty},D_{\infty}].</math></center>
 +
 
}}
 
}}

Aktualna wersja na dzień 12:14, 26 wrz 2020

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: