Teoria kategorii dla informatyków/Ćwiczenia 11: Monady

From Studia Informatyczne

==Zadanie 11.1==

Udowodnij, że jeśli F\dashv G oraz T=GF, to naturalność \varepsilon implikuje, że poniższy diagram:

Grafika:tk-11.5.png

komutuje.

Rozwiązanie:

Niech f\colon A\to B będzie dowolnym morfizmem w \mathbf{D}. Naturalność \varepsilon wyraża się następująco:

Grafika:tk-11.6.png

W szczególnej sytuacji, gdy A:=FGB i f:=\varepsilon_B mamy:

Grafika:tk-11.7.png

Dla B będącego w obrazie F, tzn. dla B:=FC dla pewnego C\in \mathbf{C}_0 dostajemy:

Grafika:tk-11.8.png

Ale G jako funktor, zachowuje złożenia, więc aplikując go do ostatniego diagramu, widzimy że:

Grafika:tk-11.9.png

Pozbywając się nazw obiektów, podstawiając \mu za G\varepsilon_F oraz T=GF, mamy na koniec:

Grafika:tk-11.10.png


==Zadanie 11.2==

Niech \mathbb{T}=(T,\eta,\mu) będzie monadą nad \mathbf{C}. Pokaż że dla dowolnego X\in \mathbf{C}_0, para (TX,\mu_X) jest \mathbb{T}-algebrą.

Wskazówka:

Sformułowanie zadania jest rozwiązaniem.

Rozwiązanie:

Musimy pokazać, że \mu_X\circ \eta_{TX} = 1_{TX}, co wynika z komutowania pierwszego diagramu trójkątnego w definicji monady. Po drugie, musimy wykazać, że \mu_X\circ \mu_{TX} = \mu_X\circ T(\mu_X), co jest również prawdą z definicji monady (diagram trzeci, prostokątny, komutuje).


==Zadanie 11.3==

Udowodnij Twierdzenie 11.2.

Wskazówka:

Definiujemy jedność sprzężenia jako \eta, zaś kojedność przez komponenty jako \varepsilon_{(X,\theta)}:= \theta. Potem wykorzystać Twierdzenie 9.3.

Rozwiązanie:

Zauważmy, po pierwsze, że:

G^{\mathbb{T}}F^{\mathbb{T}}= T,

a zatem mamy kandydata na jedność sprzężenia: \eta\colon 1_{\mathbf{C}}\to G^{\mathbb{T}}F^{\mathbb{T}}. Jak zdefiniować kojedność? Jeśli (X,\theta) jest \mathbb{T}-algebrą, to wiemy, że diagram:

Grafika:tk-11.11.png

komutuje. Ale to właśnie oznacza, że \theta jest morfizmem \mathbb{T}-algebr: \theta\colon (TX,\mu_X)\to (X,\theta). A zatem wolno nam zdefiniować kojedność, jak to zaproponowaliśmy we Wskazówce, jako \varepsilon_{(X,\theta)}:= \theta. Pierwszy z diagramów trójkątnych z Twierdzenia 9.3 to:

Grafika:tk-11.12.png

który redukuje się do znanego już komutującego diagramu: drugiego diagramu trójkątnego w definicji monady. Drugi z diagramów trójkątnych z Twierdzenia 9.3 to:

Grafika:tk-11.13.png

który redukuje się do znanego z definicji \mathbb{T}-algebry komutującego diagramu:

Grafika:tk-11.14.png

To kończy dowód, że F^{\mathbb{T}}\dashv G^{\mathbb{T}}. Indukowana monada to:

(G^{\mathbb{T}}F^{\mathbb{T}}, \eta, G^{\mathbb{T}}\varepsilon_{^{\mathbb{T}}}) = (T,\eta,\mu)=\mathbb{T}.

==Zadanie 11.4==

Niech \mathbb{T}=(T\colon P\to P,1_P\leq T,TT\leq T) będzie monadą nad posetem (P,\leq). Pokaż, od jakiego sprzężenia pochodzi ta monada.

Wskazówka:

Wykorzystaj konstrukcję kategorii Eilenberga - Moore'a. Zauważ, że P^{\mathbb{T}} to poset izomorficzny z podzbiorem P składającym się z punktów stałych funkcji T.

Rozwiązanie:

Po pierwsze, zobaczmy jak wyglądają \mathbb{T}-algebry. Są to pary (x,Tx\leq x) dla x\in P, czyli te spośród elementów x\in P, dla których prawdą jest, że Tx\leq x. Ale przecież własności monady implikują, że zawsze x\leq Tx, a zatem \mathbb{T}-algebry to punkty stałe funkcji T .Morfizm \mathbb{T}-algebr (x,Tx\leq x), (y,Ty\leq y) istnieje, o ile x\leq y. A zatem P^{\mathbb{T}} jest częściowym porządkiem izomorficznym ze zbiorem (\mathrm{fix}(T),\leq) (punkty stałe T z porządkiem indukowanym z P). Funktor G^{\mathbb{T}}, który dla prostoty oznaczymy tu g, można zatem interpretować jako zanurzenie g\colon \mathrm{fix}(T)\to P. Funktor F^{\mathbb{T}}, oznaczany f, jest funkcją monotoniczną typu P\to \mathrm{fix}(T), która każdemu elementowi x\in P przypisuje punkt stały Tx\in P. Wniosek: f jest obcięciem funkcji T do typu P\to \mathrm{fix}(T). Oczywiście wtedy fgx=x dla dowolnego x\in P. Pokażmy, że f\dashv g, czyli dla dowolnych a,b\in P, fa\leq b wtedy i tylko wtedy, gdy a\leq gb w P. Załóżmy fa\leq b. Wówczas z monotoniczności g dostajemy gfa\leq gb. Z definicji monady wynika, że a\leq Ta, co czytamy też jako a\leq gfa, co w końcu daje: a\leq gfa\leq gb. Odwrotnie, załóżmy a\leq gb. Z monotoniczności f i faktu fg=1_P, co zauważyliśmy w poprzednim paragrafie, mamy natychmiast: fa\leq fgb=1_Pb=b. To kończy dowód faktu, że: f\dashv g.


==Zadanie 11.5==

Udowodnij, że (\mathcal{P}, \{ ...\}, \bigcup) jest monadą nad \mathbf{Set} dla kowariantnego funktora potęgowego \mathcal{P}\colon \mathbf{Set}\to\mathbf{Set}.

Rozwiązanie:

Pokażemy, że kolejne równania definiujące monadę są spełnione.

Niech S\subseteq \mathcal{P} X. Wówczas (\mu_X\circ\mathcal{P}\eta_X)(S)=\mu_X(\eta_X[S])=\bigcup(\{\{ z\}\mid z\in S \})=S. A zatem \mu_X\circ \mathcal{P}\eta_X=1_{\mathcal{P}}. Po drugie, (\mu_X\circ (\eta_{\mathcal{P}})_X)(S)=\bigcup\{ S\} = S, co daje \mu_X\circ (\eta_{\mathcal{P}})_X=1_{\mathcal{P}}. W końcu, niech \alpha \subseteq \mathcal{P}\mathcal{P} X. Wtedy (\mu_X\circ \mathcal{P}\mu_X)(\alpha)=\bigcup\{\bigcup W\mid W\in \alpha\}, a z drugiej strony (\mu_X\circ \mu_{\mathcal{P} X})(\alpha)=\bigcup\bigcup \alpha. Łatwa teoriomnogościowa równość \bigcup\{\bigcup W\mid W\in \alpha\} = \bigcup\bigcup \alpha, dowodzi zatem, że \mu_X\circ \mathcal{P}\mu_X = \mu_X\circ \mu_{\mathcal{P} X}, co należało pokazać.

==Zadanie 11.6==

Niech (M,*,e) będzie monoidem. Udowodnij, że funktor

M\times (-)\colon \mathbf{Set}\to\mathbf{Set}

wraz z transformacjami naturalnymi \eta_X(x):=(e,x) oraz \mu_X(m_2*(m_1,x)):=(m_2*m_1,x) definiuje monadę \mathbb{T}, której \mathbb{T}-algebrami są M-automaty.

Rozwiązanie:

Oznaczmy T=M\times (-). Jest oczywiste że T jest endofunktorem na \mathbf{Set}. Zauważmy, że M-algebra to para (X,\delta), gdzie \delta\colon T(X)=M\times X\to X, która spełnia dwa warunki wynikające z komutowania dwóch diagramów w definicji M-algebry. Te dwa równania to dokładnie te same równania, które widzieliśmy w Zadaniu 1.11! To znaczy, że M-algebrami są M-automaty.

Sprawdźmy teraz aksjomaty monady:

\aligned (\mu_X\circ \eta){TX})(m,x) &=& \mu_X(e,(m,x))\\ &=& (e*m,x))\\ &=& (m,x))\\ &=& (m*e,x))\\ &=& \mu_X(m,(e,x))\\ &=& \mu_X((1_M\times \eta_X)(e,x))\\ &=& \mu_X((T\eta_X)(e,x))\\ &=& (\mu_X\circ T\eta_X)(e,x)), \endaligned

co dowodzi, że (\mu_X\circ \eta){TX})=1_{TX}=(\mu_X\circ T\eta_X).

Po drugie:

\aligned (\mu_X\circ T(\mu_X))(k,(m,(n,x))) &=& \mu_X(k, \mu_X((m,(n,x))))\\ &=& \mu_X(k,(m*n,x))\\ &=& (k*m*n,x))\\ &=& \mu_X((k*m,(n,x)))\\ &=& (\mu_X\circ\mu_{TX})(k,(m,(n,x))), \endaligned

co pokazuje \mu_X\circ T(\mu_X)=\mu_X\circ\mu_{TX} i kończy dowód.

==Zadanie 11.7==

Udowodnij, że funktor (-)_{\bot}\colon \mathbf{Pos}\to\mathbf{Pos}_{\bot}, który dodaje do posetu nowy element najmniejszy wraz z funktorem zapominania indukuje monadę nad \mathbf{Pos}. Jakie są algebry dla tej monady?

Wskazówka:

(1) Pełna definicja dla podobnego funktora jest podana w Zadaniu 14.3. (2) \mathbf{Pos}_{\bot} to oczywiście kategoria posetów, które posiadają element najmniejszy i funkcji monotonicznych zachowujących elementy najmniejsze.

Rozwiązanie:

Przypomnijmy, że dla funkcji monotonicznej f\colon X\to Y, f_{\bot}\colon X_{\bot}\to Y_{\bot} jest funkcją, która działa tak samo jak f oraz zachowuje element najmniejszy, tj. f_{\bot}(\bot_X):=\bot_Y. Oczywiście w ten sposób (-)_{\bot} jest dobrze zdefiniowanym funktorem. Jest on lewym sprzężeniem do funktora zapominania U\colon Pos\to\mathbf{Pos}_{\bot}, a zatem U(-)_{\bot} jest endofunktorem na \mathbf{Pos}. Jednością tej monady nie może być nic innego, jak transformacja \eta_X(x):=x, zaś mnożeniem transformacja, której komponent \mu_X jest identycznością dla elementów, które są różne od elementu najmniejszego i (dokładnie jednego) elementu bezpośrednio nad nim. Te dwa wyróżnione elementy zostają posyłane w element najmniejszy kodziedziny.

Algebra dla tej monady to para (X,k), gdzie k\colon U(-)_{\bot}(X)\to X jest funkcją monotoniczną, która musi spełniać w szczególności k \eta_X =1_X. Funkcja k jest zatem retrakcją, więc epi, więc surjekcją. W koniunkcji z drugim aksjomatem algebry dostajemy natychmiast, że k(\bot) jest najmniejszym elementem X, a co za tym idzie, k jest identycznością, gdy obetniemy ją do X.

==Zadanie 11.8==

Wykaż, że algebrami dla monady nad \mathbf{Set} indukowanej przez kowariantny funktor potęgowy \mathcal{P} są półkraty zupełne i homomorfizmy tych półkrat (tzn. funkcje zachowujące dowolne suprema).

Wskazówka:

Jedynie naszkicujemy dowód.

Rozwiązanie:

Algebrą dla tej monady jest każda para (\mathcal{P} X,h\colon \mathcal{P} X\to X), która spełnia: h(\{ x\})=x oraz dla dowolnego \alpha\subseteq \mathcal{P} X:

h(\{h(A)\mid A\in \alpha\})= h(\bigcup\alpha).

Mając strukturę algebry na X, możemy teraz zdefiniować częściowy porządek na X jako:

x\leq y \iff h(\{x,y\})=y.

Zwrotność tej relacji wynika z pierwszego z warunków na h. Antysymetria wynika z równości zbiorów \{ x,y\}=\{ y,x\}. Przechodniość wynika z drugiego z warunków na h, bo dla x\leq y i y\leq z mamy:

h(\{ x,z\}) = h(\{ x\}\cup \{ y,z\})= h(\{ x,y\}\cup \{ z\})=h(\{ y,z\})=z.

W tym porządku istnieją dowolne suprema dane jako \bigvee S := h(S).

Co więcej, każdy morfizm algebr jest funkcją zachowującą dowolne suprema. Te obserwacje wskazują nam funktor z \mathcal{P}-algebr w kategorię \mathbf{SLat} półkrat. W rzeczywistości ten funktor jest częścią równoważności tych dwóch kategorii.


