% (find-angg "LATEX/2009dnc-monads.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009dnc-monads.tex && latex    2009dnc-monads.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009dnc-monads.tex && pdflatex 2009dnc-monads.tex"))
% (eev "cd ~/LATEX/ && Scp 2009dnc-monads.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (defun d () (interactive) (find-dvipage "~/LATEX/2009dnc-monads.dvi"))
% (find-dvipage "~/LATEX/2009dnc-monads.dvi")
% (find-pspage  "~/LATEX/2009dnc-monads.pdf")
% (find-pspage  "~/LATEX/2009dnc-monads.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2009dnc-monads.ps 2009dnc-monads.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2009dnc-monads.ps 2009dnc-monads.dvi && ps2pdf 2009dnc-monads.ps 2009dnc-monads.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage  "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2009dnc-monads.pdf" (ee-twupfile "LATEX/2009dnc-monads.pdf") 'over)
% (ee-cp "~/LATEX/2009dnc-monads.pdf" (ee-twusfile "LATEX/2009dnc-monads.pdf") 'over)

\documentclass[oneside]{book}
\usepackage[latin1]{inputenc}
\usepackage{edrx08}       % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty"  -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex   % (find-dn4ex "edrxheadfoot.tex")
\begin{document}

\input 2009dnc-monads.dnt

%
% (eedn4-51-bounded)

%Index of the slides:
%\msk
% To update the list of slides uncomment this line:
%\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")

% (find-es "xypic" "two-and-three")
% (find-LATEX "2008comprcat.tex" "dtt-adjunctions")

\def\sm#1{\begin{smallmatrix}#1\end{smallmatrix}}
\def\catAK{{\catA_T}}
\def\catAEM{{\catA^T}}
\def\KOBJ#1#2{[#1 \diagxyto/-->/<150> #2]}
\def\EMOBJT#1#2{[#1 \diagxyto/<-/<150>^{#2} T#1]}

If $L$ and $R$ are (proto-)functors going in opposite directions
between two (proto-)categories, say,
%
$$\catB \two/<-`->/<150>^L_R \catA$$
%
then a {\sl proto-adjunction}, $L \dashv R$, is an 8-uple,
%
$$(\catA, \catB, L, R, \flat, \sharp, \eta, \ee)$$
%
that we draw as:
%
%D diagram adj1
%D 2Dx     100    +30     +30   +30
%D 2D  100 S1B   LA <---| A     T0A
%D 2D       |     |       |      |
%D 2D       |     |  <->  |      |
%D 2D       v     v       v      v
%D 2D  +30 S0B    B |---> RB    T1A
%D 2D                           
%D 2D  +20     \catB <=> \catA  
%D 2D
%D (( S1B .tex= LRB S0B .tex= B
%D    S1B S0B -> .plabel= l _B
%D ))
%D (( T0A .tex= A T1A .tex= RLA
%D    T0A T1A -> .plabel= r \eta_A
%D ))
%D (( LA A B RB
%D    @ 0 @ 1 <-|
%D    @ 0 @ 2 -> .PLABEL= _(0.43) f^\flat
%D    @ 0 @ 2 -> .PLABEL= _(0.57) g
%D    @ 1 @ 3 -> .PLABEL= ^(0.43) f
%D    @ 1 @ 3 -> .PLABEL= ^(0.57) g^\sharp
%D    @ 0 @ 3 harrownodes nil 20 nil <-| sl^
%D    @ 0 @ 3 harrownodes nil 20 nil |-> sl_
%D    @ 2 @ 3 |-> 
%D ))
%D (( \catB \catA <- sl^ .plabel= a L
%D    \catB \catA -> sl_ .plabel= b R
%D ))
%D enddiagram
%D
$$\diag{adj1}$$

% [Transpositions, unit, counit]

There is some redundancy in this definition, as we may reconstruct
some of the entities $\flat$, $\sharp$, $\eta$, $\ee$ in terms of the
other ones:
%
%D diagram adj-redundancy
%D 2Dx     100     +30    +30     +30     +30     +30
%D 2D  100                U0 <--| U1                 
%D 2D                   / |        |                 
%D 2D  +15              | |  <--|  |                 
%D 2D                   | v        v                 
%D 2D  +15              | U2 <--| U3                 
%D 2D                   | |                          
%D 2D  +15 L0 <--| L1   \ |               R0 <--| R1            
%D 2D      |        |    vv               |        |            
%D 2D  +15 |  <--|  |     U4      D0      |  |-->  | 
%D 2D      v        v              | \    v        v 
%D 2D  +15 L2 |--> L3              | |    R2 |--> R3 
%D 2D                              v |    
%D 2D  +15                D1 |--> D2 |    
%D 2D                     |        | |               
%D 2D  +15                |  |-->  | /               
%D 2D                     v        vv                
%D 2D  +15                D3 |--> D4                 
%D 2D
%D 2D  +15
%D 2D
%D (( U0 .tex= LA  U1 .tex= A
%D    U2 .tex= LRB U3 .tex= RB
%D    U4 .tex= B
%D    U0 U1 <-|
%D    U0 U4 -> .slide= -16pt .plabel= l \sm{f^\flat\;:=\\Lf;_B}
%D    U0 U2 -> .plabel= l Lf
%D    U1 U3 -> .plabel= r f
%D    U0 U3 harrownodes nil 20 nil <-|
%D    U2 U3 |->
%D    U2 U4 -> .plabel= l _B
%D ))
%D ((             D0 .tex= A
%D    D1 .tex= LA D2 .tex= RLA
%D    D3 .tex= B  D4 .tex= RB
%D    D0 D2 -> .plabel= r \eta_A
%D    D1 D2 |->
%D    D1 D3 -> .plabel= l g
%D    D2 D4 -> .plabel= r Rg
%D    D0 D4 -> .slide= 16pt .plabel= r \sm{g^\sharp\;:=\\\eta_A;Rg}
%D    D1 D4 harrownodes nil 20 nil |->
%D    D3 D4 |->
%D    D3 D4 -> .plabel= l _B
%D ))
%D (( L0 .tex= LRB L1 .tex= RB
%D    L2 .tex= B   L3 .tex= RB
%D    L0 L1 <-|
%D    L0 L2 -> .plabel= l \sm{_B\;:=\\{\id_{RB}}^\flat}
%D    L1 L3 -> .plabel= r \id_{RB}
%D    L2 L3 |->
%D    L0 L3 harrownodes nil 20 nil <-|
%D ))
%D (( R0 .tex= LA R1 .tex= A
%D    R2 .tex= LA R3 .tex= RLA
%D    R0 R1 <-|
%D    R0 R2 -> .plabel= l \id_{LA}
%D    R1 R3 -> .plabel= r \sm{\mu_A\;:=\\{\id_{LA}}^\sharp}
%D    R2 R3 |->
%D    R0 R3 harrownodes nil 20 nil |->
%D ))
%D enddiagram
%D
$$\diag{adj-redundancy}$$

A {\sl protomonad} for a proto-endofunctor $T: \catA \to \catA$ is a
4-uple:
%
$$(\catA, T, \eta, \mu)$$
%
that we draw as:
%
$$A \diagxyto/->/<150>^{\eta_A} TA \diagxyto/<-/<150>^{\mu_A} TTA$$

% [unit, multiplication]

A {\sl proto-comonad} for a proto-endofunctor $S: \catB \to \catB$ is a
4-uple:
%
$$(\catB, S, , )$$
%
that we draw as:
%
$$B \diagxyto/<-/<150>^{_B} SB \diagxyto/->/<150>^{_B} SSB$$

% [counit, comultiplication]

Each proto-adjunction induces both a proto-monad and a proto-comonad.
We draw all these together as:
%
%D diagram adj-with-monads-1
%D 2Dx     100    +30     +30   +30
%D 2D  100 S2B
%D 2D       ^
%D 2D       |
%D 2D       |
%D 2D  +30 S1B   LA <---| A     T0A
%D 2D       |     |       |      |
%D 2D       |     |  <->  |      |
%D 2D       v     v       v      v
%D 2D  +30 S0B    B |---> RB    T1A
%D 2D                            ^
%D 2D  +15                       |
%D 2D                            |
%D 2D  +15     \catB <=> \catA  T2A
%D 2D
%D (( S2B .tex= LRLRB S1B .tex= LRB S0B .tex= B
%D    S2B S1B <- .plabel= l _B
%D    S1B S0B -> .plabel= l _B
%D ))
%D (( T0A .tex= A T1A .tex= RLA T2A .tex= RLRLA
%D    T0A T1A -> .plabel= r \eta"A
%D    T1A T2A <- .plabel= r \mu"A
%D ))
%D (( LA A B RB
%D    @ 0 @ 1 <-|
%D    @ 0 @ 2 -> .PLABEL= _(0.43) f^\flat
%D    @ 0 @ 2 -> .PLABEL= _(0.57) g
%D    @ 1 @ 3 -> .PLABEL= ^(0.43) f
%D    @ 1 @ 3 -> .PLABEL= ^(0.57) g^\sharp
%D    @ 0 @ 3 harrownodes nil 20 nil <-| sl^
%D    @ 0 @ 3 harrownodes nil 20 nil |-> sl_
%D    @ 2 @ 3 |-> 
%D ))
%D (( \catB \catA <- sl^ .plabel= a L
%D    \catB \catA -> sl_ .plabel= b R
%D ))
%D enddiagram
%D
$$\diag{adj-with-monads-1}$$

We define $\mu_A := R({\id_{RLA}}^\flat)$ and $_B := L({\id_{LRB}}^\sharp)$:
%:
%:                \id_{RLA}:RLA->RLA                    \id_{LRB}:LRB->LRB
%:           --------------------------              ---------------------------
%:           {\id_{RLA}}^\flat:LRLA->LA              {\id_{LRB}}^\sharp:RB->RLRB
%:  --------------------------------------    -------------------------------------
%:  \mu_A:=R({\id_{RLA}}^\flat):RLRLA->RLA    _B:=L({\id_{LRB}}^\sharp):LRB->LRLRB
%:
%:  ^def-muA                                  ^def-deltaB
%:
$$\ded{def-muA} \qquad \ded{def-deltaB}$$

We have seen how a proto-adjunction induces a proto-monad; now we will
see how a proto-monad induces {\sl two} proto-adjunctions.

\msk

{\bf The Kleisli proto-adjunction}

\ssk

The {\sl Kleisli proto-category} of a proto-monad $(\catA, T, \eta,
\mu)$ is the proto-category:
%
$$\catAK := ((\catAK)_0, \Hom_\catAK, \id_\catAK, ¢_\catAK)$$
%
where $(\catAK)_0$ is equal to $\catA_0$, ut we write the objects of
$(\catAK)_0$ in a funny way: an object $A Ý \catA$ becomes
%
$$\KOBJ{A}{TA}$$
%
when we regard it as an object of $(\catAK)_0$.

A morphism in $\Hom_\catAK(\KOBJ{A}{TA}, \KOBJ{C}{TC})$ is just a map
$f:A \to TC$ in $\Hom_\catA(A, TC)$. We write it as $[f]:
\Hom_\catAK(\KOBJ{A}{TA}, \KOBJ{C}{TC})$ to stress that its (formal)
type is different from $f$.

The identity operation, $\id_\catAK$, is the $\eta$ (the ``unit'') of
the monad in disguise:
%
$$\id_\catAK(\KOBJ{A}{TA}) := [\eta_\catA]$$

Note that:
%:
%:  A:\catA_0
%:  ------------
%:  \eta_A:A->TA
%:  -----------------------------------
%:  [\eta_A]:\KOBJ{A}{TA}->\KOBJ{A}{TA}
%:  ---------------------------------------------------------------Ð{ren}
%:  \id_\catAK(\KOBJ{A}{TA}):\Hom_\catAK(\KOBJ{A}{TA},\KOBJ{A}{TA})
%:
%:  ^typing-id-kleisli
%:
$$\ded{typing-id-kleisli}$$

The composition, $¢_\catAK$, needs a trick: if $f:A \to TC$ and $g: C
\to TE$ then $[f];[g] := [f;Tg;\mu_E]$. In diagrams:
%
%D diagram kleisli-id-and-comp
%D 2Dx     100    +60   +30    +30
%D 2D  100 A0     A{}
%D 2D       |        \
%D 2D       |         \
%D 2D       v          v
%D 2D  +30 A1           TA
%D 2D
%D 2D  +30 KA     A
%D 2D       |       \
%D 2D       |        \
%D 2D       v         v
%D 2D  +30 KC     C ..> TC
%D 2D       |       \      \
%D 2D       |        \      \
%D 2D       v         v      v
%D 2D  +30 KE     E ..> TE <-- TTE
%D 2D
%D (( A0 .tex= \usebox{\myboxa}
%D    A1 .tex= \usebox{\myboxa}
%D    A0 A1 -> .plabel= r \id=[\eta_A]
%D ))
%D (( A{} TA -> .plabel= r \eta_A
%D ))
%D (( KA .tex= \usebox{\myboxa}
%D    KC .tex= \usebox{\myboxc}
%D    KE .tex= \usebox{\myboxe}
%D    KA KC -> .plabel= r [f]
%D    KC KE -> .plabel= r [g]
% D    KA KE -> .slide= 25pt .plabel= r \sm{[f];[g]\;:=\\"[f;Tg;\mu_E]}
%D    KA KE -> .slide= 27pt .plabel= r \sm{[f];[g]\;:=\\"[f;Tg;\mu_E]}
%D ))
%D (( A TC -> .plabel= r f
%D    C TC -->
%D    C TE -> .plabel= r g   TC TTE -> .plabel= r Tg
%D    E TE --> TE TTE <- .plabel= b \mu_E
%D ))
%D
%D enddiagram
%D
$$\savebox{\myboxa}{$\KOBJ{A}{TA}$}
  \savebox{\myboxc}{$\KOBJ{C}{TC}$}
  \savebox{\myboxe}{$\KOBJ{E}{TE}$}
  \diag{kleisli-id-and-comp}
$$

The dashed arrow in, say, $\KOBJ{A}{TA}$, is to suggest three things:

that morphisms in $\catAK$ follow the dirrection of the
`$\diagxyto/-->/<150>$',

that a morphism $A \to TA$ is not part of the definition of an object
$\KOBJ{A}{TA}$,

that the `$\diagxyto/-->/<150>$' is the ghost of the unit of the monad
--- the unit would go from $A$ to $TA$, but it is not used in the
definitions; nevertheless, its memory remains.

\msk

We can draw the Kleisli (proto-)adjunction as:
%
%D diagram kleisli-adj
%D 2Dx     100    +50     +30   +25
%D 2D  100 S2B
%D 2D       ^
%D 2D       |
%D 2D       |
%D 2D  +30 S1B   KA <---| A     T0A
%D 2D       |     |       |      |
%D 2D       |     |  <->  |      |
%D 2D       v     v       v      v
%D 2D  +30 S0B   KC |---> TC    T1A
%D 2D                            ^
%D 2D  +15                       |
%D 2D                            |
%D 2D  +15    \catAK <=> \catA  T2A
%D 2D
%D (( KA .tex= \usebox{\myboxa}
%D    KC .tex= \usebox{\myboxc}
%D    KA A <-|
%D    KA KC -> .PLABEL= _(0.41) f^\flat:=[f]
%D    KA KC -> .PLABEL= _(0.59) [g]
%D     A TC -> .PLABEL= ^(0.41) f
%D     A TC -> .PLABEL= ^(0.59) [g]^\sharp:=g
%D    KA TC harrownodes nil 20 nil <-| sl^
%D    KA TC harrownodes nil 20 nil |-> sl_
%D    KC TC |-> 
%D ))
%D (( \catAK \catA
%D    @ 0 @ 1 <- sl^ .plabel= a L_T
%D    @ 0 @ 1 -> sl_ .plabel= b R_T
%D ))
%D (( S2B .tex= \usebox{\myboxe}
%D    S1B .tex= \usebox{\myboxd}
%D    S0B .tex= \usebox{\myboxc}
%D    S2B S1B <- .plabel= l \mu?
%D    S1B S0B -> .plabel= l \cc
%D ))
%D (( T0A .tex= A
%D    T1A .tex= TA
%D    T2A .tex= TTA
%D    T0A T1A -> .plabel= r \eta_A
%D    T1A T2A <- .plabel= r \mu_A
%D ))
%D enddiagram
%D
$$\savebox{\myboxa}{$\KOBJ{A}{TA}$}
  \savebox{\myboxc}{$\KOBJ{C}{TC}$}
  \savebox{\myboxd}{$\KOBJ{TC}{TTC}$}
  \savebox{\myboxe}{$\KOBJ{TTC}{TTTC}$}
  \diag{kleisli-adj}
$$


\bsk

{\bf The Eilenberg-Moore proto-adjunction}

\msk

The {\sl Eilenberg-Moore proto-category} for a proto-monad $(\catA, T,
\eta, \mu)$ is:
%
$$\catAEM := ((\catAEM)_0, \Hom_\catAEM, \id_\catAEM, ¢_\catAEM)$$
%
where an object of $(\catAEM)_0$ is a pair $(A,\aa)$ (a
``proto-algebra''), that we write as:
%
$$\EMOBJT{A}{\aa}$$
%
We use a non-dashed arrow, `$\diagxyto/<-/<150>$', to stress that
the map $\aa:\Hom_\catA(TA, A)$ is part of the definition of the
object.

A (proto-)morphism $f:\EMOBJT{A}{\aa} \to \EMOBJT{C}{\cc}$ is just a
morphism $f:\Hom_\catA(A,C)$. The identity $\id_\catAEM$ and the
composition $¢_\catAEM$ are defined in the obvious way (inherited from
$\catA$).

The Eilenberg-Moore adjunction can be drawn as:
%
%D diagram em-adj
%D 2Dx     100    +50       +40    +30
%D 2D  100 S2B
%D 2D       ^
%D 2D       |
%D 2D       |
%D 2D  +30 S1B    EMA <---| A     T0A
%D 2D       |      |        |      |
%D 2D       |      |   <->  |      |
%D 2D       v      v        v      v
%D 2D  +30 S0B    EMC |---> TC    T1A
%D 2D                              ^
%D 2D  +15      \catAEM <=> \catA  |
%D 2D                              |
%D 2D  +15                        T2A
%D 2D
%D (( EMA .tex= \usebox{\myboxa}
%D    EMC .tex= \usebox{\myboxc}
%D    EMA A <-|
%D    EMA EMC -> .PLABEL= _(0.41) f^\flat:=Tf;\cc
%D    EMA EMC -> .PLABEL= _(0.59) g
%D      A  TC -> .PLABEL= ^(0.41) f
%D      A  TC -> .PLABEL= ^(0.59) g^\sharp:=\eta_A;g
%D    EMA  TC harrownodes nil 20 nil <-| sl^
%D    EMA  TC harrownodes nil 20 nil |-> sl_
%D    EMC  TC |-> 
%D ))
%D (( \catAEM \catA
%D    @ 0 @ 1 <- sl^ .plabel= a L^T
%D    @ 0 @ 1 -> sl_ .plabel= b R^T
%D ))
%D (( S2B .tex= \usebox{\myboxe}
%D    S1B .tex= \usebox{\myboxd}
%D    S0B .tex= \usebox{\myboxc}
%D    S2B S1B <- .plabel= l \mu?
%D    S1B S0B -> .plabel= l \cc
%D ))
%D (( T0A .tex= A
%D    T1A .tex= TA
%D    T2A .tex= TTA
%D    T0A T1A -> .plabel= r \eta_A
%D    T1A T2A <- .plabel= r \mu_A
%D ))
%D enddiagram
%D
$$\savebox{\myboxa}{$\EMOBJT{TA}{\mu_A}$}
  \savebox{\myboxc}{$\EMOBJT{C}{\cc}$}
  \savebox{\myboxd}{$\EMOBJT{TC}{T\cc}$}
  \savebox{\myboxe}{$\EMOBJT{TTC}{TT\cc}$}
  \diag{em-adj}
$$
%
where [two triangles showing the transpositions]:

%D diagram em-transpositions
%D 2Dx     100
%D 2D  100
%D 2D
%D 2D  +20
%D 2D
%D ((
%D
%D ))
%D enddiagram
%D
$$\diag{em-transpositions}$$


\bsk

{\bf The Comparison Theorem}

\msk

If $\catB \two/<-`->/<150>^L_R \catA$ and $\catB'
\two/<-`->/<150>^{L'}_{R'} \catA$ are two proto-adjunctions --- the
full definition with `$\flat$'s, `$\sharp$'s, `$\eta$'s and `$$'s
will not be relevant now --- then a {\sl proto-comparison} from $L'
\dashv R'$ to $L \dashv R$ is just a proto-functor $F:B' \to B$ such
that


%D diagram comparison
%D 2Dx     100     +40
%D 2D  100 \catB'
%D 2D
%D 2D  +20         \catA
%D 2D
%D 2D  +20 \catB
%D 2D
%D (( \catB' \catA \catB
%D    @ 0 @ 2 ->
%D    @ 0 @ 1 -> sl^ 
%D
%D
%D ))
%D enddiagram
%D
$$\diag{comparison}$$










%

\end{document}

% Local Variables:
% coding:           raw-text-unix
% ee-anchor-format: "«%s»"
% End:
