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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

==Zadanie 11.1==

Udowodnij, że jeśli FG oraz T=GF, to naturalność ε implikuje, że poniższy diagram:

komutuje.

Rozwiązanie:


==Zadanie 11.2==

Niech 𝕋=(T,η,μ) będzie monadą nad 𝐂. Pokaż że dla dowolnego X𝐂0, para (TX,μX) jest 𝕋-algebrą.

Wskazówka:
Rozwiązanie:


==Zadanie 11.3==

Udowodnij Twierdzenie 11.2.

Wskazówka:
Rozwiązanie:

==Zadanie 11.4==

Niech 𝕋=(T:PP,1PT,TTT) będzie monadą nad posetem (P,). Pokaż, od jakiego sprzężenia pochodzi ta monada.

Wskazówka:
Rozwiązanie:


==Zadanie 11.5==

Udowodnij, że (𝒫,{...},) jest monadą nad 𝐒𝐞𝐭 dla kowariantnego funktora potęgowego 𝒫:𝐒𝐞𝐭𝐒𝐞𝐭.

Rozwiązanie:

==Zadanie 11.6==

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

M×():𝐒𝐞𝐭𝐒𝐞𝐭

wraz z transformacjami naturalnymi ηX(x):=(e,x) oraz μX(m2*(m1,x)):=(m2*m1,x) definiuje monadę 𝕋, której 𝕋-algebrami są M-automaty.

Rozwiązanie:

==Zadanie 11.7==

Udowodnij, że funktor ():𝐏𝐨𝐬𝐏𝐨𝐬, który dodaje do posetu nowy element najmniejszy wraz z funktorem zapominania indukuje monadę nad 𝐏𝐨𝐬. Jakie są algebry dla tej monady?

Wskazówka:
Rozwiązanie:

==Zadanie 11.8==

Wykaż, że algebrami dla monady nad 𝐒𝐞𝐭 indukowanej przez kowariantny funktor potęgowy 𝒫 są półkraty zupełne i homomorfizmy tych półkrat (tzn. funkcje zachowujące dowolne suprema).

Wskazówka:
Rozwiązanie:


==Zadanie 11.9==

Wykaż, że sprzężenie F𝕋G𝕋, od którego pochodzi monada 𝕋 jest obiektem końcowym pewnej kategorii, w następującym sensie: jeśli FG dla F:𝐂𝐃:G jest sprzężeniem, które indukuje 𝕋, to istnieje dokładnie jeden funktor K:𝐃𝐂𝕋 taki, że dwa poniższe diagramy komutują:

Taki funktor K:𝐃𝐂𝕋 nazywa się funktorem porównawczym (ang. comparison functor) dla sprzężenia FG.

Uwaga
Dowodzi się, że sprzężenie F𝕋G𝕋 rzeczywiście nie jest jedynym, które indukuje 𝕋, a zatem K w ogólności nie trywializuje się. Okazuje się, że dla 𝐂 można skonstruować tak zwaną kategorię Kliesliego oznaczaną 𝐂𝕋, która jest w ogólności różna od 𝐂𝕋 i parę funktorów F𝕋:𝐂𝐂𝕋:G𝕋 z F𝕋G𝕋, gdzie to sprzężenie indukuje 𝕋. 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:
Rozwiązanie: