TKI Moduł 13

Twierdzenie o istnieniu granic w Dcpo

Udowodnijmy teraz podstawowe twierdzenie na temat diagramów w kategorii Dcpo.

Twierdzenie. W Dcpo istnieją granice dowolnych diagramów.

Dowód: Dowód przeprowadzimy dla szczególnego diagramu:

(Dowód ogólny jest analogiczny lecz wymaga bardziej technicznego zapisu, wiec go pominiemy.) Pokażemy, że granica powyższego diagramu jest dana jako

$D=\{(x_0,x_1,...)\mid (\mathrm{\forall }n\in \omega )(f_n(x_{n+1})=x_n)\}$.

Zauważmy, że zbiór $D$ jest posetem, w którym elementy są uporządkowane po współrzędnych (to znaczy, że porządek jest dziedziczony z produktu ${\mathrm{\Pi }}_{n\in \omega }{D}_n$. Jeśli $G\subseteq D$ jest zbiorem skierowanym, to dla każdego $n\in \omega$zbiór ${\pi }_n[G]=\{x_n\mid x\in G\}$jest skierowanym podzbiorem $D_n$. Niech $y_n=\bigvee \{x_n\mid x\in G\}$. Z ciągłości funkcji tworzących diagram mamy: $f_n(y_{n+1})=\bigvee f_n(\{x_{n+1}\mid x\in G\})=\bigvee \{x_n\mid x\in G\}=y_n$. To znaczy, że $(y_0,y_1,...)\in D$ i, jak łatwo zauważyć, element ten jest supremum skierowanym zbioru $G$. Pokazaliśmy więc, że $D\in$ Dcpo.

Udowodnimy teraz, że $D$ wraz z projekcjami $\{{\pi }_n:D\to D_n\mid n\in \omega \}$ jest granicą. Po pierwsze, dla $G\subseteq D$ mamy

${\pi }_n(\bigvee G)=y_n=\bigvee \{x_n\mid x\in G\}=\bigvee {\pi }_n[G]$

a więc projekcje są ciągłe. Po drugie, jeśli $\{g_k:E\to D_k\mid k\in \omega \}$ jest dowolną inną granicą, to zdefiniujmy $h:E\to D$ jako $h(x)=(g_0(x),g_1(x),...)$. Z definicji powyższej wynika, że dla każdego $k\in \omega$ mamy $\pi_k \circ h = g_k</math>. Zauważmy, że to świadczy o jednoznaczności wyboru $h$. A zatem $D$ jest granicą omawianego diagramu. Co więcej, z jednoznaczności granicy wnioskujemy, że $D\cong E$. QED

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ć poewne restrykcje zarówno na kształ 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 posetów zupełnych. 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 $D\cong [D\to D]$. Okazuje się, że jego nietrywialne rozwiązania istnieja! Tak więc istnieją posety, które są izomorficzne z przestrzenią swoich ciągłych endofunkcji! Jeden z takich częściowych porządków skonstruujemy poniżej, pod koniec wykładu.

Twierdzenie. Rozważmy diagram $F$ w kategorii Dcpo taki, że:

1. Wierzchołkami $F$ są posety $D_0,D_1,D_2,..$.;

2. Dla $n\le m$ istnieją funkcje $e_{mn}:D_n\to D_m$ i $p_{nm}:D_m\to D_n$ tworzące parę e-p; 3. Dla każdego $n\in \omega$ mamy $e_{nn}=1_{D_n}$;

4. Dla $n\le m\le k$ mamy $e_{kn}=e_{km}\circ e_{mn}$ oraz $p_{nk}=p_{nm}\circ p_{mk}$.

Zdefiniujmy:

$D=\{(x_0,x_1,...)\mid (\mathrm{\forall }n\le m)(x_n=p_{nm}(x_m))\}$

$p_m:D\to D_m,(x_0,x_1,...)\mapsto x_m,m\in \omega$

$e_m:D_m\to D,x\mapsto (\underset{k\ge n,m}{\bigvee }{p}_{nk}\circ e_{km}(x)\mid n\in \omega )$.

Wtedy:

5. Para $(e_m,p_m)$ jest parą e-p i zachodzi $\underset{n\in \omega }{\bigvee }{e}_n\circ p_n=1_D$,

6.$\{p_n:D\to D_n\}$ jest granicą diagramu $F$. Jeśli $\{g_n:C\to D_n\}$ jest dowolną inną granicą, to izmorfizm $h:C\to D$ jest dany jako $h(x)=(g_n(x)\mid n\in \omega )$ lub $h=\underset{n}{\bigvee }{e}_n\circ g_n$;

7.$\{e_n:D_n\to D\}$ jest granicą odwrotną diagramu $F$. Jeśli $\{f_n:E\to D_n\}$ jest dowolną inną granicą, to izmorfizm $f:D\to E$ jest dany jako $f(x_n\mid n\in \omega )=\underset{n}{\bigvee }{f}_n(x_n)$ lub $f=\underset{n}{\bigvee }{f}_n\circ p_n$.

Dowód: W Twierdzeniu ??? pokazaliśmy już, że granicą diagramu jest $\{p_n:D\to D_n\}$ i że izomorfizm $h:C\to D$ ma (pierwszą z) postulowanych postaci. Pokażmy teraz, że funkcje $e_m$ są dobrze zdefiniowane, tj. że $y=e_m(x)$ należy do $D$ dla dowolnego $m\in \omega$. Niech $m$ będzie dowolne i załóżmy, że $n\le n^{\prime }$. Mamy:

$p_{n{n}^{\prime }}(y_{n^{\prime }})=p_{n{n}^{\prime }}(\underset{k\ge n^{\prime },m}{\bigvee }{p}_{n^{\prime }k}\circ e_{km}(x))=\underset{k\ge n^{\prime },m}{\bigvee }{p}_{n{n}^{\prime }}\circ p_{n^{\prime }k}\circ e_{km}(x)=\underset{k\ge n^{\prime },m}{\bigvee }{p}_{nk}\circ e_{km}(x)=y_n$.

W dowodzie korzystaliśmy kolejno z: definicji $y_{n^{\prime }}$, ciągłości $p_{n{n}^{\prime }}$ i definicji $y_n$. A zatem $y=(y_0,y_1,...)\in D$. Co więcej, funkcje $e_m$ są ciągłe, gdyż tylko funkcje ciągłe zostały użyte w ich definicji.

Przejdźmy do dowodu (5). Niech $m\in \omega$. Mamy:

$e_m\circ p_m(x_n\mid n\in \omega )=e_m(x_m)=(\underset{k\ge n,m}{\bigvee }{p}_{nk}\circ e_{km}(x_m)\mid n\in \omega )=(\underset{k\ge n,m}{\bigvee }{p}_{nk}\circ e_{km}\circ p_{mk}(x_k)\mid n\in \omega )\subseteq (\underset{k\ge n,m}{\bigvee }{p}_{nk}(x_k)\mid n\in \omega )=(\underset{k\ge n}{\bigvee }{p}_{nk}(x_k)\mid n\in \omega )=(x_n\mid n\in \omega )$.

Ponadto, $p_m\circ e_m(x)=p_m(\underset{k\ge n,m}{\bigvee }{p}_{nk}\circ e_{km}(x)\mid n\in \omega )=\underset{k\ge m}{\bigvee }{p}_{mk}\circ e_{km}(x)=x$.

Bliższa analiza pokazuje, że $e_m\circ p_m$ pozostawi niezmienione te elementy ciągu $(x_n\mid n\in \omega )$ gdzie $n\le m$:

$p_n(e_m\circ p_m(x_n\mid n\in \omega ))=...=p_n(\underset{k\ge n,m}{\bigvee }{p}_{nk}\circ e_{km}\circ p_{mk}(x_k)\mid n\in \omega )=p_n(\underset{k\ge n,m}{\bigvee }{p}_{nm}\circ p_{mk}\circ e_{km}\circ p_{mk}(x_k)\mid n\in \omega )=p_n(\underset{k\ge n,m}{\bigvee }{p}_{nm}\circ p_{mk}(x_k)\mid n\in \omega )=p_n(\underset{k\ge n}{\bigvee }{p}_{nk}(x_k)\mid n\in \omega )=p_n(\underset{k\ge n}{\bigvee }{x}_n\mid n\in \omega )=p_n(x_n\mid n\in \omega )=x_n$.

To dowodzi, że $\underset{n}{\bigvee }{e}_n\circ p_n=1_D$, czyli (5).

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

$h=1_D\circ h=\underset{n}{\bigvee }{E}_n\circ p_n\circ h=\bigvee e_m\circ g_n$

co kończy dowód (6).

Do pokazania pozostała nam (7), czyli fakt, że $\{e_n:D_n\to D\}$ jest granicą odwrotną diagramu $F$ Jeśli $\{f_n:E\to D_n\}$ jest dowolną inną granicą, to sprawdźmy najpierw czy funkcja $f=\underset{n}{\bigvee }{f}_n\circ p_n$ jest dobrze zdefiniowana, tj. czy supremum jest nad zbiorem skierowanym. Ale tak jest, ponieważ dla $n\le m$:

$f_n\circ p_n=f_m\circ e_{mn}\circ p_{nm}\circ p_m⊑f_m\circ p_m$.

Co więcej,

$f\circ e_m=\underset{n\le m}{\bigvee }{f}_n\circ p_n\circ e_m=\underset{n\le m}{\bigvee }{f}_n\circ p_n\circ e_n\circ e_{nm}=\underset{n\le m}{\bigvee }{f}_n\circ e_{nm}=\underset{n\le m}{\bigvee }{f}_m=f_m.$

W końcu pokażemy, że funkcja $f$ o podanych własnościach jest tylko jedna. Jeśli dla $f^{\prime }:D\to E$ zachodzi $f^{\prime }\circ e_m=f_m$, to $f^{\prime }\circ e_m\circ p_m=f_m\circ p_m$, a zatem $\underset{m}{\bigvee }{f}^{\prime }\circ e_m\circ p_m=\underset{m}{\bigvee }{f}_m\circ p_m$ czyli z ciągłości $f^{\prime }$: $f^{\prime }(\underset{m}{\bigvee }\circ e_m\circ p_m)=\underset{m}{\bigvee }{f}_m\circ p_m$. Ale $\underset{m}{\bigvee }\circ e_m\circ p_m=1_D$ oraz $\underset{m}{\bigvee }{f}_m\circ p_m=f$ co daje $f^{\prime }\circ 1_D=f$ czyli $f^{\prime }=f$. QED.

Kategoria ${\mathrm{D}\mathrm{c}\mathrm{p}\mathrm{o}}_{\mathrm{\perp }}^{EP}$

W tej kategorii obiektami są posety zupełne posiadające element najmniejszy, zaś morfizmami są pary e-p, o których była mowa na początku wykładu ???. Złożenie morfizmów

definiujemy w naturalny sposób jako morfizm

Czy $(e_2\circ e_1,p_1\circ p_2)$ jest parą e-p? Tak, ponieważ: $e_2\circ e_1\circ p_1\circ p_2⊑e_2\circ 1_E\circ p_2=e_2\circ p_2⊑1_F$ oraz $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$. A zatem złożenie par e-p jest dobrze zdefiniowane, a co za tym idzie, i co łatwo już teraz pokazać, $Dcp{o}_{\mathrm{\perp }}^{EP}$ jest kategorią.

Definicja. Nazwijmy $\omega$-kategorią każdą kategorię, w której diagram postaci

posiada granicę odwrotną.

Zauważmy, że twierdzenie o zgodności granicy prostej i odwrotnej (Twierdzenie ???) mówi, że $Dcp{o}_{\mathrm{\perp }}^{EP}$ jest $\omega$-kategorią!

Definicja. Funktor $F$ między $\omega$-kategoriami nazywamy ciągłym, jeśli zachowuje granice odwrotne, t.j. jeśli $D_{\mathrm{\infty }}$ jest granicą diagramu ???, to $F(D_{\mathrm{\infty }})$ jest granicą diagramu

Lemat. Niech $\mathbf{𝐀}$ będzie $\omega$-kategorią, $F:\mathbf{𝐀}\to \mathbf{𝐀}$ funktorem ciągłym, $f:A\to F(A)$ morfizmem w $\mathbf{𝐀}$ oraz niech diagram

posiada granicę odwrotną $D_{\mathrm{\infty }}$. Wówczas $D_{\mathrm{\infty }}\cong F(D_{\mathrm{\infty }})$.

Dowód: Skoro $D_{\mathrm{\infty }}$ jest granicą odwrotną diagramu ???, to

komutuje. W szczególności

komutuje i jak łatwo zauważyć $D_{\mathrm{\infty }}$ jest jego granicą. Ale z ciągłości $F$ mamy, że diagram

komutuje i $F(D_{\mathrm{\infty }})$ jest jego granicą. A zatem $D_{\mathrm{\infty }}\cong F(D_{\mathrm{\infty }})$ wynika z Lematu ???. QED.

Przykład. Przekątna $\mathrm{\Delta }:\mathbf{𝐃}\mathbf{𝐜}\mathbf{𝐩}\mathbf{𝐨}\to \mathbf{𝐃}\mathbf{𝐜}\mathbf{𝐩}\mathbf{𝐨}\times \mathbf{𝐃}\mathbf{𝐜}\mathbf{𝐩}\mathbf{𝐨}$, $a\mapsto (a,a)$; $f\mapsto (f,f)$ dla $a\in {\mathbf{𝐃}\mathbf{𝐜}\mathbf{𝐩}\mathbf{𝐨}}_0$ $f\in {\mathbf{𝐃}\mathbf{𝐜}\mathbf{𝐩}\mathbf{𝐨}}_1$ 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. Funktor $F:{𝒟}\to {ℰ}$ pomiędzy kategoriami posetów ${𝒟},{ℰ}$ jest \mathit{ lokalnie ciągły} jeśli przekształcenia $f\mapsto F(f)$ typu $\mathrm{H}\mathrm{o}\mathrm{m}(D,D^{\prime })\to \mathrm{H}\mathrm{o}\mathrm{m}(F(D),F(D^{\prime }))$ są ciągłe w sensie Scotta dla każdej pary obiektów $D,D^{\prime }\in {{𝒟}}_0$.

Dla przykładu przeczytajmy tę definicję dla bifunktora $F:{\mathbf{𝐃}\mathbf{𝐜}\mathbf{𝐩}\mathbf{𝐨}}^{op}\times \mathbf{𝐃}\mathbf{𝐜}\mathbf{𝐩}\mathbf{𝐨}\to \mathbf{𝐃}\mathbf{𝐜}\mathbf{𝐩}\mathbf{𝐨}$: funktor $F$ jest lokalnie ciągły, jeśli dla dowolnych zbiorów skierowanych $A\subseteq [D_2\to D_1]$ i $B\subseteq [D_3\to D_4]$, gdzie $D_1,...,D_4\in {\mathbf{𝐃}\mathbf{𝐜}\mathbf{𝐩}\mathbf{𝐨}}_0$ mamy $F(\bigvee A,\bigvee B)=\underset{f\in A,g\in G}{\bigvee }F(f,g)$. Zauważmy, że supremum po prawej stronie istnieje w $[F(D_1,D_3)\to F(D_2,D_4)]$.

Przykład. Eksponent $[\mathrm{\_}\to \mathrm{\_}]:{\mathbf{𝐃}\mathbf{𝐜}\mathbf{𝐩}\mathbf{𝐨}}^{op}\times \mathbf{𝐃}\mathbf{𝐜}\mathbf{𝐩}\mathbf{𝐨}\to \mathbf{𝐃}\mathbf{𝐜}\mathbf{𝐩}\mathbf{𝐨}$ jest lokalnie ciągły, ponieważ $[f\to g]=curry(g\circ ev\circ (1\times f))$ jest złożeniem funkcji ciągłych w sensie Scotta.

Lemat. Niech funktor $F:{\mathbf{𝐃}\mathbf{𝐜}\mathbf{𝐩}\mathbf{𝐨}}_{\mathrm{\perp }}^{op}\times {\mathbf{𝐃}\mathbf{𝐜}\mathbf{𝐩}\mathbf{𝐨}}_{\mathrm{\perp }}\to {\mathbf{𝐃}\mathbf{𝐜}\mathbf{𝐩}\mathbf{𝐨}}_{\mathrm{\perp }}$ będzie lokalnie ciągły. Wtedy istnieje ciągły funktor $\hat{F}:Dcp{o}_{\mathrm{\perp }}^{EP}\times Dcp{o}_{\mathrm{\perp }}^{EP}\to Dcp{o}_{\mathrm{\perp }}^{EP}$ którego działanie na obiekty jest takie samo, jak funktora $F$.

Dowód: Połóżmy $\hat{F}(a,b)=F(a,b)$, gdzie $a,b$ są posetami ciągłymi z elementami najmniejszymi. Rozważmy pary e-p:

Możemy wówczas stworzyć diagram

i para morfizmów powyżej jest parą e-p. Rzeczywiście: $F(e,s)\circ F(p,j)=F(p\circ e,s\circ j)=F(1_a,1_b)=1_{F(a,b))}$. Wykorzystaliśmy kolejno: kontrawariantność $F$ dla pierwszego argumentu, własności par e-p i definicję funktora. Ponadto, $F(p,j)\circ F(e,s)=F(e\circ p,j\circ s)⊑F(1_{a^{\prime }},1_{b^{\prime }})=1_{F(a^{\prime },b^{\prime })}$. Wykorzystaliśmy kolejno: definicję funktora, monotoniczność $F$, która wynika z lokalnej ciągłości i w końcu definicję $F$ jeszcze raz.

Zdefiniujmy zatem $\hat{F}((e,p),(j,s))=(F(p,j),F(e,s))$. Oczywiście,\ $\hat{F}$ jest funktorem. Aby pokazać ciągłość, załóżmy, że mamy w $Dcp{o}_{\mathrm{\perp }}^{EP}\times Dcp{o}_{\mathrm{\perp }}^{EP}$ diagram

$(A_1,B_1)\to (A_2,B_2)\to (A_3,B_3)\to ...$

który ma granicę odwrotną $(D,E)$. A to znaczy, że w $\mathbf{𝐃}\mathbf{𝐜}\mathbf{𝐩}\mathbf{𝐨}$ mamy dwa diagramy:

$A_1\to A_2\to A_3\to ..$.

i

$B_1\to B_2\to B_3\to ...$

których granicami są odpowienio $D$ i $E$ Z twierdzenia o koincydencji granicy prostej i odwrotnej (Twierdzenie ???) wiemy, że zachodzi $1_D=\underset{n}{\bigvee }{e}_n\circ p_n$ oraz $1_E=\underset{n}{\bigvee }{j}_n\circ s_n$, a więc $1_{(D,e)}=\bigvee (e_n\circ p_n,j_n\circ s_n)$. Aplikując lokalną ciągłość $F$ do ostatniej równości mamy

$1_{\hat{F}(D,E)}=\hat{F}(1_{(D,e)})=(F(1_D,1_E),F(1_D,1_E))=\bigvee (F(e_n\circ p_n,j_n\circ s_n),F(e_n\circ p_n,j_n\circ s_n))$.

Ale Twierdzenie ??? mówi, że ostatnia równość charakteryzuje granicę odwrotną diagramu w $Dcp{o}_{\mathrm{\perp }}^{EP}$:

$\hat{F}(A_1,B_1)\to \hat{F}(A_2,B_2)\to \hat{F}(A_3,B_3)\to ..$.

a zatem $\hat{F}(D,E)=F(D,E)$ jest tą szukaną granicą odwrotną, co należało pokazać. QED.

Twierdzenie Scotta

Zgodnie z poprzednim twierdzeniem możemy zdefiniować Eksponent $Exp:Dcp{o}_{\mathrm{\perp }}^{EP}\times Dcp{o}_{\mathrm{\perp }}^{EP}\to Dcp{o}_{\mathrm{\perp }}^{EP}$ jako $\widehat{[\mathrm{\_}\to \mathrm{\_}]}$, który jest ciągły (ponieważ eksponent $[\mathrm{\_}\to \mathrm{\_}]$ jest lokalnie ciągły). Rozważmy złożenie:

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

Mamy $F(P)=Exp\circ \mathrm{\Delta }(P)=Exp(P,P)=[\mathrm{\_}\to \mathrm{\_}](P,P)=[P\to P]$ Podobnie $F(Q)=[Q\to Q]$ Działanie na morfizmach:

$F(e,p)=Exp((e,p),(e,p))=([\mathrm{\_}\to \mathrm{\_}](p,e),[\mathrm{\_}\to \mathrm{\_}](e,p))=([p\to e],[e\to p])$.

A zatem otrzymujemy:

Wiemy już, że para funkcji powyżej tworzy parę e-p! Przypomnijmy jeszcze raz jak działają funkcje $[p\to e]$ i $[e\to p]$ na elementy z odpowiednio $[P\to P]$ i $[Q\to Q]$: przykładowo, dla $f\in [P\to P]$ mamy dla $q\in Q$

$[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)$

to znaczy $[p\to e](f)=e\circ f\circ p$ Podobnie $[e\to p](g)=p\circ g\circ e$ dla $g\in [Q\to Q]$.

Zauważmy w końcu, że dla dowolnego posetu zupełnego $P$, jeśli jako $e:P\to F(P)$ weźmiemy funkcję $y\mapsto \lambda x.y$, zaś jako $p:F(P)\to P$ weźmiemy funkcję $f\mapsto f(\mathrm{\perp })$, to para $(e,p)$ jest parą e-p typu $P\to F(P)$.

A zatem otrzymujemy końcowy wniosek:

Twierdzenie (Dana Scott). Niech $P$ będzie posetem zupełnym z elementem najmniejszym $\mathrm{\perp }$. Zdefiniujmy diagram w $\mathbf{𝐃}\mathbf{𝐜}\mathbf{𝐩}\mathbf{𝐨}$ jak następuje:

gdzie

1. $D_0=P$; $D_{n+1}=[D_n\to D_n]$

2. $e_0:P\to [P\to P]$ jest funkcją $\lambda y.\lambda x.y$; $p_0:[P\to P]\to P$ jest funkcją $\lambda f.f(\mathrm{\perp })$.

3.$e_{n+1}:[D_n\to D_n]=D_{n+1}\to [D_{n+1}\to D_{n+1}]$ jest funkcją $\lambda f.e_n\circ f\circ p_n$; $p_{n+1}:[D_{n+1}\to D_{n+1}]\to [D_n\to D_n]$ jest funkcją $\lambda g.p_n\circ g\circ e_n$.

Niech $D_{\mathrm{\infty }}$ będzie granicą diagramu

w $\mathbf{𝐃}\mathbf{𝐜}\mathbf{𝐩}\mathbf{𝐨}$. Wówczas $D_{\mathrm{\infty }}\cong [D_{\mathrm{\infty }}\to D_{\mathrm{\infty }}]$.