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

Aktualna wersja na dzień 22:18, 11 wrz 2023

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}, . . .) ∣ (\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

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

Definicja. Nazwijmy $ω$ -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 $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

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

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

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

komutuje. W szczególności

komutuje i jak łatwo zauważyć $D_{\infty}$ jest jego granicą. Ale z ciągłości $F$ mamy, że 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 \mathit{ 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:

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^{'}}, 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:

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) = 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:

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:

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

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

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

Aktualna wersja na dzień 22:18, 11 wrz 2023

Spis treści

Twierdzenie o istnieniu granic w Dcpo

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

@@ Linia 1: / Linia 1: @@
+== Twierdzenie o istnieniu granic w '''Dcpo''' ==
 Udowodnijmy teraz podstawowe twierdzenie na temat diagramów w kategorii '''Dcpo'''.
@@ Linia 5: / Linia 7: @@
 Dowód: Dowód przeprowadzimy dla szczególnego diagramu:
-[DIAGRAM]
+[[Grafika:Diag13.0.png]]
 (Dowód ogólny jest analogiczny lecz wymaga bardziej ''technicznego'' zapisu, wiec go pominiemy.) Pokażemy, że granica powyższego diagramu jest dana jako
-<math> D = \{(x_0, x_1, ... )\mid (\forall n\in \omega)(f_n(x_{n+1}) = x_n)\}.</math>
+<math>D = \{(x_0, x_1, ... )\mid (\forall n\in \omega)(f_n(x_{n+1}) = x_n)\}</math>.
-Zauważmy, że zbiór <math>D </math> jest posetem, w którym elementy są uporządkowane ''po współrzędnych'' (to znaczy, że porządek jest ''dziedziczony'' z produktu <math>\Pi_{n\in \omega} D_n</math>. Jeśli <math>G\subseteq D</math> jest zbiorem skierowanym, to dla każdego <math>n\in \omega </math>zbiór <math>\pi_n[G]= \{x_n\mid x\in G\}</math>jest skierowanym podzbiorem <math>D_n </math>. Niech <math>y_n = \bigvee \{x_n\mid x\in G\} </math>. Z ciągłości funkcji tworzących diagram mamy: <math>f_n(y_{n+1}) = \bigvee f_n(\{x_{n+1}\mid x\in G\})=  \bigvee \{x_{n}\mid x\in G\} = y_n</math>. To znaczy, że <math>(y_0, y_1, ...)\in D </math> i, jak łatwo zauważyć, element ten jest supremum skierowanym zbioru <math>G</math>. Pokazaliśmy więc, że <math>D\in</math> '''Dcpo'''.
+Zauważmy, że zbiór <math>D</math> jest posetem, w którym elementy są uporządkowane ''po współrzędnych'' (to znaczy, że porządek jest ''dziedziczony'' z produktu <math>\Pi_{n\in \omega} D_n</math>. Jeśli <math>G\subseteq D</math> jest zbiorem skierowanym, to dla każdego <math>n\in \omega</math>zbiór <math>\pi_n[G]= \{x_n\mid x\in G\}</math>jest skierowanym podzbiorem <math>D_n</math>. Niech <math>y_n = \bigvee \{x_n\mid x\in G\}</math>. Z ciągłości funkcji tworzących diagram mamy: <math>f_n(y_{n+1}) = \bigvee f_n(\{x_{n+1}\mid x\in G\})=  \bigvee \{x_{n}\mid x\in G\} = y_n</math>. To znaczy, że <math>(y_0, y_1, ...)\in D</math> i, jak łatwo zauważyć, element ten jest supremum skierowanym zbioru <math>G</math>. Pokazaliśmy więc, że <math>D\in</math> '''Dcpo'''.
 Udowodnimy teraz, że <math>D</math> wraz z projekcjami <math>\{\pi_n\colon D\to D_n\mid n\in \omega\}</math> jest granicą. Po pierwsze, dla <math>G\subseteq D</math> mamy
-<math>\pi_n(\bigvee G) = y_n = \bigvee \{x_{n}\mid x\in G\} = \bigvee \pi_n[G],</math>
+<math>\pi_n(\bigvee G) = y_n = \bigvee \{x_{n}\mid x\in G\} = \bigvee \pi_n[G]</math>
-a więc projekcje są ciągłe. Po drugie, jeśli <math>\{g_k\colon E\to D_k\mid k\in \omega\}</math> jest dowolną inną granicą, to zdefiniujmy <math>h\colon E\to D </math> jako <math>h(x) = (g_0(x), g_1(x), ...)</math>. Z definicji powyższej wynika, że dla każdego <math>k\in \omega</math> mamy $\pi_k \circ h = g_k</math>.  Zauważmy, że to świadczy o jednoznaczności
+a więc projekcje są ciągłe. Po drugie, jeśli <math>\{g_k\colon E\to D_k\mid k\in \omega\}</math> jest dowolną inną granicą, to zdefiniujmy <math>h\colon E\to D</math> jako <math>h(x) = (g_0(x), g_1(x), ...)</math>. Z definicji powyższej wynika, że dla każdego <math>k\in \omega</math> mamy $\pi_k \circ h = g_k</math>.  Zauważmy, że to świadczy o jednoznaczności
-wyboru <math>h</math>.  A zatem <math>D</math> jest granicą omawianego diagramu. Co więcej, z jednoznaczności granicy wnioskujemy, że <math>D\cong E </math>. QED
+wyboru <math>h</math>.  A zatem <math>D</math> jest granicą omawianego diagramu. Co więcej, z jednoznaczności granicy wnioskujemy, że <math>D\cong E</math>. 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.
@@ Linia 31: / Linia 33: @@
 '''Twierdzenie'''. Rozważmy diagram <math>F</math>  w kategorii '''Dcpo''' 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> i  <math>p_{nm}\colon D_m\to D_n</math>  tworzące parę e-p;
@@ Linia 40: / Linia 42: @@
 Zdefiniujmy:
-<math>D = \{ (x_0, x_1, ...)\mid (\forall n\leq m)(x_n=p_{nm}(x_m)) \},</math>
+<math>D = \{ (x_0, x_1, ...)\mid (\forall n\leq m)(x_n=p_{nm}(x_m)) \}</math>
 <math>p_m\colon D\to D_m,\ \ (x_0, x_1, ...)\mapsto x_m, \ m\in \omega</math>
-<math>e_m\colon D_m\to D, \ x\mapsto (\bigvee_{k\geq n,m} p_{nk}\circ e_{km}(x)\mid n\in \omega).</math>
+<math>e_m\colon D_m\to D, \ x\mapsto (\bigvee_{k\geq n,m} p_{nk}\circ e_{km}(x)\mid n\in \omega)</math>.
 Wtedy:
@@ Linia 53: / Linia 55: @@
 .<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_n f_n(x_n)</math>  lub <math>f = \bigvee_n f_n\circ p_n</math>.
+Dowód: W Twierdzeniu ??? 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. 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:
+<math>p_{nn'}(y_{n'})   =  p_{nn'}(\bigvee_{k\geq n',m} p_{n'k}\circ e_{km}(x)) =  \bigvee_{k\geq n',m} p_{nn'}\circ p_{n'k}\circ e_{km}(x) = \bigvee_{k\geq n',m} p_{nk}\circ e_{km}(x)=  y_n</math>.
+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.
+Przejdźmy do dowodu (5). Niech <math>m\in \omega</math>. Mamy:
+<math>e_m\circ p_m (x_n\mid n\in \omega) = e_m(x_m) = (\bigvee_{k\geq n,m} p_{nk}\circ e_{km}(x_m)\mid n\in\omega)  = (\bigvee_{k\geq n,m} p_{nk}\circ e_{km} \circ p_{mk} (x_k)\mid n\in\omega) \subseteq (\bigvee_{k\geq n,m} p_{nk} (x_k)\mid n\in\omega) = (\bigvee_{k\geq n} p_{nk} (x_k)\mid n\in\omega) = (x_n\mid n\in\omega)</math>.
+Ponadto, <math>p_m\circ e_m (x) = p_m (\bigvee_{k\geq n,m} p_{nk}\circ e_{km}(x)\mid n\in\omega ) =  \bigvee_{k\geq m} p_{mk}\circ e_{km}(x) = x</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>:
+<math>p_n(e_m\circ p_m (x_n\mid n\in \omega)) = ... = p_n(\bigvee_{k\geq n,m} p_{nk}\circ e_{km} \circ p_{mk} (x_k)\mid n\in\omega)  = p_n(\bigvee_{k\geq n,m} p_{nm}\circ p_{mk} \circ e_{km} \circ p_{mk} (x_k)\mid n\in\omega)  = p_n(\bigvee_{k\geq n,m} p_{nm}\circ  p_{mk} (x_k)\mid n\in\omega)  = p_n(\bigvee_{k\geq n} p_{nk} (x_k)\mid n\in\omega) = p_n(\bigvee_{k\geq n} x_n\mid n\in\omega) = p_n(x_n\mid n\in\omega) = x_n</math>.
+To dowodzi, że <math>\bigvee_n e_n\circ p_n = 1_{D}</math>, czyli (5).
+Korzystając z powyższego mamy też natychmiast:
+<math>h = 1_D\circ h = \bigvee_n E_n\circ p_n\circ h = \bigvee e_m \circ g_n</math>
+co kończy dowód (6).
+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_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>:
+<math>f_n \circ p_n = f_m \circ e_{mn}\circ p_{nm}\circ p_m\sqsubseteq f_m\circ p_m</math>.
+Co więcej,
+<math>f\circ e_m = \bigvee_{n\leq m} f_n\circ p_n\circ e_m = \bigvee_{n\leq m} f_n\circ p_n\circ e_n\circ e_{nm} = \bigvee_{n\leq m} f_n\circ e_{nm} = \bigvee_{n\leq m} f_m  = f_m.</math>
+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 <math>\bigvee_m f'\circ e_m \circ p_m = \bigvee_m f_m\circ p_m</math> czyli z ciągłości <math>f'</math>: <math>f'(\bigvee_m \circ e_m \circ p_m) = \bigvee_m f_m\circ p_m</math>. Ale <math>\bigvee_m \circ e_m \circ p_m = 1_D</math>  oraz <math>\bigvee_m f_m\circ p_m = f</math>   co daje <math>f'\circ 1_D = f</math>   czyli <math>f'=f</math>. QED.
+== Kategoria <math>\mathrm{Dcpo}^{EP}_{\bot}</math> ==
+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
+[[Grafika:Diag13.1.png]]
+definiujemy w naturalny sposób jako morfizm
+[[Grafika:Diag13.2.png]]
+Czy <math>(e_2\circ e_1, p_1\circ p_2)</math>  jest parą e-p? Tak, ponieważ: <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> oraz <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>. A zatem złożenie par e-p jest dobrze zdefiniowane, a co za tym idzie, i co łatwo już teraz pokazać, <math>Dcpo^{EP}_{\bot}</math>  jest kategorią.
+'''Definicja'''. Nazwijmy '''<math>\omega</math>-kategorią''' każdą kategorię, w której diagram postaci
+[[Grafika:Diag13.3.png]]
+posiada granicę odwrotną.
+Zauważmy, że twierdzenie o zgodności granicy prostej i odwrotnej (Twierdzenie ???) mówi, że <math>Dcpo^{EP}_{\bot}</math>  jest <math>\omega</math>-kategorią!
+'''Definicja'''. Funktor <math>F</math>  między <math>\omega</math>-kategoriami nazywamy '''ciągłym''', jeśli zachowuje granice odwrotne, t.j. jeśli <math>D_{\infty}</math>  jest granicą diagramu ???, to <math>F(D_{\infty})</math> jest granicą diagramu
+[[Grafika:Diag13.4.png]]
+'''Lemat'''. 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
+[[Grafika:Diag13.5.png]]
+posiada granicę odwrotną <math>D_{\infty}</math>. Wówczas <math>D_{\infty}\cong F(D_{\infty})</math>.
+Dowód: Skoro <math>D_{\infty}</math>  jest granicą odwrotną diagramu
+???, to
+[[Grafika:Diag13.6.png]]
+komutuje. W szczególności
+[[Grafika:Diag13.7.png]]
+komutuje i jak łatwo zauważyć <math>D_{\infty}</math>  jest jego granicą. Ale
+z ciągłości <math>F</math> mamy, że diagram
+[[Grafika:Diag13.8.png]]
+komutuje i <math>F(D_{\infty})</math> jest jego granicą. A zatem <math>D_{\infty}
+\cong F(D_{\infty})</math> wynika z Lematu ???. QED.
+'''Przykład'''. 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.
+== 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 <math>F\colon \mathcal{D}\to \mathcal{E}</math> pomiędzy kategoriami posetów <math>\mathcal{D}, \mathcal{E}</math>  jest \mathit{ 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 \mathcal{D}_0</math>.
+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 [D_2\to D_1]</math> i <math>B\subseteq [D_3\to D_4]</math>, gdzie <math>D_1, ..., D_4\in \mathbf{Dcpo}_0</math> mamy <math>F(\bigvee A, \bigvee B) = \bigvee_{f\in A, g\in G} F(f,g)</math>. Zauważmy, że supremum po prawej stronie istnieje w <math>[F(D_1,D_3)\to F(D_2, D_4)]</math>.
+'''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
+\mathbf{Dcpo}_{\bot}</math>  będzie lokalnie ciągły. Wtedy istnieje ciągły funktor <math>\widehat{F}\colon Dcpo^{EP}_{\bot}\times Dcpo^{EP}_{\bot}\to Dcpo^{EP}_{\bot}</math>
+którego działanie na obiekty jest takie samo, jak funktora <math>F</math>.
+Dowód: Połóżmy <math>\widehat{F}(a,b) = F(a,b)</math>, gdzie <math>a,b</math> są posetami ciągłymi z elementami najmniejszymi. Rozważmy pary e-p:
+[[Grafika:Diag13.9.png]]
+Możemy wówczas stworzyć diagram
+[[Grafika:Diag13.10.png]]
+i para morfizmów powyżej jest parą e-p. Rzeczywiście: <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>. Wykorzystaliśmy kolejno: kontrawariantność <math>F</math> dla pierwszego argumentu, własności par e-p i definicję funktora. Ponadto,
+<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:
+[[Grafika:Diag13.11.png]]
+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ę:
+[[Grafika:Diag13.12.png]]
+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:
+[[Grafika:Diag13.13.png]]
+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:
+[[Grafika:Diag13.14.png]]
+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
+[[Grafika:Diag13.15a.png]]
+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

Aktualna wersja na dzień 22:18, 11 wrz 2023

Twierdzenie o istnieniu granic w Dcpo

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}$