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