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