[INCLUDE TH/speedbar.blogme] [SETFAVICON dednat4/dednat4-icon.png] [# (defun c () (interactive) (find-blogme3-sh0-if "2007dnc-monads")) ;; http://angg.twu.net/2007dnc-monads.html ;; file:///home/edrx/TH/L/2007dnc-monads.html ;; (find-2005oct20seminarfile "") ;; (find-2005oct20seminar "") ;; (find-2005oct20seminar "" "original-motivation-2") ;; (find-2005oct20seminarpage 1) ;; (find-2005oct20seminarpage 31) ;; ;; «glyphs» ;; (find-TH "2007diffcats" "glyphs") ;; (eev-math-glyphs-edrx) ;; (add-to-alist 'eev-math-glyphs-name-to-char '("Delta" . 332660)) ;; (add-to-alist 'eev-math-glyphs-name-to-char '("eta" . 332727)) ;; (add-to-alist 'eev-math-glyphs-name-to-char '("mu" . 332732)) ;; (eev-math-glyphs-set 'eev-glyph-face-math "nabla" "na" "¿") ;; (eev-math-glyphs-set 'eev-glyph-face-math "Delta" "DD" "¿") ;; (eev-math-glyphs-set 'eev-glyph-face-greek "theta" "te" "") ;; (eev-math-glyphs-set 'eev-glyph-face-greek "eta" "et" "") ;; (eev-math-glyphs-set 'eev-glyph-face-greek "nu" "nu" "Û") ;; (eev-math-glyphs-set 'eev-glyph-face-greek "mu" "mu" "Û") ;; (find-glyphashtml-links "na") ;; (find-glyphashtml-links "DD") ;; (find-glyphashtml-links "te") ;; (find-glyphashtml-links "et") ;; (find-glyphashtml-links "nu") ;; (find-glyphashtml-links "mu") ;; (find-glyphashtml-links "ee") #] [lua: -- (eev-math-glyphs-edrx) -- (find-blogme3file "anggdefs.lua" "eev_math_glyphs_edrx =") eev_math_glyphs_edrx() sgmlify_table["\17"] = "⟦" sgmlify_table["\16"] = "⟧" sgmlify_table["\191"] = "Δ" sgmlify_table["\04"] = "δ" sgmlify_table["\05"] = "ε" sgmlify_table["\20"] = "η" sgmlify_table["\219"] = "μ" sgmlify_re = "([\1-\8\12\14-\31\128-\254])" -- (find-blogme3file "anggdefs.lua" " sec ") io.stdout:setvbuf("no") ] [htmlize [J Some notes on monads (Edrx, 2007)] [P 2007oct28: You are not expected to understand this! [BR] I am only using this file to store some diagrams about monads, in DNC notation (see my [__ maths math page])...] [WITHINDEX [# # «.monads» (to "monads") # «.coherence» (to "coherence") # «.manes» (to "manes") # «.kleisli» (to "kleisli") # «.eilenberg-moore» (to "eilenberg-moore") # «.resolutions» (to "resolutions") #] [RULE ----------------------------------------] [tsec «monads» (to ".monads") [++N]. Monads ============= Fix a monoid M. Notation: elements of M will be called a,b,c,... Our archetypal monad is based on the functor (×M):Set->Set. A monad over a functor T (T=(×M) for us) is triple (T,,Û) where  and Û are natural transformations:  Û . X -----> TX <----- TTX x |---> x,1 x,ab <---| x,a,b  and Û have to obey certain equations: (T;Û)=(T;Û)=id and (ÛT;Û)=(TÛ;Û). If we downcase those equations using x=>x,a as the archetype they become exactly ýa.a1=1a=a and ýa,b,c.a(bc)=(ab)c. TX --T--> TTX --Û--> TX x,a |---> x,a,1 |----> x,a1 TX --T--> TTX --Û--> TX x,a |---> x,1,a |----> x,1a TX ---------id------> TX x,a |----------------> x,a TTTX --ÛT--> TTX --Û--> TX x,a,b,c |---> x,a,bc |---> x,a(bc) TTTX --TÛ--> TTX --Û--> TX x,a,b,c |---> x,ab,c |---> x,(ab)c Here are square conditions for the two natural transformations. For any objects X and Y and any morphism x|->y, X X -----> TX x |---> x,1 | | - - | f | Tf | | v v v v Y -----> TY y |---> y,1 Y ÛX TX <---- TTX x,ab <---| x,a,b | | - - | Tf | TTf | | v v v v TY <---- TTY y,ab <---| y,a,b ÛY ] [tsec «coherence» (to ".coherence") [++N]. Where our notation fails =============================== Our notation based on (×M) is not totally faithful - sometimes it suggests that two morphisms are the same when they may be different... The square below does not need to commute. TTTX x,a,b,cd / ^ \ ^ TÛX / \ ÛTTX / \ v \ v / TTX TTTTX x,ab,cd x,a,b,c,d ^ / ^ \ ÛTX \ / TTÛX \ / \ v / v TTTX x,ab,c,d But all canonical morphisms from T^nX to TX are equal - ] [tsec «manes» (to ".manes") [++N]. A presentation of monads due to Manes ============================================ A monad can also be given by an object function S and operations f f# (X ---> S(Y)) |-> (S(X) ----> S(Y) (x|->y,a) |-> (x,b|->y,ab) X X |--> (X ----> S(X)) x -.> (x|->x,1) Subject to: (X)^# = 1_S(X) X;f^# = f f^#;g^# = (f;g^#)^# Let's expand these equations: X x|->x,1 ------ ---------- (X)^# = 1_S(X) x,a|->x,1a = x,a|->x,a f x|->y,a --- ---------- X f^# x|->x,1 x,b|->y,ab -------- ------------------- X;f^# = f x|->y,a1 = x|->y,a g y|->z,a --- ---------- f g f g^# x|->y,c y|->z,a x|->y,c y,b|->z,ab --- --- ------- ---------- ---------- ------------------- f^# g^# f;g^# x,d|->y,cd y,b|->z,ab x|->z,ac --------- --------- ----------------------- ----------- f^#;g^# = (f;g^#)^# x,d|->z,acd = x,d|->z,acd ] [tsec «kleisli» (to ".kleisli") [++N]. The Kleisli category of a monad ====================================== Notation: x:xT x xT xTT - - - | | f \ f | v v f;TG;mu | y:yT y yT yTT | - - - | | g g \ \ Tg v v v v z:zT z zT <-| zTT mu The adjunction: x':x'T <===== x' - - f;eta | <--| | v v x:xT <====== x' - - g | <--| | g g | |--> | g v v y:yT ======> yT - - h | |--> | Th;mu v v y':y'T ====> y'T ] [tsec «eilenberg-moore» (to ".eilenberg-moore") [++N]. The Eilenberg-Moore category of a monad ============================================== The adjunction: (x'T <--| x'TT) <=== x' - - - f;eta | | <-| | f v v v (xT <---| xTT) <==== x --| ---| - Tg;\aa / / <--| | g h / / |--> | eta;h v \aa v v (y <---| yT) <============== y - - - k | | |--> | k v v v (y' <--| y'T) <============= y' ] [tsec «resolutions» (to ".resolutions") [++N]. The category of resolutions for a monad ============================================== The Kleisli category is the initial resolution, the Eilenbeg-Moore category is the final one. Notation: O[yL] is not necessarily an image by L - in some arrows it just just an arbitrary object of the "other category" in an adjunction diagram. Also: O[yT] = O[yLR]. /=== x:xT <==\ // - \\ // | \\ // v \\ // /== y:yT ===\ \\ // // \\ \\ // // \\ \\ \/ // \\ \\ xL <========================== x - \\// \\ //- | /\\ \// | v \/ \\ //v v yL ===\\==================//=> yT \\ \\ // /\ \\ \\ // // \\ \/ \/ // \\ (xT <-| xTT) // \\ - - // \\ | | // \/ v v // (yT <-| yTT) The functor x:xT => xL acts on objects as L and on morphisms as the transposition. The functor yL => (yT <-| yTT) acts on objects as R (plus the counit: O[yL] |-> (yL <-| yLRL) |-> (yLR <-| yLRLR)) and on morphisms as R. ] ]] [# # Local Variables: # coding: raw-text-unix # modes: (fundamental-mode blogme-mode) # End: #]