==Zadanie 11.9==

Wykaż, że sprzężenie F^{\mathbb{T}}\dashv G^{\mathbb{T}}, od którego pochodzi monada \mathbb{T} jest obiektem końcowym pewnej kategorii, w następującym sensie: jeśli F\dashv G dla F\colon \mathbf{C}\to\mathbf{D}\colon G jest sprzężeniem, które indukuje \mathbb{T}, to istnieje dokładnie jeden funktor K\colon \mathbf{D}\to \mathbf{C}^{\mathbb{T}} taki, że dwa poniższe diagramy komutują:

Grafika:tk-11.15.png

Taki funktor K\colon \mathbf{D}\to \mathbf{C}^{\mathbb{T}} nazywa się funktorem porównawczym (ang. comparison functor) dla sprzężenia F\dashv G.

Uwaga
Dowodzi się, że sprzężenie F^{\mathbb{T}}\dashv G^{\mathbb{T}} rzeczywiście nie jest jedynym, które indukuje \mathbb{T}, a zatem K w ogólności nie trywializuje się. Okazuje się, że dla \mathbf{C} można skonstruować tak zwaną kategorię Kliesliego oznaczaną \mathbf{C}_{\mathbb{T}}, która jest w ogólności różna od \mathbf{C}^{\mathbb{T}} i parę funktorów F^{\mathbb{T}}\colon \mathbf{C}\to\mathbf{C}_{\mathbb{T}}\colon G_{\mathbb{T}} z F_{\mathbb{T}}\dashv G_{\mathbb{T}}, gdzie to sprzężenie indukuje \mathbb{T}. Dalsze wiadomości na ten temat można znaleźć na przykład w podręczniku Saundersa Mac Lane'a pt. Categories for the Working Mathematician, Springer, 1997.

Wskazówka:

Największą rolę w dowodzie grają homomorfizmy algebr K(\varepsilon_A) dla dowolnego A\in \mathbf{D}_0.

Rozwiązanie:

Przypuśćmy, że K jest funktorem, który spełnia założenia zadania. Skoro drugi diagram komutuje, mamy G^{\mathbb{T}}(KX)=GX, a zatem (bo G^{\mathbb{T}} jest funktorem zapominania) KX = (GX,h_X) dla pewnej strzałki h_X\colon GFGX = T(GX)\to GX. Zapytajmy teraz o F^{\mathbb{T}}, o którym informacja jest zawarta w pierwszym diagramie. Po chwili zauważamy, że:

(GFX,h_{FX})= KFX = F^{\mathbb{T}}(X) = (GFX,\mu_X) = (GFX,G\varepsilon_{FX}),

co daje h_{FX} = G\varepsilon_{FX}. Widzimy więc, jak strzałka h jest zdefiniowana na obrazie F. A jak jest w ogólnym przypadku?

Niech A\in \mathbf{D}_0. Skoro \varepsilon_A\colon FGA\to A jest strzałką w \mathbf{D}, to strzałka K(\varepsilon_A)\colon K(FGA)\to K(A) jest z definicji funktora K morfizmem \mathbb{T}-algebr nad \mathbf{C}. Dokładnie mówiąc, jest to morfizm pomiędzy algebrą K(FGA)=(GFGA,h_{FGA}=G\varepsilon_{FGA}) a algebrą (GA,h_A). To znaczy, że poniższy diagram komutuje:

Grafika:tk-11.16.png

Używając faktu, że \varepsilon jest kojednością sprzężenia, zgodnie z Twierdzeniem 9.3, dostajemy:

h_A = h_A\circ 1_{GFGA} = h_A\circ GFG\varepsilon_A\circ GF\eta_{GA} = G\varepsilon_A\circ G\varepsilon_{FGA}\circ GF\eta_{GA} = G\varepsilon_A\circ 1_{GA}= G\varepsilon_A.

A zatem, jeśli K istnieje, to musimy mieć:

K(f\colon A\to B)=(GA,G\varepsilon_A)\stackrel{Gf}{\to}(GB,G\varepsilon_B).

Łatwo sprawdzić, że ten przepis rzeczywiście definiuje funktor K, który spełnia zarówno równość KF=F^{\mathbb{T}}, jak i G^{\mathbb{T}}K=G. Gdyby istniały dwa takie funktory K_1,K_2, to skoro G^{\mathbb{T}}K_1 = G = G^{\mathbb{T}}K_2, wierność G^{\mathbb{T}} implikuje K_1=K_2, co kończy dowód.