|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2019notes-kleisli.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019notes-kleisli.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019notes-kleisli.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2019notes-kleisli.pdf"))
% (defun e () (interactive) (find-LATEX "2019notes-kleisli.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019notes-kleisli"))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (find-xpdfpage "~/LATEX/2019notes-kleisli.pdf")
% (find-sh0 "cp -v ~/LATEX/2019notes-kleisli.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2019notes-kleisli.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2019notes-kleisli.pdf
% file:///tmp/2019notes-kleisli.pdf
% file:///tmp/pen/2019notes-kleisli.pdf
% http://angg.twu.net/LATEX/2019notes-kleisli.pdf
% «.title» (to "title")
\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\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")
%
% (find-es "tex" "geometry")
% \usepackage[a5paper,margin=1cm]{geometry}
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
\def\DN{\Downarrow}
\def\calL{{\mathcal{L}}}
\def\calK{{\mathcal{K}}}
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% «title» (to ".title")
{\setlength{\parindent}{0em}
\footnotesize
Notes on [Kleisli65]:
``Every standard construction is induced by a pair of adjoint functors''
Proc. Amer. Math. Soc. 16 (1965), 544-546
\url{https://doi.org/10.1090/S0002-9939-1965-0177024-4}
\url{https://www.ams.org/journals/proc/1965-016-03/S0002-9939-1965-0177024-4/}
\url{https://www.ams.org/journals/proc/1965-016-03/S0002-9939-1965-0177024-4/S0002-9939-1965-0177024-4.pdf}
\ssk
These notes are at:
\url{http://angg.twu.net/LATEX/2020notes-kleisli.pdf}
}
\bsk
% (find-books "__cats/__cats.el" "kleisli")
% (find-kleisli65page (+ -543 544) "induced by the pair of adjoint" "functors F and G")
% (find-kleisli65text (+ -543 544) "induced by the pair of adjoint" "functors F and G")
(Page 544):
Left: equations (3) and (4);
Right: notation for the adjunction.
%
%D diagram ??
%D 2Dx 100 +20 +20 +20 +20
%D 2D 100 A0 B0
%D 2D
%D 2D +20 A1 B1 C0 C1 E0
%D 2D
%D 2D +20 A2 B2 C2 C3 E1
%D 2D
%D 2D +20 D0 D1 E2
%D 2D
%D ren A0 A1 A2 ==> C^2 C I
%D ren B0 B1 B2 ==> FGFGA FGA A
%D ren C0 C1 C2 C3 ==> FK K A GA
%D ren D0 D1 ==> \calL \calK
%D ren E0 E1 E2 ==> K GFK GFGFK
%D
%D (( A0 A1 <- .plabel= l p
%D A1 A2 -> .plabel= l k
%D B0 B1 <- .plabel= l FζGA
%D B1 B2 -> .plabel= l ηA
%D C0 C1 <-|
%D C0 C2 ->
%D C1 C3 ->
%D C2 C3 |->
%D D0 D1 <- sl^ .plabel= a F
%D D0 D1 -> sl_ .plabel= b G
%D E0 E1 -> .plabel= r ζK
%D E1 E2 <- .plabel= r GηFK
%D ))
%D enddiagram
%D
%D diagram comonad-equations
%D 2Dx 100 +20 +20
%D 2D 100 A0 A1 A2
%D 2D
%D 2D +20 A3 A4 A5
%D 2D
%D ren A0 A1 A2 ==> C C^2 C^3
%D ren A3 A4 A5 ==> C^2 C C^2
%D
%D (( A0 A1 <- .plabel= a Ck
%D A1 A2 -> .plabel= a Cp
%D A0 A3 <- .plabel= l kC
%D A0 A4 <- .plabel= m \id
%D A1 A4 <- .plabel= r p
%D A2 A5 <- .plabel= r pC
%D A3 A4 <- .plabel= b p
%D A4 A5 -> .plabel= b p
%D ))
%D enddiagram
%D
$$\pu
\diag{comonad-equations}
\qquad
\quad
\diag{??}
$$
The equations (1) and (2):
%
%D diagram ??
%D 2Dx 100 +20 +20 +20 +20 +20 +25 +30
%D 2D 100 B02 - B03
%D 2D | |
%D 2D +15 A0 - A1 - A2 - A3 B10 - B11 - B12 - B13
%D 2D |
%D 2D +15 B23
%D 2D
%D 2D +20 D03
%D 2D |
%D 2D +15 C0 - C1 - C2 - C3 D10 - D11 - D12 - D13
%D 2D | |
%D 2D +15 D22 - D23
%D 2D
%D ren A0 A1 A2 A3 ==> \calK \calL \calK \calL
%D ren C0 C1 C2 C3 ==> \calL \calK \calL \calK
%D ren B10 B11 B12 B13 ==> K FK GFK FGFK
%D ren D10 D11 D12 D13 ==> A GA FGA GFGA
%D ren B02 B03 B23 ==> K FK FK
%D ren D03 D22 D23 ==> GA A GA
%D
%D (( A0 A1 -> .plabel= m F
%D A1 A2 -> .plabel= m G
%D A2 A3 -> .plabel= m F
%D A0 A2 -> .curve= ^20pt
%D A1 A3 -> .curve= _20pt
%D
%D B02 B03 |->
%D B10 B11 |-> B11 B12 |-> B12 B13 |->
%D B02 B12 -> .plabel= r ζK
%D B03 B13 -> .plabel= r FζK
%D B13 B23 -> .plabel= r ηFK
%D B10 B02 |-> .curve= ^10pt
%D B11 B23 |-> .curve= _10pt
%D B03 B23 -> .slide= 25pt .plabel= r \uppereq
%D ))
%D (( C0 C1 -> .plabel= m G
%D C1 C2 -> .plabel= m F
%D C2 C3 -> .plabel= m G
%D C1 C3 -> .curve= ^20pt
%D C0 C2 -> .curve= _20pt
%D
%D D10 D11 |-> D11 D12 |-> D12 D13 |->
%D D22 D23 |->
%D D03 D13 -> .plabel= r ζGA
%D D12 D22 -> .plabel= r ηA
%D D13 D23 -> .plabel= r GηA
%D D11 D03 |-> .curve= ^10pt
%D D10 D22 |-> .curve= _10pt
%D D03 D23 -> .slide= 25pt .plabel= r \lowereq
%D ))
%D enddiagram
%D
$$\pu
\def\uppereq{\sm{ ((η*F)∘(F*ζ))K \\ = (ι*F)K }}
\def\lowereq{\sm{ ((G*η)∘(ζ*G))A \\ = (ι*G)A }}
\diag{??}
$$
% (find-books "__cats/__cats.el" "kleisli")
% (find-dn6file "diagforth.lua" "x+=")
%L forths["xy+="] = function ()
%L local dx,dy = getwordasluaexpr(), getwordasluaexpr()
%L ds:pick(0).x = ds:pick(0).x + dx
%L ds:pick(0).y = ds:pick(0).y + dy
%L end
\newpage
The triangular identities for an adjunction, in Kleisli's notation, are:
\msk
$(1) \;\; (η*F)∘(F*ζ) = ι*F$
$(2) \;\; (G*η)∘(ζ*G) = ι*G$
\msk or, in diagrams:
%
%D diagram triangular-ids
%D 2Dx 100 +20 +20 +20 +20 +20
%D 2D 100 .___________. .____.
%D 2D | v | v
%D 2D +20 A0 -> A1 -> A2 -> A3 B0 B1
%D 2D |___________^ |____^
%D 2D
%D 2D +20 .___________. .____.
%D 2D | v | v
%D 2D +20 C0 -> C1 -> C2 -> C3 D0 D1
%D 2D |___________^ |____^
%D 2D
%D ren A0 A1 A2 A3 B0 B1 ==> · · · · · ·
%D ren C0 C1 C2 C3 D0 D1 ==> · · · · · ·
%D
%D (( A0 A2 -> .plabel= m I .curve= ^20pt
%D A0 A2 midpoint xy+= 0 -6 .TeX= \DN\zeta place
%D A0 A1 -> .plabel= m F
%D A1 A2 -> .plabel= m G
%D A2 A3 -> .plabel= m F
%D A1 A3 -> .plabel= m I .curve= _20pt
%D A1 A3 midpoint xy+= 0 6 .TeX= \DN\eta place
%D
%D A3 B0 midpoint .TeX= = place
%D
%D B0 B1 -> .plabel= m F .curve= ^12pt
%D B0 B1 -> .plabel= m F .curve= _12pt
%D B0 B1 midpoint xy+= 0 0 .TeX= \DN\iota place
%D
%D C1 C3 -> .plabel= m I .curve= ^20pt
%D C1 C3 midpoint xy+= 0 -6 .TeX= \DN\zeta place
%D C0 C1 -> .plabel= m G
%D C1 C2 -> .plabel= m F
%D C2 C3 -> .plabel= m G
%D C0 C2 -> .plabel= m I .curve= _20pt
%D C0 C2 midpoint xy+= 0 6 .TeX= \DN\eta place
%D
%D C3 D0 midpoint .TeX= = place
%D
%D D0 D1 -> .plabel= m G .curve= ^12pt
%D D0 D1 -> .plabel= m G .curve= _12pt
%D D0 D1 midpoint xy+= 0 0 .TeX= \DN\iota place
%D ))
%D enddiagram
%D
$$\pu
\diag{triangular-ids}
$$
% (find-kleisli65page (+ -543 544) "(1)")
% (find-kleisli65text (+ -543 544) "(1)")
\msk
The he defines a comonad induced by that adjunction
Def: $(FG, η, F*ζ*G) =: (C,k,p)$
%D diagram def-Ckp
%D 2Dx 100 +20 +20 +20 +20 +20 +20 +20
%D 2D 100 .______________.
%D 2D | v
%D 2D 100 A0 -G> A1 -F> A2 B0 -G> B1 -F> B2 -G> B3 -F> B4
%D 2D |______________^
%D 2D .----------------------------.
%D 2D | v
%D 2D +30 C0 ---------> C1 D0 ---------> D1 ---------> D2
%D 2D |______________^
%D 2D +30
%D 2D
%D ren A0 A1 A2 B0 B1 B2 B3 B4 ==> · · · · · · · ·
%D ren C0 C1 D0 D1 D2 ==> · · · · ·
%D
%D (( A0 A1 -> .plabel= m G
%D A1 A2 -> .plabel= m F
%D A0 A2 -> .plabel= m I .curve= _20pt
%D A0 A2 midpoint xy+= 0 6 .TeX= \DN\eta place
%D
%D B1 B3 -> .plabel= m I .curve= ^20pt
%D B1 B3 midpoint xy+= 0 -6 .TeX= \DN\zeta place
%D B0 B1 -> .plabel= m G
%D B1 B2 -> .plabel= m F
%D B2 B3 -> .plabel= m G
%D B3 B4 -> .plabel= m F
%D
%D C0 C1 -> .plabel= m C
%D C0 C1 -> .plabel= m I .curve= _20pt
%D C0 C1 midpoint xy+= 0 6 .TeX= \DN\,k place
%D
%D D0 D1 -> .plabel= m C
%D D1 D2 -> .plabel= m C
%D D0 D2 -> .plabel= m I .curve= ^25pt
%D D0 D2 midpoint xy+= 0 -8 .TeX= \DN\,p place
%D ))
%D enddiagram
%D
$$\pu
\diag{def-Ckp}
$$
%D diagram kp=i
%D 2Dx 100 +30 +30 +20 +30 +30 +20 +30
%D 2D 100 .____________. .____________. .______.
%D 2D | v | v | v
%D 2D 100 A0 -> A1 -> A2 B0 -> B1 -> B2 C0 C1
%D 2D |______^ |______^ |______^
%D 2D
%D ren A0 A1 A2 B0 B1 B2 C0 C1 ==> · · · · · · · ·
%D
%D ((
%D A0 A2 -> .plabel= m C .curve= ^25pt
%D A0 A2 midpoint xy+= 0 -8 .TeX= \DN\,p place
%D A0 A1 -> .plabel= m C
%D A1 A2 -> .plabel= m C
%D A1 A2 -> .plabel= m I .curve= _20pt
%D A1 A2 midpoint xy+= 0 6 .TeX= \DN\,k place
%D
%D A2 B0 midpoint .TeX= = place
%D
%D B0 B2 -> .plabel= m C .curve= ^25pt
%D B0 B2 midpoint xy+= 0 -8 .TeX= \DN\,p place
%D B0 B1 -> .plabel= m C
%D B1 B2 -> .plabel= m C
%D B0 B1 -> .plabel= m I .curve= _20pt
%D B0 B1 midpoint xy+= 0 6 .TeX= \DN\,k place
%D
%D B2 C0 midpoint .TeX= = place
%D
%D C0 C1 -> .plabel= m C .curve= ^15pt
%D C0 C1 midpoint xy+= 0 0 .TeX= \DNι place
%D C0 C1 -> .plabel= m C .curve= _15pt
%D ))
%D enddiagram
%D
$$\pu
\diag{kp=i}
$$
%D diagram pp
%D 2Dx 100 +30 +25 +25 +20 +25 +25 +30
%D 2D 100 ._________________. ._________________.
%D 2D | | | |
%D 2D 100 A0 -> A1 ------> A3 B0 ------> B2 -> B3
%D 2D | ^ | ^
%D 2D +15 \---> A2 ---/ \---> B1 ---/
%D 2D
%D ren A0 A1 A2 A3 ==> · · · ·
%D ren B0 B1 B2 B3 ==> · · · ·
%D
%D ((
%D A0 A3 -> .plabel= m C .curve= ^25pt
%D A0 A3 midpoint xy+= 0 -8 .TeX= \DN\,p place
%D A0 A1 -> .plabel= m C
%D A1 A3 -> .plabel= m C
%D A1 A2 -> .plabel= m C .curve= _7pt
%D A2 A3 -> .plabel= m C .curve= _7pt
%D A1 A3 midpoint xy+= 0 6 .TeX= \DN\,p place
%D
%D A3 B0 midpoint .TeX= = place
%D
%D B0 B3 -> .plabel= m C .curve= ^25pt
%D B0 B3 midpoint xy+= 0 -8 .TeX= \DN\,p place
%D B0 B2 -> .plabel= m C
%D B2 B3 -> .plabel= m C
%D B0 B1 -> .plabel= m C .curve= _7pt
%D B1 B2 -> .plabel= m C .curve= _7pt
%D B0 B2 midpoint xy+= 0 6 .TeX= \DN\,p place
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{pp}
$$
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-tla: "kle"
% End: