% (find-angg "LATEX/2017cwm.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2017cwm.tex" :end))
% (defun d () (interactive) (find-pdf-page      "~/LATEX/2017cwm.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2017cwm.pdf"))
% (defun e () (interactive) (find-LATEX "2017cwm.tex"))
% (defun u () (interactive) (find-latex-upload-links "2017cwm"))
% (find-xpdfpage "~/LATEX/2017cwm.pdf")
% (find-sh0 "cp -v  ~/LATEX/2017cwm.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2017cwm.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2017cwm.pdf
%               file:///tmp/2017cwm.pdf
%           file:///tmp/pen/2017cwm.pdf
% http://angg.twu.net/LATEX/2017cwm.pdf
%
% (defun fo () (interactive) (search-forward "% «") (eek "C-a <down>"))

% «.thislinetag»		(to "thislinetag")
%
% «.intro»			(to "intro")
% «.logica-l»			(to "logica-l")
%
% «.2020-universal-arrows»	(to "2020-universal-arrows")
% «.hom»			(to "hom")
% «.comma»			(to "comma")
% «.comma-2»			(to "comma-2")
% «.universals»			(to "universals")
% «.universal-arrow-c-to-S»	(to "universal-arrow-c-to-S")
% «.universal-arrow-S-to-c»	(to "universal-arrow-S-to-c")
% «.universal-element»		(to "universal-element")
% «.yoneda-behind»		(to "yoneda-behind")
% «.yoneda-behind-2»		(to "yoneda-behind-2")
% «.yoneda»			(to "yoneda")
% «.yoneda-L»			(to "yoneda-L")
% «.yoneda-1»			(to "yoneda-1")
% «.yoneda-2»			(to "yoneda-2")
% «.yoneda-GF»			(to "yoneda-GF")
% «.adjoints»			(to "adjoints")
% «.adjoints-2»			(to "adjoints-2")
% «.adjoints-interdef-1»	(to "adjoints-interdef-1")
% «.adjoints-interdef-2»	(to "adjoints-interdef-2")
% «.monads»			(to "monads")
% «.monads-algebras»		(to "monads-algebras")
% «.monads-examples»		(to "monads-examples")
% «.monads-examples-2»		(to "monads-examples-2")
% «.kan-1»			(to "kan-1")
% «.kan-2»			(to "kan-2")
% «.kan-236»			(to "kan-236")
%
\documentclass[oneside,12pt]{article}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage{color}                % (find-LATEX "edrx15.sty" "colors")
\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-angg "LATEX/edrx15.sty")
\input edrxaccents.tex            % (find-angg "LATEX/edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-dn4ex "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
\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



\def\Nat{\text{Nat}}
\def\Id {\text{Id}}
\def\Sel{\text{S}}
\def\mtnto{\ton{·}}
\def\nameof#1{\ulcorner#1\urcorner}

% «thislinetag» (to ".thislinetag")
%L -- (find-es "luatex" "thislinetag")
%L -- (find-LATEX "dednat6/texfile.lua" "TexFile")
%L -- (find-LATEX "dednat6/block.lua" "TexLines")
%L thisline = function (n) return tf.lines[tex.inputlineno - (n or 0)] end
%L thisline = function (n) return texlines[tex.inputlineno - (n or 0)] end
%L thislinetag = function (n)
%L     local line = thisline(n)
%L     local tag = line:match("%% +[\128-\255]+([!-~]*)[\128-\255]+")
%L     if not tag then error("No tag in line "..tex.inputlineno) end
%L     return tag
%L   end
%L
\def\thislinetag{\expr{thislinetag()}}
\def\mylabel{\label{\thislinetag}}
\def⊙{\thislinetag}
\def⊙{\mylabel}
\pu

\def\Frob    {\mathsf{Frob}}
\def\Frobnat {\mathsf{Frob}^\nat}




% «intro» (to ".intro")
% (find-idarct0file "2010diags-body.tex" "mental-space")

{\setlength{\parindent}{0em}

{\bf Notes on notation: CWM}

Eduardo Ochs, 2017

Version at the bottom of the page.

eduardoochs@gmail.com

\url{http://angg.twu.net/LATEX/2017cwm.pdf}

\url{http://angg.twu.net/math-b.html\#notes-on-notation}

}

\bsk

From \url{http://angg.twu.net/math-b.html\#idarct}:
%
\begin{quotation}
Different people have different measures for ``mental space''; someone
with a good algebraic memory may feel that an expression like
{$\Frobnat: Σ_f(P∧f^*Q) \xton{\cong} Σ_fP∧Q$} is easy to remember,
while I always think diagramatically, and so what I do is that I
remember this diagram [...] and I reconstruct the formula from it.
\end{quotation}

These are very informal notes showing my favourite ways to draw the
``missing diagrams'' in MacLane's {\sl Categories for the Working
  Mathematician}, and my favourite choices of letters for them. Work
in progress changing often, contributions and chats very welcome, etc.
I am also doing something similar for parts of {\sl Sketches of an
  Elephant} --- see the link ``\#notes-on-notation'' above.

\msk

The good parts are the one on Yoneda
(pp.\pageref{yoneda-behind}--\pageref{yoneda-L}), the
``interdefinabilities'' for some components of adjunctions
(pp.\pageref{adjoints-interdef-1}--\pageref{adjoints-interdef-2}), and
the part on monads (pp.\pageref{monads}--\pageref{monads-examples-2}).
The rest is a mess.

\newpage


% «logica-l» (to ".logica-l")
% Announcement (2017ago06):
% https://mail.google.com/mail/ca/u/0/#search/yoneda/15dba04959636fec
% Subj: Fazendo os diagramas implícitos no CWM e outros livros de Categorias
% 
% Migs,
% 
% eu estou começando um projeto - totalmente informal - que talvez
% interesse a algumas pessoas daqui, e que por enquanto eu não me atrevo
% a anunciar em nenhuma lista menos beginner-friendly...
% 
% Uma das minhas áreas de pesquisa é Categorias e eu até já publiquei um
% artigo BEM bacana sobre isso, mas eu sou praticamente autodidata, o
% meu conhecimento da área tem buracos ridiculamente grandes, e eu nunca
% soube muito bem COMO estudar os livros de Categorias...
% 
% Há umas duas semanas atrás me ocorreu que eu deveria pegar alguns
% livros de Categorias, entender muito bem a notação que eles usam,
% fazer os diagramas que estão implícitos no texto (nas posições que se
% tornaram canônicas pra mim - por exemplo, numa adjunção L-|R o funtor
% L vai pra esquerda, o R vai pra direita, e os morfismos em cada
% categoria vão pra baixo; universais e Yoneda usam convenções baseadas
% nessa), definir direito as construções que no livro são tratadas como
% "óbvias" (usando notação lambda), descobrir as convenções do livro
% para nomear esses funtores e transformações naturais "óbvios" quando
% eles não são nomeados, e assim por diante.
% 
% Estou começando com o Categories for the Working Mathematician, do
% MacLane, e depois que eu terminar a parte de mônadas do CWM pretendo
% ir pro Sketches of an Elephant, do Johnstone. Tem vários outros livros
% e artigos pros quais eu gostaria de fazer o mesmo, mas por enquanto a
% prioridade deles é mais baixa.
% 
% Tou pondo os diagramas que eu tou fazendo pro CWM aqui:
% 
%   http://angg.twu.net/LATEX/2017cwm.pdf
% 
% Ainda não escrevi nem introdução, nem guidelines, nem várias outras
% coisas. Tudo ainda é muito preliminar.
% 
% Se alguém quiser participar ou conversar a respeito pode falar comigo
% ou por aqui ou em privado. Tou typesetteando os diagramas com um
% pacote que eu mesmo fiz e que não é nada user-friendly (por enquanto
% =/), mas dá pra gente interagir usando outros pacotes ou mesmo fotos
% de diagramas escritos à mão.
% 
%   [[]],
%     Eduardo Ochs =)
%     http://angg.twu.net/math-b.html
%     http://angg.twu.net/
% 
% 
% 
% 
% P.S.: Quando eu estudei o CWM, o Elephant e outros livros de
% Categorias eu acabava traduzindo as idéias deles direto pra outras
% notações - o que hoje em dia eu reconheço que foi uma idéia de jerico
% =( -, sem nunca me dar ao trabalho de fazer "dicionários de diagramas"
% detalhados que esclarecessem a tradução entre as notações.







%  _                     
% | |__   ___  _ __ ___  
% | '_ \ / _ \| '_ ` _ \ 
% | | | | (_) | | | | | |
% |_| |_|\___/|_| |_| |_|
%                        
% «hom» (to ".hom")
% (find-cwm2page (+ 9 34) "2. Contravariance and Opposites")
% (find-cwm2text (+ 9 34) "2. Contra variance and Opposites")


%   ____                                
%  / ___|___  _ __ ___  _ __ ___   __ _ 
% | |   / _ \| '_ ` _ \| '_ ` _ \ / _` |
% | |__| (_) | | | | | | | | | | | (_| |
%  \____\___/|_| |_| |_|_| |_| |_|\__,_|
%                                       
% «comma» (to ".comma")
% (find-cwm2page (+ 10 45)   "6. Comma Categories")
% (find-cwm2text (+ 10 45)   "6. Comma Categories")
% (cw7p 2 "comma")
% (cw7    "comma")

\par CWM2
\par II. Constructions on Categories
\par p.45: 6. Comma Categories (in my notation)
\bsk

The most general case is with functors $\catA \ton{F} \catB \otn{G} \catC$.

The comma category $(F↓G)$ is
%
%D diagram my-comma-1
%D 2Dx     100     +25     +30     +25  +30
%D 2D  100 B1 |--> B2 ---> B3 <--| B4   C1
%D 2D      ||      ||       |       |    |
%D 2D      ||      ||       v       v    v
%D 2D  +25 B5 |--> B6 ---> B7 <--| B8   C2
%D 2D
%D 2D  +15 B9 ---> B10 == B11 <-- B12   C3
%D 2D
%D ren B1 B2 B3 B4 ==> A FA GC C
%D ren B5 B6 B7 B8 ==> A' FA' GC' C'
%D ren B9 B10 B11 B12 ==> \catA \catB \catB \catC
%D ren C1 C2 C3 ==> (A,h,C) (A',h',C') (F↓G)
%D
%D (( B1 B2 |-> B2 B3 -> .plabel= a h B3 B4 <-|
%D    B1 B5 -> .plabel= l α B2 B6 -> .plabel= l Fα B3 B7 -> .plabel= r Fγ B4 B8 -> .plabel= r γ
%D    B5 B6 |-> B6 B7 -> .plabel= a h' B7 B8 <-|
%D    B9 B10 -> .plabel= a F B10 B11 = B11 B12 <- .plabel= a G
%D    C1 C2 -> .plabel= r (α,γ) C3 place
%D ))
%D enddiagram
%D
$$\pu
  \diag{my-comma-1}
$$

The obtain the other 8 cases I replace the functors $F$ and $G$ by
$\Id_\catB$ or $\Sel_B$, where $\Sel_B:1→\catB$ is the functor
that ``selects'' the object $B$ --- it takes the only object $•∈1$ to
$B$. For example, $(\Sel_B,\Id_\catB)$ is:
%
%D diagram my-comma-2
%D 2Dx     100     +25     +30     +25  +30
%D 2D  100 B1 |--> B2 ---> B3 <--| B4   C1
%D 2D      ||      ||       |       |    |
%D 2D      ||      ||       v       v    v
%D 2D  +25 B5 |--> B6 ---> B7 <--| B8   C2
%D 2D
%D 2D  +15 B9 ---> B10 == B11 <-- B12   C3
%D 2D
%D ren B1 B2 B3 B4 ==> • B B' B'
%D ren B5 B6 B7 B8 ==> • B B'' B''
%D ren B9 B10 B11 B12 ==> \catA \catB \catB \catB
%D ren C1 C2 C3 ==> (•,h,B') (•,h',B'') (\Sel_B↓\Id_\catB)
%D
%D (( B1 B2 |-> B2 B3 -> .plabel= a h B3 B4 <-|
%D    B1 B5 = B2 B6 = B3 B7 -> .plabel= r β B4 B8 -> .plabel= r β
%D    B5 B6 |-> B6 B7 -> .plabel= a h' B7 B8 <-|
%D    B9 B10 -> .plabel= a \Sel_B B10 B11 = B11 B12 <- .plabel= a \Id_\catB
%D    C1 C2 -> .plabel= r (\id_•,β) C3 place
%D ))
%D enddiagram
%D
$$\pu
  \diag{my-comma-2}
$$

Shorthands:

1) Use `$\_$' in the pairs and triples in the positions where the
information there is trivial --- $(\id_•,β):(•,h,B')→(•,h',B'')$
becomes $(\_,β):(\_,h,B')→(\_,h',B'')$.

2) Use $B$ instead of $\Sel_B$.

3) Use $\catB$ instead of $\Id_B$.

\msk

The correspondence with the names in CWM is:

The comma category $(F↓G)$

The category $(B↓\catB)$ of objects under $B$

The category $(\catB↓B)$ of objects over $B$

The category $(B↓G)$ of objects $G$-under $B$

The category $(F↓B)$ of objects $F$-over $B$

\msk

The nine cases:
%
$$\begin{array}{ccc}
      (F↓G) &     (F↓\catB) &     (F↓B) \\
  (\catB↓G) & (\catB↓\catB) & (\catB↓B) \\
      (B↓G) &     (B↓\catB) &    (B↓B') \\
  \end{array}
  \quad
  ⇒
  \quad
  \begin{array}{ccc}
          (F↓G) &         (F↓\Id_\catB) &    (F↓\Sel_B) \\
  (\Id_\catB↓G) & (\Id_\catB↓\Id_\catB) & (\Id_\catB↓B) \\
     (\Sel_B↓G) &    (\Sel_B↓\Id_\catB) & (\Sel_B↓\Sel_{B'}) \\
  \end{array}
$$



\newpage

%   ____                                
%  / ___|___  _ __ ___  _ __ ___   __ _ 
% | |   / _ \| '_ ` _ \| '_ ` _ \ / _` |
% | |__| (_) | | | | | | | | | | | (_| |
%  \____\___/|_| |_| |_|_| |_| |_|\__,_|
%                                       
% «comma-2» (to ".comma-2")
% (cw7p 3 "comma-2")
% (cw7    "comma-2")
% (find-cwm2page (+ 10 45)   "6. Comma Categories")
% (find-cwm2text (+ 10 45)   "6. Comma Categories")

\par CWM2
\par II. Constructions on Categories
\par p.45: 6. Comma Categories
\bsk

MacLane uses a notation with lots of names and shorthands.

\msk

Fix $C$, $b∈C$. The category $(b↓C)$ of {\sl objects under $b$} has

objects like $\ang{f,c}$, where $c∈C$ and $f:b→c$.

Fix $C$, $a∈C$. The category $(C↓a)$ of {\sl objects over $a$} has

objects like $\ang{c,f}$, where $c∈C$ and $f:c→a$.

Fix $C$, $D$, $b∈C$. $S:D→C$. The category $(b↓S)$ of {\sl objects $S$-under $b$} has

objects like $\ang{f,d}$, where $d∈D$ and $f:b→Sd$.

Fix $C$, $E$, $a∈C$. $T:E→C$. The category $(T↓a)$ of {\sl objects $T$-over $a$} has

objects like $\ang{f,d}$, where $d∈D$ and $f:b→Sd$.

Fix $C$, $D$, $E$, and $S$, $T$ with $E \ton{T} C \otn{S} D$. The {\sl comma category $(T,S)$} has

objects like $\ang{e,d,f}$, where $d∈D$, $e∈E$ and $f:Te→Sd$.

\msk

An object $b∈C$ may be regarded as a functor $b:1→C$ with image $b$.

A category $C$ may be regarded as the identity functor $C→C$.

We have:

$(b↓C)$ has objects like $\ang{*,c,f}$, where $c∈C$ and $f:b→c$.

$(C↓a)$ has objects like $\ang{c,*,f}$, where $c∈C$ and $f:c→a$.

$(b↓S)$ has objects like $\ang{*,d,f}$, where $d∈D$ and $f:b→Sd$.

$(T↓a)$ has objects like 




\newpage

%  _   _       _                          _     
% | | | |_ __ (_)_   _____ _ __ ___  __ _| |___ 
% | | | | '_ \| \ \ / / _ \ '__/ __|/ _` | / __|
% | |_| | | | | |\ V /  __/ |  \__ \ (_| | \__ \
%  \___/|_| |_|_| \_/ \___|_|  |___/\__,_|_|___/
%                                               
% «universals» (to ".universals")
% «universal-arrow-c-to-S» (to ".universal-arrow-c-to-S")
% (cw7p 4 "universal-arrow-c-to-S")
% (cw7    "universal-arrow-c-to-S")
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 9  55) "III. Universals and Limits")
% (find-cwm2text (+ 9  55) "III. Universals and Limits")
% (find-cwm2page (+ 9  55)   "1. Universal Arrows")
% (find-cwm2text (+ 9  55)   "1. Universal Arrows")
% (cw7p 4 "universal-arrow-c-to-S")

\par CWM2
\par III. Universals and Limits
\par p.55: Definition: universal arrow from $c$ to $S$
\bsk

Fix $D$, $C$, $S:D→C$, $r∈D$, $c∈C$.

Then we have functors

$D(r,-):D→\Set$ and

$C(c,S-):D→\Set$.

Every $u:c→Sr$ induces a NT
%
$\begin{array}[t]{rcrcl}
  (S-∘u) &:& D(r,-) & \mtnto & C(c,S-), \\
 (S-∘u)d &:& D(r,d) & \mtnto & C(c,Sd) \\
          &&     f' & \mto  & Sf'∘u. \\
 \end{array}
$

\msk

We say that a pair $\ang{r,u}$ is a {\sl universal arrow from $c$ to $S$}

when $(S-∘u)$ (i.e., $λd.λf'.Sf'∘u$) is a natural isomorphism, i.e., when

every $(S-∘u)d$ (i.e., $λf'.Sf'∘u$) is a bijection.

In MacLane's and in my notation:
%
%D diagram universal-from-c-to-S
%D 2Dx     100    +45
%D 2D  100        B1
%D 2D              |
%D 2D              v
%D 2D  +20 B2 |-> B3
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 B4 |-> B5
%D 2D
%D 2D  +20 A0 --> A1
%D 2D
%D 2D  +20 C0 --> C1
%D 2D
%D 2D  +20 D0 --> D1
%D
%D ren              A0 A1 ==> D C
%D ren B1   B2 B3   B4 B5 ==> c  r Sr  d Sd
%D ren              C0 C1 ==> D(r,-) C(c,S-)
%D ren              D0 D1 ==> D(r,d) C(c,Sd)
%D
%D (( A0 A1  -> .plabel= a S
%D    B1 B3  -> .plabel= r u
%D    B2 B3 |-> .plabel= a S
%D    B2 B4  -> .plabel= l f'   B3 B5 -> .plabel= r Sf'
%D    B4 B5 |-> .plabel= b S
%D    B1 B5  -> .plabel= r \sm{f=\\Sf'∘u} .slide= 20pt
%D    C0 C1  -> .plabel= a (S-∘u)
%D    C0 C1  -> .plabel= b (\cong)
%D    D0 D1  -> .plabel= a (S-∘u)d
%D    D0 D1  -> .plabel= b (\cong)
%D ))
%D enddiagram
%
%D diagram universal-from-c-to-S-my
%D 2Dx     100    +45
%D 2D  100        B1
%D 2D              |
%D 2D              v
%D 2D  +20 B2 |-> B3
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 B4 |-> B5
%D 2D
%D 2D  +20 A0 --> A1
%D 2D
%D 2D  +20 C0 --> C1
%D 2D
%D 2D  +20 D0 --> D1
%D
%D ren              A0 A1 ==> \catB \catA
%D ren B1   B2 B3   B4 B5 ==> A B RB B' RB'
%D ren              C0 C1 ==> (B,-) (A,R-)
%D ren              D0 D1 ==> (B,B') (A,RB')
%D
%D (( A0 A1  -> .plabel= a R
%D    B1 B3  -> .plabel= r u
%D    B2 B3 |->
%D    B2 B4  -> .plabel= l β   B3 B5 -> .plabel= r Rβ
%D    B4 B5 |->
%D    B1 B5  -> .plabel= r \sm{g=\\u;Rβ} .slide= 20pt
%D    C0 C1  ->
%D    D0 D1  ->
%D ))
%D enddiagram
%D
$$\pu
  \diag{universal-from-c-to-S}
  \qquad
  \diag{universal-from-c-to-S-my}
$$

\msk

As comma categories (universal arrows are initial in comma categories):
%
%D diagram univ-c-to-S-comma
%D 2Dx     100     +20     +25     +20  +25
%D 2D  100 B1 |--> B2 ---> B3 <--| B4   C1
%D 2D      ||      ||       |       |    |
%D 2D      ||      ||       v       v    v
%D 2D  +25 B5 |--> B6 ---> B7 <--| B8   C2
%D 2D
%D 2D  +15 B9 ---> B10 == B11 <-- B12   C3
%D 2D
%D ren B1 B2 B3 B4 ==> * c Sr r
%D ren B5 B6 B7 B8 ==> * c Sd d
%D ren B9 B10 B11 B12 ==> 1 C C D
%D ren C1 C2 C3 ==> 〈r,u〉 〈d,f〉 (c↓S)
%D
%D (( B1 B2 |-> B2 B3 -> .plabel= a u B3 B4 <-|
%D    B5 B6 |-> B6 B7 -> .plabel= a f B7 B8 <-|
%D    B1 B5 =   B2 B6 =   B3 B7 -> .plabel= r Sf'   B4 B8 -> .plabel= r f'
%D    B9 B10 -> .plabel= a c B10 B11 = B11 B12 <- .plabel= a S
%D    C1 C2 -> .plabel= r f' C3 place
%D ))
%D enddiagram
%D
%D diagram univ-c-to-S-comma-my
%D 2Dx     100     +20     +25     +20  +25
%D 2D  100 B1 |--> B2 ---> B3 <--| B4   C1
%D 2D      ||      ||       |       |    |
%D 2D      ||      ||       v       v    v
%D 2D  +25 B5 |--> B6 ---> B7 <--| B8   C2
%D 2D
%D 2D  +15 B9 ---> B10 == B11 <-- B12   C3
%D 2D
%D ren B1 B2 B3 B4 ==> • A RB  B
%D ren B5 B6 B7 B8 ==> • A RB' B'
%D ren B9 B10 B11 B12 ==> 1 \catA \catA \catB
%D ren C1 C2 C3 ==> (\_,u,B) (\_,g,B') (\Sel_A↓R)
%D
%D (( B1 B2 |-> B2 B3 -> .plabel= a u B3 B4 <-|
%D    B5 B6 |-> B6 B7 -> .plabel= a g B7 B8 <-|
%D    B1 B5 =   B2 B6 =   B3 B7 -> .plabel= r Rβ   B4 B8 -> .plabel= r β
%D    B9 B10 -> .plabel= a \Sel_A B10 B11 = B11 B12 <- .plabel= a R
%D    C1 C2 -> .plabel= r (\_,β) C3 place
%D ))
%D enddiagram
%D
$$\pu
  \diag{univ-c-to-S-comma}
  \qquad
  \diag{univ-c-to-S-comma-my}
$$



\newpage

%  _   _       _                          _   ____  
% | | | |_ __ (_)_   _____ _ __ ___  __ _| | |___ \ 
% | | | | '_ \| \ \ / / _ \ '__/ __|/ _` | |   __) |
% | |_| | | | | |\ V /  __/ |  \__ \ (_| | |  / __/ 
%  \___/|_| |_|_| \_/ \___|_|  |___/\__,_|_| |_____|
%                                                   
% «universal-arrow-S-to-c» (to ".universal-arrow-S-to-c")
% (cw7p 5 "universal-arrow-S-to-c")
% (cw7    "universal-arrow-S-to-c")
% (find-cwm2page (+ 9  58)   "1. Universal Arrows")
% (find-cwm2text (+ 9  58)   "1. Universal Arrows")

\par CWM2
\par III. Universals and Limits
\par p.58: Definition: universal arrow from $S$ to $c$

\bsk

Fix $D$, $C$, $S:D→C$, $r∈C$, $c∈C$.

Then we have functors

$D(-,r):D^\op→\Set$ and

$C(S-,c,):D^\op→\Set$.

Every $v:Sr→c$ induces a NT
%
$\begin{array}[t]{rcrcl}
  (v∘S-) &:& D(-,r) & \mtnto & C(S-,c), \\
 (v∘S-)d &:& D(d,r) & \mtnto & C(Sd,c)  \\
          &&     f' & \mto  & v∘Sf'. \\
 \end{array}
$

\msk

We say that a pair $\ang{r,v}$ is a {\sl universal arrow from $S$ to $c$}

when $(v∘S-)$ (i.e., $λd.λf'.v∘Sf'$) is a natural isomorphism, i.e., when

every $(v∘S-)d$ (i.e., $λf'.v∘Sf'$) is a bijection.



%D diagram universal-from-S-to-c
%D 2Dx     100    +45
%D 2D  100 A0 <-- A1
%D 2D
%D 2D  +20 B0 <-| B1
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 B2 <-| B3
%D 2D      |
%D 2D      v
%D 2D  +20 B4
%D 2D
%D 2D  +20 C0 <-- C1
%D 2D
%D 2D  +20 D0 <-- D1
%D
%D ren              A0 A1 ==> C D
%D ren B0 B1   B2 B3   B4 ==> Sd d   Sr r   c
%D ren              C0 C1 ==> C(S-,c) D(-,r)
%D ren              D0 D1 ==> C(Sd,c) D(d,r)
%D
%D (( A0 A1  <- .plabel= a S
%D    B0 B1 <-| .plabel= a S
%D    B0 B2  -> .plabel= l Sf'   B1 B3 -> .plabel= r f'
%D    B2 B3 <-| .plabel= a S
%D    B2 B4  -> .plabel= l v
%D    B0 B4  -> .plabel= l v∘Sf' .slide= -20pt
%D    C0 C1 <-  .plabel= a (S-∘u)
%D    C0 C1 <-  .plabel= b (\cong)
%D    D0 D1 <- .plabel= a (S-∘u)d
%D    D0 D1 <- .plabel= b (\cong)
%D ))
%D enddiagram
%D
$$\pu
  \diag{universal-from-S-to-c}
$$


\newpage

%  _   _       _                          _        _ _   
% | | | |_ __ (_)_   _____ _ __ ___  __ _| |   ___| | |_ 
% | | | | '_ \| \ \ / / _ \ '__/ __|/ _` | |  / _ \ | __|
% | |_| | | | | |\ V /  __/ |  \__ \ (_| | | |  __/ | |_ 
%  \___/|_| |_|_| \_/ \___|_|  |___/\__,_|_|  \___|_|\__|
%                                                        
% «universal-element» (to ".universal-element")
% (cw7p 6 "universal-element")
% (cw7    "universal-element")
% (find-cwm2page (+ 9 57) "universal element")
% (find-cwm2text (+ 9 57) "universal element")

\par CWM2
\par III. Universals and Limits
\par p.57: universal element

\bsk

Fix $D$, $H:D→\Set$.

A {\sl universal element of $H$} is a pair $\ang{r,e}$ 

% Fix $D$, $C$, $S:D→C$, $r∈D$, $c∈C$.

Then we have a functor

$D(r,-):D→\Set$.

Every $e∈Hr$, which can be seen as an arrow $e:*→Hr$,

...induces a NT 
%
$\begin{array}[t]{rcrcl}
  ((H-)e)  &:& D(r,-)? & \mtnto & C(c,S-)?, \\
  ((H-)e)d &:& D(r,d) & \mtnto & Hd \\
          &&        f & \mto  & (Hf)e?. \\
 \end{array}
$

\msk

We say that a pair $\ang{r,u}$ is a {\sl universal arrow from $c$ to $S$}

when $(S-∘u)$ (i.e., $λd.λf'.Sf'∘u$) is a natural isomorphism, i.e., when

every $(S-∘u)d$ (i.e., $λf'.Sf'∘u$) is a bijection.


%D diagram universal-element
%D 2Dx     100    +45
%D 2D  100 A0 --> A1
%D 2D
%D 2D  +20        B1
%D 2D              |
%D 2D              v
%D 2D  +20 B2 |-> B3
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 B4 |-> B5
%D 2D
%D 2D  +20 C0 --> C1
%D 2D
%D 2D  +20 D0 --> D1
%D
%D ren              A0 A1 ==> D \Set
%D ren B1   B2 B3   B4 B5 ==> *  r Hr  d Hd
%D ren              C0 C1 ==> D(r,-) H
%D ren              D0 D1 ==> D(r,d) Hd
%D
%D (( A0 A1  -> .plabel= a H
%D    B1 B3  -> .plabel= r u
%D    B2 B3 |-> .plabel= a S
%D    B2 B4  -> .plabel= l f   B3 B5 -> .plabel= r Hf
%D    B4 B5 |-> .plabel= b S
%D    B1 B5  -> .plabel= r \sm{(Hf)e\\=x} .slide= 20pt
%D    C0 C1  -> .plabel= a (S-∘u)
%D    C0 C1  -> .plabel= b (\cong)
%D    D0 D1  -> .plabel= a (S-∘u)d
%D    D0 D1  -> .plabel= b (\cong)
%D ))
%D enddiagram
%D
$$\pu
  \diag{universal-element}
$$






\newpage

% __   __                   _         _     ____  
% \ \ / /__  _ __   ___  __| | __ _  | |   | __ ) 
%  \ V / _ \| '_ \ / _ \/ _` |/ _` | | |   |  _ \ 
%   | | (_) | | | |  __/ (_| | (_| | | |___| |_) |
%   |_|\___/|_| |_|\___|\__,_|\__,_| |_____|____/ 
%                                                 
% «yoneda-behind» (to ".yoneda-behind")
% (cw7p 7 "yoneda-behind")
% (cw7    "yoneda-behind")
\label{yoneda-behind}

\par CWM2
\par III. Universals and Limits
\par p.59: 2. The Yoneda Lemma
\par {\bf The lemma behind Yoneda, in my notation}

%D diagram ??
%D 2Dx     100    +35
%D 2D  100        A1 
%D 2D              | 
%D 2D              v 
%D 2D  +20 A2 |-> A3 
%D 2D
%D 2D         ^ |    
%D 2D         | |    
%D 2D         | v    
%D 2D
%D 2D  +30 B1 --> B2 
%D 2D
%D ren A1 A2 A3 ==> A B RB
%D ren B1 B2    ==> (B,-) (A,R-)
%D
%D (( A2 A3 |-> A1 A3 -> .plabel= r η
%D    B1 B2 -> .plabel= b S
%D
%D    A2 B2 varrownodes nil 17 nil -> sl_ .plabel= l D
%D    A2 B2 varrownodes nil 17 nil <- sl^ .plabel= r U
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

There is a bijection between morphisms $η:A→RB$

and natural transformations $S:(B,-)→(A,R-)$.

$D$ is $SCf := η;Rf$, i.e., $S:=λC.λf.(η;Rf)$ and $D := λη.λC.λf.(η;Rf)$.

$U$ is $ε := SB\id_B$, i.e., $U := λS.SB\id_B$.

We want to check that $U(Dη)=η$ and $D(US)=S$.

Using just (untyped) $λ$-calculus we can prove $U(Dη)=η$ easily,

but the proof of $D(US)=S$ stops halfway...

$$\begin{array}{rcl}
  U(Dη) &=& (λS.SB(\id_B))((λη.λC.λf.(η;Rf))(η)) \\
        &=& (λS.SB(\id_B))(λC.λf.(η;Rf)) \\
        &=& (λC.λf.(η;Rf))B(\id_B) \\
        &=& (λf.(η;Rf))(\id_B) \\
        &=& η;R(\id_B) \\
        &=& η;\id_{RB} \\
        &=& η \\
  \\
  D(US) &=& (λη.λC.λf.(η;Rf))(SB(\id_B)) \\
        &=& λC.λf.((SB(\id_B));Rf) \\
  \end{array}
$$

\newpage

% __   __                   _         _     ____ ____  
% \ \ / /__  _ __   ___  __| | __ _  | |   | __ )___ \ 
%  \ V / _ \| '_ \ / _ \/ _` |/ _` | | |   |  _ \ __) |
%   | | (_) | | | |  __/ (_| | (_| | | |___| |_) / __/ 
%   |_|\___/|_| |_|\___|\__,_|\__,_| |_____|____/_____|
%                                                      
% «yoneda-behind-2» (to ".yoneda-behind")
% (cw7p 8 "yoneda-behind-2")
% (cw7    "yoneda-behind-2")

\par CWM2
\par III. Universals and Limits
\par p.59: 2. The Yoneda Lemma
\par {\bf The lemma behind Yoneda, in my notation (2)}

We need the naturality (a.k.a. the ``condition on squares'') of $S$:
%
%D diagram sqcond-1
%D 2Dx     100    +25
%D 2D  100        A1 
%D 2D              | 
%D 2D              v 
%D 2D  +20 A2 |-> A3 
%D 2D      |       | 
%D 2D      v       v 
%D 2D  +20 A4 |-> A5 
%D 2D      |       | 
%D 2D      v       v 
%D 2D  +20 A6 |-> A7 
%D 2D
%D ren  A1  A2 A3  A4 A5  A6 A7 ==> A  B RB  C RC  D RD
%D
%D (( A2 A3 |->
%D    A4 A5 |->
%D    A6 A7 |->
%D    A2 A4 -> .plabel= l f
%D    A4 A6 -> .plabel= l g
%D    A1 A3 -> .plabel= r η
%D    A3 A5 -> .plabel= r Rf
%D    A5 A7 -> .plabel= r Rg
%D    A1 A5 -> .slide= 20pt .plabel= r h
%D ))
%D enddiagram
%D
%D diagram sqcond-2
%D 2Dx     100 +25   +35 +35   +35
%D 2D  100 B1  C1 -> C2  D1 -> D2
%D 2D      |   |      |  |      v
%D 2D  +23 v   v      v  v     D4
%D 2D   +7 B2  C3 -> C4  D3 -> D5
%D 2D
%D 2D  +20     A1 -> A2
%D 2D
%D ren A1 A2 ==> (B,-) (A,R-)
%D ren B1 B2 ==> C D
%D ren C1 C2 C3 C4 ==> (B,C) (A,RC) (B,D) (A,RD)
%D ren D1 D2 D3 D4 D5 ==> f SCf f;g (SCf);Rg SD(f;g)
%D
%D (( A1 A2 -> .plabel= a S
%D    B1 B2 -> .plabel= l g
%D    C1 C2 -> .plabel= a SC
%D    C1 C3 -> .plabel= m λg.(f;g)
%D    C2 C4 -> .plabel= m λh.(h;Rg)
%D    C3 C4 -> .plabel= a SD
%D    D1 D2 |-> D2 D4 |-> D1 D3 |-> D3 D5 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{sqcond-1}
  \qquad
  \diag{sqcond-2}
$$

which yields $(SCf);Rg=SD(f;g)$. Substituting
  $\bsm{C:=B\\ D:=C\\ f:=\id_B\\ g:=f}$ in that we get

$(SB(\id_B));Rf=SC(\id_B;f)$, and so:
%
$$\begin{array}{rcl}
  D(US) &=& (λη.λC.λf.(η;Rf))(SB(\id_B)) \\
        &=& λC.λf.((SB(\id_B));Rf) \\
        &=& λC.λf.SC(\id_B;f) \\
        &=& λC.λf.SCf \\
        &=& S. \\
  \end{array}
$$

The last step can be explained as:

$$\begin{array}{rcl}
  D(US)Cf &=& (λC.λf.SCf)Cf \\
          &=& (λf.SCf)f \\
          &=& SCf \\
  \end{array}
$$



% \end{document}



\newpage

% __   __                   _       
% \ \ / /__  _ __   ___  __| | __ _ 
%  \ V / _ \| '_ \ / _ \/ _` |/ _` |
%   | | (_) | | | |  __/ (_| | (_| |
%   |_|\___/|_| |_|\___|\__,_|\__,_|
%                                   
% «yoneda» (to ".yoneda")
% (cw7p 9 "yoneda")
% (cw7    "yoneda")
% (find-cwm2page (+ 9  55) "III. Universals and Limits")
% (find-cwm2text (+ 9  55) "III. Universals and Limits")
% (find-cwm2page (+ 9  59) "2. The Yoneda Lemma")
% (find-cwm2text (+ 9  59) "2. The Yoneda Lemma")
% (find-cwm2page (+ 9  61) "Lemma (Yoneda)")
% (find-cwm2text (+ 9  61) "Lemma (Yoneda)")
% (cw7p 9 "yoneda")

\par CWM2
\par III. Universals and Limits
\par p.59: 2. The Yoneda Lemma
\par p.61: Lemma (Yoneda).
\par {\bf Yoneda in my notation:}

\msk


%D diagram yoneda-0
%D 2Dx     100 +75 +80
%D 2D  100     B0  C0
%D 2D
%D 2D  +30 A1  B1  C1
%D 2D
%D 2D  +30 A2  B2  C2
%D 2D
%D 2D  +30     B3  C3
%D 2D
%D ren    A1 A2    ==> g:A→RC  T:(C,-)→(A,R-)
%D ren B0 B1 B2 B3 ==> r∈RC    r':1→RC     T':(C,-)→(1,R-)       T'':(C,-)→R
%D ren C0 C1 C2 C3 ==> f:B→C  f':1→(B,C)  T''':(C,-)→(1,(B,-))  f^*:(C,-)→(B,-)
%D
%D (( A1 A2 <-| sl_
%D    A1 A2 |-> sl^
%D    
%D    B0 B1 <-| sl_
%D    B0 B1 |-> sl^
%D    B1 B2 <-| sl_
%D    B1 B2 |-> sl^
%D    B2 B3 <-| sl_
%D    B2 B3 |-> sl^
%D    
%D    C0 C1 <-| sl_
%D    C0 C1 |-> sl^
%D    C1 C2 <-| sl_
%D    C1 C2 |-> sl^
%D    C2 C3 <-| sl_
%D    C2 C3 |-> sl^
%D
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{yoneda-0}
$$



%D diagram yoneda-1
%D 2Dx     100    +35      +35    +35     +35    +40
%D 2D  100        A1              C1             E1
%D 2D              |               |              |
%D 2D              v               v              v
%D 2D  +30 A2 |-> A3       C2 |-> C3      E2 |-> E3
%D 2D
%D 2D         ^ |             ^ |            ^ |
%D 2D         | |     --->    | |    --->    | |
%D 2D         | v             | v            | v
%D 2D
%D 2D  +30 B1 --> B2       D1 --> D2      F1 --> F2
%D 2D          \   |           \   |          \   |
%D 2D           v  v            v  v           v  v
%D 2D  +30        B3              D3             F3    
%D 2D
%D ren A1 A2 A3 ==> A C RC
%D ren C1 C2 C3 ==> 1 C RC
%D ren E1 E2 E3 ==> 1 C (B,C)
%D ren B1 B2    ==> (C,-) (A,R-)
%D ren D1 D2 D3 ==> (C,-) (1,R-) R
%D ren F1 F2 F3 ==> (C,-) (1,(B,-)) (B,-)
%D
%D (( A2 A3 |-> A1 A3 -> .plabel= r α
%D    C2 C3 |-> C1 C3 -> .plabel= r r
%D    E2 E3 |-> E1 E3 -> .plabel= r f
%D    B1 B2 -> .plabel= b T
%D    D1 D2 -> D2 D3 <-> D1 D3 -> .plabel= b T'
%D    F1 F2 -> F2 F3 <-> F1 F3 -> .plabel= b f^*
%D
%D    A2 B2 varrownodes nil 17 nil -> sl_
%D    A2 B2 varrownodes nil 17 nil <- sl^
%D    C2 D2 varrownodes nil 17 nil -> sl_
%D    C2 D2 varrownodes nil 17 nil <- sl^ .plabel= r y
%D    E2 F2 varrownodes nil 17 nil -> sl_ .plabel= l Y
%D    E2 F2 varrownodes nil 17 nil <- sl^
%D
%D    B2 C2 harrownodes nil 20 nil ->
%D    D2 E2 harrownodes nil 20 nil ->
%D ))
%D enddiagram
%D
$$\pu
  \diag{yoneda-1}
$$

\bsk

\par Left part:
\par Fix categories $\catA$ and $\catC$, a functor $R:\catC→\catA$, and objects $A∈\catA$, $C∈\catC$.
\par We have functors $(C,-):\catC→\Set$ and $(A,R-):\catC→\Set$.
\par Each map $α:A→RC$ induces a NT $T:(C,-)→(A,R-)$ and vice-versa.
\par The formulas are $T:=λD:\catC.λf:(C,D).(a;Rf)$ and $α=T_C(\id_C)$,
\par and the `$↓↑$' is a bijection.

\msk

\par Middle part:
\par We take the left part and substitute $\catA:=\Set$ and $A:=1$.
\par The functor $R$ becomes a functor from $\catC$ to $\Set$.
\par There is a natural iso (`$\updownarrow$', unnamed) between the functors $(1,R-)$ and $R$.
\par We have a bijection between arrows $r:1→RC$ (or elements of $RC$)
\par and natural transformations $T':(C,-)→R$.
\par The {\sl Yoneda map} `$y$' in `$↓↑y$' is a bijection $y:\Nat((C,-),R)≅RC$.

\msk

\par Right part:
\par Choose an object $B∈\catC$. Take the middle part and substitute $R:=(B,-)$.
\par We get a bijection ${Y}{↓}{↑}$ between maps $f:B→C$ and NTs
\par $f^*:(C,-)→(B,-)$. The {\sl Yoneda Functor} $Y:\catC^\op→\Set^\catC$ behaves as:

%D diagram ??
%D 2Dx     100 +20 +25
%D 2D  100 A1  A2  A3
%D 2D
%D 2D  +20 A4  A5  A6
%D 2D
%D ren A1 A4 ==> B C
%D ren A2 A5 ==> B^\op C^\op
%D ren A3 A6 ==> (B,-) (C,-)
%D
%D (( A1 A4 -> .plabel= l f
%D    A2 A5 <- .plabel= l f^\op
%D    A3 A6 <- .plabel= r Yf
%D    A2 A3 |->  A5 A6 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$



\newpage

% __   __                   _         _     
% \ \ / /__  _ __   ___  __| | __ _  | |    
%  \ V / _ \| '_ \ / _ \/ _` |/ _` | | |    
%   | | (_) | | | |  __/ (_| | (_| | | |___ 
%   |_|\___/|_| |_|\___|\__,_|\__,_| |_____|
%                                           
% «yoneda-L» (to ".yoneda-L")
% (cw7p 11 "yoneda-L")
% (cw7     "yoneda-L")
% (find-cwm2page (+ 9  55) "III. Universals and Limits")
% (find-cwm2text (+ 9  55) "III. Universals and Limits")
% (find-cwm2page (+ 13 59) "2. The Yoneda Lemma")
% (find-cwm2text (+ 13 59) "2. The Yoneda Lemma")
% (find-cwm2page (+ 13 61) "Lemma (Yoneda)")
% (find-cwm2text (+ 13 61) "Lemma (Yoneda)")

\label{yoneda-L}
\par CWM2
\par III. Universals and Limits
\par p.59: 2. The Yoneda Lemma
\par p.61: Lemma (Yoneda).

\msk

%D diagram ??
%D 2Dx     100    +35      +35    +45     +35    +45
%D 2D  100        A1              C1             E1
%D 2D              |               |              |
%D 2D              v               v              v
%D 2D  +30 A2 |-> A3       C2 |-> C3      E2 |-> E3
%D 2D
%D 2D         ^ |             ^ |            ^ |
%D 2D         | |     --->    | |    --->    | |
%D 2D         | v             | v            | v
%D 2D
%D 2D  +30 B1 --> B2       D1 --> D2      F1 --> F2
%D 2D          \   |           \   |          \   |
%D 2D           v  v            v  v           v  v
%D 2D  +30        B3              D3             F3    
%D 2D
%D ren A1 A2 A3 ==> c r Sr
%D ren C1 C2 C3 ==> * r Kr
%D ren E1 E2 E3 ==> * r D(s,r)
%D ren B1 B2    ==> D(r,-) C(c,S-)
%D ren D1 D2 D3 ==> D(r,-) \Set(*,K-) K
%D ren F1 F2 F3 ==> D(r,-) \Set(*,D(s,-)) D(s,-)
%D
%D (( A2 A3 |-> A1 A3 -> .plabel= r u
%D    C2 C3 |-> C1 C3 -> .plabel= r u
%D    E2 E3 |-> E1 E3 -> .plabel= r f
%D    B1 B2 -> .plabel= b T
%D    D1 D2 -> D2 D3 <-> D1 D3 -> .plabel= b T'
%D    F1 F2 -> F2 F3 <-> F1 F3 -> .plabel= b D(f,-)
%D
%D    A2 B2 varrownodes nil 17 nil -> sl_
%D    A2 B2 varrownodes nil 17 nil <- sl^
%D    C2 D2 varrownodes nil 17 nil -> sl_
%D    C2 D2 varrownodes nil 17 nil <- sl^ .plabel= r y
%D    E2 F2 varrownodes nil 17 nil -> sl_ .plabel= l Y
%D    E2 F2 varrownodes nil 17 nil <- sl^
%D
%D    B2 C2 harrownodes nil 20 nil ->
%D    D2 E2 harrownodes nil 20 nil ->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$





% (cw7p 5)



\newpage

% __   __                   _         _ 
% \ \ / /__  _ __   ___  __| | __ _  / |
%  \ V / _ \| '_ \ / _ \/ _` |/ _` | | |
%   | | (_) | | | |  __/ (_| | (_| | | |
%   |_|\___/|_| |_|\___|\__,_|\__,_| |_|
%                                       
% «yoneda-1» (to ".yoneda-1")
% (cw7p 12 "yoneda-1")
% (cw7     "yoneda-1")
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 9  55) "III. Universals and Limits")
% (find-cwm2text (+ 9  55) "III. Universals and Limits")
% (find-cwm2page (+ 9 59) "2. The Yoneda Lemma")
% (find-cwm2text (+ 9 59) "2. The Yoneda Lemma")

\par CWM2
\par III. Universals and Limits
\par p.59: 2. The Yoneda Lemma
\par Proposition 1

\bsk

%D diagram universal-from-c-to-S-2
%D 2Dx     100    +45    +45    +45
%D 2D  100 A0 --> A1
%D 2D
%D 2D  +20        B1
%D 2D              |
%D 2D              v
%D 2D  +20 B2 |-> B3
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 B4 |-> B5
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 B6 |-> B7
%D 2D
%D 2D  +20 C0 --> C1     C2 --> C3
%D 2D
%D 2D  +20 D0 --> D1
%D 2D
%D 2D  +20 E0 --> E1     E2 --> E3
%D 2D
%D 2D  +20 F0 --> F1     F2 --> F3
%D
%D ren              A0 A1 ==> D C
%D ren B1   B2 B3   B4 B5 ==> c  r Sr  d Sd
%D ren              B6 B7 ==>         d' Sd'
%D ren              C0 C1 ==> D(r,-) C(c,S-)
%D ren              D0 D1 ==> D(r,d) C(c,Sd)
%D ren              E0 E1 ==> D(r,r) C(c,Sr)
%D ren              F0 F1 ==> 1_r \begin{array}[t]{l}S1_r∘u\\=1_{Sr}∘u\\=u\end{array}
%D ren              C2 C3 ==> D(r,-) C(c,S-)
%D ren              E2 E3 ==> D(r,r) C(c,Sr)
%D ren              F2 F3 ==> 1_r φ_r(1_r)
%D
%D (( A0 A1  -> .plabel= a S
%D    B1 B3  -> .plabel= r u
%D    B2 B3 |-> .plabel= a S
%D    B2 B4  -> .plabel= l f'   B3 B5 -> .plabel= r Sf'
%D    B4 B5 |-> .plabel= m S
%D    B1 B5  -> .plabel= r Sf'∘u .slide= 20pt
%D    B4 B6  -> .plabel= l k    B5 B7 -> .plabel= r Sk
%D    B6 B7 |-> .plabel= b S
%D    C0 C1  -> .plabel= a (S-∘u)
%D    C0 C1  -> .plabel= b (\cong)
%D    D0 D1  -> .plabel= a (S-∘u)d
%D    D0 D1  -> .plabel= b (\cong)
%D    E0 E1  -> .plabel= a (S-∘u)r
%D    E0 E1  -> .plabel= b (\cong)
%D    F0 F1 |-> .plabel= a (S-∘u)r
%D    C2 C3  -> .plabel= a φ
%D    C2 C3  -> .plabel= b (\cong)
%D    E2 E3  -> .plabel= a φ_r
%D    E2 E3  -> .plabel= b (\cong)
%D    F2 F3 |-> .plabel= a φ_r
%D ))
%D enddiagram
%D
$$\pu
  \diag{universal-from-c-to-S-2}
$$



% (find-cwm2page (+ 9 59) "2. The Yoneda Lemma")
% (find-cwm2text (+ 9 59) "2. The Yoneda Lemma")
% (cw7p 5)

%D diagram yoneda-p59
%D 2Dx     100    +35   +40    +40
%D 2D  100 A0     A1
%D 2D      |
%D 2D      v
%D 2D  +20 A2 |-> A3    B2 |-> B3
%D 2D      |       |    |       |
%D 2D      |  |->  |    |  |->  |
%D 2D      v       v    v       v
%D 2D  +20 A4 |-> A5    B4 |-> B5
%D 2D      |       |    |       |
%D 2D      |  |->  |    |  |->  |
%D 2D      v       v    v       v
%D 2D  +20 A6 |-> A7    B6 |-> B7
%D 2D
%D ren A0 A1 A2 A3 A4 A5 A6 A7 ==> r ?  r D(r,r)  d D(r,d)  d' D(r,d')
%D ren       B2 B3 B4 B5 B6 B7 ==>     r C(c,Sr)  d C(c,Sd)  d' C(c,Sd')
%D
%D (( A0 A2  -> .plabel= l ρ
%D    A2 A4  -> .plabel= l f'    A3 A5  -> .plabel= r \sm{D(r,f')=\\λρ.f'∘ρ}
%D    A4 A6  -> .plabel= l k     A5 A7  -> .plabel= r  \sm{D(r,k)=\\λf'.k∘f'}
%D    A2 A3 |-> .plabel= a D(r,-)
%D    A4 A5 |->
%D    A6 A7 |->
%D    A2 A5 harrownodes nil 20 nil |->
%D    A4 A7 harrownodes nil 20 nil |->
%D
%D    B2 B3 |-> .plabel= a C(s,S-)
%D    B4 B5 |->
%D    B6 B7 |->
%D    B2 B4  -> .plabel= l f'    B3 B5  -> .plabel= r \sm{C(c,Sf')=\\λu.Sf'∘u}
%D    B4 B6  -> .plabel= l k     B5 B7  -> .plabel= r  \sm{C(c,Sk)=\\λg.Sk∘g}
%D    B2 B5 harrownodes nil 20 nil |->
%D    B4 B7 harrownodes nil 20 nil |->
%D ))
%D enddiagram
%D
% $$\pu
%   \diag{yoneda-p59}
% $$



%D diagram yoneda-p60
%D 2Dx     100    +40
%D 2D  100 A0 --> A1
%D 2D      |       |
%D 2D      v       v
%D 2D  +30 A2 --> A3
%D 2D
%D 2D  +20 B0 --> B1
%D 2D      |       |
%D 2D      v       v
%D 2D  +30 B2 --> B3
%D 2D
%D ren A0 A1 A2 A3 ==> D(r,r) C(c,Sr) D(r,d) C(c,Sd)
%D ren B0 B1 B2 B3 ==> 1_r  φ_r(1_r) f'     C(c,Sd)
%D
%D (( A0 A1 -> .plabel= a φ_r
%D    A0 A2 -> .plabel= l D(r,f') A1 A3 -> .plabel= r C(c,Sf')
%D    A2 A3 -> .plabel= b φ_r
%D    
%D    B0 B1 |-> .plabel= a φ_r
%D    B0 B2 |-> .plabel= l λρ.f'∘ρ B1 B3 |-> .plabel= r C(c,Sf')
%D    B2 B3 |-> .plabel= b φ_r
%D    
%D ))
%D enddiagram
%D
$$\pu
  \diag{yoneda-p59}
  \qquad
  \diag{yoneda-p60}
$$





\newpage

% __   __                   _         ____  
% \ \ / /__  _ __   ___  __| | __ _  |___ \ 
%  \ V / _ \| '_ \ / _ \/ _` |/ _` |   __) |
%   | | (_) | | | |  __/ (_| | (_| |  / __/ 
%   |_|\___/|_| |_|\___|\__,_|\__,_| |_____|
%                                   
% «yoneda-2» (to ".yoneda-2")
% (cw7p 13 "yoneda-2")
% (cw7     "yoneda-2")
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 9  55) "III. Universals and Limits")
% (find-cwm2text (+ 9  55) "III. Universals and Limits")
% (find-cwm2page (+ 9  60) "2. The Yoneda Lemma")
% (find-cwm2text (+ 9  60) "2. The Yoneda Lemma")
% (find-cwm2page (+ 9  60) "Proposition 2")
% (find-cwm2text (+ 9  60) "Proposition 2")

\par CWM2
\par III. Universals and Limits
\par p.59: 2. The Yoneda Lemma
\par p.60: Proposition 2

\bsk



%
%
%
% D ---K---> Set
%
%            *
%
% r          Kr
%
% d         Kd
%
% D(r,d)    Set(*,Kd)   Kd
%
% D(r,-)    Set(*,K-)   K
%
%

%D diagram ??
%D 2Dx     100    +50    +40 
%D 2D  100 A0 --> A1
%D 2D
%D 2D  +20 B0     B1
%D 2D              |
%D 2D              |
%D 2D              v
%D 2D  +20 B2 |-> B3
%D 2D      |       |
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 B4 |-> B5
%D 2D
%D 2D  +20 C0 --> C1 --> C2
%D 2D
%D 2D  +20 D0 --> D1 --> D2
%D 2D
%D ren A0 A1 ==> D \Set
%D ren B0 B1 B2 B3 B4 B5 ==> ? * r Kr d Kd
%D ren C0 C1 C2 ==> D(r,d) \Set(*,Kd) Kd
%D ren D0 D1 D2 ==> D(r,-) \Set(*,K-) K
%D
%D (( A0 A1 -> .plabel= a K
%D
%D    B1 B3  -> .plabel= r u
%D    B2 B3 |->
%D    B2 B4  -> .plabel= l f'  B3 B5 -> .plabel= r Kf'
%D    B4 B5 |->
%D
%D    C0 C1  -> .plabel= a (K-∘u)d
%D    C0 C1  -> .plabel= b (≅)       C1 C2 -> .plabel= b (≅)
%D    D0 D1  -> .plabel= a (K-∘u)
%D    D0 D1  -> .plabel= b (≅)       D1 D2 -> .plabel= b (≅)
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$


\newpage


% __   __                   _          ____ _____ 
% \ \ / /__  _ __   ___  __| | __ _   / ___|  ___|
%  \ V / _ \| '_ \ / _ \/ _` |/ _` | | |  _| |_   
%   | | (_) | | | |  __/ (_| | (_| | | |_| |  _|  
%   |_|\___/|_| |_|\___|\__,_|\__,_|  \____|_|    
%                                                 
% «yoneda-GF» (to ".yoneda-GF")
% (cw7p 14 "yoneda-GF")
% (cw7     "yoneda-GF")
% (find-fline "/tmp/gf-yoneda.jpg")

Yoneda: GF

\ssk

$\begin{array}{rcrclclccl}
 f &:& A & → & B \\
   & & Nat(yB,F) & ↦ & Nat(yA,F) \\
   & &      c & ↦ & c∘(f∘-)    &:& yA → F \\
   & &        &    & c∘(f∘-)_C  &:& yAC → FC \\
   & &        &    &            &:& \catC(C,A) &→& FC \\
   & &        &    &            & & g         &↦& \Cat_c(f∘g) \\
 \end{array}
$



\newpage

%     _       _  _       _       _       
%    / \   __| |(_) ___ (_)_ __ | |_ ___ 
%   / _ \ / _` || |/ _ \| | '_ \| __/ __|
%  / ___ \ (_| || | (_) | | | | | |_\__ \
% /_/   \_\__,_|/ |\___/|_|_| |_|\__|___/
%             |__/                       
%
% «adjoints» (to ".adjoints")
% (cw7p 15 "adjoints")
% (cw7     "adjoints")
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 9  79) "IV. Adjoints")
% (find-cwm2page (+ 9  79)   "1. Adjunctions")
% (find-cwm2text (+ 9  79)   "1. Adjunctions")
% (find-cwm2page (+ 9  80)   "adjunction")
% (find-cwm2text (+ 9  80)   "adjunction")

\par CWM2
\par IV. Adjoints
\par p.79: Adjunctions

\bsk

Fix $X$, $A$, $F:X→A$, $G:A→X$.

Then we have functors

$A(F-,-): X^\op×A→\Set$ and

$X(-,G-): X^\op×A→\Set$.

An {\sl adjunction from $X$ to $A$} is a triple $\ang{F,G,φ}:X⇀A$

where $φ:A(F-,-)→X(-,G-)$ is a natural iso, i.e.,

for all $x∈X$, $a∈A$ this is a bijection: $φ_{x,a}:A(Fx,a)→X(x,Ga)$

and $φ$ is natural in the sense that...


%D diagram adjoints-2
%D 2Dx     100 +20 +20  +60     +40  +40     +45
%D 2D  100    micro
%D 2D
%D 2D  +20 A0 <--> A1
%D 2D
%D 2D  +20 C0 <--| C1   D0 ---> D1   E0 ---> E1
%D 2D      |        |   ^        ^   ^        ^
%D 2D      |        |   |        |   |        |
%D 2D      v        v   |        |   |        |
%D 2D  +20 C2 <--| C3   |        |   |        |
%D 2D      |        |   |        |   |        |
%D 2D      |   ->   |   |        |   |        |
%D 2D      v        v   |        |   |        |
%D 2D  +20 C4 |--> C5   D2 ---> D3   E2 ---> E3
%D 2D
%D 2D  +20 F0 <--| F1   G0 ---> G1   H0 ---> H1
%D 2D      |        |   |        |   |        |
%D 2D      |   ->   |   |        |   |        |
%D 2D      v        v   |        |   |        |
%D 2D  +20 F2 |--> F3   |        |   |        |
%D 2D      |        |   |        |   |        |
%D 2D      |        |   |        |   |        |
%D 2D      v        v   v        v   v        v
%D 2D  +20 F4 |--> F5   G2 ---> G3   H2 ---> H3
%D 2D
%D 2D  +20 a0 <--> a1
%D 2D
%D 2D  +20 B0 <--> B1
%D 2D
%D ren  micro ==> \ang{F,G,φ}:X⇀A
%D ren  A0 A1 ==> A X
%D ren  a0 a1 ==> A(F-,-) X(-,G-)
%D ren  B0 B1 ==> A(Fx,a) X(x,Ga)
%D ren  C0 C1 C2 C3 C4 C5 ==> Fx' x' Fx x a Ga
%D ren  D0 D1 D2 D3       ==> A(Fx',a) X(x',Ga) A(Fx,a) X(x,Ga)
%D ren  E0 E1 E2 E3       ==> \medE \bigE f φf
%D ren  F0 F1 F2 F3 F4 F5 ==> Fx x a Ga a' Ga'
%D ren  G0 G1 G2 G3       ==> A(Fx,a) X(x,Ga) A(Fx,a') X(x,Ga')
%D ren  H0 H1 H2 H3       ==> f φf \medH \bigH
%D (( micro place
%D    A0 A1 <- sl^ .plabel= a F
%D    A0 A1 -> sl_ .plabel= b G
%D
%D    a0 a1 <- sl^ .plabel= a φ^{-1}
%D    a0 a1 -> sl_ .plabel= b φ
%D
%D    B0 B1 <- sl^ .plabel= a φ^{-1}_{x,a}
%D    B0 B1 -> sl_ .plabel= b φ_{x,a}
%D
%D    C0 C1 <-| .plabel= a F
%D    C0 C2  -> .plabel= l Fh   C1 C3 -> .plabel= r h
%D    C2 C3 <-| .plabel= a F
%D    C2 C4  -> .plabel= l f    C3 C5 -> .plabel= r g
%D    C4 C5 |-> .plabel= b G
%D    C0 C4  -> .slide= -20pt .plabel= l \sm{(Fh)^*f\\:=\;f∘Fh}
%D    C1 C5  -> .slide=  20pt .plabel= r \sm{h^*g\;:=\\g∘h}
%D    C2 C5 harrownodes nil 20 nil |-> sl__ .plabel= l φ
%D
%D    D0 D1  -> .plabel= a φ_{x'\!,a}
%D    D0 D2  <- .plabel= l (Fh)^*   D1 D3  <- .plabel= r h^*
%D    D2 D3  -> .plabel= b φ_{x,a}
%D
%D    E0 E1  -> .plabel= a φ_{x'\!,a} .slide= 12pt
%D    E0 E2  <- .plabel= l (Fh)^*   E1 E3  <- .plabel= r h^*
%D    E2 E3  -> .plabel= b φ_{x,a}
%D
%D    F0 F1 <-| .plabel= a F
%D    F0 F2  -> .plabel= l f    F1 F3 -> .plabel= r g
%D    F0 F3 harrownodes nil 20 nil |-> sl__ .plabel= l φ
%D    F2 F3 |-> .plabel= b G
%D    F2 F4  -> .plabel= l k    F3 F5 -> .plabel= r Gk
%D    F4 F5 |-> .plabel= b G
%D    F0 F4  -> .slide= -20pt .plabel= l \sm{k_*f\;:=\\k∘f}
%D    F1 F5  -> .slide=  20pt .plabel= r \sm{(Gk)_*g\\:=\;Gk∘g}
%D
%D    G0 G1 -> .plabel= a φ_{x,a}
%D    G0 G2 -> .plabel= l k_*  G1 G3 -> .plabel= r (Gk)_*
%D    G2 G3 -> .plabel= b φ_{x,a'}
%D
%D    H0 H1 -> .plabel= a φ_{x,a}
%D    H0 H2 -> .plabel= l k_*   H1 H3 -> .plabel= r (Gk)_*
%D    H2 H3 -> .plabel= b φ_{x,a'} .slide= -12pt
%D ))
%D enddiagram
%D
$$\pu
  \def\medE{\mat{(Fh)^*f \\ = f∘Fh}}
  \def\bigE{\mat{φ(f∘Fh) \\ = \\ h^*(φf) = \\ (φf)∘h^*}}
  \def\medH{\mat{k_*f \\ = k∘f}}
  \def\bigH{\mat{(Gk)_*(φf) \\ = Gk∘φf \\ = \\ φ(k∘f)}}
  \hbox to -30pt{}
  \diag{adjoints-2}
$$






\newpage

%     _       _  _       _       _         ____  
%    / \   __| |(_) ___ (_)_ __ | |_ ___  |___ \ 
%   / _ \ / _` || |/ _ \| | '_ \| __/ __|   __) |
%  / ___ \ (_| || | (_) | | | | | |_\__ \  / __/ 
% /_/   \_\__,_|/ |\___/|_|_| |_|\__|___/ |_____|
%             |__/                               
%
% «adjoints-2» (to ".adjoints-2")
% (cw7p 16 "adjoints-2")
% (cw7     "adjoints-2")
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 9  79) "IV. Adjoints")
% (find-cwm2page (+ 9  79)   "1. Adjunctions")
% (find-cwm2text (+ 9  79)   "1. Adjunctions")
% (find-cwm2page (+ 9  80)   "adjunction")
% (find-cwm2text (+ 9  80)   "adjunction")

\par CWM2
\par IV. Adjoints
\par p.79: Adjunctions - the naturality of $φ$

\bsk

Fix $X$, $A$, $F:X→A$, $G:A→X$, $\ang{F,G,φ}:X⇀A$.

Remember that we have functors

$A(F-,-): X^\op×A→\Set$ and

$X(-,G-): X^\op×A→\Set$,

and $φ:A(F-,-)→X(-,G-)$ is a natural transformation (and a natural iso)...

Let $〈h,k〉:〈x,a〉→〈x',a'〉$ be a morphism in $X^\op×A$.

The naturality of $φ$ is easier to see in this diagram:


%D diagram adjoints-3
%D 2Dx     100 +20 +20  +65     +65  +40     +45
%D 2D  100    micro
%D 2D
%D 2D  +20 A0 <--> A1
%D 2D
%D 2D  +20 C0 <--| C1   D0 ---> D1
%D 2D      |        |   |        |
%D 2D      |        |   |        |
%D 2D      v        v   v        v
%D 2D  +20 C2 <--| C3   D2 ---> D3
%D 2D      |        | 
%D 2D      |   ->   |
%D 2D      v        v
%D 2D  +20 C4 |--> C5   E0 ---> E1
%D 2D      |        |   |        |
%D 2D      |        |   |        |
%D 2D      v        v   v        v
%D 2D  +20 C6 |--> C7   E2 ---> E3
%D 2D
%D 2D  +20 a0 <--> a1   F0 ---> F1
%D 2D                   |        |
%D 2D                   |        v
%D 2D  +20 B0 <--> B1   |       F3
%D 2D  +10              F2 ---> F4
%D 2D
%D ren  micro ==> \ang{F,G,φ}:X⇀A
%D ren  A0 A1 ==> A X
%D ren  a0 a1 ==> A(F-,-) X(-,G-)
%D ren  B0 B1 ==> A(Fx,a) X(x,Ga)
%D ren  C0 C1 C2 C3 C4 C5 C6 C7 ==> Fx' x' Fx x a Ga a' Ga'
%D ren  D0 D1 D2 D3       ==> A(F-,-)〈x,a〉 X(-,G-)〈x,a〉 A(F-,-)〈x',a'〉 X(-,G-)〈x',a'〉
%D ren  E0 E1 E2 E3       ==> A(Fx,a) X(x,Ga) A(Fx',a') X(x',Ga')
%D ren  F0 F1 F2 F3 F4    ==> f φf k∘f∘Fh gk∘φf∘h φ(k∘f∘Fh)
%D # ren  G0 G1 G2 G3       ==> A(Fx,a) X(x,Ga) A(Fx,a') X(x,Ga')
%D # ren  H0 H1 H2 H3       ==> f φf \medH \bigH
%D (( micro place
%D    A0 A1 <- sl^ .plabel= a F
%D    A0 A1 -> sl_ .plabel= b G
%D
%D    a0 a1 <- sl^ .plabel= a φ^{-1}
%D    a0 a1 -> sl_ .plabel= b φ
%D
%D    B0 B1 <- sl^ .plabel= a φ^{-1}_{x,a}
%D    B0 B1 -> sl_ .plabel= b φ_{x,a}
%D
%D    C0 C1 <-| .plabel= a F
%D    C0 C2  -> .plabel= l Fh   C1 C3 -> .plabel= r h
%D    C2 C3 <-| .plabel= a F
%D    C2 C4  -> .plabel= l f    C3 C5 -> .plabel= r φf
%D    C4 C5 |-> .plabel= b G
%D    C4 C6  -> .plabel= l k    C5 C7 -> .plabel= r Gk
%D    C6 C7 |-> .plabel= b G
%D
%D    C0 C6  -> .slide= -20pt .plabel= l k∘f∘Fh
%D    C1 C7  -> .slide=  20pt .plabel= r gk∘φf∘h
%D    C2 C5 harrownodes nil 20 nil |-> sl__ .plabel= l φ
%D
%D    D0 D1  -> .plabel= a φ〈a,x〉
%D    D0 D2  -> .plabel= l A(F-,-)〈k,h〉   D1 D3  -> .plabel= r X(-,G-)〈k,h〉
%D    D2 D3  -> .plabel= b φ〈a',x'〉
%D
%D    E0 E1  -> .plabel= a φ_{x,a}
%D    E0 E2  -> .plabel= l A(Fh,k)   E1 E3  -> .plabel= r X(h,Gk)
%D    E2 E3  -> .plabel= b φ_{x'\!,a'}
%D
%D    F0 F1 |-> F1 F3 |->   F0 F2 |-> F2 F4 |->
%D
%D    # E0 E1  -> .plabel= a φ_{x'\!,a} .slide= 12pt
%D    # E0 E2  <- .plabel= l (Fh)^*   E1 E3  <- .plabel= r h^*
%D    # E2 E3  -> .plabel= b φ_{x,a}
%D
%D    # F0 F1 <-| .plabel= a F
%D    # F0 F2  -> .plabel= l f    F1 F3 -> .plabel= r g
%D    # F0 F3 harrownodes nil 20 nil |-> sl__ .plabel= l φ
%D    # F2 F3 |-> .plabel= b G
%D    # F2 F4  -> .plabel= l k    F3 F5 -> .plabel= r Gk
%D    # F4 F5 |-> .plabel= b G
%D    # F0 F4  -> .slide= -20pt .plabel= l \sm{k_*f\;:=\\k∘f}
%D    # F1 F5  -> .slide=  20pt .plabel= r \sm{(Gk)_*g\\:=\;Gk∘g}
%D
%D    # G0 G1 -> .plabel= a φ_{x,a}
%D    # G0 G2 -> .plabel= l k_*  G1 G3 -> .plabel= r (Gk)_*
%D    # G2 G3 -> .plabel= b φ_{x,a'}
%D
%D    # H0 H1 -> .plabel= a φ_{x,a}
%D    # H0 H2 -> .plabel= l k_*   H1 H3 -> .plabel= r (Gk)_*
%D    # H2 H3 -> .plabel= b φ_{x,a'} .slide= -12pt
%D ))
%D enddiagram
%D
$$\pu
  \def\medE{\mat{(Fh)^*f \\ = f∘Fh}}
  \def\bigE{\mat{φ(f∘Fh) \\ = \\ h^*(φf) = \\ (φf)∘h^*}}
  \def\medH{\mat{k_*f \\ = k∘f}}
  \def\bigH{\mat{(Gk)_*(φf) \\ = Gk∘φf \\ = \\ φ(k∘f)}}
  \hbox to -30pt{}
  \diag{adjoints-3}
$$




\newpage

%  ___       _               _       __ 
% |_ _|_ __ | |_ ___ _ __ __| | ___ / _|
%  | || '_ \| __/ _ \ '__/ _` |/ _ \ |_ 
%  | || | | | ||  __/ | | (_| |  __/  _|
% |___|_| |_|\__\___|_|  \__,_|\___|_|  
%                                       
% «adjoints-interdef-1» (to ".adjoints-interdef-1")
% (cw7p 17 "adjoints-interdef-1")
% (cw7     "adjoints-interdef-1")
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 9  79) "IV. Adjoints")
% (find-cwm2page (+ 9  82)   "adjunction")
% (find-cwm2text (+ 9  82)   "adjunction")
% (find-cwm2page (+ 9  83)   "Theorem 2")
% (find-cwm2text (+ 9  83)   "Theorem 2")
% (find-angg "LATEX/2017adjunctions.tex")
% (cw7p 6)

\label{adjoints-interdef-1}
\par CWM2
\par IV. Adjoints
\par p.82: Adjunctions - interdefinabilities
\par (In MacLane's notation; unrevised)

\bsk

$F⊣G$, \;\; $〈F,G,φ〉:X⇀A$,

$\A \two/<-`->/<200>^F_G X$,
\;\;
$A(F-,-) \two/<-`->/<200>^{φ^{-1}}_φ X(-,G-)$.


%D diagram ??
%D 2Dx     100    +30
%D 2D  100 A0 <-| A1
%D 2D      |       |
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 A2 <-| A3
%D 2D      |       |
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 A4 |-> A5
%D 2D      |       |
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 A6 |-> A7
%D 2D
%D ren A0 A1 A2 A3 A4 A5 A6 A7 ==> Fx' x' Fx x a Ga a' Ga'
%D 
%D (( A0 A1 <-|
%D    A0 A2 -> .plabel= l Fh   A1 A3 -> .plabel= r h
%D    A2 A3 <-|
%D    A2 A4 -> .plabel= l \sm{φ^{-1}g\\f}   A3 A5 -> .plabel= r  \sm{g\\φf}
%D    A2 A5 harrownodes nil 20 nil <-| sl^ .plabel= a φ^{-1}
%D    A2 A5 harrownodes nil 20 nil |-> sl_ .plabel= b φ
%D    A4 A5 |->
%D    A4 A6 -> .plabel= l k   A5 A7 -> .plabel= r Gk
%D    A6 A7 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$



%D diagram ??
%D 2Dx     100    +30  +50   +30  +40   +30
%D 2D  100             C0    C1   E0    E1
%D 2D
%D 2D
%D 2D
%D 2D  +20 A0 <-| A1   C2    C3   E2    E3
%D 2D      |       |
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 A2 |-> A3   C4    C5   E4    E5
%D 2D
%D 2D
%D 2D
%D 2D  +20 B0 <-| B1   D0    D1   F0    F1
%D 2D      |       |
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 B2 |-> B3   D2    D3   F2    F3
%D 2D
%D 2D
%D 2D
%D 2D  +20             D4    D5   F4    F5
%D 2D
%D ren A0 A1 A2 A3 ==> Fx x Fx GFx
%D ren B0 B1 B2 B3 ==> FGa Ga a Ga
%D ren C0 C1 C2 C3 C4 C5 ==> Fx x FGa Ga a ?
%D ren D0 D1 D2 D3 D4 D5 ==> ? x Fx GFx a Ga
%D ren E0 E1 E2 E3 E4 E5 ==> Fx' x' ? x Fx GFx
%D ren F0 F1 F2 F3 F4 F5 ==> FGa Ga a ? a' Ga'
%D 
%D (( A0 A1 <-|
%D    A0 A2 -> .plabel= a \id_{Fx} A1 A3 -> .plabel= r \sm{ηx=\\(\id_{Fx})^♯}
%D    A2 A3 |->
%D    A0 A3 harrownodes nil 20 nil |-> sl_ .plabel= b φ
%D
%D    B0 B1 <-|
%D    B0 B2 -> .plabel= l \sm{ε_a=\\φ^{-1}(\id_{Ga})} B1 B3 -> .plabel= r \id_{Ga}
%D    B2 B3 |->
%D    B0 B3 harrownodes nil 20 nil <-| sl^ .plabel= a φ^{-1}
%D    
%D    C0 C1 <-|
%D    C0 C2 ->  .plabel= l Fg C1 C3 -> .plabel= r g
%D    C2 C3 <-|
%D    C2 C4 -> .plabel= l ε_a C3 C4 <-|
%D    C0 C4 -> .slide= -15pt .plabel= l \sm{φ^{-1}g=\\ε_a∘Fg}
%D
%D    D1 D2 |-> D1 D3 -> .plabel= r η_x
%D    D2 D3 |->
%D    D2 D4 -> .plabel= l f D3 D5 -> .plabel= r Gf
%D    D4 D5 |->
%D    D1 D5 -> .slide= 15pt .plabel= r \sm{φf=\\Gf∘η_x}
%D
%D    E0 E1 <-|
%D    E0 E4 -> .plabel= l \sm{Fh=\\φ^{-1}(η_x∘h)} E1 E3 -> .plabel= r h
%D    E3 E4 |-> E3 E5 -> .plabel= r η_x
%D    E4 E5 |->
%D
%D    F0 F1 |->
%D    F0 F2 -> .plabel= l ε_a F1 F2 <-|
%D    F1 F5 -> .plabel= r \sm{Gk=\\φ(k∘ε_a)}
%D    F2 F4 -> .plabel= l k
%D    F4 F5 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$


Theorem 2. $〈L,R,♯〉:\catA→\catB$ is completely determined by:

(i) $L, R, η$, with each $η_A$ universal

(ii) $G, F_0$ and universal arrows $η_A$

(iii) $F, G, ε$ with each $ε_a$ universal

(iv) $F, G_0$ and universal arrows $ε_a$

(v) 



\newpage

%  ___       _               _       __   ____  
% |_ _|_ __ | |_ ___ _ __ __| | ___ / _| |___ \ 
%  | || '_ \| __/ _ \ '__/ _` |/ _ \ |_    __) |
%  | || | | | ||  __/ | | (_| |  __/  _|  / __/ 
% |___|_| |_|\__\___|_|  \__,_|\___|_|   |_____|
%                                               
% «adjoints-3» (to ".adjoints-3")
% «adjoints-interdef-2» (to ".adjoints-interdef-2")
% (cw7p 18 "adjoints-interdef-2")
% (cw7     "adjoints-interdef-2")
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 9  79) "IV. Adjoints")
% (find-cwm2page (+ 9  82)   "adjunction")
% (find-cwm2text (+ 9  82)   "adjunction")
% (find-cwm2page (+ 9  83)   "Theorem 2")
% (find-cwm2text (+ 9  83)   "Theorem 2")
% (find-angg "LATEX/2017adjunctions.tex")

\label{adjoints-interdef-2}
\par CWM2
\par IV. Adjoints
\par p.82: Adjunctions - interdefinabilities
\par (In my notation)

\bsk

$L⊣R$, \;\; $〈L,R,♯〉:\catA→\catB$,

$\catB \two/<-`->/<200>^L_R \catA$,
\;\;
$\catB(L-,-) \two/<-`->/<200>^♭_♯ \catA(-,R-)$.


%D diagram ??
%D 2Dx     100    +30
%D 2D  100 A0 <-| A1
%D 2D      |       |
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 A2 <-| A3
%D 2D      |       |
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 A4 |-> A5
%D 2D      |       |
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 A6 |-> A7
%D 2D
%D ren A0 A1 A2 A3 A4 A5 A6 A7 ==> LA' A' LA A B RB B' RB'
%D 
%D (( A0 A1 <-|
%D    A0 A2 -> .plabel= l Lα   A1 A3 -> .plabel= r α
%D    A2 A3 <-|
%D    A2 A4 -> .plabel= l \sm{g^♭\\f}   A3 A5 -> .plabel= r  \sm{g\\f^♯}
%D    A2 A5 harrownodes nil 20 nil <-| sl^ .plabel= a ♭
%D    A2 A5 harrownodes nil 20 nil |-> sl_ .plabel= b ♯
%D    A4 A5 |->
%D    A4 A6 -> .plabel= l β   A5 A7 -> .plabel= r Rβ
%D    A6 A7 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$



%D diagram ??
%D 2Dx     100    +30  +50   +30  +40   +30
%D 2D  100             C0    C1   E0    E1
%D 2D
%D 2D
%D 2D
%D 2D  +20 A0 <-| A1   C2    C3   E2    E3
%D 2D      |       |
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 A2 |-> A3   C4    C5   E4    E5
%D 2D
%D 2D
%D 2D
%D 2D  +20 B0 <-| B1   D0    D1   F0    F1
%D 2D      |       |
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 B2 |-> B3   D2    D3   F2    F3
%D 2D
%D 2D
%D 2D
%D 2D  +20             D4    D5   F4    F5
%D 2D
%D ren A0 A1 A2 A3 ==> LA A LA RLA
%D ren B0 B1 B2 B3 ==> LRB RB B RB
%D ren C0 C1 C2 C3 C4 C5 ==> LA A LRB RB B ?
%D ren D0 D1 D2 D3 D4 D5 ==> ? A LA RLA B RB
%D ren E0 E1 E2 E3 E4 E5 ==> LA' A' ? A LA RLA
%D ren F0 F1 F2 F3 F4 F5 ==> LRB RB B ? B' RB'
%D 
%D (( A0 A1 <-|
%D    A0 A2 -> .plabel= a \id_{LA} A1 A3 -> .plabel= r \sm{η_A=\\(\id_{LA})^♯}
%D    A2 A3 |->
%D    A0 A3 harrownodes nil 20 nil |-> sl_ .plabel= b ♯
%D
%D    B0 B1 <-|
%D    B0 B2 -> .plabel= l \sm{ε_B=\\(\id_{RB})^β} B1 B3 -> .plabel= r \id_{RB}
%D    B2 B3 |->
%D    B0 B3 harrownodes nil 20 nil <-| sl^
%D    
%D    C0 C1 <-|
%D    C0 C2 ->  .plabel= l Lg C1 C3 -> .plabel= r g
%D    C2 C3 <-|
%D    C2 C4 -> .plabel= l ε_B C3 C4 <-|
%D    C0 C4 -> .slide= -15pt .plabel= l \sm{g^♭=\\Lg;ε_B}
%D
%D    D1 D2 |-> D1 D3 -> .plabel= r η_A
%D    D2 D3 |->
%D    D2 D4 -> .plabel= l f D3 D5 -> .plabel= r Rf
%D    D4 D5 |->
%D    D1 D5 -> .slide= 15pt .plabel= r \sm{f^♯=\\η_A;Rf}
%D
%D    E0 E1 <-|
%D    E0 E4 -> .plabel= l \sm{Lα=\\(α;η_A)^♭} E1 E3 -> .plabel= r α
%D    E3 E4 |-> E3 E5 -> .plabel= r η_A
%D    E4 E5 |->
%D
%D    F0 F1 |->
%D    F0 F2 -> .plabel= l ε_B F1 F2 <-|
%D    F1 F5 -> .plabel= r \sm{Rβ=\\ε_B;β}
%D    F2 F4 -> .plabel= l β
%D    F4 F5 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$


Theorem 2. $〈L,R,♯〉:\catA→\catB$ is completely determined by:

(i) $L, R, η$, with each $η_A$ universal

(ii) $G, F_0$ and universal arrows $η_A$

(iii) $F, G, ε$ with each $ε_a$ universal

(iv) $F, G_0$ and universal arrows $ε_a$

(v) 



\newpage

%  __  __                       _     
% |  \/  | ___  _ __   __ _  __| |___ 
% | |\/| |/ _ \| '_ \ / _` |/ _` / __|
% | |  | | (_) | | | | (_| | (_| \__ \
% |_|  |_|\___/|_| |_|\__,_|\__,_|___/
%                                     
% «monads» (to ".monads")
% (cw7p 19 "monads")
% (cw7     "monads")
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 9 137) "VI. Monads and Algebras")
% (find-cwm2text (+ 9 137) "VI. Monads and Algebras")
% (find-cwm2page (+ 9 137)   "1. Monads in a Category")

\label{monads}
\par CWM2
\par VI. Monads and Algebras
\par p.137: Monads

\bsk

Fix $X$, $T:X→X$, $μ:T^2 \mtnto T$, $η:I_X \mtnto T$.

Then we can make a diagram:

%D diagram monads-1
%D 2Dx     100   +30   +30   +30   +30   +30
%D 2D  100 A0 -> A1 <- A2    C0 -> C1 <- C2    
%D 2D                                          
%D 2D  +20 B0 -> B1 <- B2    D0 -> D1 <- D2    
%D 2D      | \    |     |    | \    |     |    
%D 2D      |  \   |     |    |  \   |     |    
%D 2D      v   v  v     v    v   v  v     v    
%D 2D  +30 B3 -> B4 <- B5    D3 -> D4 <- D5    
%D 2D
%D ren  A0 A1 A2  ==> I T T^2
%D ren  B0 B1 B2  ==> T T^2 T^3
%D ren  B3 B4 B5  ==> T^2 T T^2
%D 
%D ren  C0 C1 C2  ==> x Tx T^2x
%D ren  D0 D1 D2  ==> Tx T^2x T^3x
%D ren  D3 D4 D5  ==> T^2x Tx T^2x
%D 
%D (( A0 A1 -> .plabel= a η    A1 A2 <- .plabel= a μ
%D
%D    B0 B1 -> .plabel= a Tη   B1 B2 <- .plabel= a Tμ
%D    B0 B3 -> .plabel= a ηT   B0 B4 -> .plabel= m \id
%D    B1 B4 -> .plabel= r μ    B2 B5 -> .plabel= r μT
%D    B3 B4 -> .plabel= b μ    B4 B5 <- .plabel= b μ
%D
%D    C0 C1 -> .plabel= a ηx    C1 C2 <- .plabel= a μx
%D
%D    D0 D1 -> .plabel= a T(ηx) D1 D2 <- .plabel= a T(μx)
%D    D0 D3 -> .plabel= a η(Tx) D0 D4 -> .plabel= m \id
%D    D1 D4 -> .plabel= r μx    D2 D5 -> .plabel= r μ(Tx)
%D    D3 D4 -> .plabel= b μx    D4 D5 <- .plabel= b μx
%D    
%D ))
%D enddiagram
%D
$$\pu
  \diag{monads-1}
$$

A {\sl monad $T=\ang{T,η,μ}$ in a category $X$} is a triple as above

that obeys $μ∘ηT = I_X = μ∘Tη$ and $μ∘Tμ=μ∘μT$.


\newpage





%  __  __                       _             _           
% |  \/  | ___  _ __   __ _  __| |___    __ _| | __ _ ___ 
% | |\/| |/ _ \| '_ \ / _` |/ _` / __|  / _` | |/ _` / __|
% | |  | | (_) | | | | (_| | (_| \__ \ | (_| | | (_| \__ \
% |_|  |_|\___/|_| |_|\__,_|\__,_|___/  \__,_|_|\__, |___/
%                                               |___/     
%
% «monads-algebras» (to ".monads-algebras")
% (cw7p 20 "monads-algebras")
% (cw7     "monads-algebras")
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 9 139)   "2. Algebras for a Monad")
% (find-cwm2text (+ 9 139)   "2. Algebras for a Monad")

\par CWM2
\par VI. Monads and Algebras
\par 2. Algebras for a monad
\par p.140: $T$-algebras

\bsk

Fix $X$ and a monad $T=\ang{T,η,μ}$ in $X$.

A {\sl $T$-algebra} is a pair $\ang{x,h}$ with $x∈X$ and $h:Tx→x$

that obeys $\id_x = h∘ηx$, $h∘μx=h∘Th$:
%
%D diagram algebra-1
%D 2Dx     100   +30   +30
%D 2D  100 A0 -> A1 <- A2
%D 2D         \   |     |
%D 2D          v  v     v
%D 2D  +30       A3 <- A4
%D 2D
%D ren A0 A1 A2   A3 A4 ==> x Tx T^2x    x Tx
%D 
%D (( A0 A1 -> .plabel= a ηx   A1 A2 <- .plabel= a μx
%D    A0 A3 -> .plabel= l \id  A1 A3 -> .plabel= r h   A2 A4 -> .plabel= r Th
%D    A3 A4 <- .plabel= b h
%D ))
%D enddiagram
%D
%D diagram algebra-2
%D 2Dx     100   +30   +30
%D 2D  100 A0 -> A1 <- A2
%D 2D      |   /     /
%D 2D      v  v     v
%D 2D  +30 A3 <- A4
%D 2D
%D ren A0 A1 A2   A3 A4 ==> x Tx T^2x    x Tx
%D 
%D (( A0 A1 -> .plabel= a ηx   A1 A2 <- .plabel= a μx
%D    A0 A3 -> .plabel= l \id  A1 A3 -> .plabel= r h   A2 A4 -> .plabel= r Th
%D    A3 A4 <- .plabel= b h
%D ))
%D enddiagram
%D
$$\pu
  \diag{algebra-1}
  \quad
  \text{or}
  \quad
  \diag{algebra-2}
$$


% (find-cwm2page (+ 9 139)   "2. Algebras for a Monad")
% (find-cwm2text (+ 9 139)   "2. Algebras for a Monad")

A morphism $f:\ang{x,h}→\ang{x',h'}$ (in the category $X^T$ of $T$-algebras)

is a morphism $f:x→x'$ obeying $f∘h = h'∘Tf$.
%
%D diagram algebra-3
%D 2Dx     100   +30
%D 2D  100 x <-- Tx
%D 2D      |      |
%D 2D      v      v
%D 2D  +30 x' <- Tx'
%D 2D
%D (( x  Tx  <- .plabel= a h
%D    x   x' -> .plabel= l f    Tx Tx' -> .plabel= r Tf
%D    x' Tx' <- .plabel= b h'
%D ))
%D enddiagram
%D
$$\pu
  \diag{algebra-3}
$$

\newpage




%  __  __                       _                     
% |  \/  | ___  _ __   __ _  __| |___    _____  _____ 
% | |\/| |/ _ \| '_ \ / _` |/ _` / __|  / _ \ \/ / __|
% | |  | | (_) | | | | (_| | (_| \__ \ |  __/>  <\__ \
% |_|  |_|\___/|_| |_|\__,_|\__,_|___/  \___/_/\_\___/
%                                                     
% «monads-examples» (to ".monads-examples")
% (cw7p 21 "monads-examples")
% (cw7     "monads-examples")
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 9 139)   "2. Algebras for a Monad")
% (find-cwm2text (+ 9 139)   "2. Algebras for a Monad")

\par CWM2
\par VI. Monads and Algebras
\par First examples

\bsk

Let $M$ be a monoid.

We will call its identity $e$ and its elements $a,b,c$, etc.

Multiplication in $M$ will be written as $ab$.

Let $Q,R,S$ be (arbitrary) sets.

Then $T=(×M):\Set→\Set$ and $\ang{×M, η, μ}$ is a monad on $\Set$, where:

$\begin{array}{rcrcl}
 ηS &:& S &→& S×M \\
     && s &↦& \ang{s,e} \\
 \end{array}
$
%
\quad
and
\quad
%
$\begin{array}{rcrcl}
 μS &:&   (S×M)×M &→& S×M \\
     && \ang{\ang{s,a},b} &↦& \ang{s,ab}. \\
 \end{array}
$

In $λ$-notation they are $η = λS.λs.〈s,e〉$ and $μ = λS.λ〈〈s,a〉,b〉.〈s,ab〉$.

Note that the conditions on $η$ and $μ$, that we gave abstractly as:
%
%D diagram monads-1
%D 2Dx     100   +30   +30   +30   +30   +30
%D 2D  100 A0 -> A1 <- A2    C0 -> C1 <- C2    
%D 2D                                          
%D 2D  +20 B0 -> B1 <- B2    D0 -> D1 <- D2    
%D 2D      | \    |     |    | \    |     |    
%D 2D      |  \   |     |    |  \   |     |    
%D 2D      v   v  v     v    v   v  v     v    
%D 2D  +30 B3 -> B4 <- B5    D3 -> D4 <- D5    
%D 2D
%D ren  A0 A1 A2  ==> I T T^2
%D ren  B0 B1 B2  ==> T T^2 T^3
%D ren  B3 B4 B5  ==> T^2 T T^2
%D 
%D ren  C0 C1 C2  ==> x Tx T^2x
%D ren  D0 D1 D2  ==> Tx T^2x T^3x
%D ren  D3 D4 D5  ==> T^2x Tx T^2x
%D 
%D (( # A0 A1 -> .plabel= a η    A1 A2 <- .plabel= a μ
%D    # 
%D    # B0 B1 -> .plabel= a Tη   B1 B2 <- .plabel= a Tμ
%D    # B0 B3 -> .plabel= a ηT   B0 B4 -> .plabel= m \id
%D    # B1 B4 -> .plabel= r μ    B2 B5 -> .plabel= r μT
%D    # B3 B4 -> .plabel= b μ    B4 B5 <- .plabel= b μ
%D
%D    C0 C1 -> .plabel= a ηx    C1 C2 <- .plabel= a μx
%D
%D    D0 D1 -> .plabel= a T(ηx) D1 D2 <- .plabel= a T(μx)
%D    D0 D3 -> .plabel= a η(Tx) D0 D4 -> .plabel= m \id
%D    D1 D4 -> .plabel= r μx    D2 D5 -> .plabel= r μ(Tx)
%D    D3 D4 -> .plabel= b μx    D4 D5 <- .plabel= b μx
%D    
%D ))
%D enddiagram
%D
$$\pu
  \diag{monads-1}
$$

become:

%D diagram monads-xM
%D 2Dx     100   +35 +5  +5    +30 +10     +40
%D 2D  100 A0 ---------> A1    A2 <------- A3
%D 2D
%D 2D  +20 B0 ---------> B1    C0 <------- C1
%D 2D      |   \          |    |            |
%D 2D      |    \         |    |            |
%D 2D      |     \        |    |            |
%D 2D      |      \       v    v            |
%D 2D  +25 |       v     B3    C2           |
%D 2D  +5  v         B4                     v
%D 2D  +5 B2 -> B5                C3 <---- C4
%D 2D
%D ren A0 A1       ==> q     〈q,e〉
%D ren B0 B1 B2 B4 ==> 〈q,a〉 〈〈q,e〉,a〉  〈〈q,a〉,e〉 〈q,a〉
%D ren B5 B3       ==> 〈q,ea〉 〈q,ae〉
%D ren A2 A3       ==> 〈q,ab〉 〈〈q,a〉,b〉
%D ren C0 C1 C4    ==> 〈〈q,ab〉,c〉 〈〈〈q,a〉,b〉,c〉 〈〈q,a〉,bc〉
%D ren C2 C3       ==> 〈q,(ab)c〉 〈q,a(bc)〉
%D 
%D (( A0 A1 |->
%D    B0 B1 |->  B0 B2 |->   B0 B4 |->
%D    B2 B5 |->  B1 B3 |->
%D
%D    A2 A3 <-|
%D    C0 C1 <-|   C0 C2 |-> C1 C4 |->
%D    C3 C4 <-|
%D ))
%D enddiagram
%D
$$\pu
  \diag{monads-xM}
$$



\newpage

%  __  __                       _                       ____  
% |  \/  | ___  _ __   __ _  __| |___    _____  _____  |___ \ 
% | |\/| |/ _ \| '_ \ / _` |/ _` / __|  / _ \ \/ / __|   __) |
% | |  | | (_) | | | | (_| | (_| \__ \ |  __/>  <\__ \  / __/ 
% |_|  |_|\___/|_| |_|\__,_|\__,_|___/  \___/_/\_\___/ |_____|
%                                                     
% «monads-examples-2» (to ".monads-examples-2")
% (cw7p 22 "monads-examples-2")
% (cw7     "monads-examples-2")
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 9 139)   "2. Algebras for a Monad")
% (find-cwm2text (+ 9 139)   "2. Algebras for a Monad")

\label{monads-examples-2}
\par CWM2
\par VI. Monads and Algebras
\par First examples (2)

\bsk

Fix a monoid $M$ and sets $Q, R$.

An {\sl action of $M$ on a set $Q$} is a map
$\begin{array}[t]{rcrcl}
 h &:&  Q×M &→& Q \\
    && \ang{q,a} &↦& qa \\
 \end{array}
$

obeying $q(ab)=(qa)b$ and $qe=q$.

An {\sl action of $M$ on a set $R$} is a map
$\begin{array}[t]{rcrcl}
 h' &:&  R×M &→& R \\
    && \ang{r,a} &↦& qa \\
 \end{array}
$

obeying $r(ab)=(ra)b$ and $re=r$.

Note that we don't {\sl write} $h$ or $h'$.



\newpage

%  _  __            
% | |/ /__ _ _ __   
% | ' // _` | '_ \  
% | . \ (_| | | | | 
% |_|\_\__,_|_| |_| 
%                   
% «kan-1» (to ".kan-1")
% (cw7p 23 "kan-1")
% (cw7     "kan-1")
% (find-cwm2page (+ 9  83)    "unit and counit")
% (find-cwm2page (+ 7 233) "X. Kan Extensions")
% (find-cwm2page (+ 7 233)   "1. Adjoints and Limits")
% (find-cwm2page (+ 7 235)   "2. Weak Universality")
% (find-cwm2page (+ 7 236)   "3. The Kan Extension")
% (find-cwm2page (+ 7 240)   "4. Kan Extensions as Coends")
% (find-cwm2page (+ 7 243)   "5. Pointwise Kan Extensions")
% (find-cwm2page (+ 7 245)   "6. Density")
% (find-cwm2page (+ 7 248)   "7. All Concepts Are Kan Extensions")
% (cw7p 15)

{\bf Kan extensions in my notation}

\ssk

Archetypal example: the functor $Δ:\Set→\Set^{••}$

has both adjoints: $\text{Colim}⊣Δ⊣\text{Lim}$.

I will refer to the unit $η$ of $\text{Colim}⊣Δ$ as $\text{injs}$

and to the counit $ε$ of $Δ⊣\text{Lim}$ as $\text{projs}$.

\def\D#1#2{{(#1\phantom{E}#2)}}

%D diagram my-kan-1
%D 2Dx     100  +40     +40
%D 2D  100 L1   A1 |--> A2
%D 2D      |    |        |
%D 2D      v    |  <-->  |
%D 2D  +30 L2   v        v
%D 2D   +5      A3 <--| A4
%D 2D   +5 L3   |        |
%D 2D      |    |  <-->  |
%D 2D      v    v        v
%D 2D  +30 L4   A5 |--> A6
%D 2D           
%D 2D  +20      A7 <==> A8
%D 2D
%D ren A1 A2 ==> \D{B}{C} B{+}C
%D ren A3 A4 ==> \D{D}{D} D
%D ren A5 A6 ==> \D{E}{F} E{×}F
%D ren A7 A8 ==> \Set^{••} \Set
%D ren L1 L2 ==> \D{B}{C} \D{B{+}C}{B{+}C}
%D ren L3 L4 ==> \D{E{×}F}{E{×}F} \D{E}{F}
%D
%D (( A1 A2 |->
%D    A1 A3 -> A2 A4 ->
%D    A3 A4 <-|
%D    A3 A5 -> A4 A6 ->
%D    A5 A6 |->
%D    A7 A8 -> sl^^ .plabel= a \text{Colim}
%D    A7 A8 <-      .plabel= m Δ
%D    A7 A8 -> sl__ .plabel= b \text{Lim}
%D
%D    L1 L2 -> .plabel= l \text{injs}_\D{B}{C}
%D    L3 L4 -> .plabel= l \text{projs}_\D{E}{F}
%D ))
%D enddiagram
%D
$$\pu
  \diag{my-kan-1}
$$

%D diagram my-kan-2
%D 2Dx     100     +45     +60     +45  +60
%D 2D  100 B1 |--> B2 ---> B3 <--| B4   \Init
%D 2D      ||      ||       |       |
%D 2D      ||      ||       v       v
%D 2D  +25 B5 |--> B6 ---> B7 <--| B8
%D 2D
%D 2D  +20 B9 ---> B10 == B11 <-- B12
%D 2D
%D 2D  +30 C1 |--> C2 ---> C3 <--| C4
%D 2D      |       |       ||      ||
%D 2D      v       v       ||      ||
%D 2D  +25 C5 |--> C6 ---> C7 <--| C8   \Term
%D 2D
%D 2D  +20 C9 ---> C10 == C11 <-- C12
%D 2D
%D ren B1 B2 B3 B4 ==> • \D{B}{C} \D{B{+}C}{B{+}C} B{+}C 
%D ren B5 B6 B7 B8 ==> • \D{B}{C} \D{D}{D} D 
%D ren B9 B10 B11 B12 ==> 1 \Set^{••} \Set^{••} \Set
%D
%D ren C1 C2 C3 C4 ==> D \D{D}{D} \D{E}{F} •
%D ren C5 C6 C7 C8 ==>  E{×}F \D{E{×}F}{E{×}F} \D{E}{F} •
%D ren C9 C10 C11 C12 ==> \Set \Set^{••} \Set^{••} 1
%D
%D (( B1 B2 |-> B2 B3 -> .plabel= a \D{i}{i'} B3 B4 <-|
%D    B1 B5 = B2 B6 = B3 B7 -> B4 B8 ->
%D    B5 B6 |-> B6 B7 -> B7 B8 <-|
%D    B9 B10 -> .plabel= a \Sel_\D{B}{C} B10 B11 = B11 B12 <- .plabel= a Δ
%D    \Init place
%D ))
%D
%D (( C1 C2 |-> C2 C3 -> C3 C4 <-|
%D    C1 C5 = C2 C6 = C3 C7 -> C4 C8 ->
%D    C5 C6 |-> C6 C7 -> .plabel= a \D{π}{π'} C7 C8 <-|
%D    C9 C10 -> .plabel= a Δ C10 C11 = C11 C12 <- .plabel= a \Sel_\D{E}{F}
%D    \Term place
%D ))
%D enddiagram
%D
$$\pu
  \def\Init{⇐
    \begin{tabular}[c]{l}
    $(•, \D{i}{i'}, B{+}C)$ \\
    is an initial object in \\
    $(\Sel_\D{B}{C}↓Δ)$
    \end{tabular}
  }
  \def\Term{⇐
    \begin{tabular}[c]{l}
    $(E{×}F, \D{π}{π'}, •)$ \\
    is a terminal object in \\
    $(Δ↓\Sel_\D{E}{F})$
    \end{tabular}
  }
  \diag{my-kan-2}
$$



\newpage


%  _  __             ____  
% | |/ /__ _ _ __   |___ \ 
% | ' // _` | '_ \    __) |
% | . \ (_| | | | |  / __/ 
% |_|\_\__,_|_| |_| |_____|
%                          
% «kan-2» (to ".kan-2")
% (cw7p 24 "kan-2")
% (cw7     "kan-2")

{\bf Kan extensions in my notation}

\ssk

Archetypal example: the functor $f^*:\Set^4→\Set^6$

has both adjoints: $\text{Colim}⊣f^*⊣\text{Lim}$.

I will refer to the unit $η$ of $\text{Colim}⊣f^*$ as $\text{injs}$

and to the counit $ε$ of $f^*⊣\text{Lim}$ as $\text{projs}$.

\def\D#1#2{{(#1\phantom{E}#2)}}

\def\misp{\!\!\!\!\!\!\!\!\!\!}
\def\mi{\misp→\misp}
\def\Four#1#2#3#4{
  \left(\mat{
       &   & #1 \\
       &   & ↓ \\
    #2 &\mi& #3 \\
    ↓ &   &   \\
    #4 &   &   \\
  }\right)
}
\def\Six#1#2#3#4#5#6{
  \left(\mat{
    #1 &\mi& #2 \\
    ↓  &   & ↓ \\
    #3 &\mi& #4 \\
    ↓ &   &  ↓ \\
    #5 &\mi& #6 \\
  }\right)
}


%D diagram my-kan-1
%D 2Dx     100  +60     +60  +60
%D 2D  100 L1   A1 |--> A2   R1
%D 2D      |    |        |   | 
%D 2D      v    |  <-->  |   | 
%D 2D  +60 L2   v        v   v
%D 2D   +5      A3 <--| A4   R2
%D 2D   +5 L3   |        |   |
%D 2D      |    |  <-->  |   | 
%D 2D      v    v        v   v 
%D 2D  +60 L4   A5 |--> A6   R3
%D 2D           
%D 2D  +40      A7 <==> A8
%D 2D
%D ren A1 A2 ==> \Four{C_2}{C_3}{C_4}{C_5} \Six{0}{C_2}{C_3}{C_4}{C_5}{C_\text{po}}
%D ren A3 A4 ==> \Four{D_2}{D_3}{D_4}{D_5} \Six{D_1}{D_2}{D_3}{D_4}{D_5}{D_6}
%D ren A5 A6 ==> \Four{E_2}{E_3}{E_4}{E_5} \Six{E_\text{pb}}{E_2}{E_3}{E_4}{E_5}{1}
%D ren A7 A8 ==> \Set^4 \Set^6
%D ren R1 ==> \Six{0}{D_2}{D_3}{D_4}{D_5}{D_\text{po}}
%D ren R2 ==> \Six{D_1}{D_2}{D_3}{D_4}{D_5}{D_6}
%D ren R3 ==> \Six{D_\text{pb}}{D_2}{D_3}{D_4}{D_5}{1}
%D
%D (( A1 A2 |->
%D    A1 A3 -> A2 A4 ->
%D    A3 A4 <-|
%D    A3 A5 -> A4 A6 ->
%D    A5 A6 |->
%D    A7 A8 -> sl^^ .plabel= a \text{Colim}
%D    A7 A8 <-      .plabel= m f^*
%D    A7 A8 -> sl__ .plabel= b \text{Lim}
%D
%D    R1 R2 -> .plabel= r \text{injs}_\D{B}{C}
%D    R2 R3 -> .plabel= r \text{projs}_\D{E}{F}
%D ))
%D enddiagram
%D
$$\pu
  \diag{my-kan-1}
$$



\newpage


%  _  __             ____  _____  __   
% | |/ /__ _ _ __   |___ \|___ / / /_  
% | ' // _` | '_ \    __) | |_ \| '_ \ 
% | . \ (_| | | | |  / __/ ___) | (_) |
% |_|\_\__,_|_| |_| |_____|____/ \___/ 
%                                      
% «kan-236» (to ".kan-236")
% (cw7p 25 "kan-236")
% (cw7     "kan-236")
% (find-cwm2page (+ 7 236)   "3. The Kan Extension")

{\bf Kan extensions in my notation}

\ssk

\def\Ran{\text{Ran}}


%D diagram universal-from-S-to-c
%D 2Dx     100    +30   +25
%D 2D  100 B0 <-| B1
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 B2 <-| B3 == B3'
%D 2D      |
%D 2D      v
%D 2D  +20 B4
%D 2D
%D 2D  +15 C0 <-- C1
%D 2D
%D 2D  +15 D0 --> D1
%D
%D ren B0 B1   B2 B3   B4 ==> SK S   RK R   T
%D ren            B3'     ==> \Ran_K{T}
%D ren              C0 C1 ==> A^M A^C
%D ren              D0 D1 ==> M C
%D
%D (( B0 B1 <-| .plabel= a A^K
%D    B0 B2  -> .plabel= l σK   B1 B3 -> .plabel= r σ
%D    B2 B3 <-| .plabel= a A^K
%D    B3 B3'  =
%D    B2 B4  -> .plabel= l ε
%D    B0 B4  -> .plabel= l α .slide= -20pt
%D    C0 C1 <-  .plabel= a A^K
%D    D0 D1 ->  .plabel= a K
%D ))
%D enddiagram
%D
$$\pu
  \diag{universal-from-S-to-c}
$$




%
%            f
%  • |--> c --> Km <---| m
%
%  • |--> c --> Km' <--| m'
%            f'
%
%
%
%
%   (c↓K) --Q--> M --T--> A 
%
%






\end{document}

% Local Variables:
% coding: utf-8-unix
% ee-anchor-format: "«%s»"
% ee-tla: "cw7"
% End:
