Teoria kategorii dla informatyków/Wykład 11: Monady: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
m
 
(Nie pokazano 1 pośredniej wersji utworzonej przez tego samego użytkownika)
Linia 1: Linia 1:
 +
 
{{kotwica|wyklad11|}}
 
{{kotwica|wyklad11|}}
  
Linia 6: Linia 7:
 
==W poszukiwaniu kategorii algebraicznych==
 
==W poszukiwaniu kategorii algebraicznych==
  
Z pewnością na kategorie algebraiczne nie nadają się wszystkie kategorie konkretne, które charakteryzują się tym, że posiadają funktor zapominania o kodziedzinie <math>\mathbf{Set}</math> (Definicja [[Teoria_kategorii_dla_informatyków/TKI_Moduł_5#mod5:def:konkret| 5.?]]). Nawet, gdybyśmy dodatkowo zażądali, aby tenże funktor zapominania <math>G\colon \mathbf{C}\to \mathbf{Set}</math> miał lewe sprzężenie <math>F\dashv G</math>, które wskazuje jak odbudować w sposób wolny zapomnianą strukturę, to sytuacja ciągle nie jest zadowalająca. Na przykład, funktor zapominania <math>\mathbf{Top}\to \mathbf{Set}</math> ma lewe sprzężenie a my nie chcemy traktować <math>\mathbf{Top}</math> jako kategorii algebraicznej. Ale stąd warto rozpocząć poszukiwania, gdyż wszelkie kategorie, od których oczekujemy algebraiczności, jak <math>\mathbf{Grp}</math> czy <math>\mathbf{Mon}</math> posiadają lewe sprzężenia do funktorów zapominania, które przypisują zbiorom odpowiednie '''algebry wolne'''.
+
Z pewnością na kategorie algebraiczne nie nadają się wszystkie kategorie konkretne, które charakteryzują się tym, że posiadają funktor zapominania o kodziedzinie <math>\mathbf{Set}</math> ([[Teoria_kategorii_dla_informatyków/Wykład_5:_Funktory_i_transformacje_naturalne#mod5:def:konkret|Definicja 5.9]]). Nawet, gdybyśmy dodatkowo zażądali, aby tenże funktor zapominania <math>G\colon \mathbf{C}\to \mathbf{Set}</math> miał lewe sprzężenie <math>F\dashv G</math>, które wskazuje jak odbudować w sposób wolny zapomnianą strukturę, to sytuacja ciągle nie jest zadowalająca. Na przykład, funktor zapominania <math>\mathbf{Top}\to \mathbf{Set}</math> ma lewe sprzężenie, a my nie chcemy traktować <math>\mathbf{Top}</math> jako kategorii algebraicznej. Ale stąd warto rozpocząć poszukiwania, gdyż wszelkie kategorie, od których oczekujemy algebraiczności, jak <math>\mathbf{Grp}</math> czy <math>\mathbf{Mon}</math>, posiadają lewe sprzężenia do funktorów zapominania, które przypisują zbiorom odpowiednie '''algebry wolne'''.
  
Niech zatem <math>F\colon \mathbf{C}\to \mathbf{D}</math> i <math>G\colon \mathbf{D}\to \mathbf{C}</math> będą sprzężone: <math>F\dashv G</math>. Rozważmy funktor <math>T\colon \mathbf{C}\to\mathbf{C}</math> będący złożeniem funktorów <math>F</math> i <math>G</math>: <math>T=GF</math>. Jedność <math>\eta\colon 1_{\mathbf{C}}\to GF</math> sprzężenia ma zatem typ <math>1\to T</math>. Informacje o kojedności <math>\varepsilon\colon FG\to 1_{\mathbf{D}}</math> również nietrudno zakodować w terminach funktora <math>T</math>, bowiem skoro <math>\varepsilon\colon FG\to 1</math>, to <math>\varepsilon_F\colon FGF\to F</math> (przypomnijmy definicję: <math>\varepsilon_F(-):=\varepsilon_{F(-)}</math>), a co za tym idzie: <math>G\varepsilon_F\colon GFGF\to GF</math>. Transformacja <math>G\varepsilon_F</math> jest naturalna; jeśli oznaczymy ją jako <math>\mu</math>, to dostajemy <math>\mu\colon TT\to T</math>. Diagramy trójkątne charakteryzujące sprzężenie z Twierdzenia [[Teoria_kategorii_dla_informatyków/TKI_Moduł_?#mod9:thm:adjtriangle| ?]]
+
Niech zatem <math>F\colon \mathbf{C}\to \mathbf{D}</math> i <math>G\colon \mathbf{D}\to \mathbf{C}</math> będą sprzężone: <math>F\dashv G</math>. Rozważmy funktor <math>T\colon \mathbf{C}\to\mathbf{C}</math> będący złożeniem funktorów <math>F</math> i <math>G</math>: <math>T=GF</math>. Jedność <math>\eta\colon 1_{\mathbf{C}}\to GF</math> sprzężenia ma zatem typ <math>1\to T</math>. Informacje o kojedności <math>\varepsilon\colon FG\to 1_{\mathbf{D}}</math> również nietrudno zakodować w terminach funktora <math>T</math>, bowiem skoro <math>\varepsilon\colon FG\to 1</math>, to <math>\varepsilon_F\colon FGF\to F</math> (przypomnijmy definicję: <math>\varepsilon_F(-):=\varepsilon_{F(-)}</math>), a co za tym idzie: <math>G\varepsilon_F\colon GFGF\to GF</math>. Transformacja <math>G\varepsilon_F</math> jest naturalna; jeśli oznaczymy ją jako <math>\mu</math>, to dostajemy <math>\mu\colon TT\to T</math>. Diagramy trójkątne charakteryzujące sprzężenie z [[Teoria_kategorii_dla_informatyków/Wykład_9:_Sprzężenia_I#mod9:thm:adjtriangle|Twierdzenia 9.3]] dają nam następujące komutujące trójkąty:
dają nam następujące komutujące trójkąty:
 
  
\begin{diagram}
+
<center>[[Grafika:tk-11.1.png]]</center>
T & \rTo^{\eta_T} & TT        & & & &  TT & \lTo^{T\eta} & T \\
 
  & \rdTo_{1_T}  & \dTo_{\mu} & & & &  \dTo^{\mu} & \ldTo_{1_T} & \\
 
  &              & T          & & & &  T & & \\
 
\end{diagram}
 
  
Naturalność <math>\varepsilon</math> daje dodatkowo komutujący diagram (Zadanie [[Teoria_kategorii_dla_informatyków/TKI_Ćwiczenia_?#mod11:zad1| ?]]).
+
Naturalność <math>\varepsilon</math> daje dodatkowo komutujący diagram (Zadanie [[Teoria_kategorii_dla_informatyków/Ćwiczenia_11:_Monady#mod11:zad1|Zadanie 11.1]]).
  
\begin{diagram}
+
<center>[[Grafika:tk-11.2.png]]</center>
TTT & \rTo^{T\mu} & TT\\
 
\dTo^{\mu_T} & & \dTo_{\mu}\\
 
TT & \rTo_{\mu} & T\\
 
\end{diagram}
 
  
 
Widzimy więc, że po wprowadzeniu endofunktora <math>T</math> i prostym przekształceniu sprzężenia, od którego pochodzi, pojawiła się pewna struktura. Dobrze wyróżnić je definicją i dokładnie zbadać:
 
Widzimy więc, że po wprowadzeniu endofunktora <math>T</math> i prostym przekształceniu sprzężenia, od którego pochodzi, pojawiła się pewna struktura. Dobrze wyróżnić je definicją i dokładnie zbadać:
  
  
{{definicja|6.1 [monada]|mod11:def:monada| '''Monadą''' w kategorii <math>\mathbf{C}</math> nazywamy trójkę <math>\mathbb{T} = (T,\eta,\mu)</math>, gdzie <math>T\colon\mathbf{C}\to\mathbf{C}</math> jest funktorem, zaś <math>\eta\colon 1_{\mathbf{C}}\to T</math> i <math>\mu\colon TT\to T</math> - tranformacjami naturalnymi takimi, że:
+
{{definicja|11.1 [monada]|mod11:def:monada| '''Monadą''' w kategorii <math>\mathbf{C}</math> nazywamy trójkę <math>\mathbb{T} = (T,\eta,\mu)</math>, gdzie <math>T\colon\mathbf{C}\to\mathbf{C}</math> jest funktorem, zaś <math>\eta\colon 1_{\mathbf{C}}\to T</math> i <math>\mu\colon TT\to T</math> - tranformacjami naturalnymi takimi, że:
  
 
<center><math>\mu\circ \mu T = \mu \circ T\mu,</math></center>
 
<center><math>\mu\circ \mu T = \mu \circ T\mu,</math></center>
Linia 34: Linia 26:
 
<center><math>\mu \circ \eta_T = 1 = \mu\circ T\eta,</math></center>
 
<center><math>\mu \circ \eta_T = 1 = \mu\circ T\eta,</math></center>
  
tzn. takimi że powyższe trzy diagramy komutują.
+
tzn. takimi, że powyższe trzy diagramy komutują.
 
}}
 
}}
  
Linia 41: Linia 33:
  
  
Czy struktura monady <math>\mathbb{T}=(T,\eta, \mu)</math> nad kategorią <math>\mathbf{C}</math> zawsze pochodzi od pewnego sprzężenia? Zauważmy, że aby odpowiedzieć na to pytanie musimy przede wszystkim odnaleźć ''drugą'' kategorię <math>\mathbf{D}</math> i dwa funktory <math>F\colon \mathbf{C}\to \mathbf{D}</math>, <math>G\colon \mathbf{D}\to\mathbf{C}</math>, <math>F\dashv G</math> takie, że <math>T=GF</math>. Okazuje się, że odpowiedź jest pozytywna: każda monada pochodzi od pewnego sprzężenia a tak naprawdę istnieje wiele sprzężeń indukujących daną monadę. Te sprzężenia tworzą oddzielną kategorię. My wskażemy obiekt końcowy tej kategorii.
+
Czy struktura monady <math>\mathbb{T}=(T,\eta, \mu)</math> nad kategorią <math>\mathbf{C}</math> zawsze pochodzi od pewnego sprzężenia? Zauważmy, że aby odpowiedzieć na to pytanie musimy przede wszystkim odnaleźć ''drugą'' kategorię <math>\mathbf{D}</math> i dwa funktory <math>F\colon \mathbf{C}\to \mathbf{D}</math>, <math>G\colon \mathbf{D}\to\mathbf{C}</math>, <math>F\dashv G</math> takie, że <math>T=GF</math>. Okazuje się, że odpowiedź jest pozytywna: każda monada pochodzi od pewnego sprzężenia, a tak naprawdę istnieje wiele sprzężeń indukujących daną monadę. Te sprzężenia tworzą oddzielną kategorię. My wskażemy obiekt końcowy tej kategorii.
  
Dla monady <math>\mathbb{T}=(T,\eta,\mu)</math> nad <math>\mathbf{C}</math> definiujemy <math>\mathbb{T}</math>-algebrę jako parę <math>(X,\theta)</math>, gdzie <math>X\in \mathbf{C}_0</math>, <math>\theta\colon TX\to X</math> oraz
+
Dla monady <math>\mathbb{T}=(T,\eta,\mu)</math> nad <math>\mathbf{C}</math> definiujemy <math>\mathbb{T}</math>-algebrę jako parę <math>(X,\theta)</math>, gdzie <math>X\in \mathbf{C}_0</math>, <math>\theta\colon TX\to X</math> oraz:
  
\begin{diagram}
+
<center>[[Grafika:tk-11.3.png]]</center>
X & \rTo^{\eta_X} & TX & & & & TTX & \rTo^{\mu_X} & TX\\
 
&\rdTo^{1_X} & \dTo_{\theta} & & & & \dTo^{T\theta} & & \dTo_{\theta}\\
 
& & X & & & & TX & \rTo_{\theta} & X\\
 
\end{diagram}
 
  
 
Morfizmem <math>\mathbb{T}</math>-algebr <math>f\colon (X,\theta)\to (Y,\gamma)</math> jest morfizm <math>f\colon X\to Y\in \mathbf{C}_1</math> taki, że poniższy diagram komutuje:
 
Morfizmem <math>\mathbb{T}</math>-algebr <math>f\colon (X,\theta)\to (Y,\gamma)</math> jest morfizm <math>f\colon X\to Y\in \mathbf{C}_1</math> taki, że poniższy diagram komutuje:
  
\begin{diagram}
+
<center>[[Grafika:tk-11.4.png]]</center>
TX & \rTo^{Tf} & TY\\
 
\dTo^{\theta} & & \dTo_{\gamma}\\
 
X & \rTo_{f} & Y\\
 
\end{diagram}
 
  
Kategorię <math>\mathbb{T}</math>-algebr będziemy oznaczać <math>\mathbf{C}^{\mathbb{T}}</math>. Nazywamy ją od nazwisk odkrywców: kategorią Eilenberga-Moore'a. Zobaczmy, że istnieje naturalny funktor zapominania <math>G^{\mathbb{T}}\colon \mathbf{C}^{\mathbb{T}}\to \mathbf{C}</math> definiowany jako:
+
Kategorię <math>\mathbb{T}</math>-algebr będziemy oznaczać <math>\mathbf{C}^{\mathbb{T}}</math>. Nazywamy ją od nazwisk odkrywców: kategorią Eilenberga - Moore'a. Zobaczmy, że istnieje naturalny funktor zapominania <math>G^{\mathbb{T}}\colon \mathbf{C}^{\mathbb{T}}\to \mathbf{C}</math> definiowany jako:
  
  
Linia 68: Linia 52:
 
<center><math>F^{\mathbb{T}}(f\colon X\to Y):= Tf\colon (TX,\mu_X)\to (TY,\mu_Y).</math></center>
 
<center><math>F^{\mathbb{T}}(f\colon X\to Y):= Tf\colon (TX,\mu_X)\to (TY,\mu_Y).</math></center>
  
W Zadaniu [[Teoria_kategorii_dla_informatyków/TKI_Ćwiczenia_?#mod11:zad2| ?]] pokażemy, że <math>(TX,\mu_X)</math> dla dowolnego <math>X</math> jest rzeczywiście algebrą, zaś w Zadaniu następnym nr [[Teoria_kategorii_dla_informatyków/TKI_Ćwiczenia_?#mod11:zad3| ?]] udowodnimy, że
+
W [[Teoria_kategorii_dla_informatyków/Ćwiczenia_11:_Monady#mod11:zad2|Zadaniu 11.2]] pokażemy, że <math>(TX,\mu_X)</math> dla dowolnego <math>X</math> jest rzeczywiście algebrą, zaś w Zadaniu następnym nr [[Teoria_kategorii_dla_informatyków/Ćwiczenia_11:_Monady#mod11:zad3|11.3]] udowodnimy, że
  
  
  
{{twierdzenie|6.2 [każda monada pochodzi od sprzężenia]|mod11:thm:EM|
+
{{twierdzenie|11.2 [każda monada pochodzi od sprzężenia]|mod11:thm:EM|
  
 
<center><math>F^{\mathbb{T}}\dashv G^{\mathbb{T}}</math></center>
 
<center><math>F^{\mathbb{T}}\dashv G^{\mathbb{T}}</math></center>
Linia 82: Linia 66:
  
 
* Niech <math>(P,\leq)</math> będzie częściowym porządkiem. Monadą nad <math>P</math> jest funkcja monotoniczna <math>T\colon P\to P</math> taka, że <math>x\leq Tx</math> oraz <math>TTx\leq Tx</math> dla dowolnego <math>x\in P</math>. (Te dwie nierówności wyrażają typu transformacji <math>\eta</math> i <math>\mu</math>. Diagramy w definicji monady komutują, bo relacja <math>\leq</math> jest przechodnia.) Powyższe zależności dla <math>T</math> implikują, że <math>Tx\leq TTx</math>, czyli <math>TT=T</math>. Funkcja <math>T</math> jest więc idempotentna i traktuje się ją zwykle jako '''operację domknięcia'''.
 
* Niech <math>(P,\leq)</math> będzie częściowym porządkiem. Monadą nad <math>P</math> jest funkcja monotoniczna <math>T\colon P\to P</math> taka, że <math>x\leq Tx</math> oraz <math>TTx\leq Tx</math> dla dowolnego <math>x\in P</math>. (Te dwie nierówności wyrażają typu transformacji <math>\eta</math> i <math>\mu</math>. Diagramy w definicji monady komutują, bo relacja <math>\leq</math> jest przechodnia.) Powyższe zależności dla <math>T</math> implikują, że <math>Tx\leq TTx</math>, czyli <math>TT=T</math>. Funkcja <math>T</math> jest więc idempotentna i traktuje się ją zwykle jako '''operację domknięcia'''.
* Kowariantny funktor potęgowy <math>\mathcal{P}\colon \mathbf{Set}\to\mathbf{Set}</math> indukuje monadę, gdzie <math>\eta_X\colon X\to \mathcal{P}(X)</math> jest zanurzeniem <math>\eta_X(x)=\{ x\}</math>, zaś mnożenie <math>\mu_X\colon \mathcal{P}\mathcal{P}(X)\to\mathcal{P}(X)</math> jest sumą zbiorów: <math>\mu_X(\mathcal{S})=\bigcup \alpha</math>. Własności tej monady bardzo dobrze podsumowują teoriomnogościowe własności sumy w połączeniu z notacją <math>\{ ...\}</math> służącą do konstrukcji zbiorów. W Zadaniu [[Teoria_kategorii_dla_informatyków/TKI_Ćwiczenia_?#mod11:zad5| ?]] przedstawiamy dowód, że <math>(\mathcal{P}, \{\cdot\}, \bigcup)</math> jest monadą nad <math>\mathbf{Set}</math>. Identyczny dowód pokazuje, że <math>\mathcal{P}_{fin}\colon \mathbf{Set}_{fin}\to\mathbf{Set}_{fin}</math> (kowariantny funktor potęgowy na zbiorach skończonych) indukuje monadę nad <math>\mathbf{Set}_{fin}</math>.
+
* Kowariantny funktor potęgowy <math>\mathcal{P}\colon \mathbf{Set}\to\mathbf{Set}</math> indukuje monadę, gdzie <math>\eta_X\colon X\to \mathcal{P}(X)</math> jest zanurzeniem <math>\eta_X(x)=\{ x\}</math>, zaś mnożenie <math>\mu_X\colon \mathcal{P}\mathcal{P}(X)\to\mathcal{P}(X)</math> jest sumą zbiorów: <math>\mu_X(\mathcal{S})=\bigcup \alpha</math>. Własności tej monady bardzo dobrze podsumowują teoriomnogościowe własności sumy w połączeniu z notacją <math>\{ ...\}</math> służącą do konstrukcji zbiorów. W [[Teoria_kategorii_dla_informatyków/Ćwiczenia_11:_Monady#mod11:zad5|Zadaniu 11.5]] przedstawiamy dowód, że <math>(\mathcal{P}, \{\cdot\}, \bigcup)</math> jest monadą nad <math>\mathbf{Set}</math>. Identyczny dowód pokazuje, że <math>\mathcal{P}_{fin}\colon \mathbf{Set}_{fin}\to\mathbf{Set}_{fin}</math> (kowariantny funktor potęgowy na zbiorach skończonych) indukuje monadę nad <math>\mathbf{Set}_{fin}</math>.
* Niech <math>(M,*,e)</math> będzie monoidem. Funktor <math>M\times (-)\colon \mathbf{Set}\to\mathbf{Set}</math> wraz z transformacjami naturalnymi <math>\eta_X(x):=(e,x)</math> oraz <math>\mu_X(m_2*(m_1,x)):=(m_2*m_1,x)</math> definiuje monadę <math>\mathbb{T}</math>. <math>\mathbb{T}</math>-algebry to <math>M</math>-automaty, które poznaliśmy w Zadaniu [[Teoria_kategorii_dla_informatyków/TKI_Ćwiczenia_?#mod1:zad11| ?]]. Szczegóły tej konstrukcji opisujemy w Zadaniu [[Teoria_kategorii_dla_informatyków/TKI_Ćwiczenia_?#mod11:zad6| ?]].
+
* Niech <math>(M,*,e)</math> będzie monoidem. Funktor <math>M\times (-)\colon \mathbf{Set}\to\mathbf{Set}</math> wraz z transformacjami naturalnymi <math>\eta_X(x):=(e,x)</math> oraz <math>\mu_X(m_2*(m_1,x)):=(m_2*m_1,x)</math> definiuje monadę <math>\mathbb{T}</math>. <math>\mathbb{T}</math>-algebry to <math>M</math>-automaty, które poznaliśmy w [[Teoria_kategorii_dla_informatyków/Ćwiczenia_1:_Teoria_kategorii_jako_abstrakcyjna_teoria_funkcji#mod1:zad11|Zadaniu 1.11]]. Szczegóły tej konstrukcji opisujemy w [[Teoria_kategorii_dla_informatyków/Ćwiczenia_11:_Monady#mod11:zad6|Zadaniu 11.6]].
* Funktor <math>\mathrm{List}\colon \mathbf{Set}\to \mathbf{Mon}</math> z przykładu [[Teoria_kategorii_dla_informatyków/TKI_Moduł_?#mod5:ex:List| ?]] jest lewym sprzężeniem do funktora zapominania <math>U\colon \mathbf{Mon}\to \mathbf{Set}</math>. Złożenie <math>T=UF</math> jest funktorem, który zbiorowi <math>X</math> przypisuje <math>T(X)</math>, będący zbiorem skończonych słów nad <math>X</math>. Jedność jest oczywiście zanurzeniem elementu <math>x\in X</math> w listę jednoelementową <math>[x]</math>. Jak zdefiniować mnożenie w tej monadzie? Jako <math>\mu\colon TTX\to TX</math> proponujemy transformację naturalną, która liście list
+
* Funktor <math>\mathrm{List}\colon \mathbf{Set}\to \mathbf{Mon}</math> z [[Teoria_kategorii_dla_informatyków/Wykład_5:_Funktory_i_transformacje_naturalne#mod5:ex:List|Przykładu 5.3]] jest lewym sprzężeniem do funktora zapominania <math>U\colon \mathbf{Mon}\to \mathbf{Set}</math>. Złożenie <math>T=UF</math> jest funktorem, który zbiorowi <math>X</math> przypisuje <math>T(X)</math> będący zbiorem skończonych słów nad <math>X</math>. Jedność jest oczywiście zanurzeniem elementu <math>x\in X</math> w listę jednoelementową <math>[x]</math>. Jak zdefiniować mnożenie w tej monadzie? Jako <math>\mu\colon TTX\to TX</math> proponujemy transformację naturalną, która liście list:
  
 
<center><math>[[x_1,...,x_n],[y_1,...,y_m],...,[z_1,...,z_l]]</math></center>
 
<center><math>[[x_1,...,x_n],[y_1,...,y_m],...,[z_1,...,z_l]]</math></center>
  
przypisze listę
+
przypisze listę:
  
 
<center><math>[x_1,...,x_n,y_1,...,y_m,...,z_1,...,z_l].</math></center>
 
<center><math>[x_1,...,x_n,y_1,...,y_m,...,z_1,...,z_l].</math></center>
  
 
Łatwo pokazać, że <math>\mathbb{T}=(T,\eta,\mu)</math> jest monadą nad <math>\mathbf{Set}</math>. Okazuje się, że kategoria <math>\mathbb{T}</math>-algebr jest równoważna z kategorią monoidów <math>\mathbf{Mon}</math>.
 
Łatwo pokazać, że <math>\mathbb{T}=(T,\eta,\mu)</math> jest monadą nad <math>\mathbf{Set}</math>. Okazuje się, że kategoria <math>\mathbb{T}</math>-algebr jest równoważna z kategorią monoidów <math>\mathbf{Mon}</math>.
* Rozważmy sprzężenie <math>F\dashv G</math> dla funktora wolnego <math>F\colon \mathbf{Set}\to\mathbf{Grp}</math> i funktora zapominania <math>G\colon \mathbf{Grp}\to \mathbf{Set}</math>. Niech <math>\mathbb{T}</math> będzie monadą indukowaną przez to sprzężenie. A zatem <math>T(X)</math> jest zbiorem podkładowym wolnej grupy nad zbiorem <math>X</math> (czy Czytelnik pamięta z kursu algebry jak taka grupa jest tworzona?). Jeśli <math>(X,\theta)</math> jest <math>\mathbb{T}</math>-algebrą, dostaniemy strukturę grupy na <math>X</math> jeśli zdefiniujemy działanie jako <math>x\cdot y := \theta(\langle x\rangle\langle y\rangle)</math>, gdzie <math>x\mapsto \langle x\rangle</math> jest ''włożeniem generatorów'', tzn. <math>\eta_X\colon X\to TX</math>, <math>\eta_X(x):=\langle x\rangle</math>, zaś <math>\langle x\rangle\langle y\rangle</math> jest mnożeniem w wolnej grupie nad <math>X</math>. Za pomocą tej konstrukcji, dostajemy funktor <math>\mathbf{Set}^{\mathbb{T}}\to \mathbf{Grp}</math>. Odwrotnie, jeśli <math>G</math> jest grupą, to homomorfizm <math>f_G\colon F(G)\to G</math>, definiowany jako mnożenie liter słowa z <math>F(G)</math> za pomocą działania grupy <math>G</math>, daje wraz z <math>G</math> <math>\mathbb{T}</math>-algebrę <math>(G,f_G)</math>, a zatem obiektową część funktora typu <math>\mathbf{Grp}\to\mathbf{Set}^{\mathbb{T}}</math>. Uwaga! Para funktorów, których szkic konstrukcji pokazaliśmy stanowi równoważność kategorii <math>\mathbf{Grp}</math> i <math>\mathbf{Set}^{\mathbb{T}}</math>.
+
* Rozważmy sprzężenie <math>F\dashv G</math> dla funktora wolnego <math>F\colon \mathbf{Set}\to\mathbf{Grp}</math> i funktora zapominania <math>G\colon \mathbf{Grp}\to \mathbf{Set}</math>. Niech <math>\mathbb{T}</math> będzie monadą indukowaną przez to sprzężenie. A zatem <math>T(X)</math> jest zbiorem podkładowym wolnej grupy nad zbiorem <math>X</math> (czy Czytelnik pamięta z kursu algebry, jak taka grupa jest tworzona?). Jeśli <math>(X,\theta)</math> jest <math>\mathbb{T}</math>-algebrą, dostaniemy strukturę grupy na <math>X</math>, jeśli zdefiniujemy działanie jako <math>x\cdot y := \theta(\langle x\rangle\langle y\rangle)</math>, gdzie <math>x\mapsto \langle x\rangle</math> jest ''włożeniem generatorów'', tzn. <math>\eta_X\colon X\to TX</math>, <math>\eta_X(x):=\langle x\rangle</math>, zaś <math>\langle x\rangle\langle y\rangle</math> jest mnożeniem w wolnej grupie nad <math>X</math>. Za pomocą tej konstrukcji dostajemy funktor <math>\mathbf{Set}^{\mathbb{T}}\to \mathbf{Grp}</math>. Odwrotnie, jeśli <math>G</math> jest grupą, to homomorfizm <math>f_G\colon F(G)\to G</math>, definiowany jako mnożenie liter słowa z <math>F(G)</math> za pomocą działania grupy <math>G</math>, daje wraz z <math>G</math> <math>\mathbb{T}</math>-algebrę <math>(G,f_G)</math>, a zatem obiektową część funktora typu <math>\mathbf{Grp}\to\mathbf{Set}^{\mathbb{T}}</math>. Uwaga! Para funktorów, których szkic konstrukcji pokazaliśmy, stanowi równoważność kategorii <math>\mathbf{Grp}</math> i <math>\mathbf{Set}^{\mathbb{T}}</math>.
  
  
Linia 105: Linia 89:
  
  
Monady są wykorzystywane m.in. w funkcyjnym języku programowania Haskell. Struktura monady doskonale nadaje się do specyfikacji: (a) operacji wejścia/wyjścia; (b) wyłapywania wyjątków (takich jak np. dzielenie przez zero); (c) interfejsów graficznych. Formalnie, monada w Haskellu jest pewnym typem danych, bardzo czytelnie opisuje tę sytuację w przypadku monady I/O (wejścia wyjścia) fragment wykładu Paradygmaty programowania. Tenże Haskellowy typ danych jest tak naprawdę inastancją klasy Monad. Ta klasa wyposażona jest zawsze w dwie funkcje: <math>>>=</math> i return:
+
Monady są wykorzystywane m.in. w funkcyjnym języku programowania Haskell. Struktura monady doskonale nadaje się do specyfikacji: (a) operacji wejścia/wyjścia; (b) wyłapywania wyjątków (takich jak np. dzielenie przez zero); (c) interfejsów graficznych. Formalnie, monada w Haskellu jest pewnym typem danych, bardzo czytelnie opisuje tę sytuację w przypadku monady I/O (wejścia/wyjścia) fragment wykładu Paradygmaty programowania. Tenże Haskellowy typ danych jest tak naprawdę inastancją klasy Monad. Ta klasa wyposażona jest zawsze w dwie funkcje: <math>>>=</math> i return:
  
\begin{verbatim}
+
<nowiki>
 
class Monad m where
 
class Monad m where
 
     return :: a -> m a
 
     return :: a -> m a
 
     (>>=) :: m a -> (a -> m b) -> m b
 
     (>>=) :: m a -> (a -> m b) -> m b
\end{verbatim}
+
</nowiki>
  
Funkcja return oczywiście pełni rolę jedności monady, zaś operacja >>= zawiera całą informację o funktorze indukującym monadę i mnożeniu. Dokładniej mówiąc, funktor indukujący monadę oznacza się jako
+
Funkcja return oczywiście pełni rolę jedności monady, zaś operacja >>= zawiera całą informację o funktorze indukującym monadę i mnożeniu. Dokładniej mówiąc, funktor indukujący monadę oznacza się jako:
  
\begin{verbatim}
+
<nowiki>map :: (t -> u) -> (M t -> M u)</nowiki>,
map :: (t -> u) -> (M t -> M u)
 
\end{verbatim}
 
  
zaś mnożenie monady jako
+
zaś mnożenie monady jako:
  
\begin{verbatim}
+
<nowiki>join :: M(Mt) -> Mt</nowiki>.
join :: M(Mt) -> Mt
 
\end{verbatim}
 
  
 
Wtedy mamy następującą listę zależności pomiędzy tymi operacjami:
 
Wtedy mamy następującą listę zależności pomiędzy tymi operacjami:
  
\begin{verbatim}
+
<nowiki> (map f) m</nowiki> jest tym samym, co:  <nowiki>m >>= (\x -> return (f x))</nowiki>,
(map f) m  jest tym samym, co:  m >>= (\x -> return (f x)) join m
+
 
jest tym samym, co:  m >>= (\x -> x) m >>= f   jest tym samym,
+
<nowiki>join m</nowiki> jest tym samym, co:  <nowiki>m >>= (\x -> x)</nowiki>,
co:  join ((map f) m)
+
 
\end{verbatim}
+
<nowiki>m >>= f</nowiki>  jest tym samym, co:  <nowiki>join ((map f) m)</nowiki>.

Aktualna wersja na dzień 12:12, 27 lis 2006

Ważną klasę kategorii tworzą takie, których obiektami są zbiory z pewną dodatkową strukturą algebraiczną, zaś morfizmami - funkcje, które tą strukturę zachowują. Takie kategorie moglibyśmy z powodzeniem nazwać kategoriami algebraicznymi nad . Rozważania nad odpowiednią definicją algebraiczności doprowadzą nas do odkrycia ciekawej struktury kategoryjnej: monady, która jest niejako ukryta w każdym sprzężeniu między funktorami.


W poszukiwaniu kategorii algebraicznych

Z pewnością na kategorie algebraiczne nie nadają się wszystkie kategorie konkretne, które charakteryzują się tym, że posiadają funktor zapominania o kodziedzinie (Definicja 5.9). Nawet, gdybyśmy dodatkowo zażądali, aby tenże funktor zapominania miał lewe sprzężenie , które wskazuje jak odbudować w sposób wolny zapomnianą strukturę, to sytuacja ciągle nie jest zadowalająca. Na przykład, funktor zapominania ma lewe sprzężenie, a my nie chcemy traktować jako kategorii algebraicznej. Ale stąd warto rozpocząć poszukiwania, gdyż wszelkie kategorie, od których oczekujemy algebraiczności, jak czy , posiadają lewe sprzężenia do funktorów zapominania, które przypisują zbiorom odpowiednie algebry wolne.

Niech zatem i będą sprzężone: . Rozważmy funktor będący złożeniem funktorów i : . Jedność sprzężenia ma zatem typ . Informacje o kojedności również nietrudno zakodować w terminach funktora , bowiem skoro , to (przypomnijmy definicję: ), a co za tym idzie: . Transformacja jest naturalna; jeśli oznaczymy ją jako , to dostajemy . Diagramy trójkątne charakteryzujące sprzężenie z Twierdzenia 9.3 dają nam następujące komutujące trójkąty:

Tk-11.1.png

Naturalność daje dodatkowo komutujący diagram (Zadanie Zadanie 11.1).

Tk-11.2.png

Widzimy więc, że po wprowadzeniu endofunktora i prostym przekształceniu sprzężenia, od którego pochodzi, pojawiła się pewna struktura. Dobrze wyróżnić je definicją i dokładnie zbadać:


Definicja 11.1 [monada]

Monadą w kategorii nazywamy trójkę , gdzie jest funktorem, zaś i - tranformacjami naturalnymi takimi, że:

tzn. takimi, że powyższe trzy diagramy komutują.


Uwaga
Dla sprzężenia , monada nazywa się monadą indukowaną przez . Jak każde pojęcie kategoryjne, monada ma swój odpowiednik dualny: komonadę. Każde sprzężenie indukuje komonadę .


Czy struktura monady nad kategorią zawsze pochodzi od pewnego sprzężenia? Zauważmy, że aby odpowiedzieć na to pytanie musimy przede wszystkim odnaleźć drugą kategorię i dwa funktory , , takie, że . Okazuje się, że odpowiedź jest pozytywna: każda monada pochodzi od pewnego sprzężenia, a tak naprawdę istnieje wiele sprzężeń indukujących daną monadę. Te sprzężenia tworzą oddzielną kategorię. My wskażemy obiekt końcowy tej kategorii.

Dla monady nad definiujemy -algebrę jako parę , gdzie , oraz:

Tk-11.3.png

Morfizmem -algebr jest morfizm taki, że poniższy diagram komutuje:

Tk-11.4.png

Kategorię -algebr będziemy oznaczać . Nazywamy ją od nazwisk odkrywców: kategorią Eilenberga - Moore'a. Zobaczmy, że istnieje naturalny funktor zapominania definiowany jako:


Z drugiej strony, dla dowolnego , para jest tak zwaną wolną -algebrą, oznaczaną jako . Operacja rozszerza się do funktora , jeśli położymy:

W Zadaniu 11.2 pokażemy, że dla dowolnego jest rzeczywiście algebrą, zaś w Zadaniu następnym nr 11.3 udowodnimy, że


Twierdzenie 11.2 [każda monada pochodzi od sprzężenia]

Monada indukowana przez to sprzężenie jest monadą .

Przykłady monad

  • Niech będzie częściowym porządkiem. Monadą nad jest funkcja monotoniczna taka, że oraz dla dowolnego . (Te dwie nierówności wyrażają typu transformacji i . Diagramy w definicji monady komutują, bo relacja jest przechodnia.) Powyższe zależności dla implikują, że , czyli . Funkcja jest więc idempotentna i traktuje się ją zwykle jako operację domknięcia.
  • Kowariantny funktor potęgowy indukuje monadę, gdzie jest zanurzeniem , zaś mnożenie jest sumą zbiorów: . Własności tej monady bardzo dobrze podsumowują teoriomnogościowe własności sumy w połączeniu z notacją służącą do konstrukcji zbiorów. W Zadaniu 11.5 przedstawiamy dowód, że jest monadą nad . Identyczny dowód pokazuje, że (kowariantny funktor potęgowy na zbiorach skończonych) indukuje monadę nad .
  • Niech będzie monoidem. Funktor wraz z transformacjami naturalnymi oraz definiuje monadę . -algebry to -automaty, które poznaliśmy w Zadaniu 1.11. Szczegóły tej konstrukcji opisujemy w Zadaniu 11.6.
  • Funktor z Przykładu 5.3 jest lewym sprzężeniem do funktora zapominania . Złożenie jest funktorem, który zbiorowi przypisuje będący zbiorem skończonych słów nad . Jedność jest oczywiście zanurzeniem elementu w listę jednoelementową . Jak zdefiniować mnożenie w tej monadzie? Jako proponujemy transformację naturalną, która liście list:

przypisze listę:

Łatwo pokazać, że jest monadą nad . Okazuje się, że kategoria -algebr jest równoważna z kategorią monoidów .

  • Rozważmy sprzężenie dla funktora wolnego i funktora zapominania . Niech będzie monadą indukowaną przez to sprzężenie. A zatem jest zbiorem podkładowym wolnej grupy nad zbiorem (czy Czytelnik pamięta z kursu algebry, jak taka grupa jest tworzona?). Jeśli jest -algebrą, dostaniemy strukturę grupy na , jeśli zdefiniujemy działanie jako , gdzie jest włożeniem generatorów, tzn. , , zaś jest mnożeniem w wolnej grupie nad . Za pomocą tej konstrukcji dostajemy funktor . Odwrotnie, jeśli jest grupą, to homomorfizm , definiowany jako mnożenie liter słowa z za pomocą działania grupy , daje wraz z -algebrę , a zatem obiektową część funktora typu . Uwaga! Para funktorów, których szkic konstrukcji pokazaliśmy, stanowi równoważność kategorii i .


Dwa ostatnie przykłady wskazują nam to, czego szukaliśmy od początku wykładu: odpowiedzi na pytanie, jakie kategorie chcemy uważać za algebraiczne!

Uwaga
Slogan: Kategoria jest algebraiczna, jeśli jest równoważna kategorii dla pewnej monady nad . W ten sposób algebraiczne są grupy, grupy abelowe, monoidy, pierścienie, algebry Boole'a, półkraty, zwarte przestrzenie Hausdorffa. Przykładem kategorii, która nie jest algebraiczna są zupełne algebry Boole'a.


Monady w Haskellu

Monady są wykorzystywane m.in. w funkcyjnym języku programowania Haskell. Struktura monady doskonale nadaje się do specyfikacji: (a) operacji wejścia/wyjścia; (b) wyłapywania wyjątków (takich jak np. dzielenie przez zero); (c) interfejsów graficznych. Formalnie, monada w Haskellu jest pewnym typem danych, bardzo czytelnie opisuje tę sytuację w przypadku monady I/O (wejścia/wyjścia) fragment wykładu Paradygmaty programowania. Tenże Haskellowy typ danych jest tak naprawdę inastancją klasy Monad. Ta klasa wyposażona jest zawsze w dwie funkcje: i return:

class Monad m where return :: a -> m a (>>=) :: m a -> (a -> m b) -> m b

Funkcja return oczywiście pełni rolę jedności monady, zaś operacja >>= zawiera całą informację o funktorze indukującym monadę i mnożeniu. Dokładniej mówiąc, funktor indukujący monadę oznacza się jako:

map :: (t -> u) -> (M t -> M u),

zaś mnożenie monady jako:

join :: M(Mt) -> Mt.

Wtedy mamy następującą listę zależności pomiędzy tymi operacjami:

(map f) m jest tym samym, co: m >>= (\x -> return (f x)),

join m jest tym samym, co: m >>= (\x -> x),

m >>= f jest tym samym, co: join ((map f) m).