% (find-angg "LATEX/2019notes-monads.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019notes-monads.tex" :end))
% (defun d () (interactive) (find-pdf-page      "~/LATEX/2019notes-monads.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2019notes-monads.pdf"))
% (defun b () (interactive) (find-zsh "bibtex 2019notes-monads; makeindex 2019notes-monads"))
% (defun e () (interactive) (find-LATEX "2019notes-monads.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019notes-monads"))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (setq revert-without-query '("pdf$"))
% (find-xpdfpage "~/LATEX/2019notes-monads.pdf")
% (find-sh0 "cp -v  ~/LATEX/2019notes-monads.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2019notes-monads.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2019notes-monads.pdf
%               file:///tmp/2019notes-monads.pdf
%           file:///tmp/pen/2019notes-monads.pdf
% http://angg.twu.net/LATEX/2019notes-monads.pdf

% «.defs»			(to "defs")
% «.title-page»			(to "title-page")
% «.components»			(to "components")
% «.eqs-natural-iso»		(to "eqs-natural-iso")
% «.eqs-triangle»		(to "eqs-triangle")
% «.archetypal-monad»		(to "archetypal-monad")
% «.archetypal-monad-mrs»	(to "archetypal-monad-mrs")
% «.archetypal-monad-mrnts»	(to "archetypal-monad-mrnts")
% «.or-more-abstractly»		(to "or-more-abstractly")
% «.every-adjunction-induces»	(to "every-adjunction-induces")

% «.resolutions»		(to "resolutions")
% «.pasting-diagrams»		(to "pasting-diagrams")
% «.monads»			(to "monads")
% «.algebras»			(to "algebras")
% «.eilenberg-moore»		(to "eilenberg-moore")
% «.eilenberg-moore-abs»	(to "eilenberg-moore-abs")
% «.kleisli»			(to "kleisli")
% «.kleisli-adj»		(to "kleisli-adj")

\documentclass[oneside]{book}
\usepackage[colorlinks,urlcolor=brown]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
\usepackage{colorweb}                  % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof}   % For derivation trees ("%:" lines)
\input diagxy        % For 2D diagrams ("%D" lines)
%\xyoption{curve}    % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx15}               % (find-LATEX "edrx15.sty")
\input edrxaccents.tex            % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
\usepackage[paperwidth=11.5cm, paperheight=9cm,
            %total={6.5in,4in},
            %textwidth=4in,  paperwidth=4.5in,
            %textheight=5in, paperheight=4.5in,
            %a4paper,
            top=1.5cm, bottom=.5cm, left=1cm, right=1cm, includefoot
           ]{geometry}
%
\begin{document}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

\directlua{dofile "edrxtikz.lua"} % (find-LATEX "edrxtikz.lua")
\directlua{dofile "edrxpict.lua"} % (find-LATEX "edrxpict.lua")
%L V.__tostring = function (v) return format("(%.3f,%.3f)", v[1], v[2]) end



% «defs» (to ".defs")

\def\DN{\Downarrow}

\def\CatEM#1#2{\mathbf{EM}(#2)}
\def\CatKL#1#2{\mathbf{KL}(#2)}
\def\EM#1#2#3{\,[#1 \overset{#3}{\longleftarrow} #2]\,}
\def\coEM#1#2#3{\,[#1 \overset{#3}{\longrightarrow} #2]\,}
%L forths["-->"] = function () pusharrow("-->") end

% (find-kopkadaly4page (+ 12 263) "variable length")
% (find-kopkadaly4text (+ 12 263) "variable length")
\def\toon#1{\xrightarrow{#1}}

% (find-LATEX "edrx15.sty" "colors-2019")
\long\def\ColorRed   #1{{\color{Red1}#1}}
\long\def\ColorViolet#1{{\color{MagentaVioletLight}#1}}
\long\def\ColorViolet#1{{\color{Violet!50!black}#1}}
\long\def\ColorGreen #1{{\color{SpringDarkHard}#1}}
\long\def\ColorGreen #1{{\color{SpringGreenDark}#1}}
\long\def\ColorGreen #1{{\color{SpringGreen4}#1}}
\long\def\ColorGray  #1{{\color{GrayLight}#1}}
\long\def\ColorGray  #1{{\color{black!30!white}#1}}

\setlength{\parindent}{0em}



%  _____ _ _   _      
% |_   _(_) |_| | ___ 
%   | | | | __| |/ _ \
%   | | | | |_| |  __/
%   |_| |_|\__|_|\___|
%                     
% «title-page»  (to ".title-page")
% (nilp 1 "title-page")
% (nil    "title-page")
% (ntyp 1 "title-page")
% (nty    "title-page")
% (find-es "tex" "huge")
% (find-LATEX "2019logicday.tex" "title-page")

\begin{center}

\Large 

{\bf

Notes on Monads

}

\normalsize

\msk

Eduardo Ochs (UFF, Brazil)

\footnotesize

\url{http://angg.twu.net/math-b.html\#intro-tys-lfc}

\end{center}


\newpage

\noedrxfooter

%   ____                                             _       
%  / ___|___  _ __ ___  _ __   ___  _ __   ___ _ __ | |_ ___ 
% | |   / _ \| '_ ` _ \| '_ \ / _ \| '_ \ / _ \ '_ \| __/ __|
% | |__| (_) | | | | | | |_) | (_) | | | |  __/ | | | |_\__ \
%  \____\___/|_| |_| |_| .__/ \___/|_| |_|\___|_| |_|\__|___/
%                      |_|                                   
%
% «components»  (to ".components")
% (nmop 2 "components")
% (nmo    "components")

{\bf An adjunction/monad/comonad: components}

% (find-LATEX "2017cwm.tex" "adjoints-interdef-1")

%D diagram adjunction-monad-comonad-full
%D 2Dx     100   +30   +25    +30  +25   +30
%D 2D  100 CCB  LRLRB  La <-| a
%D 2D      ^     ^     |      |
%D 2D      |     |     v      v
%D 2D  +30 CB    LRB   LA <-| A    A'    IA
%D 2D      |     |     |      |    |     |
%D 2D      v     v     v      v    v     v
%D 2D  +30 IB    B'    B |--> RB   RLA   TA
%D 2D                  |      |    ^     ^
%D 2D                  v      v    |     |
%D 2D  +30             b |--> Rb  RLRLA  TTA
%D 2D                                 
%D 2D  +15           catB <> catA         
%D 2D
%D ren IB CB  CCB   ==> I_\catB C C^2
%D ren B' LRB LRLRB ==> B LRB LRLRB
%D ren A' RLA RLRLA ==> A RLA RLRLA
%D ren IA TA TTA    ==> I_\catA T T^2
%D ren catA catB    ==> \catA \catB
%D
%D ren La a b Rb    ==> LA' A' B' RB'
%D
%D (( CCB CB    <- .plabel= l ν
%D    CB IB     -> .plabel= l ε
%D    LRLRB LRB <- .plabel= l LηRB
%D    LRB B'    -> .plabel= l εB
%D
%D    # LA A <-|
%D    # LA B ->
%D    # A B harrownodes nil 20 nil <->
%D    # A RB ->
%D    # B RB |->
%D
%D    La a <-|
%D    La LA -> .plabel= l Lα
%D    La A harrownodes nil 20 nil <-| .plabel= a L_1
%D    a A -> .plabel= r α
%D    LA A <-| .plabel= a L_0
%D    LA B -> .plabel= l \sm{g^♭\\f}
%D    A B harrownodes nil 20 nil <-| sl^ .plabel= a ♭
%D    A B harrownodes nil 20 nil |-> sl_ .plabel= b ♯
%D    A RB -> .plabel= r \sm{g\\f^♯}
%D    B RB |-> .plabel= b R_0
%D    B b -> .plabel= l β
%D    B Rb harrownodes nil 20 nil |-> .plabel= b R_1
%D    RB Rb -> .plabel= r Rβ
%D    b Rb |->
%D
%D    A' RLA    -> .plabel= r ηA
%D    RLA RLRLA <- .plabel= r RεLA
%D    IA TA     -> .plabel= r η
%D    TA TTA    <- .plabel= r μ
%D
%D    catB catA <- sl^ .plabel= a L
%D    catB catA -> sl_ .plabel= b R
%D ))
%D
%D enddiagram
%D
%D diagram adjunction-monad-comonad-names
%D 2Dx     100 +15 +15 +15 +15
%D 2D  100 ν       L_1
%D 2D  +15 C       L_0
%D 2D  +15 ε       mid     η
%D 2D  +15         R_0     T
%D 2D  +15         R_1     μ
%D 2D
%D 2D  +30    \catB   \catA
%D 2D
%D ren mid ==> \sm{♭\\♯}
%D
%D (( ν place C place ε place
%D    L_1 place L_0 place mid place R_0 place R_1 place
%D    η place T place μ place
%D    \catB place \catA place
%D ))
%D enddiagram
%D
\pu
$$\scalebox{0.70}{$
  \diag{adjunction-monad-comonad-full}
  \qquad
  \qquad
  \diag{adjunction-monad-comonad-names}
  $}
