Quick
index
main
eev
maths
blogme
dednat4
littlelangs

emacs
lua
(la)tex
fvwm
tcl
forth
icon
debian
debian-rj
w32/AIX
politics
personal
heroes
irc
contact

Some notes on monads (Edrx, 2007)

2007oct28: You are not expected to understand this!
I am only using this file to store some diagrams about monads, in DNC notation (see my math page)...

Quick index:
1. 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

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

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

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

5. 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'

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