TKI Moduł 13: Różnice pomiędzy wersjami

Wersja z 18:01, 20 cze 2006

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:

[DIAGRAM]

(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}, . . .) ∣ (\forall n \in ω) (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 $Π_{n \in ω} D_{n}$ . Jeśli $G \subseteq D$ jest zbiorem skierowanym, to dla każdego $n \in ω$ zbiór $π_{n} [G] = {x_{n} ∣ x \in G}$ jest skierowanym podzbiorem $D_{n}$ . Niech $y_{n} = ⋁ {x_{n} ∣ x \in G}$ . Z ciągłości funkcji tworzących diagram mamy: $f_{n} (y_{n + 1}) = ⋁ f_{n} ({x_{n + 1} ∣ x \in G}) = ⋁ {x_{n} ∣ 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 ${π_{n} : D \to D_{n} ∣ n \in ω}$ jest granicą. Po pierwsze, dla $G \subseteq D$ mamy

$π_{n} (⋁ G) = y_{n} = ⋁ {x_{n} ∣ x \in G} = ⋁ π_{n} [G],$

a więc projekcje są ciągłe. Po drugie, jeśli ${g_{k} : E \to D_{k} ∣ k \in ω}$ 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 ω$ 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 ≅ 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 ≅ [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 \leq m$ istnieją funkcje $e_{m n} : D_{n} \to D_{m}$ i $p_{n m} : D_{m} \to D_{n}$ tworzące parę e-p; 3. Dla każdego $n \in ω$ mamy $e_{n n} = 1_{D_{n}}$ ;

4. Dla $n \leq m \leq k$ mamy $e_{k n} = e_{k m} \circ e_{m n}$ oraz $p_{n k} = p_{n m} \circ p_{m k}$ .

Zdefiniujmy:

$D = {(x_{0}, x_{1}, . . .) ∣ (\forall n \leq m) (x_{n} = p_{n m} (x_{m}))},$

$p_{m} : D \to D_{m}, (x_{0}, x_{1}, . . .) \mapsto x_{m}, m \in ω$

$e_{m} : D_{m} \to D, x \mapsto (\underset{k \geq n, m}{⋁} p_{n k} \circ e_{k m} (x) ∣ n \in ω) .$

Wtedy:

5. Para $(e_{m}, p_{m})$ jest parą e-p i zachodzi $\underset{n \in ω}{⋁} 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) ∣ n \in ω)$ lub $h = \underset{n}{⋁} 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} ∣ n \in ω) = \underset{n}{⋁} f_{n} (x_{n})$ lub $f = \underset{n}{⋁} 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 ω$ . Niech $m$ będzie dowolne i załóżmy, że $n \leq n^{'}$ . Mamy:

$p_{n n^{'}} (y_{n^{'}}) = p_{n n^{'}} (\underset{k \geq n^{'}, m}{⋁} p_{n^{'} k} \circ e_{k m} (x)) = \underset{k \geq n^{'}, m}{⋁} p_{n n^{'}} \circ p_{n^{'} k} \circ e_{k m} (x) = \underset{k \geq n^{'}, m}{⋁} p_{n k} \circ e_{k m} (x) = y_{n} .$

W dowodzie korzystaliśmy kolejno z: definicji $y_{n^{'}}$ , ciągłości $p_{n n^{'}}$ 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 ω$ . Mamy:

$e_{m} \circ p_{m} (x_{n} ∣ n \in ω) = e_{m} (x_{m}) = (\underset{k \geq n, m}{⋁} p_{n k} \circ e_{k m} (x_{m}) ∣ n \in ω) = (\underset{k \geq n, m}{⋁} p_{n k} \circ e_{k m} \circ p_{m k} (x_{k}) ∣ n \in ω) \subseteq (\underset{k \geq n, m}{⋁} p_{n k} (x_{k}) ∣ n \in ω) = (\underset{k \geq n}{⋁} p_{n k} (x_{k}) ∣ n \in ω) = (x_{n} ∣ n \in ω) .$

Ponadto, $p_{m} \circ e_{m} (x) = p_{m} (\underset{k \geq n, m}{⋁} p_{n k} \circ e_{k m} (x) ∣ n \in ω) = \underset{k \geq m}{⋁} p_{m k} \circ e_{k m} (x) = x$ .

Bliższa analiza pokazuje, że $e_{m} \circ p_{m}$ pozostawi niezmienione te elementy ciągu $(x_{n} ∣ n \in ω)$ gdzie $n \leq m$ :

$p_{n} (e_{m} \circ p_{m} (x_{n} ∣ n \in ω)) = . . . = p_{n} (\underset{k \geq n, m}{⋁} p_{n k} \circ e_{k m} \circ p_{m k} (x_{k}) ∣ n \in ω) = p_{n} (\underset{k \geq n, m}{⋁} p_{n m} \circ p_{m k} \circ e_{k m} \circ p_{m k} (x_{k}) ∣ n \in ω) = p_{n} (\underset{k \geq n, m}{⋁} p_{n m} \circ p_{m k} (x_{k}) ∣ n \in ω) = p_{n} (\underset{k \geq n}{⋁} p_{n k} (x_{k}) ∣ n \in ω) = p_{n} (\underset{k \geq n}{⋁} x_{n} ∣ n \in ω) = p_{n} (x_{n} ∣ n \in ω) = x_{n} .$

To dowodzi, że $\underset{n}{⋁} e_{n} \circ p_{n} = 1_{D}$ , czyli (5).

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

$h = 1_{D} \circ h = \underset{n}{⋁} E_{n} \circ p_{n} \circ h = ⋁ 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}{⋁} f_{n} \circ p_{n}$ jest dobrze zdefiniowana, tj. czy supremum jest nad zbiorem skierowanym. Ale tak jest, ponieważ dla $n \leq m$ :

$f_{n} \circ p_{n} = f_{m} \circ e_{m n} \circ p_{n m} \circ p_{m} ⊑ f_{m} \circ p_{m} .$

Co więcej,

$f \circ e_{m} = \underset{n \leq m}{⋁} f_{n} \circ p_{n} \circ e_{m} = \underset{n \leq m}{⋁} f_{n} \circ p_{n} \circ e_{n} \circ e_{n m} = \underset{n \leq m}{⋁} f_{n} \circ e_{n m} = \underset{n \leq m}{⋁} f_{m} = f_{m} .$

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

Kategoria ${D c p o}_{⊥}^{E P}$

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

[DIAGRAM]

definiujemy w naturalny sposób jako morfizm

[DIAGRAM]

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ć, $D c p o_{⊥}^{E P}$ jest kategorią.

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

[DIAGRAM]

posiada granicę odwrotną.

Zauważmy, że twierdzenie o zgodności granicy prostej i odwrotnej (Twierdzenie ???) mówi, że $D c p o_{⊥}^{E P}$ jest $ω$ -kategorią!

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

[DIAGRAM]

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

[DIAGRAM]

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

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

[DIAGRAM]

komutuje. W szczególności

[DIAGRAM]

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

[DIAGRAM]

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

Przykład. Przekątna $Δ : 𝐃 𝐜 𝐩 𝐨 \to 𝐃 𝐜 𝐩 𝐨 \times 𝐃 𝐜 𝐩 𝐨$ , $a \mapsto (a, a)$ ; $f \mapsto (f, f)$ dla $a \in {𝐃 𝐜 𝐩 𝐨}_{0}$ $f \in {𝐃 𝐜 𝐩 𝐨}_{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 {\em lokalnie ciągły} jeśli przekształcenia $f \mapsto F (f)$ typu $H o m (D, D^{'}) \to H o m (F (D), F (D^{'}))$ są ciągłe w sensie Scotta dla każdej pary obiektów $D, D^{'} \in 𝒟_{0}$ .

Dla przykładu przeczytajmy tę definicję dla bifunktora $F : {𝐃 𝐜 𝐩 𝐨}^{o p} \times 𝐃 𝐜 𝐩 𝐨 \to 𝐃 𝐜 𝐩 𝐨$ : 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 {𝐃 𝐜 𝐩 𝐨}_{0}$ mamy $F (⋁ A, ⋁ B) = \underset{f \in A, g \in G}{⋁} 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 $[_\to_] : {𝐃 𝐜 𝐩 𝐨}^{o p} \times 𝐃 𝐜 𝐩 𝐨 \to 𝐃 𝐜 𝐩 𝐨$ jest lokalnie ciągły, ponieważ $[f \to g] = c u r r y (g \circ e v \circ (1 \times f))$ jest złożeniem funkcji ciągłych w sensie Scotta.

Lemat. Niech funktor $F : {𝐃 𝐜 𝐩 𝐨}_{⊥}^{o p} \times {𝐃 𝐜 𝐩 𝐨}_{⊥} \to {𝐃 𝐜 𝐩 𝐨}_{⊥}$ będzie lokalnie ciągły. Wtedy istnieje ciągły funktor $\hat{F} : D c p o_{⊥}^{E P} \times D c p o_{⊥}^{E P} \to D c p o_{⊥}^{E P}$ 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:

[DIAGRAM]

Możemy wówczas stworzyć diagram

[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^{'}}, 1_{b^{'}}) = 1_{F (a^{'}, b^{'})} .$ 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 $D c p o_{⊥}^{E P} \times D c p o_{⊥}^{E P}$ 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 $𝐃 𝐜 𝐩 𝐨$ 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}{⋁} e_{n} \circ p_{n}$ oraz $1_{E} = \underset{n}{⋁} j_{n} \circ s_{n}$ , a więc $1_{(D, e)} = ⋁ (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})) = ⋁ (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 $D c p o_{⊥}^{E P}$ :

$\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 $E x p : D c p o_{⊥}^{E P} \times D c p o_{⊥}^{E P} \to D c p o_{⊥}^{E P}$ jako $\hat{[_\to_]}$ , który jest ciągły (ponieważ eksponent $[_\to_]$ jest lokalnie ciągły). Rozważmy złożenie:

[DIAGRAM]

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ę:

[DIAGRAM]

Mamy $F (P) = E x p \circ Δ (P) = E x p (P, P) = [_\to_] (P, P) = [P \to P]$ Podobnie $F (Q) = [Q \to Q]$ Działanie na morfizmach:

$F (e, p) = E x p ((e, p), (e, p)) = ([_\to_] (p, e), [_\to_] (e, p)) = ([p \to e], [e \to p]) .$

A zatem otrzymujemy:

[DIAGRAM]

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) = c u r r y (e \circ e v \circ (1 \times p)) (f) (q) = (e \circ e v \circ (1 \times p)) (f, q) = e (e v ((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 λ x . y$ , zaś jako $p : F (P) \to P$ weźmiemy funkcję $f \mapsto f (⊥)$ , 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 $⊥$ . Zdefiniujmy diagram w $𝐃 𝐜 𝐩 𝐨$ jak następuje:

[DIAGRAM]

gdzie

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

2. $e_{0} : P \to [P \to P]$ jest funkcją $λ y . λ x . y$ ; $p_{0} : [P \to P] \to P$ jest funkcją $λ f . f (⊥)$ .

3. $e_{n + 1} : [D_{n} \to D_{n}] = D_{n + 1} \to [D_{n + 1} \to D_{n + 1}]$ jest funkcją $λ 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ą $λ g . p_{n} \circ g \circ e_{n}$ .

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

[DIAGRAM]

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

@@ Linia 155: / Linia 155: @@
 '''Przykład'''. Eksponent <math>[\_\to \_]\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'''. Niech funktor <math>F\colon \mathbf{Dcpo}^{op}_{\bot}\times \mathbf{Dcpo}_{\bot}\to
@@ Linia 172: / Linia 171: @@
 <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>
 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.
+Zdefiniujmy zatem <math>\widehat{F}((e,p),(j,s)) = (F(p,j),F(e,s))</math>. Oczywiście,\ <math>\widehat{F}</math>  jest funktorem. Aby pokazać ciągłość, załóżmy, że mamy w <math>Dcpo^{EP}_{\bot}\times Dcpo^{EP}_{\bot}</math>  diagram
+<math>(A_1,B_1)\to  (A_2,B_2)\to (A_3,B_3)\to...,</math>
+który ma granicę odwrotną <math>(D,E)</math>. A to znaczy, że w <math>\mathbf{Dcpo}</math> mamy
+dwa diagramy:
+<math>A_1\to A_2\to A_3\to...</math>
+i
+<math>B_1\to B_2\to B_3\to...,</math>
+których granicami są odpowienio <math>D</math> i <math>E</math>   Z twierdzenia o koincydencji granicy prostej i odwrotnej (Twierdzenie ???) wiemy, że zachodzi <math>1_D = \bigvee_n e_n\circ p_n</math>  oraz <math>1_E = \bigvee_n j_n\circ s_n</math>, a więc <math>1_{(D,e)} = \bigvee (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
+<math>1_{\widehat{F}(D,E)} = \widehat{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)).</math>
+Ale Twierdzenie ??? mówi, że ostatnia równość charakteryzuje granicę odwrotną diagramu w <math>Dcpo^{EP}_{\bot}</math>:
+<math>\widehat{F}(A_1,B_1)\to \widehat{F}(A_2,B_2)\to \widehat{F}(A_3,B_3)\to ...</math>
+a zatem <math>\widehat{F}(D,E)=F(D,E)</math> jest tą szukaną granicą odwrotną, co należało pokazać. QED.
+== Twierdzenie Scotta ==
+Zgodnie z poprzednim twierdzeniem możemy zdefiniować Eksponent <math>Exp\colon Dcpo^{EP}_{\bot}\times Dcpo^{EP}_{\bot} \to Dcpo^{EP}_{\bot}</math>  jako <math>\widehat{[\_\to\_ ]}</math>, który jest ciągły (ponieważ eksponent <math>[\_\to\_ ]</math>  jest lokalnie ciągły). Rozważmy złożenie:
+[DIAGRAM]
+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ę:
+[DIAGRAM]
+Mamy <math>F(P) = Exp\circ \Delta(P) = Exp(P,P) = [\_\to\_ ](P,P) = [P\to P]</math>   Podobnie <math>F(Q) = [Q\to Q]</math>   Działanie na morfizmach:
+<math>F(e,p) = Exp((e,p),(e,p))  = ([\_\to\_ ](p,e), [\_\to\_ ](e,p)) = ([p\to e], [e\to p]).</math>
+A zatem otrzymujemy:
+[DIAGRAM]
+Wiemy już, że para funkcji powyżej tworzy parę e-p! Przypomnijmy jeszcze raz jak działają funkcje <math>[p\to e]</math>  i <math>[e\to p]</math> na elementy z odpowiednio <math>[P\to P]</math>  i <math>[Q\to Q]</math>: przykładowo, dla <math>f\in [P\to P]</math>  mamy dla <math>q\in Q</math>
+<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>
+to znaczy <math>[p\to e](f) = e\circ f\circ p</math>   Podobnie <math>[e\to p](g) = p\circ g\circ e</math>  dla <math>g\in [Q\to Q]</math>.
+Zauważmy w końcu, że dla dowolnego posetu zupełnego <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:
+'''Twierdzenie (Dana Scott)'''. Niech <math>P</math> będzie posetem zupełnym z elementem najmniejszym <math>\bot</math>. Zdefiniujmy diagram w <math>\mathbf{Dcpo}</math>  jak następuje:
+[DIAGRAM]
+gdzie
+. <math>D_0 = P</math>; <math>D_{n+1} = [D_n \to D_n]</math>
+. <math>e_0\colon P\to [P\to P]</math>  jest funkcją <math>\lambda y .\lambda x.y</math>;    <math>p_0\colon [P\to P]\to P</math>  jest funkcją <math>\lambda f
+.f(\bot)</math>.
+.<math>e_{n+1}\colon [D_n\to D_n] = D_{n+1} \to [D_{n+1}\to 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}\to D_{n+1}]\to [D_n\to 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
+[DIAGRAM]
+w <math>\mathbf{Dcpo}</math>. Wówczas <math>D_{\infty}\cong [D_{\infty}\to D_{\infty}]</math>.

TKI Moduł 13: Różnice pomiędzy wersjami

Wersja z 18:01, 20 cze 2006

Spis treści

Twierdzenie o zgodności granicy prostej i odwrotnej

Kategoria ${D c p o}_{⊥}^{E P}$

Lokalna ciągłość funktorów

Twierdzenie Scotta

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia

TKI Moduł 13: Różnice pomiędzy wersjami

Wersja z 18:01, 20 cze 2006

Twierdzenie o zgodności granicy prostej i odwrotnej

Kategoria Dcpo⊥EP

Lokalna ciągłość funktorów

Twierdzenie Scotta

Menu nawigacyjne

Szukaj

Kategoria ${D c p o}_{⊥}^{E P}$