$$





\newpage

% «eqs-natural-iso»  (to ".eqs-natural-iso")

{\bf The equations induced by the natural isomorphism}

\ssk

$f^{♯♭} = f$, $g^{♭♯} = g$, plus:
%
%D diagram adjunction-natural-isos
%D 2Dx       100    +30  +30    +45  +35    +40
%D 2D  100   La <-| a    L1 <-- L0   l1 <-| l0
%D 2D        |      |    |       |   v       -
%D 2D  +22   v      v    v       v   l3      v
%D 2D   +8   LA <-| A    L3 <-- L2   l3' <| l2
%D 2D        |      |   
%D 2D        v      v   
%D 2D  +30   B |--> RB   R0 --> R1   r0 |-> r1
%D 2D        |      |    |       |   -       v
%D 2D  +22   v      v    v       v   v      r3
%D 2D   +8   b |--> Rb   R2 --> R3   r2 |-> r3'  
%D 2D                                 
%D 2D  +15 catB <> catA         
%D 2D
%D ren La a b Rb    ==> LA' A' B' RB'
%D ren catA catB    ==> \catA \catB
%D
%D ren L0 L1 L2 L3  ==> (A{→}RB) (LA{→}B) (A'{→}RB') (LA'{→}B')
%D ren R1 R0 R3 R2  ==> (A{→}RB) (LA{→}B) (A'{→}RB') (LA'{→}B')
%D ren l0 l1 l3   l2 l3'  ==> g g^♭ Lα;g^♭;β   α;g;Rβ (α;g;Rβ)^♭
%D ren r0 r1 r3   r2 r3'  ==> f f^♯ α;f^♯;Rβ   Lα;f;β (Lα;f;β)^♯
%D
%D (( La a <-|
%D    La LA -> .plabel= l Lα
%D    La A harrownodes nil 20 nil <-|  # .plabel= a L_1
%D    a A -> .plabel= r α
%D    LA A <-|                         # .plabel= a L_0
%D    LA B -> .plabel= l \sm{g^♭\\f}
%D    A B harrownodes nil 20 nil <-| sl^ .plabel= a ♭
%D    A B harrownodes nil 20 nil |-> sl_ .plabel= b ♯
%D    A RB -> .plabel= r \sm{g\\f^♯}
%D    B RB |->                         # .plabel= b R_0
%D    B b -> .plabel= l β
%D    B Rb harrownodes nil 20 nil |->  # .plabel= b R_1
%D    RB Rb -> .plabel= r Rβ
%D    b Rb |->
%D
%D    catB catA <- sl^ .plabel= a L
%D    catB catA -> sl_ .plabel= b R
%D
%D    L0 L1 -> .plabel= a ♭
%D    L0 L2 ->
%D    L1 L3 ->
%D    L2 L3 -> .plabel= a ♭
%D
%D    R0 R1 -> .plabel= a ♯
%D    R0 R2 ->
%D    R1 R3 ->
%D    R2 R3 -> .plabel= a ♯
%D
%D    l0 l1  |->
%D    l0 l2  |->
%D    l1 l3  |->
%D    l2 l3' |->
%D
%D    r0 r1  |->
%D    r0 r2  |->
%D    r1 r3  |->
%D    r2 r3' |->
%D ))
%D
%D enddiagram
%
$$\pu
  \scalebox{0.8}{$
  \diag{adjunction-natural-isos}
  $}
$$




\newpage

%  _____     _                   _        _     _     
% |_   _| __(_) __ _ _ __   __ _| | ___  (_) __| |___ 
%   | || '__| |/ _` | '_ \ / _` | |/ _ \ | |/ _` / __|
%   | || |  | | (_| | | | | (_| | |  __/ | | (_| \__ \
%   |_||_|  |_|\__,_|_| |_|\__, |_|\___| |_|\__,_|___/
%                          |___/                      
%
% «eqs-triangle»  (to ".eqs-triangle")
% (nmop 4 "eqs-triangle")
% (nmo    "eqs-triangle")
% https://ncatlab.org/nlab/show/triangle+identities
% https://ncatlab.org/nlab/show/string+diagram

{\bf The triangle identities}

$LηA;εLA = \id_A$, \;\; $ηRB;RεB=\id_B$.

$g^♭ := Lg;εB$, \;\;\;\;\;\;\;\; $f^♯ := ηA;Rf$.
%
%D diagram triangle-identities
%D 2Dx     100  +25  +25  +25   +20   +20   +25   +30
%D 2D  100 .----------.         /---------> a02 - a03
%D 2D      |          v         |            v     v
%D 2D  +15 A0 - A1 - A2 - A3    a10 - a11 - a12 - a13
%D 2D           |__________^          |            v
%D 2D  +15                            \---------> a23
%D 2D
%D 2D  +25      .__________.          /---------> b03
%D 2D           |          v          |            v
%D 2D  +15 B0 - B1 - B2 - B3    b10 - b11 - b12 - b13
%D 2D      |__________^         |            v     v
%D 2D  +15                      \---------> b22 - b23
%D 2D
%D ren  A0  A1  A2  A3 ==> \catA \catB \catA \catB
%D ren         a02 a03 ==>        A   LA
%D ren a10 a11 a12 a13 ==> A LA RLA LRLA
%D ren             a23 ==>            LA
%D
%D ren  B0  B1  B2  B3 ==> \catB \catA \catB \catA
%D ren             b03 ==>            RB
%D ren b10 b11 b12 b13 ==> B RB LRB RLRB
%D ren         b22 b23 ==>        B   RB
%D
%D (( A0 A1 -> .plabel= m L
%D    A1 A2 -> .plabel= m R
%D    A2 A3 -> .plabel= m L
%D    A0 A2 -> .curve= ^25pt
%D    A0 A2 midpoint xy+= 0 -9 .TeX= \DNη place
%D    A1 A3 -> .curve= _25pt
%D    A1 A3 midpoint xy+= 0  9 .TeX= \DNε place
%D    
%D    a10 a02 |-> .curve= ^15pt
%D    a02 a03 |->
%D
%D    a10 a11 |->
%D    a11 a12 |->
%D    a12 a13 |->
%D    
%D    a11 a23 |-> .curve= _15pt
%D
%D    a02 a12 -> .plabel= r  ηA
%D    a03 a13 -> .plabel= r LηA
%D    a13 a23 -> .plabel= r εLA
%D ))
%D (( B0 B1 -> .plabel= m R
%D    B1 B2 -> .plabel= m L
%D    B2 B3 -> .plabel= m R
%D    B1 B3 -> .curve= ^25pt
%D    B1 B3 midpoint xy+= 0 -9 .TeX= \DNη place
%D    B0 B2 -> .curve= _25pt
%D    B0 B2 midpoint xy+= 0  9 .TeX= \DNε place
%D    
%D    b11 b03 |-> .curve= ^15pt
%D
%D    b10 b11 |->
%D    b11 b12 |->
%D    b12 b13 |->
%D    
%D    b10 b22 |-> .curve= _15pt
%D    b22 b23 |->
%D
%D    b12 b22  -> .plabel= r  εB
%D    b03 b13  -> .plabel= r ηRB
%D    b13 b23  -> .plabel= r RεB
%D ))
%D enddiagram
%D
$$\pu
  \scalebox{0.9}{$
  \diag{triangle-identities}
  $}
$$




\newpage


%     _             _          _                     _   __  __ 
%    / \   _ __ ___| |__   ___| |_ _   _ _ __   __ _| | |  \/  |
%   / _ \ | '__/ __| '_ \ / _ \ __| | | | '_ \ / _` | | | |\/| |
%  / ___ \| | | (__| | | |  __/ |_| |_| | |_) | (_| | | | |  | |
% /_/   \_\_|  \___|_| |_|\___|\__|\__, | .__/ \__,_|_| |_|  |_|
%                                  |___/|_|                     
%
% «archetypal-monad»  (to ".archetypal-monad")
% (nmop 2 "archetypal-monad")
% (nmo    "archetypal-monad")

{\bf Archetypal case}

Our archetypal case is a monoid $M$,

with elements denoted as $1,x,y,z,\ldots$,

that has a multiplication (associative, with unit 1).

\ssk

The monoid $M$ \ColorRed{acts} on sets called $A, B, C, \ldots$,

and \ColorRed{action} is written as a multiplication.

\ssk

We want to translate our operations on $M$ 

to operations on the functor $(M{×})$. \;\ColorGray{Why? Long story...}

\ssk

We start with:
%
% We have:
%
$$
\begin{array}{c}
1x = x = x1 \\
x(yz)=(xy)z \\
x(\ColorRed{ya})=(xy)a \\
\ColorRed{1a}=a \\
\end{array}
\quad
\Rightarrow
\quad
\begin{array}{c}
(1x)a = xa = (x1)a \\
(x(yz))a=((xy)z)a \\
x(\ColorRed{ya})=(xy)a \\
\ColorRed{1a}=a \\
\end{array}
$$

\newpage

%  __  __                   _     _              _           
% |  \/  | ___  _ __   ___ (_) __| |  _ __ _   _| | ___  ___ 
% | |\/| |/ _ \| '_ \ / _ \| |/ _` | | '__| | | | |/ _ \/ __|
% | |  | | (_) | | | | (_) | | (_| | | |  | |_| | |  __/\__ \
% |_|  |_|\___/|_| |_|\___/|_|\__,_| |_|   \__,_|_|\___||___/
%                                                            
% «archetypal-monad-mrs»  (to ".archetypal-monad-mrs")
% (nmop 3 "archetypal-monad-mrs")
% (nmo    "archetypal-monad-mrs")

{\bf The archetypal monad: the monoid rules}

The top two lines are the ``monoid rules'',

the bottow two lines are the ``action rules''.

We can draw the monoid rules as a diagram:
%
%D diagram monoid-rules-internal
%D 2Dx     100   +45 +35    +55
%D 2D  100 A --> B1  B2 <-- C
%D 2D      | \    |  |      |
%D 2D      |  \   v  |      |
%D 2D  +20 |   v E1  v      |
%D 2D  +8  v     E2  E4     v
%D 2D  +8  D --> E3  E5 <-- F
%D 2D
%D ren A B1 B2 C ==> (x,a) (x,(1,a)) (x,(yz,a)) (x,(y,(z,a)))
%D ren  E1 E2 E3 ==> (x1,a) (x,a) (1x,a)
%D ren D E4 E5 F ==> (1,(x,a)) (x(yz),a) ((xy)z,a) (xy,(z,a))
%D
%D (( A B1 |-> B1 E1 |->
%D    A E2 |->
%D    A D |-> D E3 |->
%D    C B2 |-> B2 E4 |->
%D    C F |-> F E5 |->
%D ))
%D enddiagram
%D
\pu
$$\begin{array}{c}
  (1x)a = xa = (x1)a \\
  (x(yz))a=((xy)z)a \\
  % x(\ColorRed{ya})=(xy)a \\
  % \ColorRed{1a}=a \\
  \\
  \diag{monoid-rules-internal}
  \end{array}
$$

\newpage

%  __  __      
% |  \/  |_  __
% | |\/| \ \/ /
% | |  | |>  < 
% |_|  |_/_/\_\
%              
% «archetypal-monad-mrnts»  (to ".archetypal-monad-mrnts")
% (nmop 4 "archetypal-monad-mrnts")
% (nmo    "archetypal-monad-mrnts")

{\bf The monoid rules in terms of natural transformations}
%
%D diagram monoid-rules-external
%D 2Dx     100   +45   +65
%D 2D  100 A --> B <-- C
%D 2D      | \   |     |
%D 2D      v  v  v     v
%D 2D  +30 D --> E <-- F
%D 2D
%D ren A B C ==> M×A M×(M×A) M×(M×(M×A))
%D ren D E F ==> M×(M×A) M×A M×(M×A)
%D
%D (( A B -> .plabel= a TηA
%D    B C <- .plabel= a TμA
%D    A D -> .plabel= l ηTA
%D    A E -> .plabel= m \id_A
%D    B E -> .plabel= r μA
%D    C F -> .plabel= r μTA
%D    D E -> .plabel= a μA
%D    E F <- .plabel= a μA
%D ))
%D enddiagram
%D
\pu
$$\def×{{\times}}
  \begin{array}{c}
  \diag{monoid-rules-internal} \\
  \\
  \diag{monoid-rules-external} \\
  \end{array}
$$


\newpage

%   ___                                          _         
%  / _ \ _ __   _ __ ___   ___  _ __ ___    __ _| |__  ___ 
% | | | | '__| | '_ ` _ \ / _ \| '__/ _ \  / _` | '_ \/ __|
% | |_| | |    | | | | | | (_) | | |  __/ | (_| | |_) \__ \
%  \___/|_|    |_| |_| |_|\___/|_|  \___|  \__,_|_.__/|___/
%                                                          
% «or-more-abstractly»  (to ".or-more-abstractly")
% (nmop 5 "or-more-abstractly")
% (nmo    "or-more-abstractly")

{\bf Or, more abstractly...}

%D diagram monoid-rules-external-T
%D 2Dx     100   +40   +40
%D 2D  100 A --> B <-- C
%D 2D      | \   |     |
%D 2D      v  v  v     v
%D 2D  +30 D --> E <-- F
%D 2D
%D ren A B C ==> TA T^2A T^3A
%D ren D E F ==> T^2A TA T^2A
%D
%D (( A B -> .plabel= a TηA
%D    B C <- .plabel= a TμA
%D    A D -> .plabel= l ηTA
%D    A E -> .plabel= m \id_A
%D    B E -> .plabel= r μA
%D    C F -> .plabel= r μTA
%D    D E -> .plabel= a μA
%D    E F <- .plabel= a μA
%D ))
%D enddiagram
%D
%D diagram monad-h
%D 2Dx     100  +20  +20
%D 2D  100 1 -> T <- T^2
%D 2D
%D (( 1 T -> .plabel= a η
%D    T T^2 <- .plabel= a μ
%D ))
%D enddiagram
%D
%D diagram monad-obeys
%D 2Dx     100   +30   +30
%D 2D  100 A --> B <-- C
%D 2D      | \   |     |
%D 2D      |  \  |     |
%D 2D      v   v v     v
%D 2D  +30 D --> E <-- F
%D 2D
%D ren A B C ==> T T^2 T^3
%D ren D E F ==> T^2 T T^2
%D
%D (( A B -> .plabel= a Tη
%D    B C <- .plabel= a Tμ
%D    A D -> .plabel= l ηT
%D    A E -> .plabel= m \id
%D    B E -> .plabel= r μ
%D    C F -> .plabel= r μT
%D    D E -> .plabel= b μ
%D    E F <- .plabel= b μ
%D ))
%D enddiagram
%D
\pu
%
$$\begin{array}[c]{cc}
  \diag{monoid-rules-external-T} \\
  \\
  \diag{monad-h} \quad
  \diag{monad-obeys} \\
  \end{array}
$$




\newpage

% «every-adjunction-induces»  (to ".every-adjunction-induces")
% (nmop 6 "every-adjunction-induces")
% (nmo     "every-adjunction-induces")

{\bf Every adjunction induces a monad and a comonad}
%
%D diagram adjunction-induces-monad-comonad
%D 2Dx     100   +30   +20    +30  +20   +30
%D 2D  100 CCB  LRLRB     
%D 2D      ^     ^     
%D 2D      |     |     
%D 2D  +30 CB    LRB   LA <-| A    A'    IA
%D 2D      |     |     |      |    |     |
%D 2D      v     v     v      v    v     v
%D 2D  +30 IB    B'    B |--> RB   RLA   TA
%D 2D                              ^     ^
%D 2D                              |     |
%D 2D  +30                        RLRLA  TTA
%D 2D                                 
%D 2D  +15           catB <> catA         
%D 2D
%D ren IB CB  CCB   ==> I_\catB C C^2
%D ren B' LRB LRLRB ==> B LRB LRLRB
%D ren A' RLA RLRLA ==> A RLA RLRLA
%D ren IA TA TTA    ==> I_\catA T T^2
%D ren catA catB    ==> \catA \catB
%D
%D (( CCB CB    <- .plabel= l ν
%D    CB IB     -> .plabel= l ε
%D    LRLRB LRB <- .plabel= l LηRB
%D    LRB B'    -> .plabel= l εB
%D
%D    LA A <-|
%D    LA B ->
%D    A RB ->
%D    B RB |->
%D    A B harrownodes nil 20 nil <->
%D
%D    A' RLA    -> .plabel= r ηA
%D    RLA RLRLA <- .plabel= r RεLA
%D    IA TA     -> .plabel= r η
%D    TA TTA    <- .plabel= r μ
%D
%D    catB catA <- sl^ .plabel= a L
%D    catB catA -> sl_ .plabel= b R
%D ))
%D
%D enddiagram
%D
%D diagram adjunction-cells
%D 2Dx     100 +30 +30
%D 2D  100 B   A
%D 2D
%D 2D  +30     B'  A'
%D 2D
%D ren B A B' A' ==> \catB \catA \catB \catA
%D
%D (( B A  -> .plabel= a R
%D    B B' -> .plabel= l I_\catB
%D    A B' -> .plabel= m L
%D    A A' -> .plabel= r I_\catA
%D    B' A' -> .plabel= b R
%D    B B' varrownodes nil 17 8 => .slide=  8pt .plabel= r ε
%D    A A' varrownodes 8 17 nil => .slide= -8pt .plabel= l η
%D ))
%D enddiagram
%D
\pu
$$\scalebox{0.75}{$
  \diag{adjunction-induces-monad-comonad}
  \qquad
  \qquad
  \diag{adjunction-cells}
  $}
$$




\newpage

{\bf The internal view of $Rε∘ηR=\id_R$}
%
%D diagram adjunction-cells-internal
%D 2Dx     100    +60    +60
%D 2D  100 B0 |-> A0
%D 2D         /   -  |->
%D 2D  +40     \  v      A1
%D 2D  +15      > B1 |-> A2
%D 2D  +15        B2 |-> A3
%D 2D
%D ren B0 A0 ==> B RB
%D ren B1 B2 ==> LRB B
%D ren A1 A2 A3 ==> RB RLRB RB
%D
%D (( B0 A0 |-> A0 A1 |->
%D    A0 B1 |-> B1 A2 |->
%D    B0 B2 |-> B2 A3 |->
%D    B1 B2 -> .plabel= r εB
%D    A1 A2 -> .plabel= r ηRB
%D    A2 A3 -> .plabel= r RεB
%D
%D    # B0 B1 varrownodes nil 17 8 => .slide=  8pt .plabel= r ε
%D    # A0 A2 varrownodes 8 17 nil => .slide= -8pt .plabel= l η
%D ))
%D enddiagram
%D
\pu
$$
  \scalebox{0.75}{$
  \begin{array}{c}
  \diag{adjunction-cells} \phantom{mm} \\
  \\
  \diag{adjunction-cells-internal} \\
  \end{array}
  $}
$$


\end{document}



\newpage


%  ____                 _       _   _                 
% |  _ \ ___  ___  ___ | |_   _| |_(_) ___  _ __  ___ 
% | |_) / _ \/ __|/ _ \| | | | | __| |/ _ \| '_ \/ __|
% |  _ <  __/\__ \ (_) | | |_| | |_| | (_) | | | \__ \
% |_| \_\___||___/\___/|_|\__,_|\__|_|\___/|_| |_|___/
%                                                     
% «resolutions»  (to ".resolutions")

%L _DiagOuter_ = 30
%L _DiagInner_ = 18
%L _HorizOuter_ = 70
%L _HorizInner_ = 20
%
%D diagram resolutions
%D 2Dx     100 +90 +90
%D 2D  100     B1
%D 2D  +20     B2
%D 2D
%D 2D  +50 C1      A1
%D 2D  +20 C2      A2
%D 2D
%D 2D  +50     D1
%D 2D  +20     D2
%D 2D
%D ren A1 B1 ==> A [RL]A
%D ren B2 A2 ==> [RL]B RLB
%D
%D ren C1 C2 ==> LA LB
%D
%D ren D1 D2 ==> \EM{RLA}{(RL)^2A}{μA} \EM{RLB}{(RL)^2B}{μB}
%D
%D (( A1 A2 ->
%D    B1 B2 ->
%D    C1 C2 ->
%D    D1 D2 ->
%D
%D    # Top adjunction
%D    B1 A1                         dharrownodes nil _DiagOuter_ nil <-|
%D    B1 B2 midpoint A1 A2 midpoint dharrownodes nil _DiagInner_ nil <->
%D    B2 A2                         dharrownodes nil _DiagOuter_ nil |->
%D
%D    # Middle adjunction
%D    C1 A1 harrownodes nil _HorizOuter_ nil <-|
%D    C1 A2 harrownodes nil _HorizInner_ nil <->
%D    C2 A2 harrownodes nil _HorizOuter_ nil |->
%D
%D    # Bottom adjunction
%D    D1 A1                         dharrownodes nil _DiagOuter_ nil <-|
%D    D1 D2 midpoint A1 A2 midpoint dharrownodes nil _DiagInner_ nil <->
%D    D2 A2                         dharrownodes nil _DiagOuter_ nil |->
%D
%D    # Top factorization
%D    B1 C1                         dharrownodes nil -_DiagOuter_ nil |->
%D  # B1 B2 midpoint C1 C2 midpoint dharrownodes nil -_DiagInner_ nil |->
%D    B2 C2                         dharrownodes nil -_DiagOuter_ nil |->
%D
%D    # Bottom factorization
%D    C1 D1                         dharrownodes nil _DiagOuter_ nil |->
%D  # C1 C2 midpoint D1 D2 midpoint dharrownodes nil _DiagInner_ nil |->
%D    C2 D2                         dharrownodes nil _DiagOuter_ nil |->
%D ))
%D enddiagram
%D
%D diagram coresolutions
%D 2Dx     100 +90 +90
%D 2D  100     B1
%D 2D  +20     B2
%D 2D
%D 2D  +50 A1      C1
%D 2D  +20 A2      C2
%D 2D
%D 2D  +50     D1
%D 2D  +20     D2
%D 2D
%D ren A2 B2 ==> B 〈LR〉B
%D ren B1 A1 ==> 〈LR〉A LRA
%D
%D ren C1 C2 ==> RA RB
%D
%D ren D1 D2 ==> \coEM{LRA}{(LR)^2A}{νA} \coEM{LRB}{(LR)^2B}{νB}
%D
%D (( A1 A2 ->
%D    B1 B2 ->
%D    C1 C2 ->
%D    D1 D2 ->
%D
%D    # Top adjunction
%D    A1 B1                         dharrownodes nil _DiagOuter_ nil <-|
%D    B1 B2 midpoint A1 A2 midpoint dharrownodes nil _DiagInner_ nil <->
%D    A2 B2                         dharrownodes nil _DiagOuter_ nil |->
%D
%D    # Middle adjunction
%D    C1 A1 harrownodes nil _HorizOuter_ nil <-|
%D    C1 A2 harrownodes nil _HorizInner_ nil <->
%D    C2 A2 harrownodes nil _HorizOuter_ nil |->
%D
%D    # Bottom adjunction
%D    D1 A1                         dharrownodes nil _DiagOuter_ nil <-|
%D    D1 D2 midpoint A1 A2 midpoint dharrownodes nil _DiagInner_ nil <->
%D    D2 A2                         dharrownodes nil _DiagOuter_ nil |->
%D
%D    # Top factorization
%D    B1 C1                         dharrownodes nil _DiagOuter_ nil |->
%D  # B1 B2 midpoint C1 C2 midpoint dharrownodes nil _DiagInner_ nil |->
%D    B2 C2                         dharrownodes nil _DiagOuter_ nil |->
%D
%D    # Bottom factorization
%D    C1 D1                         dharrownodes nil -_DiagOuter_ nil |->
%D  # C1 C2 midpoint D1 D2 midpoint dharrownodes nil -_DiagInner_ nil |->
%D    C2 D2                         dharrownodes nil -_DiagOuter_ nil |->
%D ))
%D enddiagram
%D
\pu

%D diagram resolutions-small
%D 2Dx     100 +35 +35
%D 2D  100     B
%D 2D
%D 2D  +30 C       A
%D 2D
%D 2D  +30     D
%D 2D
%D ren A ==> \catA
%D ren B ==> 𝐛{Kle}_{(L⊣R)}
%D ren C ==> \catB
%D ren D ==> 𝐛{EM}_{(L⊣R)}
%D
%D (( B A <- sl^
%D    B A -> sl_
%D    C A <- sl^ .plabel= a L
%D    C A -> sl_ .plabel= b R
%D    D A <- sl^
%D    D A -> sl_
%D    B C ->
%D    C D ->
%D ))
%D enddiagram
%D
%D diagram coresolutions-small
%D 2Dx     100 +35 +35
%D 2D  100     B
%D 2D
%D 2D  +30 A       C
%D 2D
%D 2D  +30     D
%D 2D
%D ren A ==> \catB
%D ren B ==> 𝐛{coKle}_{(L⊣R)}
%D ren C ==> \catA
%D ren D ==> 𝐛{coEM}_{(L⊣R)}
%D
%D (( A B <- sl^
%D    A B -> sl_
%D    A C <- sl^ .plabel= a L
%D    A C -> sl_ .plabel= b R
%D    A D <- sl^
%D    A D -> sl_
%D    B C ->
%D    C D ->
%D ))
%D enddiagram
%D
\pu


Resolutions:

Kleisli is initial and

Eilenberg-Moore is final

in the category of resolutions

\bsk

$\diag{resolutions-small}
$

\bsk

$$\diag{resolutions}
$$

\newpage

Coresolutions:

coKleisli is initial and

coEilenberg-Moore is final

in the category of coresolutions

\bsk

$\diag{coresolutions-small}
$

\bsk

$$\diag{coresolutions}
$$


\newpage


% «pasting-diagrams»  (to ".pasting-diagrams")

% eta_A : A -> RLA
% eta   : Id_\catA -> RL
% eps_B : LRB -> B
% eps   : LR  -> \Id_\catB
% 
%               Id_\catA                                  Id_\catA                            
%         ------------------                        ------------------                
%        /       ||         \                      /       ||         \               
%       /        || eta      \                    /        || eta_A    v              
%      /         \/           v                  -         \/           A |---L---> LA  
%   \catA --L-> \catB --R-> \catA --L-> \catB   A |---L--> LA |---R--> RLA |--L--> LRLA 
%                 \           ||          /                 -           ||          LA  
%                  \          || eps     /                   \          || eps_LA  ^    
%                   \         \/        /                     \         \/        /           
%                    -------------------                       -------------------            
%                         Id_\catB                                  Id_\catB          
%                                                                                       
%                           Id_\catA                                  Id_\catA        
%                     ------------------                        ------------------            
%                    /       ||         \                      /       ||         \           
%                   /        || eta      \                    /        || eta_RB   v    
%                  /         \/           v                  -         \/          RB   
%   \catB --R-> \catA --L-> \catB --R-> \catA  B |----R---> RB |--L--> LRB ---R-> RLRB  
%     \           ||          /                 \           ||          B |---R--> RB   
%      \          || eps     /                   \          || eps_B   ^              
%       \         \/        /                     \         \/        /               
%        -------------------                       -------------------                
%             Id_\catB                                  Id_\catB                        


%D diagram pasting-A->LA-ext
%D 2Dx       100        +30          +30         +30
%D 2D  100             Id_\catA			    
%D 2D	         ------------------		    
%D 2D	        /       ||         \		    
%D 2D	       /        || eta_A    v		    
%D 2D  +20    -         \/           A' |---L--> LA'  
%D 2D  +8    A |---L--> LA |---R--> RLA |--L--> LRLA 
%D 2D  +8                -           ||         LA''  
%D 2D	                  \          || eps_LA  ^    
%D 2D	                   \         \/        /	    
%D 2D	                    -------------------	    
%D 2D	                         Id_\catB	    
%D 2D	                                             
%D ren A LA RLA LRLA ==> \catA \catB \catA \catB
%D
%D ((   A   LA -> .plabel= m L
%D     LA  RLA -> .plabel= m R
%D    RLA LRLA -> .plabel= m L
%D     A   RLA -> .curve= ^30pt .plabel= a \id_\catA
%D    LA  LRLA -> .curve= _30pt .plabel= b \id_\catB
%D
%D      A  RLA varrownodes nil 20 24 => .plabel= r η
%D     LA LRLA varrownodes 22 20 nil => .plabel= r ε
%D ))
%D enddiagram
%D
%D diagram pasting-A->LA-int
%D 2Dx       100        +30          +30         +30
%D 2D  100             Id_\catA			    
%D 2D	         ------------------		    
%D 2D	        /       ||         \		    
%D 2D	       /        || eta_A    v		    
%D 2D  +20    -         \/           A' |---L--> LA'  
%D 2D  +8    A |---L--> LA |---R--> RLA |--L--> LRLA 
%D 2D  +8                -           ||         LA''  
%D 2D	                  \          || eps_LA  ^    
%D 2D	                   \         \/        /	    
%D 2D	                    -------------------	    
%D 2D	                         Id_\catB	    
%D 2D	                                             
%D ren A' LA' LA'' ==> A LA LA
%D
%D ((   A   LA -> .plabel= m L
%D     LA  RLA -> .plabel= m R
%D    RLA LRLA -> .plabel= m L
%D     A'  LA' -> .plabel= m L
%D     A    A' -> .curve= ^30pt .plabel= a \id_\catA
%D    LA  LA'' -> .curve= _30pt .plabel= b \id_\catB
%D
%D     A RLA varrownodes nil 20 24 => .plabel= r \eta_A
%D   LA LA'' varrownodes 22 20 nil => .plabel= r \ee_{LA}
%D ))
%D enddiagram
%D
%D diagram pasting-B->RA-int
%D 2Dx     100          +35         +35        +35
%D 2D  100                        Id_\catA	    
%D 2D	                    ------------------	    
%D 2D	                   /       ||         \	    
%D 2D                     /        || eta_RB   v    
%D 2D +20                -         \/         RB''   
%D 2D +8   B |----R---> RB |--L--> LRB ---R-> RLRB  
%D 2D +8    \           ||          B' |--R--> RB'   
%D 2D        \          || eps_B   ^               
%D 2D         \         \/        /                
%D 2D          -------------------                 
%D 2D               Id_\catB                        
%D 2D
%D ren B' RB' RB'' ==> B RB RB
%D
%D ((   B   RB -> .plabel= m R
%D     RB  LRB -> .plabel= m L
%D    LRB RLRB -> .plabel= m R
%D     B'  RB' -> .plabel= m L
%D    RB  RB'' -> .curve= ^30pt .plabel= a \id_\catA
%D     B    B' -> .curve= _30pt .plabel= b \id_\catB
%D
%D    RB RB'' varrownodes nil 20 24 => .plabel= r \eta_{RB}
%D     B   B' varrownodes 22 20 nil => .plabel= r \ee_{LA}
%D ))
%D enddiagram
%D
%D diagram pasting-B->RA-ext
%D 2Dx     100          +35         +35        +35
%D 2D  100                        Id_\catA	    
%D 2D	                    ------------------	    
%D 2D	                   /       ||         \	    
%D 2D                     /        || eta_RB   v    
%D 2D +20                -         \/         RB''   
%D 2D +8   B |----R---> RB |--L--> LRB ---R-> RLRB  
%D 2D +8    \           ||          B' |--R--> RB'   
%D 2D        \          || eps     ^               
%D 2D         \         \/        /                
%D 2D          -------------------                 
%D 2D               Id_\catB                        
%D 2D
%D ren B RB LRB RLRB ==> \catB \catA \catB \catA
%D
%D ((   B   RB -> .plabel= m R
%D     RB  LRB -> .plabel= m L
%D    LRB RLRB -> .plabel= m R
%D     B'  RB' -> .plabel= m L
%D    RB  RLRB -> .curve= ^30pt .plabel= a \id_\catA
%D     B   LRB -> .curve= _30pt .plabel= b \id_\catB
%D
%D    RB RLRB varrownodes nil 20 24 => .plabel= r \eta_{RB}
%D     B  LRB varrownodes 22 20 nil => .plabel= r \ee_{LA}
%D ))
%D enddiagram
%D

\pu
  
$$\diag{pasting-A->LA-ext}
$$

$$\diag{pasting-A->LA-int}
$$

$$\diag{pasting-B->RA-int}
$$

$$\diag{pasting-B->RA-ext}
$$

\newpage







%  __  __                       _     
% |  \/  | ___  _ __   __ _  __| |___ 
% | |\/| |/ _ \| '_ \ / _` |/ _` / __|
% | |  | | (_) | | | | (_| | (_| \__ \
% |_|  |_|\___/|_| |_|\__,_|\__,_|___/
%                                     
% «monads» (to ".monads")

Monads:

\bsk


\fbox{%
\begin{tabular}[c]{l}
  $T$ is a monad on $\catC$ \\
  means: \\
  $\catC$ is a category \\
  $T=(T,η,μ)$ [ab.lang.] \\
  $T:\catC→\catC$ [ftr]  \\
  $η:1→T$ [nt]   \\
  $μ:T^2→T$ [nt] \\
  obeying: \\
  $μ∘ηT=\id=μ∘Tη$, \\
  $μ∘Tμ=μ∘μT$ \\
\end{tabular}}
%
%D diagram monad-h
%D 2Dx     100  +20  +20
%D 2D  100 1 -> T <- T^2
%D 2D
%D (( 1 T -> .plabel= a η
%D    T T^2 <- .plabel= a μ
%D ))
%D enddiagram
%D
%D diagram monad-obeys
%D 2Dx     100   +30   +30
%D 2D  100 A --> B <-- C
%D 2D      | \   |     |
%D 2D      |  \  |     |
%D 2D      v   v v     v
%D 2D  +30 D --> E <-- F
%D 2D
%D ren A B C ==> T T^2 T^3
%D ren D E F ==> T^2 T T^2
%D
%D (( A B -> .plabel= a Tη
%D    B C <- .plabel= a Tμ
%D    A D -> .plabel= l ηT
%D    A E -> .plabel= m \id
%D    B E -> .plabel= r μ
%D    C F -> .plabel= r μT
%D    D E -> .plabel= b μ
%D    E F <- .plabel= b μ
%D ))
%D enddiagram
%D
\pu
%
$\begin{array}[c]{cc}
\diag{monad-h}
&
\hskip-1em
\fbox{%
\begin{tabular}{l}
$1:\catC→\catC$ [ftr] \\
$T:\catC→\catC$ [ftr] \\
$T^2:\catC→\catC$ [ftr] \\
\end{tabular}}
\\
\diag{monad-obeys} \\
\end{array}
$

\bsk



\fbox{%
\begin{tabular}{l}
Archetypal monad: \\
$(M,1,·)$ is a monoid, \\
$T=(M×)$ \\
$ηA=λa.(1,a)$ \\
$μA=λ(x,(y,a)).(xy,a)$ \\
\end{tabular}}
%
\begin{tabular}{l}
In the archetypal monad \\
the equations \\
$μ∘ηT=\id=μ∘Tη$ \\
and $μ∘Tμ=μ∘μT$ \\
become monoid axioms: \\
\end{tabular}


%D diagram ??
%D 2Dx     100   +30   +30
%D 2D  100 A --> B <-- C
%D 2D      | \   |     |
%D 2D      |  \  |     |
%D 2D      v   v v     v
%D 2D  +30 D --> E <-- F
%D 2D
%D ren A B C ==> TA T^2A T^3A
%D ren D E F ==> T^2A TA T^2A
%D
%D (( A B -> .plabel= a TηA
%D    B C <- .plabel= a TμA
%D    A D -> .plabel= l ηTA
%D    A E -> .plabel= m \id
%D    B E -> .plabel= r μA
%D    C F -> .plabel= r μTA
%D    D E -> .plabel= b μA
%D    E F <- .plabel= b μA
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

\newpage

%     _    _            _                   
%    / \  | | __ _  ___| |__  _ __ __ _ ___ 
%   / _ \ | |/ _` |/ _ \ '_ \| '__/ _` / __|
%  / ___ \| | (_| |  __/ |_) | | | (_| \__ \
% /_/   \_\_|\__, |\___|_.__/|_|  \__,_|___/
%            |___/                          
%
% «algebras» (to ".algebras")

Algebras

\msk

\fbox{%
\begin{tabular}[c]{l}
An algebra for a monad $(\catC,T)$ is \\
a pair $(Q,α)$ where $Q∈\catC$ and \\
$α$ is an arrow $Q \diagxyto/<-/<150>^{α} TQ$ obeying \\
$α∘ηQ=\id$, \\
$α∘μQ=α∘Tα$ \\
\end{tabular}}
%
%D diagram ??
%D 2Dx     100 +30 +30
%D 2D  100 A   B   C
%D 2D
%D 2D  +30     E   F
%D 2D
%D ren A B C ==> Q TQ T^2Q
%D ren   E F ==>    Q TQ
%D
%D (( A B -> .plabel= a ηQ
%D    B C <- .plabel= a μQ
%D    A E -> .plabel= l \id
%D    B E -> .plabel= r α
%D    C F -> .plabel= r Tα
%D    E F <- .plabel= b α
%D ))
%D enddiagram
%D
$\pu
 \cdiag{??}
$

\bsk

\fbox{%
\begin{tabular}[c]{l}
The archetypal algebras \\
on $(M×)$ are actions \\
$·:M×Q→Q$. \\
An action obeys \\
$1·q=q$ and \\
$(x·y)·q=x·(y·q)$. \\
\end{tabular}}
%
%D diagram ??
%D 2Dx     100   +35 +20    +40
%D 2D  100 A --> B1  B2 <-- C
%D 2D        \    |  |      |
%D 2D         \   v  v      |
%D 2D  +25     v E1  E3     v
%D 2D  +8        E2  E4 <-- F
%D 2D
%D ren A B1 B2 C ==> q (1,q) (xy,q) (x,(y,q))
%D ren E1 E2 E3 E4 F ==> 1q q (xy)q x(yq) (x,yq)
%D
%D (( A B1 -> B1 E1 ->
%D    A E2 ->
%D    C B2 -> B2 E3 ->
%D    C F  -> F E4 ->
%D ))
%D enddiagram
%D
$\pu
  \cdiag{??}
$

\bsk

Morphisms of algebras:

\msk

\fbox{%
\begin{tabular}[c]{l}
A morphism between \\
algebras $(Q,α)$ and $(S,β)$ \\
is a map $f:Q→S$ obeying \\
$f∘α=β∘Tf$. \\
Notation: \\
$f:(Q,α)→(S,β)$ \\
\end{tabular}}
%
%D diagram ??
%D 2Dx     100 +30
%D 2D  100 A   B
%D 2D
%D 2D  +30 C   D
%D 2D
%D ren A B C D ==> Q TQ S TS
%D
%D (( A B <- .plabel= a α
%D    A C -> .plabel= l f
%D    B D -> .plabel= r Tf
%D    C D <- .plabel= a β
%D    
%D ))
%D enddiagram
%D
$\pu
  \cdiag{??}
$

\bsk

\fbox{%
\begin{tabular}[c]{l}
In the archetypal case a morphism \\
of algebras $f:(Q,α)→(S,β)$ is an \\
$f:Q→S$ obeying \\
$∀(x,q)∈M×Q.f(xq)=xf(q)$. \\
\end{tabular}}
%
%D diagram ??
%D 2Dx     100   +35
%D 2D  100 A <-- B
%D 2D      |     |
%D 2D      v     |
%D 2D  +20 C1    v
%D 2D  +8  C2 <- D
%D 2D
%D ren A B C1 C2 D ==> xq (x,q)   f(xq) xf(q) (x,f(q))
%D
%D (( B A |-> A C1 |->
%D    B D |-> D C2 |->
%D ))
%D enddiagram
%D
$\pu
  \cdiag{??}
$

\bsk

If $(\catC,T)$ is a monad then

we write $\CatEM{\catC}{T}$ for the

the category of $T$-algebras.

(``Eilenberg-Moore'')

\msk

Amazing fact! We have an adjunction:

$\CatEM{\catC}{T}
 \two/<-`->/^L_R
 \catC
$

\newpage


%  _____ _      _       _                          __  __ 
% | ____| | ___(_)_ __ | |__   ___ _ __ __ _      |  \/  |
% |  _| | |/ _ \ | '_ \| '_ \ / _ \ '__/ _` |_____| |\/| |
% | |___| |  __/ | | | | |_) |  __/ | | (_| |_____| |  | |
% |_____|_|\___|_|_| |_|_.__/ \___|_|  \__, |     |_|  |_|
%                                      |___/              
%
% «eilenberg-moore» (to ".eilenberg-moore")
% (nmop 19 "eilenberg-moore")
% (nmo     "eilenberg-moore")

{\bf Eilenberg-Moore}

Here is the adjunction

$\CatEM{\catC}{T}
 \two/<-`->/^L_R
 \catC
$,

sided by how to construct

the transpositions `$·^♭$' and `$·^♯$':

($h^♭=α∘Th$, $k^♭=k∘ηB$)

%D diagram ??
%D 2Dx     100  +30  +40    +40  +20  +30 
%D 2D  100           LA <-| A    
%D 2D                |      |    
%D 2D                v      v    
%D 2D  +30 a    b    LB <-| B    e -> f   
%D 2D      |  / |    |      |      \  |   
%D 2D      v v  v    v      v       v v   
%D 2D  +30 c <- d    C |--> RC        g
%D 2D                |      |    
%D 2D                v      v    
%D 2D  +30           D |--> RD   
%D 2D                            
%D 2D  +20           E <==> F    
%D 2D
%D ren LA A ==> \EM{TA}{T^2A}{μA} A
%D ren LB B ==> \EM{TB}{T^2B}{μB} B
%D ren C RC ==> \EM{Q}{TQ}{α} Q
%D ren D RD ==> \EM{S}{TS}{β} S
%D ren E F  ==> \CatEM{\catC}{T} \catC
%D
%D (( LA A <-| .plabel= a L
%D    LB B <-|
%D    C RC |->
%D    D RD |-> .plabel= b R
%D    LA LB -> .plabel= l Tf
%D    LB C ->  .plabel= l \sm{h^♭\\k}
%D    C D ->   .plabel= l g
%D    A B ->   .plabel= r f
%D    B RC ->  .plabel= r \sm{h\\k^♯}
%D    RC RD -> .plabel= r g
%D    LA  B harrownodes nil 20 nil <-|
%D    LB RC harrownodes nil 20 nil <-| sl^
%D    LB RC harrownodes nil 20 nil |-> sl_
%D    C  RD harrownodes nil 20 nil |->
%D    E F <- sl^ .plabel= a L
%D    E F -> sl_ .plabel= b R
%D ))
%D
%D ren a b c d ==> B TB Q TQ
%D ren e f g ==> B TB Q
%D
%D (( a c -> .plabel= l h
%D    b d -> .plabel= r Th
%D    d c -> .plabel= b α
%D    b c --> .plabel= m h^♭
%D    
%D    e f -> .plabel= a ηB
%D    f g -> .plabel= r k
%D    e g --> .plabel= m k^♯
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

We will usually draw it ---

and most other adjunctions ---

like this:


%D diagram ??
%D 2Dx     100  +50    +40  +20
%D 2D  100 G    LB <-| B    I   
%D 2D      |    |      |    |
%D 2D      v    v      v    v
%D 2D  +30 H    C |--> RC   J
%D 2D                       
%D 2D  +20      E <==> F    
%D 2D
%D ren LB B ==> \EM{TA}{T^2A}{μA} A
%D ren C RC ==> \EM{Q}{TQ}{α} Q
%D ren E F  ==> \CatEM{\catC}{T} \catC
%D ren G H  ==> \EM{TQ}{T^2Q}{μQ} \EM{Q}{TQ}{α}
%D ren I J  ==> A TA
%D
%D (( LB B <-|
%D    LB C ->  .plabel= l \sm{Th;α\\k}
%D    B RC ->  .plabel= r \sm{h\\η;k}
%D    LB RC harrownodes nil 20 nil <-| sl^
%D    LB RC harrownodes nil 20 nil |-> sl_
%D    C RC |->
%D
%D    E F <- sl^ .plabel= a L
%D    E F -> sl_ .plabel= b R
%D    
%D    G H -> .plabel= l α
%D    I J -> .plabel= r ηA
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$




\newpage

%  _____ _ _            _                          __  __         _         
% | ____(_) | ___ _ __ | |__   ___ _ __ __ _      |  \/  |   __ _| |__  ___ 
% |  _| | | |/ _ \ '_ \| '_ \ / _ \ '__/ _` |_____| |\/| |  / _` | '_ \/ __|
% | |___| | |  __/ | | | |_) |  __/ | | (_| |_____| |  | | | (_| | |_) \__ \
% |_____|_|_|\___|_| |_|_.__/ \___|_|  \__, |     |_|  |_|  \__,_|_.__/|___/
%                                      |___/                                
%
% «eilenberg-moore-abs» (to ".eilenberg-moore-abs")
% (nmop 4)

The Eilenberg-Moore adjunction:

concrete vs.\ abstract

\msk

We will sometimes place this two diagrams side by side...

When viewed abstractly, the adjunction $\CatEM{\catC}{T} \two/<-`->/^L_R \catC $

is a tuple $(L, R, ♭, ♯, η, ε)$, or $(L_E, R_E, ♭_E, ♯_E, η_E, ε_E)$;

the diagram at the right shows how each component is defined.

%D diagram eilenberg-moore-thin
%D 2Dx     100  +35    +30  +20
%D 2D  100      LA <-| A    
%D 2D           |      |    
%D 2D           v      v    
%D 2D  +30 G    LB <-| B    I  
%D 2D      |    |      |    |
%D 2D      v    v      v    v
%D 2D  +30 H    C |--> RC   J
%D 2D           |      |    
%D 2D           v      v    
%D 2D  +30      D |--> RD   
%D 2D                       
%D 2D  +20      E <==> F    
%D 2D
%D ren LA A ==> (TA,μA) A
%D ren LB B ==> (TB,μB) B
%D ren C RC ==> (Q,α) Q
%D ren D RD ==> (S,β) S
%D ren E F  ==> \CatEM{\catC}{T} \catC
%D
%D ren G H  ==> (TQ,μQ) (Q,α)
%D ren I J  ==> B TB
%D
%D (( LA A <-| # .plabel= a L
%D    LB B <-|
%D    C RC |->
%D    D RD |-> # .plabel= b R
%D    LA LB -> .plabel= l Tf
%D    LB C ->  .plabel= l \sm{Th;α\\k}
%D    C D ->   .plabel= l g
%D    A B ->   .plabel= r f
%D    B RC ->  .plabel= r \sm{h\\η;k}
%D    RC RD -> .plabel= r g
%D    LA  B harrownodes nil 20 nil <-|
%D    LB RC harrownodes nil 20 nil <-| sl^
%D    LB RC harrownodes nil 20 nil |-> sl_
%D    C  RD harrownodes nil 20 nil |->
%D    E F <- sl^ .plabel= a L
%D    E F -> sl_ .plabel= b R
%D    
%D    G H -> .plabel= l α
%D    I J -> .plabel= r ηA
%D ))
%D
%D enddiagram
%D
%$$\pu
%  \diag{eilenberg-moore-thin}
%$$
%
%
%D diagram eilenberg-moore-abstract
%D 2Dx     100  +20    +30  +20
%D 2D  100      LA <-| A    
%D 2D           |      |    
%D 2D           v      v    
%D 2D  +30 G    LB <-| B    I  
%D 2D      |    |      |    |
%D 2D      v    v      v    v
%D 2D  +30 H    C |--> RC   J
%D 2D           |      |    
%D 2D           v      v    
%D 2D  +30      D |--> RD   
%D 2D                       
%D 2D  +20      E <==> F    
%D 2D
%D ren LA A ==> LA A
%D ren LB B ==> LB B
%D ren C RC ==> X RX
%D ren D RD ==> Y RY
%D ren E F  ==> \CatEM{\catC}{T} \catC
%D
%D ren G H  ==> LRX X
%D ren I J  ==> A RLA
%D
%D (( LA A <-| # .plabel= a L
%D    LB B <-|
%D    C RC |->
%D    D RD |-> # .plabel= b R
%D    LA LB -> .plabel= l Lf
%D    LB C ->  .plabel= l \sm{h^♭\\k}
%D    C D ->   .plabel= l g
%D    A B ->   .plabel= r f
%D    B RC ->  .plabel= r \sm{h\\k^♯}
%D    RC RD -> .plabel= r Rg
%D    LA  B harrownodes nil 20 nil <-|
%D    LB RC harrownodes nil 20 nil <-| sl^
%D    LB RC harrownodes nil 20 nil |-> sl_
%D    C  RD harrownodes nil 20 nil |->
%D    E F <- sl^ .plabel= a L
%D    E F -> sl_ .plabel= b R
%D    
%D    G H -> .plabel= l εX
%D    I J -> .plabel= r ηA
%D ))
%D
%D enddiagram
%D
%$$\pu
%  \diag{eilenberg-moore-abstract}
%$$

$$\pu
  \diag{eilenberg-moore-abstract}
  \qquad
  \diag{eilenberg-moore-thin}
$$









\newpage


%  _  ___      _     _ _ 
% | |/ / | ___(_)___| (_)
% | ' /| |/ _ \ / __| | |
% | . \| |  __/ \__ \ | |
% |_|\_\_|\___|_|___/_|_|
%                        
% «kleisli» (to ".kleisli")

{\bf The Kleisli category}

Fix a monad $T$ on $\catC$.

The Kleisli category $\CatKL{\catC}{T}$ has

the same objects as $\catC$, but

strange morphisms,

strange identities and a

strange composition:

$\begin{array}{rcl}
 [T]A \toon{[T]f} [T]B         &=& A \toon{f} TB        \\[5pt]\relax
 [T]A \toon{\id} [T]A          &=&                      \\\relax
 [T]A \toon{[T](ηA)} [T]A      &=& A \toon{ηA} TA       \\[5pt]\relax
 [T]A \toon{[T]f;[T]g} [T]C    &=&                      \\\relax
 [T]A \toon{[T](f;Tg;μC)} [T]B &=& A \toon{f;Tg;μC} TB  \\
 \end{array}
$

\msk

%D diagram ??
%D 2Dx     100 +30 +30
%D 2D  100 A   
%D 2D
%D 2D  +30 B   TB
%D 2D
%D 2D  +30 C   TC  T^2C
%D 2D
%D # ren ==>
%D
%D (( A TB -> .plabel= r f
%D    B TC -> .plabel= l g
%D    TB T^2C -> .plabel= r Tg
%D    C place
%D    TC T^2C <- .plabel= b μC
%D    A TC -->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

\msk

Identities work as expected, and composition is associative:

$[T]f;\id = [T]f;[T]η = [T](f;Tη;μ) = [T](f;\id) = [T]f$

$id;[T]f = [T]η;[T]f = [T](η;Tf;μ) = [T](f;η;μ) = [T]f$

$[T]f;([T]g;[T]h) = [T]f;[T](g;Th;μ) = [T](f;T(g;Th;μ);μ) = [T](f;Tg;TTh;Tμ;μ)$

$([T]f;[T]g);[T]h = [T](f;Tg;μ);[T]h = [T](f;Tg;μ;Th;μ) = [T](f;Tg;TTh;Tμ;μ)$

Note that we write just `$η$' and `$μ$' for `$ηA$', `$μC$', etc.



\newpage

%  _  ___      _     _ _             _  _ 
% | |/ / | ___(_)___| (_)   __ _  __| |(_)
% | ' /| |/ _ \ / __| | |  / _` |/ _` || |
% | . \| |  __/ \__ \ | | | (_| | (_| || |
% |_|\_\_|\___|_|___/_|_|  \__,_|\__,_|/ |
%                                    |__/ 
%
% «kleisli-adj» (to ".kleisli-adj")
% (nmop 4)

{\bf The Kleisli adjunction}

We have an adjunction:

$\CatKL{\catC}{T}
 \two/<-`->/^L_R
 \catC
$

Here's how to construct its components:

%D diagram kleisli-adj
%D 2Dx     100  +35    +40  +30
%D 2D  100      LA <-| A    
%D 2D           |      |    
%D 2D           v      v    
%D 2D  +30 G    LB <-| B    I
%D 2D      |    |      |    |   
%D 2D      v    v      v    v   
%D 2D  +30 H    C |--> RC   J
%D 2D           |      |    
%D 2D           v      v    
%D 2D  +30      D |--> RD   
%D 2D                       
%D 2D  +20      E <==> F    
%D 2D
%D ren LA A ==> [T]A A
%D ren LB B ==> [T]B B
%D ren C RC ==> [T]C TC
%D ren D RD ==> [T]D TD
%D ren E F  ==> \CatKL{\catC}{T} \catC
%D ren G H  ==> [T]TC [T]C
%D ren I J  ==> B TB
%D
%D (( LA A <-| .plabel= a L
%D    LB B <-|
%D    C RC |->
%D    D RD |-> .plabel= b R
%D    LA LB -> .plabel= l [T](f;η)
%D    LB C ->  .plabel= l \sm{[T]h\\\relax[T]k}
%D    C D ->   .plabel= l [T]g
%D    A B ->   .plabel= r f
%D    B RC ->  .plabel= r \sm{h\\k}
%D    RC RD -> .plabel= r Tg;μ
%D    LA  B harrownodes nil 20 nil <-|
%D    LB RC harrownodes nil 20 nil <-| sl^
%D    LB RC harrownodes nil 20 nil |-> sl_
%D    C  RD harrownodes nil 20 nil |->
%D    E F <- sl^ .plabel= a L
%D    E F -> sl_ .plabel= b R
%D    G H -> .plabel= l [T]\id
%D    I J -> .plabel= r ηB
%D ))
%D enddiagram
%D
$$\pu
  \diag{kleisli-adj}
$$










% \end{document}














\end{document}

% Local Variables:
% coding: utf-8-unix
% ee-tla: "nmo"
% End:
