Teoria kategorii dla informatyków/Wykład 14: Teoria dziedzin III

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).

Przykładem takiego równania jest $D ≅ [D, D]$ . 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

F

w kategorii

𝐃 𝐜 𝐩 𝐨

taki, że:

Wierzchołkami $F$ są posety $D_{0}, D_{1}, D_{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.
Dla każdego $n \in ω$ mamy $e_{n n} = 1_{D_{n}}$ .
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 (⋁_{k \geq n, m}^{↓} p_{n k} \circ e_{k m} (x) ∣ n \in ω)

Wtedy:

Para $(e_{m}, p_{m})$ jest parą e-p i zachodzi $⋁_{n \in ω}^{↓} e_{n} \circ p_{n} = 1_{D}$ .
${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 = ⋁_{n}^{↓} e_{n} \circ g_{n}$ .
${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 ω) = ⋁_{n}^{↓} f_{n} (x_{n})$ lub $f = ⋁_{n}^{↓} f_{n} \circ p_{n}$ .

Dowód

W dowodzie Twierdzenia 14.1 podanym w Zadaniu 14.1

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:

\begin{aligned} p_{n n^{'}} (y_{n^{'}}) & = & p_{n n^{'}} (⋁_{k \geq n^{'}, m}^{↓} p_{n^{'} k} \circ e_{k m} (x)) \\ = & ⋁_{k \geq n^{'}, m}^{↓} p_{n n^{'}} \circ p_{n^{'} k} \circ e_{k m} (x) \\ = & ⋁_{k \geq n^{'}, m}^{↓} p_{n k} \circ e_{k m} (x) = y_{n} . \end{aligned}

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:

\begin{aligned} e_{m} \circ p_{m} (x_{n} ∣ n \in ω) & = & e_{m} (x_{m}) = (⋁_{k \geq n, m}^{↓} p_{n k} \circ e_{k m} (x_{m}) ∣ n \in ω) \\ = & (⋁_{k \geq n, m}^{↓} p_{n k} \circ e_{k m} \circ p_{m k} (x_{k}) ∣ n \in ω) ⊑ (⋁_{k \geq n, m}^{↓} p_{n k} (x_{k}) ∣ n \in ω) \\ = & (⋁_{k \geq n}^{↓} p_{n k} (x_{k}) ∣ n \in ω) = (x_{n} ∣ n \in ω) . \end{aligned}

Ponadto:

\begin{aligned} p_{m} \circ e_{m} (x) & = & p_{m} (⋁_{k \geq n, m}^{↓} p_{n k} \circ e_{k m} (x) ∣ n \in ω) \\ = & ⋁_{k \geq m}^{↓} p_{m k} \circ e_{k m} (x) \\ = & x . \end{aligned}

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

\begin{aligned} p_{n} (e_{m} \circ p_{m} (x_{n} ∣ n \in ω)) & = & . . . \\ = & p_{n} (⋁_{k \geq n, m}^{↓} p_{n k} \circ e_{k m} \circ p_{m k} (x_{k}) ∣ n \in ω) \\ = & p_{n} (⋁_{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} (⋁_{k \geq n, m}^{↓} p_{n m} \circ p_{m k} (x_{k}) ∣ n \in ω) \\ = & p_{n} (⋁_{k \geq n}^{↓} p_{n k} (x_{k}) ∣ n \in ω) \\ = & p_{n} (⋁_{k \geq n}^{↓} x_{n} ∣ n \in ω) \\ = & p_{n} (x_{n} ∣ n \in ω) \\ = & x_{n} . \end{aligned}

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

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

h = 1_{D} \circ h = ⋁_{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 = ⋁_{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} = ⋁_{n \leq m}^{↓} f_{n} \circ p_{n} \circ e_{m} = ⋁_{n \leq m}^{↓} f_{n} \circ p_{n} \circ e_{n} \circ e_{n m} = ⋁_{n \leq m}^{↓} f_{n} \circ e_{n m} = ⋁_{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:

⋁_{m}^{↓} f^{'} \circ e_{m} \circ p_{m} = ⋁_{m}^{↓} f_{m} \circ p_{m}

czyli z ciągłości $f^{'}$ :

f^{'} (⋁_{m}^{↓} \circ e_{m} \circ p_{m}) = ⋁_{m}^{↓} f_{m} \circ p_{m}

Ale

⋁_{m}^{↓} \circ e_{m} \circ p_{m} = 1_{D}

oraz

⋁_{m}^{↓} f_{m} \circ p_{m} = f

, co daje

f^{'} \circ 1_{D} = f

, czyli

f^{'} = f

.

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

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ć, ${𝐃 𝐜 𝐩 𝐨}_{⊥}^{E P}$ jest kategorią.

Definicja 14.3 [Omega-kategoria]

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 14.2 - mówi, że

{𝔻 𝕔 𝕡 𝕠}_{⊥}^{E P}

jest

ω

-kategorią!

Definicja 14.4 [Funktor ciągły]

Funktor

F

między

ω

-kategoriami nazywamy ciągłym, jeśli zachowuje granice odwrotne, tj.: jeśli

D_{\infty}

jest kogranicą powyższego diagramu, to

F (D_{\infty})

jest kogranicą diagramu:

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

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

.

Zauważmy, że 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 14.6

Funktor

F : 𝐃 \to 𝐄

pomiędzy kategoriami posetów

𝐃, 𝐄

jest 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}, D_{1}]$ i $B \subseteq^{↑} [D_{3}, D_{4}]$ , gdzie $D_{1}, . . ., D_{4} \in {𝐃 𝐜 𝐩 𝐨}_{0}$ , mamy:

F (⋁^{↓} A, ⋁^{↓} B) = ⋁_{f \in A, g \in G}^{↓} F (f, g)

Zauważmy, że supremum po prawej stronie istnieje w $[F (D_{1}, D_{3}), F (D_{2}, D_{4})]$ .

Dla przykładu, eksponent $[-, -] : {𝐃 𝐜 𝐩 𝐨}^{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 14.7 [istnienie funktorów ciągłych]

Niech funktor

F : {𝐃 𝐜 𝐩 𝐨}_{⊥}^{o p} \times {𝐃 𝐜 𝐩 𝐨}_{⊥} \to {𝐃 𝐜 𝐩 𝐨}_{⊥}

będzie lokalnie ciągły. Wtedy istnieje ciągły funktor

\hat{F} : {𝐃 𝐜 𝐩 𝐨}_{⊥}^{E P} \times {𝐃 𝐜 𝐩 𝐨}_{⊥}^{E P} \to {𝐃 𝐜 𝐩 𝐨}_{⊥}^{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ą dcpo 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 ${𝐃 𝐜 𝐩 𝐨}_{⊥}^{E P} \times {𝐃 𝐜 𝐩 𝐨}_{⊥}^{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ą odpowiednio $D$ i $E$ . Z twierdzenia o koincydencji granicy prostej i odwrotnej (Twierdzenie 14.2) wiemy, że zachodzi $1_{D} = ⋁_{n}^{↓} e_{n} \circ p_{n}$ oraz $1_{E} = ⋁_{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 14.2 mówi, że ostatnia równość charakteryzuje granicę odwrotną diagramu w ${𝐃 𝐜 𝐩 𝐨}_{⊥}^{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ć.

Twierdzenie Scotta

Zgodnie z poprzednim twierdzeniem możemy zdefiniować Eksponent $E x p : {𝐃 𝐜 𝐩 𝐨}_{⊥}^{E P} \times {𝐃 𝐜 𝐩 𝐨}_{⊥}^{E P} \to {𝐃 𝐜 𝐩 𝐨}_{⊥}^{E P}$ jako $\hat{[-, -]}$ , który jest ciągły (ponieważ eksponent $[-, -]$ jest lokalnie ciągły). Rozważmy złożenie ${𝐃 𝐜 𝐩 𝐨}_{⊥}^{E P} \overset{Δ}{\to} {𝐃 𝐜 𝐩 𝐨}_{⊥}^{E P} \times {𝐃 𝐜 𝐩 𝐨}_{⊥}^{E P} \overset{E x p}{\to} {𝐃 𝐜 𝐩 𝐨}_{⊥}^{E P}$ 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) = [-, -] (P, P) = [P, P]$ . Podobnie $F (Q) = [Q, Q]$ . Działanie na morfizmach:

F (e, p) = E x p ((e, p), (e, p)) = ([-, -] (p, e), [-, -] (e, p)) = ([p, e], [e, p])

A zatem otrzymujemy:

Wiemy już, że para funkcji powyżej tworzy parę e-p! Przypomnijmy jeszcze raz, jak działają funkcje $[p, e]$ i $[e, p]$ na elementy z odpowiednio $[P, P]$ i $[Q, Q]$ . Przykładowo, dla $f \in [P, 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, e] (f) = e \circ f \circ p$ . Podobnie $[e, p] (g) = p \circ g \circ e$ dla $g \in [Q, Q]$ .

Zauważmy w końcu, że dla dowolnego dcpo $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 14.8 [Scott]

Niech

P

będzie dcpo z elementem najmniejszym

⊥

. Zdefiniujmy diagram w

𝐃 𝐜 𝐩 𝐨

, jak następuje:

gdzie:

$D_{0} = P$ , $D_{n + 1} = [D_{n}, D_{n}]$ ,
$e_{0} : P \to [P, P]$ jest funkcją $λ y . λ x . y$ .

$p_{0} : [P, P] \to P$ jest funkcją $λ f . f (⊥)$ .

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

Teoria kategorii dla informatyków/Wykład 14: Teoria dziedzin III

Spis treści

Twierdzenie o zgodności granicy prostej i odwrotnej

Kategoria dcpo i par 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