% (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:
