|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (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: