|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2017yoneda.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2017yoneda.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2017yoneda.pdf"))
% (defun b () (interactive) (find-zsh "biber 2017yoneda"))
% (defun e () (interactive) (find-LATEX "2017yoneda.tex"))
% (defun u () (interactive) (find-latex-upload-links "2017yoneda"))
% (find-xpdfpage "~/LATEX/2017yoneda.pdf")
% (find-sh0 "cp -v ~/LATEX/2017yoneda.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2017yoneda.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2017yoneda.pdf
% file:///tmp/2017yoneda.pdf
% file:///tmp/pen/2017yoneda.pdf
% http://angg.twu.net/LATEX/2017yoneda.pdf
%
% «.abstract» (to "abstract")
% «.index-of-sections» (to "index-of-sections")
% «.internal-view» (to "internal-view")
% «.shape-and-notation» (to "shape-and-notation")
% «.Y0» (to "Y0")
% «.naturality» (to "naturality")
% «.stressing-bijections» (to "stressing-bijections")
% «.stronger-yoneda» (to "stronger-yoneda")
% «.representables» (to "representables")
% «.universals» (to "universals")
% «.adjunctions» (to "adjunctions")
% «.contravariant» (to "contravariant")
% «.embeddings» (to "embeddings")
% «.generic-figures» (to "generic-figures")
% «.morphisms-of-C-sets» (to "morphisms-of-C-sets")
% «.yoneda-in-RRZ» (to "yoneda-in-RRZ")
% «.CWM» (to "CWM")
% «.riehl» (to "riehl")
% «.awodey» (to "awodey")
%
\documentclass[oneside]{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")
%
\usepackage[backend=biber,
style=alphabetic]{biblatex} % (find-es "tex" "biber")
\addbibresource{catsem-u.bib}
%
\begin{document}
\catcode`\^^J=10
\directlua{dofile("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\und#1#2{\underbrace{#1}_{#2}}
\def\Nat{\mathrm{Nat}}
\def\ph{\phantom}
% (find-LATEX "edrx17defs.tex" "fcded")
\def\fcdiag#1{\fbox{$\diag{#1}$}}
\title{A skeleton for the proof of the Yoneda Lemma (working draft)}
\author{Eduardo Ochs}
\maketitle
% \setlength{\extrarowheight}{1pt}
% _ _ _ _
% / \ | |__ ___| |_ _ __ __ _ ___| |_
% / _ \ | '_ \/ __| __| '__/ _` |/ __| __|
% / ___ \| |_) \__ \ |_| | | (_| | (__| |_
% /_/ \_\_.__/|___/\__|_| \__,_|\___|\__|
%
% «abstract» (to ".abstract")
% (find-es "tex" "abstract")
\begin{abstract}
These notes consists of five parts.
The first part explains how to draw the ``internal view'' of a
diagram (or of a function, functor, natural transformation, etc).
The second part shows that a certain diagram, that we call diagram Y0,
is the ``skeleton'' of the proof of the Yoneda Lemma in the following
sense. In order to interpret that diagram formally we have to infer
the types of all its entities, and then infer (by ``term inference'',
as in \cite{OchsIDARCT}, obtaining untyped $λ$-terms) the actions on
morphisms of the four functors in Y0, and also the actions of the four
natural transformations and the actions of three bijections. The
bijections are called $B_1$, $B_2$ and $B_3$, where $B_1$ is easy to
construct, $B_2$ is obtained from $B_1$ by substituing a generic
functor and a generic object that appear in $B_1$ by specific ones,
and $B_3$ is $B_2$ composed with two trivial bijections, one at each
side. The statement of the Yoneda Lemma is essentially just ``$B_3$ is
a bijection''. In Category Theory texts above a certain level most
term inferences are treated as ``obvious'', so a (skeleton of a) proof
of the Yoneda Lemma is just diagram Y0 plus ``do the obvious type
inferences and term inferences''.
The third part discusses a gap in the second part. The ``bijection''
$B_3$ converts a map $f∈\Hom_\catC(B,C)$ into a natural transformation
$T''∈\Nat((C,-),(B,-))$ and a $T''$ into an $f$, but what we got in
the second part is just a pair of $λ$-terms of the right types,
$(B_3,B_3^{-1})$, without the proofs that $B_3^{-1}(B_3(f))=f$ and
that $B_3(B_3^{-1}(T''))=T''$. In the language of \cite{OchsIDARCT}
what we did was to drop, or erase, a lot of information (mainly the
``equational parts'') and then work in the ``syntactical world''; we
obtained a ``skeleton of a proof'' that must now must be ``lifted'' to
the ``real world'' by completing some missing parts. It turns out that
$B_3^{-1}(B_3(f))=f$ is trivial, but $B_3(B_3^{-1}(T''))=T''$ only
holds if $T''$ obeys the ``naturality condition'' that comes from it
being a natural transformation. The moral of the story so far is that
90\% of the proof of the Yoneda Lemma can be extracted from diagram Y0
if we do the ``obvious'' type and term inferences on it (``for some
value of 90\%'', of course); only a tiny part of the proof needs
things that get erased in the passage to the skeleton.
The fourth part uses these tools to state and prove three other
``Yoneda Lemmas'' and to define universal arrows, universal elements,
representable functors, and to show how some of these ideas are
motivated by adjunctions.
The fifth part uses all this to build ``bridges'' between several
notations. The less trivial case is how to translate between our
notation and the one in Reyes, Reyes and Zolfaghari's {\sl Generic
Figures and Their Glueings}; the translations between our notation
and MacLane's, Riehl's and Awodey's are easy (but only RRZ has been
written in details at the moment).
\end{abstract}
% \begin{abstract}
%
% We show that a certain diagram, that we call diagram Y0, is the
% ``skeleton'' of the proof of the Yoneda Lemma in the following sense.
% In order to interpret that diagram formally we have to infer the types
% of all its entities, and then infer (by ``term inference'', as in
% \cite{OchsIDARCT}, obtaining untyped $λ$-terms) the actions on
% morphisms of the four functors in Y0, and also the actions of the four
% natural transformations and the actions of three bijections. The
% bijections are called $B_1$, $B_2$ and $B_3$, where $B_1$ is easy to
% construct, $B_2$ is obtained from $B_1$ by substituing a generic
% functor and a generic object that appear in $B_1$ by specific ones,
% and $B_3$ is $B_2$ composed with two trivial bijections, one at each
% side. The statement of the Yoneda Lemma is essentially just ``$B_3$ is
% a bijection'', and this process constructs two arrows,
% $B_3:\Hom_\catC(B,C)→\Nat((C,-),(B,-))$ and
% $B_3^{-1}:\Nat((C,-),(B,-))→\Hom_\catC(B,C)$. In Category Theory texts
% above a certain level most term inferences are treated as ``obvious'',
% so a (skeleton of a) proof of the Yoneda Lemma is just diagram Y0 plus
% ``do the obvious type inferences and term inferences''.
%
% In a skeleton of a proof we drop, or erase, lots of information from
% the ``real'' proof and leave it to be reconstructed later. In the
% skeleton for the Yoneda Lemma described above we dropped the
% ``equational part'' (see sec.12 of \cite{OchsIDARCT}), and after that
% all the typings. When we do these erasings a bijection $f$ becomes
% just a pair $(f,f^{-1})$ of operations, {\sl without the proofs that
% their composites are identities} (a ``proto-bijection'' in the
% terminology of \cite{OchsIDARCT}). Our skeleton for the Yoneda Lemma
% yields $B_3$ and $B_3^{-1}$ (and $B_1$, $B_1^{-1}$, $B_2$, $B_2^{-1}$)
% as $λ$-terms, but not yet the proofs that $B_3^{-1}(B_3(f))=f$ and
% that $B_3(B_3^{-1}(T''))=T''$. It turns out that if we prove that
% $B_1$ is a ``real bijection'' then it follows that $B_2$ and $B_3$ are
% ``real bijections'', too. Proving that $B_1^{-1}(B_1(g))=g$ always
% holds is easy and can be done in untyped $λ$-calculus, but to prove
% that $B_1(B_1^{-1}(T))=T$ we need information from the ``equational
% part''; $B_1(B_1^{-1}(T))=T$ only holds if $T$ obeys the ``naturality
% condition'' that comes from it being a natural transformation.
%
% The moral of the story is that 90\% of the proof of the Yoneda Lemma
% can be extracted from diagram Y0 if we do the ``obvious'' type and
% term inferences on it (``for some value of 90\%'', of course); only a
% tiny part of the proof needs things that get erased in the passage to
% the skeleton.
%
% The last sections of this draft build ``bridges'' for translating
% between our notations (and diagrams) and some standard ones --- mainly
% \cite{ReyesZolf} (sec.\ref{RRZ}) and \cite{CWM2} (sec.\ref{CWM}).
%
% % {\bf Warning:} this is just a working draft whose main intent is to
% % show how to interpret diagrams as skeletons of categorical proofs.
%
% \end{abstract}
% ___ _ __ _ _
% |_ _|_ __ __| | _____ __ ___ / _| ___ ___ ___| |_(_) ___ _ __ ___
% | || '_ \ / _` |/ _ \ \/ / / _ \| |_ / __|/ _ \/ __| __| |/ _ \| '_ \/ __|
% | || | | | (_| | __/> < | (_) | _| \__ \ __/ (__| |_| | (_) | | | \__ \
% |___|_| |_|\__,_|\___/_/\_\ \___/|_| |___/\___|\___|\__|_|\___/|_| |_|___/
%
% «index-of-sections» (to ".index-of-sections")
% (yonp 2 "index-of-sections")
% (yona "index-of-sections")
% (find-es "tex" "tableofcontents")
% (find-es "tex" "dottedtocline")
% \tableofcontents
% (find-LATEXfile "2017yoneda.toc")
\bsk
Index of sections:
{\makeatletter
\renewcommand*\l@section{\@dottedtocline{1}{1.5em}{2.3em}}
\@starttoc{toc}
}
\bsk
% \newpage
%
% % ___ _ _ _ _
% % |_ _|_ __ | |_ _ __ ___ __| |_ _ ___| |_(_) ___ _ __
% % | || '_ \| __| '__/ _ \ / _` | | | |/ __| __| |/ _ \| '_ \
% % | || | | | |_| | | (_) | (_| | |_| | (__| |_| | (_) | | | |
% % |___|_| |_|\__|_| \___/ \__,_|\__,_|\___|\__|_|\___/|_| |_|
% %
% {\bf Important!} This is just a working draft whose main intent is to
% show how to interpret diagrams as skeletons of categorical proofs;
% also, this is part of a two bigger projects:
%
% \url{http://angg.twu.net/math-b.html\#notes-on-notation}
%
% \url{http://angg.twu.net/math-b.html\#lclt}
% ___ _ _ _
% |_ _|_ __ | |_ ___ _ __ _ __ __ _| | __ _(_) _____ __
% | || '_ \| __/ _ \ '__| '_ \ / _` | | \ \ / / |/ _ \ \ /\ / /
% | || | | | || __/ | | | | | (_| | | \ V /| | __/\ V V /
% |___|_| |_|\__\___|_| |_| |_|\__,_|_| \_/ |_|\___| \_/\_/
%
% «internal-view» (to ".internal-view")
\section{Internal views}
\label{internal-view}
\def\ooo(#1,#2){\begin{picture}(0,0)\put(0,0){\oval(#1,#2)}\end{picture}}
\def\oooo(#1,#2){{\setlength{\unitlength}{1ex}\ooo(#1,#2)}}
% (find-books "__cats/__cats.el" "lawvere")
% (find-books "__cats/__cats.el" "riehl")
% (find-LATEX "catsem-u.bib" "bib-LawvereSchanuel")
% (find-LATEX "catsem-u.bib" "bib-Riehl")
{\sl Note:} this section is an {\sl introduction} to the idea of
``internal views'' of categorical diagrams. I first saw this idea in
\cite{LawvereSchanuel}, p.13, but it is used in other places too ---
for example in p.17 of \cite{RiehlCTIC}. I used it a lot in
\cite{OchsIDARCT}, but there I insisted on a notion of ``downcasing''
that I've since abandoned.
\msk
When I was a kid my first exposure to functions was through diagrams
like this:
%
%D diagram first-blob-function
%D 2Dx 100 +20 +20
%D 2D 100 a0 |--> b0
%D 2D +08 a1 |--> b1
%D 2D +08 a2 |--> b2
%D 2D +08 a3 |--> b3
%D 2D +08 a4 |--> b4
%D 2D
%D ren a0 a1 a2 a3 a4 ==> 0 1 2 3 4
%D ren b0 b1 b2 b3 b4 ==> 0 1 2 3 4
%D (( a0 a2 midpoint .TeX= \oooo(7,12) y+= -2 place
%D b0 b4 midpoint .TeX= \oooo(7,17) y+= -2 place
%D a0 b0 ->
%D a1 b2 ->
%D a2 b4 ->
%D b1 place
%D b3 place
%D a0 relplace -7 -7 \phantom{foo}
%D b4 relplace 7 7 \phantom{bar}
%D ))
%D enddiagram
%D
$$\pu
\diag{first-blob-function}
$$
%
after a while --- actually years --- the blob-sets got names, like
$A$, $B$, $\N$, $\R$, the functions got names like $f$, $g$,
$√{\phantom{a}}$, and several conventions were established: we didn't
have to draw all elements in the blob-sets; we could draw a ``generic
element'', $n$, and indicate that it goes to $\sqrt{n}$; and we could
draw an ``external view'' of the function above or below the
``internal view'' given by the blobs:
%
%D diagram second-blob-function
%D 2Dx 100 +20 +20
%D 2D 100 a-1 |--> b-1
%D 2D +08 a0 |--> b0
%D 2D +08 a1 |--> b1
%D 2D +08 a2 |--> b2
%D 2D +08 a3 |--> b3
%D 2D +08 a4 |--> b4
%D 2D +14 a5 |--> b5
%D 2D +25 \N ---> \R
%D 2D
%D ren a-1 a0 a1 a2 a3 a4 a5 ==> -1 0 1 2 3 4 n
%D ren b-1 b0 b1 b2 b3 b4 b5 ==> -1 0 1 \sqrt{2} \sqrt{3} 2 \sqrt{n}
%D (( a0 a5 midpoint .TeX= \oooo(7,23) y+= -2 place
%D b-1 b5 midpoint .TeX= \oooo(7,25) y+= -2 place
%D b-1 place
%D a0 b0 ->
%D a1 b1 ->
%D a2 b2 ->
%D a3 b3 ->
%D a4 b4 ->
%D a5 b5 ->
%D \N \R -> .plabel= a \sqrt{\phantom{a}}
%D a-1 relplace -7 -7 \phantom{foo}
%D b5 relplace 7 7 \phantom{bar}
%D ))
%D enddiagram
%D
$$\pu
\diag{second-blob-function}
$$
Then the internal view gradually disappeared from our mathematical
practice, and we started to write functions like this,
%
$$\begin{array}{c}
\begin{array}{rrcl}
\sqrt{\phantom{a}}: & \N & → & \R \\
& n & ↦ & \sqrt{n} \\
\end{array}
\;\;,\qquad
\begin{array}{rrcl}
f: & A & → & B \\
& a & ↦ & f(a) \\
\end{array}
\;\;,
\\ \\
\begin{array}{rrcl}
·: & C×D & → & E \\
& (c,d) & ↦ & c·d \\
\end{array}
\qquad
\qquad
\end{array}
$$
%
which makes a clear distinction between the tailless arrow, `$→$', and
the arrow with tail, `$↦$': $f:A→B$ is a function that takes elements
(plural!) from $A$ to elements of $B$, and $n↦\sqrt(n)$ is an element
(in the singular) being taken to another. Rewriting our diagram for
the internal and the external views of ``$\sqrt{\ph{a}}$'' without
blobs, it becomes:
%
%D diagram first-unblob-function
%D 2Dx 100 +30
%D 2D 100 a4 |--> b4
%D 2D +12 a5 |--> b5
%D 2D +25 \N ---> \R
%D 2D
%D ren a4 a5 ==> 4 n
%D ren b4 b5 ==> 2 \sqrt{n}
%D (( a4 b4 |-> .plabel= a \sqrt{\ph{a}}
%D a5 b5 |-> .plabel= a \sqrt{\ph{a}}
%D \N \R -> .plabel= a \sqrt{\ph{a}}
%D ))
%D enddiagram
%D
%D diagram second-unblob-function
%D 2Dx 100 +30
%D 2D 100 a4 |--> b4
%D 2D +12 a5 |--> b5
%D 2D +25 \N ---> \R
%D 2D
%D ren a4 a5 ==> 4 n
%D ren b4 b5 ==> 2 \sqrt{n}
%D (( a4 relplace 0 -6 \ph{a}
%D a5 b5 |-> .plabel= a {} # \sqrt{\ph{a}}
%D \N \R -> .plabel= a \sqrt{\ph{a}}
%D ))
%D enddiagram
%D
$$\pu
\diag{first-unblob-function}
\;\;,
\quad
\text{or simply:}
\qquad
\diag{second-unblob-function}
$$
We will often use the convention that $f:A→B$ is a function from $A$
to $B$, but $A→B$ is the set of all functions from $A$ to $B$ ---
i.e., $(A→B)=B^A$ and $f:A→B$ means $f∈(A→B)$ --- on `$↦$'s this
doesn't hold, and the names on `$↦$'s can be omitted.
The internal view of a functor $F:\catA→\catC$ is more complex. The
category $\catA$ has not only ``points'' (the objects of $\catA$) but
also ``arrows'' (the morphisms of $\catA$). The functor $F$ takes a
morphism $g:A→B$ in $\catA$ to a morphism $Fg:FA→FB$ in $\catC$; and
sometimes we will denote the action of $F$ on objects by $F_0$ and its
action on morphisms by $F_1$, so a diagram with the internal and the
external views of $F$ may be drawn, for example, as:
%
%D diagram internal-view-1
%D 2Dx 100 +30
%D 2D 100 A |--> F_0A
%D 2D | |
%D 2D | |-> |
%D 2D v v
%D 2D +30 B |--> F_0B
%D 2D
%D 2D +15 \catA \catC
%D
%D (( A F_0A |-> .plabel= a F_0
%D B F_0B |-> .plabel= a F_0
%D A B -> .plabel= l g
%D F_0A F_0B -> .plabel= r F_1g
%D \catA \catC -> .plabel= a F
%D A F_0B harrownodes nil 20 nil |-> .plabel= a F_1
%D ))
%D enddiagram
%D
%D diagram internal-view-2
%D 2Dx 100 +30
%D 2D 100 A |--> FA
%D 2D | |
%D 2D | |-> |
%D 2D v v
%D 2D +30 B |--> FB
%D 2D
%D 2D +15 \catA \catC
%D
%D (( A FA |->
%D B FB |->
%D A B -> .plabel= l g
%D FA FB -> .plabel= r Fg
%D \catA \catC -> .plabel= a F
%D A FB harrownodes nil 20 nil |->
%D ))
%D enddiagram
%D
$$\pu
\diag{internal-view-1}
\qquad
\text{or as:}
\qquad
\diag{internal-view-2}
$$
The ``action'' of a natural transformation $T:F→G$, where
$F,G:\catA→\catB$ are functors, consists of a single operation --- not
two as in functors --- that expects an object $A∈\catA$ and returns a
morphism $TA:FA→GA$ in $\catB$. We can represent that action as
$A↦(TA:FA→GA)$ or $A↦(FA \ton{TA} GA)$, or as a diagram:
%
%D diagram NT1
%D 2Dx 100 +20 +20 +20
%D 2D 100 \catA A
%D 2D
%D 2D +30 \catB FA GA
%D 2D
%D 2D +15 F G
%D
%D (( \catA \catB -> sl_ .plabel= l F
%D \catA \catB -> sl^ .plabel= r G
%D A FA |-> .plabel= a F
%D A GA |-> .plabel= a G
%D FA GA -> .plabel= m TA
%D A FA GA midpoint -> .plabel= m T
%D F G -> .plabel= a T
%D ))
%D enddiagram
%D
$$\pu
\diag{NT1}
$$
The ``naturality condition'' of a natural transformation $T:F→G$ is
the assurance that for every arrow $α:A→A'$ in $\catA$ this square
commutes:
%
%D diagram NT2
%D 2Dx 100 +15 +30
%D 2D 100 A0 B0 B1
%D 2D
%D 2D +30 A1 B2 B3
%D 2D
%D 2D +15 C0 C1
%D 2D
%D ren A0 A1 ==> A A'
%D ren B0 B1 B2 B3 ==> FA GA FA' GA'
%D ren C0 C1 ==> F G
%D
%D (( A0 A1 -> .plabel= l α
%D B0 B1 -> .plabel= a TA
%D B0 B2 -> .plabel= l Fα
%D B1 B3 -> .plabel= r Gα
%D B2 B3 -> .plabel= a TA'
%D C0 C1 -> .plabel= a T
%D ))
%D enddiagram
%D
$$\pu
\diag{NT2}
$$
Diagrams like the one above will be our favorite ways to draw internal
views of natural transformations. Note that the arrows for the
functors $F$ and $G$ are left implicit.
We will sometimes use diagrams like this to show the internal view of
a commutative diagram, especially when it is in $\Set$:
%
%D diagram commutative-0
%D 2Dx 100 +30 +30 +30
%D 2D 100 A0 A1 B0 B1
%D 2D
%D 2D +24 B2
%D 2D +6 A2 A3 B3 B4
%D 2D
%D ren A0 A1 A2 A3 ==> A B C D
%D ren B0 B1 B2 B3 B4 ==> a f(a) h(f(a)) g(a) k(g(a))
%D
%D (( A0 A1 -> .plabel= a f
%D A0 A2 -> .plabel= l g
%D A1 A3 -> .plabel= r h
%D A2 A3 -> .plabel= a k
%D
%D B0 B1 -> .plabel= a f
%D B0 B3 -> .plabel= l g
%D B1 B2 -> .plabel= r h
%D B3 B4 -> .plabel= a k
%D ))
%D enddiagram
%D
$$\pu
\diag{commutative-0}
$$
%
the internal view shows that $h(f(a))=k(g(a))$ for every $a∈A$.
\msk
Our favorite way to choose names for the components of an adjunction
and to draw its internal view is this:
%
%D diagram adj
%D 2Dx 100 +25
%D 2D 100 LA A
%D 2D
%D 2D +25 B RB
%D 2D
%D 2D +15 \catB \catA
%D 2D
%D (( LA A <-|
%D LA B -> .plabel= l \sm{g^♭\\f\\}
%D A RB -> .plabel= r \sm{g\\f^♯}
%D B RB |->
%D LA RB harrownodes nil 20 nil <-| sl^ .plabel= a ♭_{AB}
%D LA RB harrownodes nil 20 nil |-> sl_ .plabel= b ♯_{AB}
%D \catB \catA <- sl^ .plabel= a L
%D \catB \catA -> sl_ .plabel= b R
%D ))
%D enddiagram
%D
$$\pu
\diag{adj}
$$
%
The adjunction $L⊣R$ ``is'' a bijection $\Hom_\catB(LA,B)
\two/<-`->/^{♭_{AB}}_{♯_{AB}} \Hom_\catA(A,RB)$ for each $A$ in
$\catA$ and each $B$ in $\catB$. Note that the functor $L$ appears at
the left of the `$⊣$' and of the `$,$', and it goes left; the functor
$R$ appears at the right of the `$⊣$' and of the `$,$', and it goes
right; the direction `$♭$' of the bijection goes left in the diagram,
and it pulls the functor in $g:A→RB$ to the left of the `$→$'; the
direction `$♯$' of the bijection goes right in the diagram and pushes
the functor in $f:LA→B$ to the right of the `$→$'.
\msk
When $\catC$ is a finite category that can be drawn explicitly, like
this,
%
%D diagram CV1
%D 2Dx 100 +20
%D 2D 100 B
%D 2D
%D 2D +20 A C
%D 2D
%D
%D (( A C -> .plabel= a f
%D B C -> .plabel= r g
%D ))
%D enddiagram
%D
$$\pu
\diag{CV1}
$$
%
we can represent functors from $\catC$ to other categories very
compactly using a positional notation similar to the ones in sec.1 of
\cite{OchsPH1}. For example, this diagram
%
%D diagram CV2
%D 2Dx 100 +35
%D 2D 100 B
%D 2D
%D 2D +25 A C
%D 2D
%D ren A B C ==> \{1,2\} \{3,4\} \{5,6\}
%D
%D (( A C -> .plabel= a \sm{1↦5\\2↦6}
%D B C -> .plabel= r \sm{3↦5\\5↦6}
%D ))
%D enddiagram
%D
$$\pu
\diag{CV2}
$$
%
can be intepreted as a functor $F:\catC→\Set$ with $F(A)=\{1,2\}$,
$F(f)=\{(1,5),(2,6)\}$ and so on --- we {\sl define} $F$ by the
internal view of its image.
% \url{http://angg.twu.net/math-b.html#idarct}
% \url{http://angg.twu.net/LATEX/idarct-preprint.pdf}
% ____ _ __ _
% / ___|| |__ __ _ _ __ ___ / / _ __ ___ | |_
% \___ \| '_ \ / _` | '_ \ / _ \ / / | '_ \ / _ \| __|
% ___) | | | | (_| | |_) | __/ / / | | | | (_) | |_
% |____/|_| |_|\__,_| .__/ \___| /_/ |_| |_|\___/ \__|
% |_|
%
% «shape-and-notation» (to ".shape-and-notation")
\section{Changing shape, changing notation}
\label{shape-and-notation}
The translation between two languages for diagrams can be done in two
steps --- changing shape and changing notation --- that are
independent and can be applied in any order. In the example below we
start with a diagram from \cite{ReyesZolf} (see
sec.\ref{yoneda-in-RRZ}) at the top left; moving right changes its
shape to show the internal view of its natural transformation, and
moving down changes its notation to the one in sec.\ref{naturality}:
%
%D diagram YR2-mini-1
%D 2Dx 100 +30 +25
%D 2D 100 A1 A2 A3
%D 2D +24
%D 2D +6 A0
%D 2D
%D 2D +15 B0 B1 B2
%D 2D
%D ren A0 A1 A2 A3 ==> F' F h_F X
%D ren B0 B1 B2 ==> \bbC \Set^{\bbC^\op} \Set^{\bbC^\op}
%D
%D (( A0 A1 -> .plabel= l f
%D A1 A2 --> .plabel= a 1_F
%D A2 A3 -> .plabel= a Φ
%D A0 A2 --> .plabel= b f
%D ))
%D enddiagram
%D
%D diagram YR2-mini-1-my
%D 2Dx 100 +30 +30
%D 2D 100 A1 A2 A3
%D 2D +24
%D 2D +6 A0
%D 2D
%D 2D +15 B0 B1 B2
%D 2D
%D ren A0 A1 A2 A3 ==> C' C (-,C) R
%D ren B0 B1 B2 ==> \bbC \Set^{\bbC^\op} \Set^{\bbC^\op}
%D
%D (( A0 A1 -> .plabel= l h
%D A1 A2 --> .plabel= a \id_C
%D A2 A3 -> .plabel= a T
%D A0 A2 --> .plabel= b h
%D ))
%D enddiagram
%D
%D diagram YR2-mini-2
%D 2Dx 100 +20 +30 +30 +30
%D 2D 100 C0 D0 D1 E0 E1
%D 2D +24 E2
%D 2D +6 C1 D2 D3 E3 E4
%D 2D
%D 2D +15 D4 D5
%D 2D
%D ren C0 C1 ==> F F'
%D ren D0 D1 D2 D3 D4 D5 ==> h_FF X(F) h_FF' X(F') h_F X
%D ren E0 E1 E2 E3 E4 ==> 1_F Φ_F(1_F) Φ_F(1_F).f f Φ_{F'}(f)
%D ren E0 E1 E2 E3 E4 ==> 1_F Φ(1_F) Φ(1_F).f f Φ(f)
%D
%D (( C0 C1 <- .plabel= l f
%D D0 D1 -> .plabel= a Φ_F
%D D0 D2 -> .plabel= l h_Ff
%D D1 D3 -> .plabel= r X(f)
%D D2 D3 -> .plabel= a Φ_{F'}
%D D4 D5 -> .plabel= a Φ
%D
%D E0 E1 |-> E1 E2 |-> E0 E3 |-> E3 E4 |->
%D ))
%D enddiagram
%D
%D diagram YR2-mini-2-my
%D 2Dx 100 +25 +30 +30 +30
%D 2D 100 C0 D0 D1 E0 E1
%D 2D +24 E2
%D 2D +6 C1 D2 D3 E3 E4
%D 2D
%D 2D +15 D4 D5
%D 2D
%D ren C0 C1 ==> C C'
%D ren D0 D1 D2 D3 D4 D5 ==> (C,C) RC (C',C) RC' (-,C) R
%D ren E0 E1 E2 E3 E4 ==> \id_C TC\id_C TC\id_C;Rh h TC'h
%D
%D (( C0 C1 <- .plabel= l f
%D D0 D1 -> .plabel= a TC
%D D0 D2 -> .plabel= l (h,C)
%D D1 D3 -> .plabel= r Rh
%D D2 D3 -> .plabel= a TC'
%D D4 D5 -> .plabel= a T
%D
%D E0 E1 |-> E1 E2 |-> E0 E3 |-> E3 E4 |->
%D ))
%D enddiagram
%D
%D diagram shape-and-notation
%D 2Dx 100 +130
%D 2D 100 A B
%D 2D
%D 2D +85 C D
%D 2D
%D
%D (( A .tex= \fcdiag{YR2-mini-1} BOX
%D B .tex= \fcdiag{YR2-mini-2} BOX
%D C .tex= \fcdiag{YR2-mini-1-my} BOX
%D D .tex= \fcdiag{YR2-mini-2-my} BOX
%D A B -> A C -> B D -> C D ->
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{shape-and-notation}
$$
% __ _____
% \ \ / / _ \
% \ V / | | |
% | || |_| |
% |_| \___/
%
% «Y0» (to ".Y0")
\section{Interpreting diagrams Y0, Y1, and Y2}
\label{Y0}
My favorite diagram for remembering the {\sl proof} of (one of the
forms of) the Yoneda Lemma is this one (``diagram Y0''):
%
%D diagram Y0
%D 2Dx 100 +40 +30 +40
%D 2D 100 A1 C1
%D 2D
%D 2D +25 A2 A3 C2 C3
%D 2D
%D 2D +30 B0 B1 D0 D1
%D 2D
%D 2D +30 D3
%D 2D
%D ren A1 A2 A3 ==> A C RC
%D ren C1 C2 C3 ==> 1 C (B,C)
%D ren B0 B1 ==> (C,-) (A,R-)
%D ren D0 D1 D3 ==> (C,-) (1,(B,-)) (B,-)
%D
%D (( A1 A3 -> # .plabel= r g
%D A2 A3 |->
%D B0 B1 -> # .plabel= b T
%D A2 B1 varrownodes nil 20 nil <->
%D
%D C1 C3 -> # .plabel= r f'
%D C2 C3 |->
%D D0 D1 -> # .plabel= b T'
%D D1 D3 <->
%D D0 D3 -> # .plabel= b f^*
%D C2 D1 varrownodes nil 20 nil <->
%D
%D A3 D0 harrownodes nil 25 nil |->
%D ))
%D enddiagram
%D
\pu
$$\diag{Y0}
$$
It is made of 11 objects in different categories, 6 morphisms, two
functors, two bijections, and a middle arrow that performs some
substitutions on the first bijection to obtain the second one. Let's
name (or ``number'') all of them:
%
%D diagram Y0o
%D 2Dx 100 +40 +30 +40
%D 2D 100 A1 C1
%D 2D
%D 2D +25 A2 A3 C2 C3
%D 2D
%D 2D +30 B0 B1 D0 D1
%D 2D
%D 2D +30 D3
%D 2D
%D ren A1 A2 A3 ==> O_1 O_2 O_3
%D ren C1 C2 C3 ==> O_4 O_5 O_6
%D ren B0 B1 ==> O_7 O_8
%D ren D0 D1 D3 ==> O_9 O_{10} O_{11}
%D
%D (( A1 A3 -> .plabel= r m_1
%D A2 A3 |-> .plabel= a F_1
%D B0 B1 -> .plabel= b m_2
%D A2 B1 varrownodes nil 20 nil <-> .plabel= l B_1
%D
%D C1 C3 -> .plabel= r m_3
%D C2 C3 |-> .plabel= a F_2
%D D0 D1 -> .plabel= b m_4
%D D1 D3 <-> .plabel= r m_5
%D D0 D3 -> .plabel= b m_6
%D C2 D1 varrownodes nil 20 nil <-> .plabel= r B_2
%D
%D A3 D0 harrownodes nil 25 nil |-> .plabel= a S
%D ))
%D enddiagram
%D
\pu
$$\diag{Y0o}
$$
The existence of a morphism $O_1 \ton{m_1} O_3$ tells us that $O_1$
and $O_3$ belong to the same category; as $O_1=A$ let's call that
category $\catA$. Similarly, $O_2 = O_5 = C$, so $O_2$ and $O_5$
belong to a category that we will call $\catC$. $O_4$ and $O_6$ belong
to the same category, and $O_4 = 1$, which is an object of $\Set$, so
$O_4$ and $O_6$ are objects of $\Set$. Similarly, $O_7 = O_9 = (C,-)$,
so $O_7$, $O_8$, $O_9$, $O_{10}$, $O_{11}$ all belong to the same
category. The functor $F_1 = R$ goes from $\catC$ to $\catA$ and the
functor $F_2$, that will turn out to be $(B,-)$, goes from $\catC$ to
$\Set$.
$(B,C)$ is a shorthand for $\Hom_\catC(B,C)$; the two objects $B$ and
$C$ have to belong to the same category so $B$ is an object of
$\catC$. $(C,-)$ is a shorthand for the functor $\Hom_\catC(C,-)$,
which goes from $\catC$ to $\Set$ (obs: $\catC$ has to be locally
small). $(C,-)$ is an object of the category of functors from $\catC$
to $\Set$, and $O_7$ to $O_{11}$, so:
%
$$\begin{array}{rrrrrrrrr}
C:\catC && A:\catA && 1:\Set && (C,-):\catC→\Set \\
B:\catC && RC:\catA && (B,C):\Set && (B,-):\catC→\Set \\
&& R:\catC→\catA && && (A,R-):\catC→\Set \\
&& && && (1,(B,-)):\catC→\Set \\
\end{array}
$$
$(A,R-)$ is a shorthand for $\Hom_\catA(A,R-): \catC→\Set$, $(B,-)$
for $\Hom_\catC(B,-): \catC→\Set$, and $(1,(B,-))$ for
$\Hom_\Set(1,\Hom(\catC(B,-)))$. $O_7$ to $O_{11}$ are all functors
from $\catC$ to $\Set$ and so objects of the category $\Set^\catC$,
and the morphisms $m_3$, $m_4$, $m_5$, $m_6$, are natural
transformations; $m_5$ is a natural isomorphism.
If we indicate in the diagram that $O_7$ to $O_{11}$ are functors and
$m_3$ to $m_6$ are NTs, we get:
%
%D diagram Y0oF
%D 2Dx 100 +40 +30 +40
%D 2D 100 A1 C1
%D 2D
%D 2D +25 A2 A3 C2 C3
%D 2D
%D 2D +30 B0 B1 D0 D1
%D 2D
%D 2D +30 D3
%D 2D
%D ren A1 A2 A3 ==> O_1 O_2 O_3
%D ren C1 C2 C3 ==> O_4 O_5 O_6
%D ren B0 B1 ==> F_4 F_4
%D ren D0 D1 D3 ==> F_5 F_6 F_7
%D
%D (( A1 A3 -> .plabel= r m_1
%D A2 A3 |-> .plabel= a F_1
%D B0 B1 -> .plabel= b T_1
%D A2 B1 varrownodes nil 20 nil <-> .plabel= l B_1
%D
%D C1 C3 -> .plabel= r m_3
%D C2 C3 |-> .plabel= a F_2
%D D0 D1 -> .plabel= b T_2
%D D1 D3 <-> .plabel= r T_3
%D D0 D3 -> .plabel= b T_4
%D C2 D1 varrownodes nil 20 nil <-> .plabel= r B_2
%D
%D A3 D0 harrownodes nil 25 nil |-> .plabel= a S
%D ))
%D enddiagram
%D
\pu
$$\diag{Y0oF}
$$
{\bf Warning:} the bijection $B_1$ is between $m_1$ and $T_1$, not
between $F_1$ and $T_1$, even though we draw it vertically; similarly,
the bijection $B_2$ is between $m_2$ and $T_2$. The reason for drawing
the diagram in this way instead of making $O_1$ and $O_2$ switch
places with one another and doing the same with $O_4$ and $O_5$ will
be explained later.
The arrow $S$ is a substitution that produces $B_2$ from $B_1$. It's
better to write it in a notation for simultaneous substitutions, not
in $λ$-calculus notation:
%
$$S = \bmat{R := (B,-) \\ \catA := \Set \\ A := 1 \\}$$
Now that we have typed most objects in diagram Y0 let's go back to the
original notation, and give names to some arrows. This is diagram Y1:
%
%D diagram Y1
%D 2Dx 100 +40 +30 +40
%D 2D 100 A1 C1
%D 2D
%D 2D +25 A2 A3 C2 C3
%D 2D
%D 2D +30 B0 B1 D0 D1
%D 2D
%D 2D +30 D3
%D 2D
%D ren A1 A2 A3 ==> A C RC
%D ren C1 C2 C3 ==> 1 C (B,C)
%D ren B0 B1 ==> (C,-) (A,R-)
%D ren D0 D1 D3 ==> (C,-) (1,(B,-)) (B,-)
%D
%D (( A1 A3 -> .plabel= r g
%D A2 A3 |-> .plabel= a R
%D B0 B1 -> .plabel= b T
%D A2 B1 varrownodes nil 20 nil -> sl_ .plabel= l B_1
%D A2 B1 varrownodes nil 20 nil <- sl^ .plabel= r B_1^{-1}
%D
%D C1 C3 -> .plabel= r f'
%D C2 C3 |-> .plabel= a (B,-)
%D D0 D1 -> .plabel= b T'
%D D1 D3 -> sl^ .plabel= r I
%D D1 D3 <- sl_ .plabel= l I^{-1}
%D D0 D3 -> .plabel= b f^*
%D C2 D1 varrownodes nil 20 nil -> sl_ .plabel= l B_2
%D C2 D1 varrownodes nil 20 nil <- sl^ .plabel= r B_2^{-1}
%D
%D A3 D0 harrownodes nil 25 nil |-> .plabel= a S
%D ))
%D enddiagram
%D
\pu
$$\diag{Y1}
$$
%
The next step is to define precisely how the four functors work. We
can do that by drawing internal views:
%
%D diagram functors
%D 2Dx 100 +30 +40 +30 +40 +30
%D 2D 100 A0 A1 B0 B1
%D 2D
%D 2D +20 A2 A3 B2 B3
%D 2D
%D 2D +20 A4 A5 B4 B5
%D 2D
%D 2D
%D 2D +30 C0 C1 D0 D1
%D 2D
%D 2D +20 C2 C3 D2 D3
%D 2D
%D 2D +20 C4 C5 D4 D5
%D 2D
%D ren A0 A1 ==> C' (C,C')
%D ren A2 A3 ==> C'' (C,C'')
%D ren A4 A5 ==> \catC \Set
%D
%D ren B0 B1 ==> C' (A,RC'))
%D ren B2 B3 ==> C'' (A,RC''))
%D ren B4 B5 ==> \catC \Set
%D
%D ren C0 C1 ==> C (B,C)
%D ren C2 C3 ==> C' (B,C')
%D ren C4 C5 ==> \catC \Set
%D
%D ren D0 D1 ==> C (1,(B,C))
%D ren D2 D3 ==> C' (1,(B,C'))
%D ren D4 D5 ==> \catC \Set
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l k
%D A1 A3 -> .plabel= r λh.(h;k)
%D A2 A3 |->
%D A4 A5 -> .plabel= a (C,-)
%D
%D B0 B1 |->
%D B0 B2 -> .plabel= l k
%D B1 B3 -> .plabel= r λg'.(g';Rk)
%D B2 B3 |->
%D B4 B5 -> .plabel= a (A,R-)
%D
%D C0 C1 |->
%D C0 C2 -> .plabel= l g
%D C1 C3 -> .plabel= r λf.(f;g)
%D C2 C3 |->
%D C4 C5 -> .plabel= a (B,-)
%D
%D D0 D1 |->
%D D0 D2 -> .plabel= l g
%D D1 D3 -> .plabel= r λf'.λe.(f'(e);g)
%D D2 D3 |->
%D D4 D5 -> .plabel= a (1,(B,-))
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{functors}
$$
The actions of the functors $(C,-)$, $(B,-)$, and $(A,R-)$ can be
inferred by term inference or by looking at the diagrams below:
%
%D diagram Y1
%D 2Dx 100 +30 +30 +25
%D 2D 100 A1 C1 B1
%D 2D
%D 2D +20 A3 C3 B2 B3
%D 2D
%D 2D +20 A5 C5 B4 B5
%D 2D
%D ren A1 A3 A5 ==> C C' C''
%D ren B2 B4 B1 B3 B5 ==> C C' A RC' RC''
%D ren C1 C3 C5 ==> B C C'
%D
%D (( A1 A3 -> .plabel= l h
%D A3 A5 -> .plabel= l k
%D A1 A5 -> .plabel= r h;k .slide= 10pt
%D
%D B2 B4 -> .plabel= l k
%D B2 B3 |-> B4 B5 |->
%D B1 B3 -> .plabel= l g'
%D B3 B5 -> .plabel= l Rk
%D B1 B5 -> .plabel= r g';Rk .slide= 10pt
%D
%D C1 C3 -> .plabel= l h
%D C3 C5 -> .plabel= l k
%D C1 C5 -> .plabel= r h;k .slide= 10pt
%D
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{Y1}
$$
%
and the action of $(1,(B,-))$ is a variant of $(B,-)$. We get:
%
$$\begin{array}{rcl}
(C,-)_0 &=& λC'.\Hom_\catC(C,C') \\
(C,-)_1 &=& λk.λh.(h;k) \\
(B,-)_0 &=& λC.\Hom_\catC(B,C) \\
(B,-)_1 &=& λg.λf.(f;g) \\
(A,R-)_0 &=& λC'.\Hom_\catA(A,RC') \\
(A,R-)_1 &=& λk.λg'.(g';Rk) \\
(1,(B,-))_0 &=& λC'.\Hom_\Set(1,\Hom_\catC(B,C')) \\
(1,(B,-))_1 &=& λk.λg'.(g';Rk) \\
\end{array}
$$
We can do the same for the natural transformations.
%
%D diagram NTs
%D 2Dx 100 +50 +35 +55 +40 +50
%D 2D 100 A0 A1 B0 B1 C0 C1
%D 2D
%D 2D +10 A2 A3 B2 B3 C2 C3
%D 2D
%D 2D +20 D0 D1 E0 E1
%D 2D
%D 2D +10 D2 D3 E2 E3
%D 2D
%D ren A0 A1 ==> (C,C') (A,RC')
%D ren A2 A3 ==> (C,-) (A,R-)
%D ren B0 B1 ==> (C,C') (1,(B,C'))
%D ren B2 B3 ==> (C,-) (1,(B,-))
%D ren C0 C1 ==> (1,(B,C')) (B,C')
%D ren C2 C3 ==> (1,(B,-)) (B,-)
%D ren D0 D1 ==> (C,C') (B,C')
%D ren D2 D3 ==> (C,-) (B,-)
%D ren E0 E1 ==> (B,C') (1,(B,C'))
%D ren E2 E3 ==> (B,-) (1,(B,-))
%D
%D (( A0 A1 -> .plabel= a λh.(g;Rh)
%D A2 A3 -> .plabel= a T
%D B0 B1 -> .plabel= a λh.λe.(f;h)
%D B2 B3 -> .plabel= a T'
%D C0 C1 -> .plabel= a λf'.f'(e)
%D C2 C3 -> .plabel= a I
%D D0 D1 -> .plabel= a λh.(f;h)
%D D2 D3 -> .plabel= a f^*
%D E0 E1 -> .plabel= a λf.λe.f
%D E2 E3 -> .plabel= a I^{-1}
%D ))
%D enddiagram
%D
$$\pu
\diag{NTs}
$$
We get:
%
$$\begin{array}{rcl}
T &=& λC'.λh.(g;Rh) \\
T' &=& λC'.λh.λe.(f;h) \\
f^* &=& λC'.λh.(f;h) \\
I &=& λC'.λf'.f'(e) \\
I^{-1} &=& λC'.λf.λe.f \\
\end{array}
$$
And we can also do the same for the bijections.
%
%D diagram bijs
%D 2Dx 100 +110
%D 2D 100 A C
%D 2D
%D 2D +30 B D
%D 2D
%D ren A B ==> g:A→RC T:(C,-)→(A,R-)
%D ren C D ==> f':1→(B,C) T':(C,-)→(1,(B,-))
%D
%D (( A B |-> sl_ .plabel= l T:=λC'.λh.(g;Rh)
%D A B <-| sl^ .plabel= r g:=TC(\id_C)
%D C D |-> sl_ .plabel= l T:=λC'.λh.(g;(B,-)(h))\;\;(?)
%D C D <-| sl^ .plabel= r f':=T'C(\id_C)
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{bijs}
$$
%
so:
%
$$\begin{array}{rcl}
B_1 &=& λg.λC'.λh.(g;Rh) \\
B_1^{-1} &=& λT.TC(\id_C) \\
B_2 &=& λf'.λC'.λh.(g;(B,-)(h))\;\;(?) \\
B_2^{-1} &=& λT'.T'C(\id_C). \\
\end{array}
$$
\bsk
Note that we used only type inference and term inference --- which is
not little, but most books and articles on CT pretend that simple type
inferences and term inferences like these are ``obvious'' --- and now
have the types and the terms for everything in diagram Y1. Let's call
the diagram below ``diagram Y2''; it is Y1 plus lots of information.
%
$$\begin{array}{c}
\diag{Y1}
\\
\\
\begin{array}{rrrrrrrrr}
C:\catC && A:\catA && 1:\Set && (C,-):\catC→\Set \\
B:\catC && RC:\catA && (B,C):\Set && (B,-):\catC→\Set \\
&& R:\catC→\catA && && (A,R-):\catC→\Set \\
&& && && (1,(B,-)):\catC→\Set \\
\end{array}
\\
\\
\begin{array}{rcl}
(C,-)_0 &=& λC'.\Hom_\catC(C,C') \\
(C,-)_1 &=& λk.λh.(h;k) \\
(B,-)_0 &=& λC.\Hom_\catC(B,C) \\
(B,-)_1 &=& λg.λf.(f;g) \\
(A,R-)_0 &=& λC'.\Hom_\catA(A,RC') \\
(A,R-)_1 &=& λk.λg'.(g';Rk) \\
(1,(B,-))_0 &=& λC'.\Hom_\Set(1,\Hom_\catC(B,C')) \\
(1,(B,-))_1 &=& λk.λg'.(g';Rk) \\
\end{array}
\\
\\
\begin{array}{rcl}
T &=& λC'.λh.(g;Rh) \\
T' &=& λC'.λh.λe.(f;h) \\
f^* &=& λC'.λh.(f;h) \\
I &=& λC'.λf'.f'(e) \\
I^{-1} &=& λC'.λf.λe.f \\
\end{array}
\\
\\
S = \bsm{R := (B,-) \\ \catA := \Set \\ A := 1 \\}
\\
\\
\begin{array}{rcl}
B_1 &=& λg.λC'.λh.(g;Rh) \\
B_1^{-1} &=& λT.TC(\id_C) \\
B_2 &=& λf'.λC'.λh.(g;(B,-)(h))\;\;(?) \\
B_2^{-1} &=& λT'.T'C(\id_C) \\
\end{array}
\\
\end{array}
$$
% _ _ _ _ _ _
% | \ | | __ _| |_ _ _ _ __ __ _| (_) |_ _ _
% | \| |/ _` | __| | | | '__/ _` | | | __| | | |
% | |\ | (_| | |_| |_| | | | (_| | | | |_| |_| |
% |_| \_|\__,_|\__|\__,_|_| \__,_|_|_|\__|\__, |
% |___/
% «naturality» (to ".naturality")
\section{$B_1$ is really a bijection}
\label{naturality}
In this diagram, that is just a part of diagram Y1 with the bijection
$B_1$ made more explicit,
%
%D diagram Y0nat
%D 2Dx 100 +40
%D 2D 100 A1
%D 2D
%D 2D +25 A2 A3
%D 2D
%D 2D +35 B0 B1
%D 2D
%D 2D +30
%D 2D
%D ren A1 A2 A3 ==> A C RC
%D ren B0 B1 ==> (C,-) (A,R-)
%D
%D (( A1 A3 -> .plabel= r g
%D A2 A3 |->
%D B0 B1 -> .plabel= b T
%D A2 B1 varrownodes nil 25 nil |-> sl_ .plabel= l \sm{T:=\\B_1(g):=\\λC'.λh.(g;Rh)}
%D A2 B1 varrownodes nil 25 nil <-| sl^ .plabel= r \sm{g:=\\B_1^{-1}(T):=\\TC(\id_C)}
%D
%D ))
%D enddiagram
%D
\pu
$$\diag{Y0nat}
$$
%
it is easy to see that $B_1^{-1}(B_1(g)) = g$:
%
$$\begin{array}{rcl}
B_1^{-1}(B_1(g)) &=& B_1^{-1}(λC'.λh.(g;Rh)) \\
&=& (λC'.λh.(g;Rh))C(\id_C) \\
&=& (λh.(g;Rh))(\id_C) \\
&=& g;R(\id_C) \\
&=& g;\id_{RC} \\
&=& g \\
\end{array}
$$
Let's try to calculate $B_1(B_1^{-1}(T))$:
%
$$\begin{array}{rcl}
B_1(B_1^{-1}(T)) &=& B_1(TC(\id_C)) \\
&=& λC'.λh.(TC(\id_C);Rh) \\
\end{array}
$$
%
This is not necessarily equal to $T$... but note that if $T$ is a
natural transformation then its naturality condition means that for
every $k:C'→C''$ this square commutes,
%
%D diagram nat-1
%D 2Dx 100 +30 +40 +35 +50
%D 2D 100 A0 B0 B1 C0 C1
%D 2D +24 C2
%D 2D +6 A1 B2 B3 C3 C4
%D 2D
%D 2D +15 B4 B5
%D 2D
%D ren A0 A1 ==> C' C''
%D ren B0 B1 B2 B3 B4 B5 ==> (C,C') (A,RC') (C,C'') (A,RC'') (C,-) (A,R-)
%D ren C0 C1 C2 C3 C4 ==> h TC'h (TC'h);Rk h;k TC''(h;k)
%D
%D (( A0 A1 -> .plabel= l k
%D
%D B0 B1 -> .plabel= a TC'
%D B2 B3 -> .plabel= b TC''
%D B0 B2 -> .plabel= l (C,-)k
%D B1 B3 -> .plabel= r (A,R-)k
%D B4 B5 -> .plabel= a T
%D
%D C0 C1 |-> .plabel= a TC'
%D C1 C2 |-> .plabel= r (λk.λh.(h;k))k
%D C0 C3 |-> .plabel= r (λk.λg'.(g';Rk))k
%D C3 C4 |-> .plabel= b TC''
%D ))
%D enddiagram
%D
$$\pu
\diag{nat-1}
$$
%
i.e., $(TC'h);Rk = TC''(h;k)$; this diagram helps understanding the
types:
%
%D diagram nat-1-types
%D 2Dx 100 +30
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +20 A4 A5
%D 2D
%D 2D +20 A6 A7
%D 2D
%D ren A1 A2 A3 A4 A5 A6 A7 ==> A C RC C' RC' C'' RC''
%D
%D (( A1 A3 -> .plabel= r r
%D A2 A4 -> .plabel= l h
%D A3 A5 -> .plabel= r Rh
%D A4 A6 -> .plabel= l k
%D A5 A7 -> .plabel= r Rk
%D
%D A1 A5 -> .slide= 20pt .plabel= r TC'h
%D A1 A7 -> .slide= 45pt .plabel= r TC''(h;k)
%D
%D A2 A3 |-> A4 A5 |-> A6 A7 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{nat-1-types}
$$
If we replace $k:C'→C''$ by $h:C→C'$ and $h$ by $\id_C$ we get:
%
$$((TC'h);Rk = TC''(h;k)) \bsm{C':=C\\C'':=C'\\k:=h\\h:=\id_C} \;\;=\;\;
(TC\id_C;Rh = TC'(\id_C;h))
$$
%
which lets us continue the calculation of $B_1(B_1^{-1}(T))$:
%
$$\begin{array}{rcl}
B_1(B_1^{-1}(T)) &=& B_1(TC(\id_C)) \\
&=& λC'.λh.(TC(\id_C);Rh) \\
&=& λC'.λh.(TC'(\id_C;h)) \\
&=& λC'.λh.TC'h \\
\end{array}
$$
%
this means that for all $C'$ and $h$ we have
%
$$\begin{array}{rcl}
B_1(B_1^{-1}(T))C'h &=& (λC'.λh.TC'h)C'h \\
&=& (λh.TC'h)h \\
&=& TC'h \\
\end{array}
$$
%
so by $η$-reduction $B_1(B_1^{-1}(T))C' = TC'$ and $B_1(B_1^{-1}(T)) =
T$.
\msk
Note that the proof of $TC\id_C;Rh = TC'h$ can be represented as a
diagram:
%
%D diagram nat-2
%D 2Dx 100 +30 +40 +35 +40
%D 2D 100 A0 B0 B1 C0 C1
%D 2D +24 C2
%D 2D +6 A1 B2 B3 C3 C4
%D 2D
%D 2D +15 B4 B5
%D 2D
%D ren A0 A1 ==> C C'
%D ren B0 B1 B2 B3 B4 B5 ==> (C,C) (A,RC) (C,C') (A,RC') (C,-) (A,R-)
%D ren C0 C1 C2 C3 C4 ==> \id_C TC\id_C (TC\id_C);Rh h TC'h
%D
%D (( A0 A1 -> .plabel= l h
%D
%D B0 B1 -> .plabel= a TC
%D B0 B2 -> .plabel= l (C,-)h
%D B1 B3 -> .plabel= r (A,R-)h
%D B2 B3 -> .plabel= a TC'
%D B4 B5 -> .plabel= a T
%D
%D C0 C1 |-> # .plabel= a TC
%D C1 C2 |-> # .plabel= r (λk.λh.(h;k))k
%D C0 C3 |-> # .plabel= r (λk.λg'.(g';Rk))k
%D C3 C4 |-> # .plabel= b TC'
%D ))
%D enddiagram
%D
$$\pu
\diag{nat-2}
$$
% __ _______
% \ \ / /___ /
% \ V / |_ \
% | | ___) |
% |_| |____/
%
% «stressing-bijections» (to ".stressing-bijections")
\section{Making the bijections more explicit}
\label{stressing-bijections}
Let's introduce a new diagram that stresses the bijections --- and
names a few bijections that were unnamed before. This is diagram Y3:
%
%D diagram Y3
%D 2Dx 100 +75
%D 2D 100 B0
%D 2D
%D 2D +30 A1 B1
%D 2D
%D 2D +30 A2 B2
%D 2D
%D 2D +30 B3
%D 2D
%D ren A1 A2 ==> g:A→RC T:(C,-)→(A,R-)
%D ren B0 B1 B2 B3 ==> f:B→C f':1→(B,C) T':(C,-)→(1,(B,-)) f^*:(C,-)→(B,-)
%D
%D (( A1 A2 |-> sl_ .plabel= l B_1
%D A1 A2 <-| sl^ .plabel= r B_1^{-1}
%D
%D B0 B1 |-> sl_ .plabel= l B_4
%D B0 B1 <-| sl^ .plabel= r B_4^{-1}
%D B1 B2 |-> sl_ .plabel= l B_2
%D B1 B2 <-| sl^ .plabel= r B_2^{-1}
%D B2 B3 |-> sl_ .plabel= l B_5
%D B2 B3 <-| sl^ .plabel= r B_5^{-1}
%D
%D A1 B2 harrownodes nil 20 nil |-> .plabel= a S
%D
%D B0 B3 |-> .slide= 60pt .plabel= l B_3
%D B0 B3 <-| .slide= 65pt .plabel= r B_3^{-1}
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{Y3}
$$
The statement of the Yoneda Lemma is just this: ``$B_3$ is a
bijection''. If we build $B_4$ and $B_5$, define $B_3$ as
$B_5∘B_2∘B_4$ and simplify the $λ$-terms we obtain that $B_3$ is just
this:
%
%D diagram Y2B3
%D 2Dx 100 +75
%D 2D 100 B0
%D 2D
%D 2D +30 B3
%D 2D
%D ren B0 B3 ==> f:B→C f^*:(C,-)→(B,-)
%D
%D (( B0 B3 |-> sl_ .plabel= l f^*:=λh.(f;h)
%D B0 B3 <-| sl^ .plabel= r f:=(f^*C)(\id_C)
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{Y2B3}
$$
A direct proof that $B_3$ and $B_3^{-1}$ are inverses to one another
requires naturality like we did in section \ref{naturality} (trust
me!), and less direct proof can be structured like this: $B_1$ is a
bijection implies that $B_2$ is a bijection, that implies that $B_3$
is a bijection.
% _ _ __ ___
% / \ ___| |_ _ __ ___ _ __ __ _ ___ _ __ \ \ / / |
% / _ \ / __| __| '__/ _ \| '_ \ / _` |/ _ \ '__| \ V /| |
% / ___ \ \__ \ |_| | | (_) | | | | (_| | __/ | | | | |___
% /_/ \_\ |___/\__|_| \___/|_| |_|\__, |\___|_| |_| |_____|
% |___/
%
% «stronger-yoneda» (to ".stronger-yoneda")
\section{A stronger Yoneda Lemma}
\label{stronger-yoneda}
If we don't replace the functor $R$ by $(B,-)$ in Y0 and we make
$\catA:=\Set$ and $A:=1$ we can build this diagram here (``diagram
Y4''),
%
%D diagram Y4
%D 2Dx 100 +40
%D 2D 100 A1
%D 2D
%D 2D +25 A2 A3
%D 2D
%D 2D +30 B0 B1
%D 2D
%D 2D +30 B2
%D 2D
%D ren A1 A2 A3 ==> 1 C RC
%D ren B0 B1 B2 ==> (C,-) (1,R-) R
%D
%D (( A1 A3 -> .plabel= r p'
%D A2 A3 |-> .plabel= a R
%D B0 B1 -> .plabel= b T'
%D B1 B2 <->
%D B0 B2 -> .plabel= b T
%D A2 B1 varrownodes nil 20 nil <->
%D
%D ))
%D enddiagram
%D
\pu
$$\diag{Y4}
$$
%
that yields a bijection between points of $RC$ and natural
transformations from $(C,-)$ to $R$ (``diagram Y5''):
%
%D diagram Y5
%D 2Dx 100
%D 2D 100 A
%D 2D
%D 2D +20 B
%D 2D
%D 2D +20 C
%D 2D
%D 2D +20 D
%D 2D
%D ren A B C D ==> p∈RC p':1→RC T':(C,-)→(1,R-) T:(C,-)→R
%D
%D (( A B |-> sl_
%D A B <-| sl^
%D B C |-> sl_
%D B C <-| sl^
%D C D |-> sl_
%D C D <-| sl^
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{Y5}
$$
This bijection feels much more abstract than the one that we were
looking at before.
% ____ _ _ _
% | _ \ ___ _ __ _ __ ___ ___ ___ _ __ | |_ __ _| |__ | | ___ ___
% | |_) / _ \ '_ \| '__/ _ \/ __|/ _ \ '_ \| __/ _` | '_ \| |/ _ \/ __|
% | _ < __/ |_) | | | __/\__ \ __/ | | | || (_| | |_) | | __/\__ \
% |_| \_\___| .__/|_| \___||___/\___|_| |_|\__\__,_|_.__/|_|\___||___/
% |_|
%
% «representables» (to ".representables")
\section{Representable functors}
\label{representables}
% _ _ _ _
% | | | |_ __ (_)_ _____ _ __ ___ __ _| |___
% | | | | '_ \| \ \ / / _ \ '__/ __|/ _` | / __|
% | |_| | | | | |\ V / __/ | \__ \ (_| | \__ \
% \___/|_| |_|_| \_/ \___|_| |___/\__,_|_|___/
%
% «universals» (to ".universals")
\section{Universal elements and universal arrows}
\label{universals}
We say that an element $p∈RC$ is a {\sl universal element} when the
natural transformation $T$ associated to it by diagram Y4 is a natural
isomorphism, i.e., when for every $C'$ the map $TC' = λh.Rhp$ is an
iso:
%
%D diagram Y6
%D 2Dx 100
%D 2D 100 A
%D 2D
%D 2D +20 B
%D 2D
%D ren A B ==> p∈RC T:(C,-)→R
%D
%D (( A B |-> sl_ .plabel= l \sm{T:=λC'.λh.Rhp}
%D A B <-| sl^ .plabel= r \sm{p:=TC\id_C}
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{Y6}
$$
A {\sl universal arrow} is an arrow $g:A→RC$ such that the associated
$T$ ($= λC'.λh.(g;Rh)$) is a natural isomorphism:
%
%D diagram Y0nat-
%D 2Dx 100 +40
%D 2D 100 A1
%D 2D
%D 2D +25 A2 A3
%D 2D
%D 2D +35 B0 B1
%D 2D
%D 2D +30
%D 2D
%D ren A1 A2 A3 ==> A C RC
%D ren B0 B1 ==> (C,-) (A,R-)
%D
%D (( A1 A3 -> .plabel= r g
%D A2 A3 |->
%D B0 B1 -> .plabel= b T
%D A2 B1 varrownodes nil 25 nil |-> sl_ .plabel= l \sm{T:=\\λC'.λh.(g;Rh)}
%D A2 B1 varrownodes nil 25 nil <-| sl^ .plabel= r \sm{g:=\\TC(\id_C)}
%D
%D ))
%D enddiagram
%D
\pu
$$\diag{Y0nat-}
$$
% _ _ _ _ _
% / \ __| |(_)_ _ _ __ ___| |_(_) ___ _ __ ___
% / _ \ / _` || | | | | '_ \ / __| __| |/ _ \| '_ \/ __|
% / ___ \ (_| || | |_| | | | | (__| |_| | (_) | | | \__ \
% /_/ \_\__,_|/ |\__,_|_| |_|\___|\__|_|\___/|_| |_|___/
% |__/
%
% «adjunctions» (to ".adjunctions")
\section{Adjunctions}
\label{adjunctions}
At the end of sec.\ref{internal-view} we presented a convention for
naming the components of an adjunction and drawing its internal view,
but we didn't include units or counits.
% An adjunction $L⊣R$ is an operation, ``natural'' in a certain sense,
% that yields a bijection $(♭_{AB},♯_{AB})$ between $(LA,B)$ and
% $(A,RB)$ for any $A∈\catA$ and $B∈\catB$:
% %
% %D diagram adj-1
% %D 2Dx 100 +25
% %D 2D 100 LA A
% %D 2D
% %D 2D +25 B RB
% %D 2D
% %D 2D +15 \catB \catA
% %D 2D
% %D # ren ==>
% %D
% %D (( LA A <-| .plabel= a L
% %D B RB |-> .plabel= b R
% %D LA B -> .plabel= l f
% %D A RB -> .plabel= r g
% %D LA RB harrownodes nil 20 nil <-| sl^ .plabel= a ♭_{AB}
% %D LA RB harrownodes nil 20 nil |-> sl_ .plabel= b ♯_{AB}
% %D
% %D \catB \catA <- sl^ .plabel= a L
% %D \catB \catA -> sl_ .plabel= b R
% %D ))
% %D enddiagram
% %D
% $$\pu
% \diag{adj-1}
% $$
For any $A∈\catA$ the unit map $η_A$, defined like this,
%
%D diagram adj-2
%D 2Dx 100 +25
%D 2D 100 LA A
%D 2D
%D 2D +25 B RB
%D 2D
%D 2D +15 \catB \catA
%D 2D
%D ren B RB ==> LA RLA
%D
%D (( LA A <-| .plabel= a L
%D B RB |-> .plabel= b R
%D LA B -> .plabel= l \id_{LA}
%D A RB -> .plabel= r \sm{η_A:=\\♯(\id_{LA})}
%D LA RB harrownodes nil 20 nil <-| sl^ .plabel= a ♭_{A,LA}
%D LA RB harrownodes nil 20 nil |-> sl_ .plabel= b ♯_{A,LA}
%D
%D \catB \catA <- sl^ .plabel= a L
%D \catB \catA -> sl_ .plabel= b R
%D ))
%D enddiagram
%D
$$\pu
\diag{adj-2}
$$
%
induces a map $(f↦(η_A;Rf)):(LA,B)→(A,RB)$ that is equal to the
bijection $♯_{AB}:(LA,B)→(A,RB)$:
%
%D diagram adj-3
%D 2Dx 100 +25
%D 2D 100 LA A
%D 2D
%D 2D +25 LA' RLA
%D 2D
%D 2D +25 B RB
%D 2D
%D 2D +15 \catB \catA
%D 2D
%D ren LA' ==> LA
%D
%D (( # LA A <-| # .plabel= a L
%D # LA LA' -> .plabel= l \id_{LA}
%D A RLA -> .plabel= r η_A
%D LA' RLA |-> # .plabel= b R
%D LA' B -> .plabel= l f
%D RLA RB -> .plabel= r Rf
%D B RB |-> # .plabel= b R
%D # A RB -> .plabel= r \sm{η_A:=\\♯(\id_{LA})}
%D LA' RB harrownodes nil 20 nil |-> .plabel= a R
%D
%D A RB -> .slide= 15pt .plabel= r η_A;Rf
%D
%D \catB \catA <- sl^ .plabel= a L
%D \catB \catA -> sl_ .plabel= b R
%D ))
%D enddiagram
%D
$$\pu
\diag{adj-3}
$$
%
the map $(f↦(η_A;Rf))$ is natural in $B$, and we can see (I'm omitting
the details now) that it induces a natural transformation
$T:(LA,-)→(A,R-)$:
%
%D diagram adj-4
%D 2Dx 100 +35
%D 2D 100 A1
%D 2D
%D 2D +25 A2 A3
%D 2D
%D 2D +25 B0 B1
%D 2D
%D ren A1 A2 A3 ==> A LA RLA
%D ren B0 B1 ==> (LA,-) (A,R-)
%D
%D (( A1 A3 -> .plabel= r η_A
%D A2 A3 |-> .plabel= a R
%D B0 B1 -> .plabel= b T
%D
%D A2 B1 varrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
$$\pu
\diag{adj-4}
$$
%
We are now in a situation similar to diagram Y0 --- we can see that
any natural transformation $T:(LA,-)→(A,R-)$ yields a map $η_A:A→RLA$
(that is not necessarily the unit of the adjuction, of course).
Now make the category $\catA$ be $\Set$, and make $A:=1$ and
$C:=LA=L1$. Then $RLA=RL1=RC$, and we get these diagrams:
%
%D diagram adj-5
%D 2Dx 100 +35
%D 2D 100 A1
%D 2D
%D 2D +25 A2 A3
%D 2D
%D 2D +25 B0 B1
%D 2D
%D 2D +25 B3
%D 2D
%D ren A1 A2 A3 ==> 1 C RC
%D ren B0 B1 B3 ==> (C,-) (1,R-) R
%D
%D (( A1 A3 -> .plabel= r p'
%D A2 A3 |-> .plabel= a R
%D B0 B1 -> .plabel= b T'
%D B1 B3 <->
%D B0 B3 -> .plabel= b T
%D
%D A2 B1 varrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
%D diagram adj-bijs
%D 2Dx 100
%D 2D 100 A
%D 2D
%D 2D +25 B
%D 2D
%D 2D +25 C
%D 2D
%D 2D +25 D
%D 2D
%D ren A B C D ==> p∈RC p':1→RC T':(C,-)→(1,R-) T:(C,-)→R
%D
%D (( A B |-> sl_
%D A B <-| sl^
%D B C |-> sl_
%D B C <-| sl^
%D C D |-> sl_
%D C D <-| sl^
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{adj-5}
\qquad
\diag{adj-bijs}
$$
%
We have a bijection between $RC=RL1$ and the set of natural
transformations from $(C,-)$ to $R$, but we also have more: when
$p':1→RL1=RC$ is a unit map of the adjunction then the corresponding
$T:(C,-)→R$ is a {\sl natural isomorphism}, so this functor $R$ is
representable and represented by $C$, the map $p':1→RC$ is a universal
arrow, $p∈RC$ is a universal element. Most (or all?) items in Examples
2.1.5 in pp.51--53 of \cite{RiehlCTIC} are applications of this idea
using adjunctions of the form $F⊣U$ --- e.g., in item (ii) the functor
$F:𝐬{Set}→f{Group}$ takes each set $A$ to the free group $FA$ having
$A$ as its set of generators.
% (find-books "__cats/__cats.el" "riehl")
% (find-riehlccpage (+ 18 50) "2.1. Representable functors")
% (find-riehlccpage (+ 18 51) "Example 2.1.5")
(To do: debug the ideas above!)
% ____ _ _ _
% / ___|___ _ __ | |_ _ __ __ ___ ____ _ _ __(_) __ _ _ __ | |_
% | | / _ \| '_ \| __| '__/ _` \ \ / / _` | '__| |/ _` | '_ \| __|
% | |__| (_) | | | | |_| | | (_| |\ V / (_| | | | | (_| | | | | |_
% \____\___/|_| |_|\__|_| \__,_| \_/ \__,_|_| |_|\__,_|_| |_|\__|
%
% «contravariant» (to ".contravariant")
% (defun dd () (interactive) (yonp 15))
\section{Two contravariant Yoneda Lemmas}
\label{contravariant}
Let's introduce some notations for dealing with opposite categories.
If $B$ and $C$ are objects of $\catC$ then $B^\op$ and $C^\op$ are
objects of $\catC^\op$; a morphism $f:B→C$ in $\catC$ is written as
$f^\op:C^\op→B^\op$ when regarded as a morphism in $\catC^\op$.
Looking at hom-sets, we have that $f∈\Hom_{\catC}(B,C)$ iff
$f^\op∈\Hom_{\catC^\op}(C^\op,B^\op)$, and in the shorthand notation
this means that $(B,C)$ and $(C^\op,B^\op)$ are equal except for the
`$\op$'s in the elements of $(C^\op,B^\op)$.
Let $G:\catC^\op→\catD$ be a contravariant functor. We will write its
action on objects as $C^\op↦GG$, and the internal view of $G$ is:
%
%D diagram contra
%D 2Dx 100 +20 +25
%D 2D 100 A0 B0 B1
%D 2D
%D 2D +20 A1 B2 B3
%D 2D
%D 2D +15 C0 C1
%D 2D
%D ren A0 A1 ==> B C
%D ren B0 B1 B2 B3 ==> B^\op GB C^\op GC
%D ren C0 C1 ==> \catC^\op \catD
%D
%D (( A0 A1 <- .plabel= l f
%D B0 B1 |->
%D B2 B3 |->
%D B0 B2 -> .plabel= l f^\op
%D B1 B3 -> .plabel= r Gf
%D C0 C1 -> .plabel= a G
%D ))
%D enddiagram
%D
$$\pu
\diag{contra}
$$
If we take Diagram Y0 and replace the category $\catC$ by $\catC^\op$
we get this; note that $R:\catC^\op→\catA$:
%
%D diagram Y0contra
%D 2Dx 100 +40 +30 +40
%D 2D 100 A1 C1
%D 2D
%D 2D +25 A2 A3 C2 C3
%D 2D
%D 2D +30 B0 B1 D0 D1
%D 2D
%D 2D +30 D3
%D 2D
%D ren A1 A2 A3 ==> A C^\op RC
%D ren C1 C2 C3 ==> 1 C^\op (B^\op,C^\op)
%D ren B0 B1 ==> (C^\op,-) (A,R-)
%D ren D0 D1 D3 ==> (C^\op,-) (1,(B^\op,-)) (B^\op,-)
%D
%D (( A1 A3 -> # .plabel= r g
%D A2 A3 |-> .plabel= a R
%D B0 B1 -> # .plabel= b T
%D A2 B1 varrownodes nil 20 nil <->
%D
%D C1 C3 -> # .plabel= r f'
%D C2 C3 |-> .plabel= a (B^\op,-)
%D D0 D1 -> # .plabel= b T'
%D D1 D3 <->
%D D0 D3 -> # .plabel= b f^*
%D C2 D1 varrownodes nil 20 nil <->
%D
%D A3 D0 harrownodes nil 25 nil |->
%D ))
%D enddiagram
%D
\pu
$$\diag{Y0contra}
$$
%
We can simplify this a bit, rewriting it as:
%
%D diagram Y0contra2
%D 2Dx 100 +40 +30 +40
%D 2D 100 A1 C1
%D 2D
%D 2D +25 A2 A3 C2 C3
%D 2D
%D 2D +30 B0 B1 D0 D1
%D 2D
%D 2D +30 D3
%D 2D
%D ren A1 A2 A3 ==> A C^\op RC
%D ren C1 C2 C3 ==> 1 C^\op (C,B)
%D ren B0 B1 ==> (-,C) (A,R-)
%D ren D0 D1 D3 ==> (-,C) (1,(-,B)) (-,B)
%D
%D (( A1 A3 -> # .plabel= r g
%D A2 A3 |-> .plabel= a R
%D B0 B1 -> # .plabel= b T
%D A2 B1 varrownodes nil 20 nil <->
%D
%D C1 C3 -> # .plabel= r f'
%D C2 C3 |-> .plabel= a (-,B)
%D D0 D1 -> # .plabel= b T'
%D D1 D3 <->
%D D0 D3 -> # .plabel= b f^*
%D C2 D1 varrownodes nil 20 nil <->
%D
%D A3 D0 harrownodes nil 25 nil |->
%D ))
%D enddiagram
%D
\pu
$$\diag{Y0contra2}
$$
If we replace $\catA$ by $\Set$ and $A$ by $1$ and complete the
triangle at the lower left we get a single diagram that states the two
contravariant Yoneda Lemmas:
%
%D diagram Y0contra3
%D 2Dx 100 +40 +30 +40
%D 2D 100 A1 C1
%D 2D
%D 2D +25 A2 A3 C2 C3
%D 2D
%D 2D +30 B0 B1 D0 D1
%D 2D
%D 2D +30 B3 D3
%D 2D
%D ren A1 A2 A3 ==> 1 C^\op RC
%D ren C1 C2 C3 ==> 1 C^\op (C,B)
%D ren B0 B1 B3 ==> (-,C) (1,R-) R
%D ren D0 D1 D3 ==> (-,C) (1,(-,B)) (-,B)
%D
%D (( A1 A3 -> # .plabel= r g
%D A2 A3 |-> .plabel= a R
%D B0 B1 -> # .plabel= b T
%D B1 B3 <->
%D B0 B3 ->
%D A2 B1 varrownodes nil 20 nil <->
%D
%D C1 C3 -> # .plabel= r f'
%D C2 C3 |-> .plabel= a (-,B)
%D D0 D1 -> # .plabel= b T'
%D D1 D3 <->
%D D0 D3 -> # .plabel= b f^*
%D C2 D1 varrownodes nil 20 nil <->
%D
%D A3 D0 harrownodes nil 25 nil |->
%D ))
%D enddiagram
%D
\pu
$$\diag{Y0contra3}
$$
The diagrams that help us understand how the functors and natural
transformations above work are:
%
%D diagram Y0contrahelp
%D 2Dx 100 +20 +30 +40 +20 +30
%D 2D 100 B1 E1
%D 2D
%D 2D +20 A0 B2 B3 D0 E2 E3
%D 2D
%D 2D +20 A1 B4 B5 D1 E4 E5
%D 2D
%D 2D +20 A2 B6 B7 D2 E6 E7
%D 2D
%D 2D +15 C6 C7 F6 F7
%D 2D
%D 2D +20 C8 F8
%D 2D
%D ren A0 A1 A2 ==> C C' C''
%D ren B1 B2 B3 B4 B5 B6 B7 ==> 1 C^\op RC {C'}^\op RC' {C''}^\op RC''
%D ren C6 C7 C8 ==> (-,C) (1,R-) R
%D ren D0 D1 D2 ==> C C' C''
%D ren E1 E2 E3 E4 E5 E6 E7 ==> 1 C^\op (C,B) {C'}^\op (C',B) {C''}^\op (C'',B)
%D ren F6 F7 F8 ==> (-,C) (1,(-,B)) (-,B)
%D
%D (( A0 A1 <- A1 A2 <-
%D B1 B3 -> B2 B3 |-> B2 B4 -> B3 B5 |-> B4 B5 |-> B4 B6 -> B5 B7 -> B6 B7 |->
%D C6 C7 -> C7 C8 <-> C6 C8 ->
%D D0 D1 <- D1 D2 <-
%D E1 E3 -> E2 E3 |-> E2 E4 -> E3 E5 |-> E4 E5 |-> E4 E6 -> E5 E7 -> E6 E7 |->
%D F6 F7 -> F7 F8 <-> F6 F8 ->
%D ))
%D enddiagram
%D
$$\pu
\diag{Y0contrahelp}
$$
The statements of these contravariant Yoneda Lemmas are:
%
%D diagram Y0contrastat
%D 2Dx 100 +70
%D 2D 100 A C
%D 2D
%D 2D +25 B D
%D 2D
%D ren A B ==> p:RC T:(-,C)→R
%D ren C D ==> f:C→B f_*:(-,C)→(-,B)
%D
%D (( A B |-> sl_ .plabel= l \sm{T:=\\λC'.λh.(Rh)(p)}
%D A B <-| sl^ .plabel= r \sm{p:=\\TC\id_C}
%D C D |-> sl_ .plabel= l \sm{f_*:=\\λC'.λh.(h;f)}
%D C D <-| sl^ .plabel= r \sm{f:=\\f_*C\id_C}
%D ))
%D enddiagram
%D
$$\pu
\diag{Y0contrastat}
$$
Note that the action of the (contravariant) functor $(-,C)$ on objects
can be written $B^\op↦(B,C)$; sometimes by abuse of language we will
denote the whole functor $(-,C)$ by $B^\op↦(B,C)$, and, similarly,
denote the covariant functor $(B,-)$ used in sec.\ref{Y0} by
$C↦(B,C)$.
% _____ _ _ _ _
% | ____|_ __ ___ | |__ ___ __| | __| (_)_ __ __ _ ___
% | _| | '_ ` _ \| '_ \ / _ \/ _` |/ _` | | '_ \ / _` / __|
% | |___| | | | | | |_) | __/ (_| | (_| | | | | | (_| \__ \
% |_____|_| |_| |_|_.__/ \___|\__,_|\__,_|_|_| |_|\__, |___/
% |___/
% «embeddings» (to ".embeddings")
% (defun dd () (interactive) (yonp 16))
\section{The Yoneda Embeddings}
\label{embeddings}
Our two ``less abstract Yoneda lemmas'' can be drawn like this:
%
%D diagram emb-1
%D 2Dx 100 +25 +40 +25
%D 2D 100 A0 A1 B0 B1
%D 2D
%D 2D +25 A2 A3 B2 B3
%D 2D
%D ren A0 A1 A2 A3 ==> B (B,-) C (C,-)
%D ren B0 B1 B2 B3 ==> B (-,B) C (-,C)
%D
%D (( A0 A2 -> .plabel= l f
%D A1 A3 <- .plabel= r f^*
%D A0 A3 harrownodes nil 20 nil <->
%D
%D B0 B2 -> .plabel= l f
%D B1 B3 -> .plabel= r f_*
%D B0 B3 harrownodes nil 20 nil <->
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{emb-1}
$$
They are usually presented at a slightly higher level, as:
%
%D diagram emb-2
%D 2Dx 100 +15 +30 +40 +30
%D 2D 100 a0 A0 A1 B0 B1
%D 2D
%D 2D +25 a1 A2 A3 B2 B3
%D 2D
%D 2D +15 a2 A4 A5 B4 B5
%D 2D
%D ren a0 a1 a2 ==> B C \catC
%D ren A0 A1 A2 A3 A4 A5 ==> B^\op (B,-) C^\op (C,-) \catC^\op \Set^{\catC}
%D ren B0 B1 B2 B3 B4 B5 ==> B (-,B) C (-,C) \catC \Set^{\catC^\op}
%D
%D (( a0 a1 -> .plabel= l f
%D a2 place
%D A0 A1 |->
%D A0 A2 <- .plabel= l f^\op
%D A1 A3 <- .plabel= r f^*
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil <->
%D A4 A5 -> .plabel= a 𝐛y
%D
%D B0 B1 |->
%D B0 B2 -> .plabel= l f
%D B1 B3 -> .plabel= r f_*
%D B2 B3 |->
%D B0 B3 harrownodes nil 20 nil <->
%D B4 B5 -> .plabel= a 𝐛y'
%D ))
%D enddiagram
%D
$$\pu
\diag{emb-2}
$$
The Yoneda Lemma says that the functors $B^\op↦(B,-)$ and $B↦(-,B)$
--- whose short names are $𝐛y$ and $𝐛y'$ --- are full and faithful.
These functors are usually called the {\sl Yoneda Embeddings}
If we expand the `$(B,-)$' and the `$(-,B)$' in $B^\op↦(B,-)$ and
$B↦(-,B)$ we get $B^\op↦(C↦(B,C))$ and $B↦(A^\op↦(A,B))$, and this
makes the actions of $𝐛y$ and $𝐛y'$ on objects very easy to
understand. A trick to figure out how $𝐛y$ and $𝐛y'$ act on morphisms
is to draw the internal views of the natural transformations $g^*$ and
$g_*$ at the right of the diagram, and rewrite $𝐛yg$ and $𝐛y'g$ in
several equivalent notations:
%
%D diagram emb-3
%D 2Dx 100 +15 +30 +40 +35 +40 +30
%D 2D 100 a0 A0 A1 A6 A8 B0 B1
%D 2D
%D 2D +40 a1 A2 A3 A7 A9 B2 B3
%D 2D
%D 2D +15 a2 A4 A5 B4 B5
%D 2D
%D 2D +25 B0 B1 B6 B8
%D 2D
%D 2D +40 B2 B3 B7 B9
%D 2D
%D 2D +15 B4 B5
%D 2D
%D ren a0 a1 a2 ==> B C \catC
%D ren A0 A1 A2 A3 A4 A5 ==> B^\op (B,-) C^\op (C,-) \catC^\op \Set^{\catC}
%D ren B0 B1 B2 B3 B4 B5 ==> B (-,B) C (-,C) \catC \Set^{\catC^\op}
%D ren A6 A7 A8 A9 ==> (B,D) (C,D) g;h h
%D ren B6 B7 B8 B9 ==> (A,B) (A,C) f f;g
%D
%D (( a0 a1 -> .plabel= l g
%D a2 place
%D A0 A1 |->
%D A0 A2 <- .plabel= l g^\op
%D A1 A3 <- .plabel= r \sm{𝐛yg:=\\g^*:=\\(g,-):=\\λD.(g;):=\\λD.λh.(g;h)}
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil <->
%D A4 A5 -> .plabel= a 𝐛y
%D A6 A7 <- .plabel= r \sm{𝐛ygD:=\\g^*D:=\\(g,D):=\\λh.(g;h)=\\(g;)}
%D A8 A9 <-|
%D
%D B0 B1 |->
%D B0 B2 -> .plabel= l g
%D B1 B3 -> .plabel= r \sm{𝐛y'g:=\\g_*:=\\(-,g):=\\λA.(;g):=\\λA.λf.(f;g)}
%D B2 B3 |->
%D B0 B3 harrownodes nil 20 nil <->
%D B4 B5 -> .plabel= a 𝐛y'
%D B6 B7 -> .plabel= r \sm{𝐛y'gA:=\\g_*A:=\\(A,g):=\\λf.(f;g)=\\(;g)}
%D B8 B9 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{emb-3}
$$
% ____
% | _ \ ___ _ _ ___ ___
% | |_) / _ \ | | |/ _ \/ __|
% | _ < __/ |_| | __/\__ \
% |_| \_\___|\__, |\___||___/
% |___/
%
% «generic-figures» (to ".generic-figures")
% (find-books "__cats/__cats.el" "reyes")
% (find-reyeszolfpage 11 "1 The category of C-Sets")
% (find-reyeszolfpage 29 "2.2 Yoneda lemma")
% (defun dd () (interactive) (yonp 19))
\section{Reading ``Generic Figures and ther Glueings''}
\label{RRZ}
\def\dto{\diagxyto/-->/<150>}
When I first tried to read Reyes, Reyes and Zolfaghari's
\cite{ReyesZolf} (``RRZ'' from here on) I got {\sl very} stuck, as I
didn't have any good methods to work on its notation bit by bit to
make it make sense to me...
Take this diagram from page 11 of the book:
%
%D diagram rrz-1
%D 2Dx 100 +20 +20
%D 2D 100 F X
%D 2D
%D 2D +20 F'
%D
%D (( F' F -> .plabel= a f
%D F X --> .plabel= a σ
%D F' X --> .plabel= b σ.f
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{rrz-1}
$$
%
We can type its entities:
%
%D diagram rrz-2
%D 2Dx 100 +30 +25 +25
%D 2D 100 F X X(F) D0
%D 2D
%D 2D +30 F' X(F') D1
%D 2D
%D 2D +15 C0 C1 C2
%D ren C0 C1 C2 ==> \bbC \Set^{\bbC^\op} \Set
%D ren D0 D1 ==> σ σ.f
%D
%D (( F' F -> .plabel= l f
%D F X --> .plabel= a σ
%D F' X --> .plabel= b σ.f
%D C0 place C1 place C2 place
%D X(F) X(F') -> .plabel= r \sm{(\,).f:=\\X(f)}
%D D0 D1 |-> .plabel= r (\,).f
%D ))
%D enddiagram
%D
$$\pu
\diag{rrz-2}
\qquad
\begin{array}{l}
\text{$\bbC$ is a category} \\
F,F'∈\bbC \\
f:F'→F \\
X:\bbC^\op→\Set \\
X(F),X(F')∈\Set \\
σ∈X(F) \\
σ.f∈X(F') \qquad σ.f = X(f)(σ) \\
\end{array}
$$
In sec.\ref{internal-view} we said that we would sometimes write $A→B$
for $B^A$ or $\Hom(A,B)$; we can do something similar for `$\dto$'. In
RRZ $F \dto^σ X$ means $σ∈X(F)$, so we will interpret $F \dto X$ as
$X(F)$ and $F \dto^σ X$ as $σ:F \dto X$.
We can make the examples in RRZ more elementary if we work with finite
mathematical objects built from integers, pairs, and sets, as done in
\cite{OchsPH1} (sec.2 and onwards). Let $𝐛M$ be the directed
(multi-)graph with labeled arrows (``DGLA'') below:
%
%D diagram M
%D 2Dx 100 +25
%D 2D 100 A
%D 2D
%D 2D +25 B C
%D 2D
%D ren A B C ==> 7 8 9
%D
%D (( A B -> sl_ .plabel= l 78
%D A B -> sl^ .plabel= r 708
%D B C -> .plabel= b 89
%D A loop (ul,ur)^{77}
%D C loop (ur,dr)^{99}
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{M}
\qquad
𝐛M = \pmat{\{7,8,9\},\csm{(7,7,77),\\(7,8,78),\\(7,8,708),\\(8,9,89),\\(9,9,99)}}
$$
We can set $\bbC$ to this category (the identity arrows are omitted),
%
%D diagram VA
%D 2Dx 100
%D 2D 100 A
%D 2D
%D 2D +25 V
%D 2D
%D # ren ==>
%D
%D (( V A -> sl^ .plabel= l s
%D V A -> sl_ .plabel= r t
%D ))
%D enddiagram
%D
$$\pu
\diag{VA}
$$
%
to define figures made of vertices and arrows. This functor
$M:\bbC^\op→\Set$
%
%D diagram VAM
%D 2Dx 100 +50
%D 2D 100 M(A) MA
%D 2D
%D 2D +40 M(V) MV
%D 2D
%D ren MA MV ==> \{77,78,708,89,99\} \{7,8,9\}
%D
%D (( M(A) M(V) -> sl_ .plabel= l M(s)
%D M(A) M(V) -> sl^ .plabel= r M(t)
%D
%D MA MV -> sl_ .plabel= l \sm{77↦7\\78↦7\\708↦7\\89↦8\\99↦9\\}
%D MA MV -> sl^ .plabel= r \sm{77↦7\\78↦8\\708↦8\\89↦9\\99↦9\\}
%D ))
%D enddiagram
%D
$$\pu
\diag{VAM}
$$
%
``is'' the DGLA $𝐛M$ above.
I am not sure what this notation means when it appears in RRZ:
%
%:
%: {V}\dto{X}
%: ----------
%: a,b,c,d,e
%:
%: ^foo
%:
$$\pu
\ded{foo}
$$
%
It may be either ``$a,b,c,d,e:{V}\dto{X}$'' or
``$({V}\dto{X})=\{a,b,c,d,e\}$''... anyway, in $M$ we have:
%:
%: {V}\dto{M} {A}\dto{M}
%: ---------- ---------------
%: 7,8,9 77,78,708,89,99
%:
%: ^fooM ^barM
%:
$$\pu
\ded{fooM} \qquad \ded{barM}
$$
%
And this is a change of figure:
%
%D diagram chfig
%D 2Dx 100 +25 +25 +25
%D 2D 100 A1 A2 B0 C0
%D 2D
%D 2D +25 A0 B1 C1
%D 2D
%D 2D +15 CC CS B2
%D 2D
%D ren CC A0 A1 A2 CS ==> \bbC V A M \Set^{\bbC^\op}
%D ren B0 B1 B2 ==> M(A) M(V) \Set
%D ren C0 C1 ==> 708 7
%D
%D (( CC place CS place
%D A0 A1 -> .plabel= l s
%D A1 A2 --> .plabel= a 708
%D A0 A2 --> .plabel= r \sm{708.s\\=7}
%D
%D B0 B1 -> .plabel= l M(s)
%D B2 place
%D C0 C1 |-> .plabel= l M(s)
%D ))
%D enddiagram
%D
$$\pu
\diag{chfig}
$$
% ____ ____ _____
% | _ \| _ \ |__ / _ __ ___ ___ _ __
% | |_) | |_) | / / | '_ ` _ \ / _ \| '__|
% | _ <| _ < / /_ | | | | | | (_) | |
% |_| \_\_| \_\/____| |_| |_| |_|\___/|_|
%
% «morphisms-of-C-sets» (to ".morphisms-of-C-sets")
\subsection{Morphisms of $\bbC$-sets}
\label{morphisms-of-C-sets}
% (find-reyeszolfpage 11 "A morphism" "of C-sets")
A {\sl Morphisms of $\bbC$-sets} $Φ:X→Y$ (see p.11 of RZZ) is a
natural transformation from $X$ to $Y$, where both $X$ and $Y$ are
$\bbC$-sets, i.e., $X,Y:\bbC^\op→\Set$. The figure at left below
appears in p.11 of RRZ except for the last line with the the category
annotations; at the right of it is an internal view, in RRZ's
notation, of the natural transformation $Φ$:
%
%D diagram mcset-1
%D 2Dx 100 +35 +30 +30 +20 +30 +30 +25
%D 2D 100 A1 A2 A3 C0 D0 D1 E0 E1
%D 2D +19 E2
%D 2D +6 A0 C1 D2 D3 E3 E4
%D 2D
%D 2D +15 B0 B1 B2 D4 D5
%D 2D
%D ren A0 A1 A2 A3 ==> F' F X Y
%D ren B0 B1 B2 ==> \bbC \Set^{\bbC^\op} \Set^{\bbC^\op}
%D ren C0 C1 ==> F F'
%D ren D0 D1 D2 D3 D4 D5 ==> X(F) Y(F) X(F') Y(F') X Y
%D ren E0 E1 E2 E3 E4 ==> σ Φ(σ) Φ(σ).f σ.f Φ(σ.f)
%D
%D (( A0 A1 -> .plabel= l f
%D A1 A2 --> .plabel= a σ
%D A2 A3 -> .plabel= a Φ
%D A0 A2 --> .plabel= m σ.f
%D B0 place B1 B2 =
%D
%D C0 C1 <- .plabel= l f
%D D0 D1 -> .plabel= a Φ_F
%D D0 D2 -> .plabel= l X(f)
%D D1 D3 -> .plabel= r Y(f)
%D D2 D3 -> .plabel= a Φ_{F'}
%D D4 D5 -> .plabel= a Φ
%D
%D E0 E1 |-> E1 E2 |-> E0 E3 |-> E3 E4 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{mcset-1}
$$
Here is a type inference for the subexpressions of the ``naturality
condition'' $Φ(σ).f = Φ(σ.f)$:
%
$$\und{
\und{\und{Φ}{:X→Y} (\und{σ}{∈X(F)})}
{∈Y(f)}
\und{.\und{f}{:F'→F}}{:Y(F)→Y(F')}
}{∈Y(F')}
=
\und{\und{Φ}{:X→Y}
(\und{\und{σ}{∈X(F)} .
\und{f}{:F'→F}
}{∈X(F')})
}{∈Y(F')}
$$
One difficulty in translating $Φ(σ).f = Φ(σ.f)$ to standard notation
is that the arguments to the dot operation are ``in the wrong order''.
If we rewrite $σ.f$ as $(.f)(σ)$ then the naturality condition becomes
$(.f)(Φ(σ)) = Φ((.f)(σ))$, i.e., $(.f)∘Φ=Φ∘(.f)$, and the easiest way
(for me) to understand the types is to write first $f:F'→F$ and
$Φ:X→Y$ and then all the rest in the diagram below:
%
%D diagram ??
%D 2Dx 100 +20 +35 +25 +30
%D 2D 100 A0 B0 B1 D0 D1
%D 2D +19 D2
%D 2D +6 A1 B2 B3 D3 D4
%D 2D
%D 2D +15 C0 C1
%D 2D
%D ren A0 A1 ==> F F'
%D ren C0 C1 ==> X Y
%D ren B0 B1 B2 B3 ==> F(X) F(Y) F'(X) F'(Y)
%D ren D0 D1 D2 D3 D4 ==> σ Φ(σ) Φ(σ).f σ.f Φ(σ.f)
%D
%D (( A0 A1 <- .plabel= l f
%D B0 B1 -> .plabel= a Φ_F
%D B0 B2 -> .plabel= l X(f)
%D B1 B3 -> .plabel= r Y(f)
%D B2 B3 -> .plabel= a Φ_{F'}
%D C0 C1 -> .plabel= a Φ
%D D0 D1 |-> D1 D2 |-> D0 D3 |-> D3 D4 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{??}
$$
%
and $(.f)(Φ(σ)) = Φ((.f)(σ))$ becomes $Y(f)(Φ_F(σ)) =
Φ_{F'}(X(f)(σ))$, and $(.f)∘Φ=Φ∘(.f)$ becomes $Y(f)∘Φ_F =
Φ_{F'}∘X(f)$.
% ____ ____ _____ __ __
% | _ \| _ \ |__ / \ \ / /__ _ __
% | |_) | |_) | / / \ V / _ \| '_ \
% | _ <| _ < / /_ | | (_) | | | |
% |_| \_\_| \_\/____| |_|\___/|_| |_|
%
% «yoneda-in-RRZ» (to ".yoneda-in-RRZ")
% (defun dd () (interactive) (yonp 21))
\subsection{The Yoneda Lemma in RRZ}
\label{yoneda-in-RRZ}
% (find-LATEXfile "catsem-u.bib" "OchsPH1")
% (find-reyeszolfpage 22 "2 Representable C-sets and Yoneda lemma")
% (find-reyeszolfpage 29 "2.2 Yoneda lemma")
The Yoneda Lemma appears in pages 22--23 and again at pages 29--30 of
the book. Let's examine the enlarged versions --- drawn with internal
views --- of some of the figures used in the proof. Our enlarged
versions will be called diagrams YR1, YR2, and YR3.
{\sl Important:} we will make one change in RRZ's notation --- where
the book writes $h_F$ we will write $(-,F)$, and where it writes $h_f$
we will write $(-,f)$; we saw in sec.\ref{embeddings} that the action
of the natural transformation $(-,f)$ (a.k.a. $f_*$) is essentially
$(f∘)$.
This (``YR1'') is from p.23:
%
%D diagram YR1
%D 2Dx 100 +35 +35 +30 +25 +40 +30 +35
%D 2D 100 A1 A2 A3 C0 D0 D1 E0 E1
%D 2D +24 E2
%D 2D +6 A0 C1 D2 D3 E3 E4
%D 2D
%D 2D +15 B0 B1 B2 D4 D5
%D 2D
%D ren A0 A1 A2 A3 ==> F''' F'' (-,F') (-,F)
%D ren B0 B1 B2 ==> \bbC \Set^{\bbC^\op} \Set^{\bbC^\op}
%D ren C0 C1 ==> F''' F''
%D ren D0 D1 D2 D3 D4 D5 ==> (F'',F') (F'',F) (F''',F') (F''',F) (-,F') (-,F)
%D ren E0 E1 E2 E3 E4 ==> g f∘g (f∘g)∘h g∘h f∘(g∘h)
%D
%D (( A0 A1 -> .plabel= l h
%D A1 A2 --> .plabel= a g
%D A2 A3 -> .plabel= a (-,f)
%D A0 A2 --> .plabel= m g∘h
%D B0 place B1 B2 =
%D
%D C0 C1 <- .plabel= l h
%D D0 D1 -> .plabel= a \sm{(F,f)\\=(f∘)\\}
%D D0 D2 -> .plabel= l \sm{(h,F')\\=(∘h)\\}
%D D1 D3 -> .plabel= r \sm{(h,F)\\=(∘h)\\}
%D D2 D3 -> .plabel= a \sm{(F',f)\\=(f∘)\\}
%D D4 D5 -> .plabel= a (-,f)
%D
%D E0 E1 |-> E1 E2 |-> E0 E3 |-> E3 E4 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{YR1}
$$
This (``YR2'') is from p.29:
%
%D diagram YR2
%D 2Dx 100 +30 +30 +30 +25 +35 +30 +35
%D 2D 100 A1 A2 A3 C0 D0 D1 E0 E1
%D 2D +24 E2
%D 2D +6 A0 C1 D2 D3 E3 E4
%D 2D
%D 2D +15 B0 B1 B2 D4 D5
%D 2D
%D ren A0 A1 A2 A3 ==> F' F (-,F) X
%D ren B0 B1 B2 ==> \bbC \Set^{\bbC^\op} \Set^{\bbC^\op}
%D ren C0 C1 ==> F F'
%D ren D0 D1 D2 D3 D4 D5 ==> (F,F) X(F) (F',F) X(F') (-,F) X
%D ren E0 E1 E2 E3 E4 ==> 1_F Φ_F(1_F) Φ_F(1_F).f f Φ_{F'}(f)
%D
%D (( A0 A1 -> .plabel= l f
%D A1 A2 --> .plabel= a 1_F
%D A2 A3 -> .plabel= a Φ
%D A0 A2 --> .plabel= b f
%D B0 place B1 B2 =
%D
%D C0 C1 <- .plabel= l f
%D D0 D1 -> .plabel= a Φ_F
%D D0 D2 -> .plabel= l \sm{(f,F)\\=(∘f)\\}
%D D1 D3 -> .plabel= r X(f)
%D D2 D3 -> .plabel= a Φ_{F'}
%D D4 D5 -> .plabel= a Φ
%D
%D E0 E1 |-> E1 E2 |-> E0 E3 |-> E3 E4 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{YR2}
$$
This (``YR3'') is also from p.29:
%
%D diagram YR3
%D 2Dx 100 +30 +30 +30 +25 +35 +30 +35
%D 2D 100 A1 A2 A3 C0 D0 D1 E0 E1
%D 2D +24 E2
%D 2D +6 A0 C1 D2 D3 E3 E4
%D 2D
%D 2D +15 B0 B1 B2 D4 D5
%D 2D
%D ren A0 A1 A2 A3 ==> F'' F' (-,F) X
%D ren B0 B1 B2 ==> \bbC \Set^{\bbC^\op} \Set^{\bbC^\op}
%D ren C0 C1 ==> F' F''
%D ren D0 D1 D2 D3 D4 D5 ==> (F',F) X(F') (F'',F) X(F'') (-,F) X
%D ren E0 E1 E2 E3 E4 ==> f Φ_F(f) Φ_F(f).g f∘g Φ_{F'}(f∘g)
%D
%D (( A0 A1 -> .plabel= l g
%D A1 A2 --> .plabel= a f
%D A2 A3 -> .plabel= a Φ
%D A0 A2 --> .plabel= b g∘f
%D B0 place B1 B2 =
%D
%D C0 C1 <- .plabel= l g
%D D0 D1 -> .plabel= a Φ_{F'}
%D D0 D2 -> .plabel= l \sm{(g,F)\\=(∘g)\\}
%D D1 D3 -> .plabel= r X(f)
%D D2 D3 -> .plabel= a Φ_{F''}
%D D4 D5 -> .plabel= a Φ
%D
%D E0 E1 |-> E1 E2 |-> E0 E3 |-> E3 E4 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{YR3}
$$
(YR1 is used to prove that $(-,f)$ is
morphism of $\bbC$-sets)
(YR2 is used to prove that $Φ_{F'}(f)$ can be calculated as
$Φ_F(1_F).f = X(f)(Φ_F(1_F))$)
(YR3 is used to prove that (???))
(To do: debug this, compare with sections \ref{naturality} and \ref{contravariant}...)
% ______ ____ __
% / ___\ \ / / \/ |
% | | \ \ /\ / /| |\/| |
% | |___ \ V V / | | | |
% \____| \_/\_/ |_| |_|
%
% «CWM» (to ".CWM")
% (find-books "__cats/__cats.el" "maclane")
% (code-pdf "cwm2" "~/books/__cats/maclane__cwm_springer_2nd_ed.pdf")
% (code-pdftotext "cwm2" "~/books/__cats/maclane__cwm_springer_2nd_ed.pdf" 9)
% (find-cwm2page (+ 9 59) "2. The Yoneda Lemma")
\section{Reading MacLane's CWM}
\label{CWM}
MacLane (in \cite{CWM2}, section III.2, pages 59--62) starts by fixing
a functor $S:D→C$ and showing that for any pair $〈r,u:c→Sr〉$, that
we draw like this,
%
%D diagram cwm1
%D 2Dx 100 +25
%D 2D 100 u
%D 2D
%D 2D +20 r |-> Sr
%D 2D
%D 2D +15 D --> C
%D 2D
%D # ren ==>
%D
%D (( u Sr -> .plabel= r u
%D r Sr |-> .plabel= a S
%D D C -> .plabel= a S
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{cwm1}
$$
%
any choice of an object $d∈D$ induces a map $φ_d:D(r,d)→C(c,Sd)$,
%
%D diagram cwm2
%D 2Dx 100 +40 +30 +40
%D 2D 100 c
%D 2D
%D 2D +20 r |-> Sr
%D 2D
%D 2D +20 d |-> Sd f' -> Sf'∘u
%D 2D
%D 2D +15 A --> B C --> D
%D 2D
%D ren A B ==> D(r,d) C(c,Sd)
%D ren C D ==> D(r,d) C(c,Sd)
%D
%D (( c Sr -> .plabel= r u
%D r d -> .plabel= l f'
%D Sr Sd -> .plabel= r Sf'
%D r Sr |-> .plabel= a S
%D d Sd |-> .plabel= a S
%D A B -> .plabel= a φ_d
%D f' Sf'∘u |-> .plabel= a φ_d
%D C D -> .plabel= a φ_d
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{cwm2}
$$
%
It turns out that $D(r,-)$ and $C(c,S-)$ are functors,
%
%D diagram cwm3
%D 2Dx 100 +30 +60 +30
%D 2D 100 A0 A1 B0 B1
%D 2D
%D 2D +20 A2 A3 B2 B3
%D 2D
%D 2D +15 A4 A5 B4 B5
%D 2D
%D ren A0 A1 B0 B1 ==> d D(r,d) d C(c,Sd)
%D ren A2 A3 B2 B3 ==> d' D(r,d') d' C(c,Sd')
%D ren A4 A5 B4 B5 ==> D \Set D \Set
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l h
%D A1 A3 -> .plabel= r \sm{(D(r,-))(h):=\\λf'.(h∘f')}
%D A2 A3 |->
%D A4 A5 -> .plabel= a D(r,-)
%D
%D B0 B1 |->
%D B0 B2 -> .plabel= l h
%D B1 B3 -> .plabel= r \sm{(C(s,S-))(h):=\\λk.(Sh∘k)}
%D B2 B3 |->
%D B4 B5 -> .plabel= a C(c,S-)
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{cwm3}
$$
%
and $φ:D(r,-)→C(c,S-)$ is a natural transformation between them:
%
%D diagram cwm3
%D 2Dx 100 +30 +40 +30 +40
%D 2D 100 A0 B0 B1 C0 C1
%D 2D +19 C2
%D 2D +6 A1 B2 B3 C3 C4
%D 2D
%D 2D +15 B4 B5
%D 2D
%D ren A0 A1 ==> d d'
%D ren B0 B1 B2 B3 B4 B5 ==> D(r,d) C(c,Sd) D(r,d') C(c,Sd') D(r,-) C(c,S-)
%D ren C0 C1 C2 C3 C4 ==> f' Sf'∘u Sh∘(Sf'∘u) h∘f' S(h∘f')∘u
%D
%D (( A0 A1 -> .plabel= l h
%D
%D B0 B1 -> .plabel= a φ_d
%D B2 B3 -> .plabel= a φ_{d'}
%D B0 B2 -> .plabel= l D(r,h)
%D B1 B3 -> .plabel= r C(c,Sh)
%D B4 B5 -> .plabel= a φ
%D
%D C0 C1 |-> C1 C2 |->
%D C0 C3 |-> C3 C4 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{cwm3}
$$
However, MacLane introduces, {\sl right in the beginning}, a concept
that I feel that should better be left to a second moment...
(To be continued!!!)
% ____ _ _ _
% | _ \(_) ___| |__ | |
% | |_) | |/ _ \ '_ \| |
% | _ <| | __/ | | | |
% |_| \_\_|\___|_| |_|_|
%
% «riehl» (to ".riehl")
% (find-books "__cats/__cats.el" "riehl")
% (find-riehlccpage (+ 18 49) "2. Universal Properties, Representability, and the Yoneda Lemma")
% (find-riehlccpage (+ 18 50) "2.1. Representable functors")
% (find-riehlccpage (+ 18 55) "2.2. The Yoneda lemma")
% (find-riehlccpage (+ 18 62) "2.3. Universal properties and universal elements")
% (find-riehlccpage (+ 18 66) "2.4. The category of elements")
% (defun dd () (interactive) (yonp 22))
\section{Reading Emily Riehl's ``CT in Context''}
\label{riehl}
The Yoneda Lemma is proved in \cite{RiehlCTIC} in section 2.2, pages
55--61.
Here's Riehl's formula 2.2.5 from pages 57--58 in the shape of our
diagram Y4:
%
%D diagram Y4-riehl
%D 2Dx 100 +40
%D 2D 100 A1
%D 2D
%D 2D +25 A2 A3
%D 2D
%D 2D +30 B0 B1
%D 2D
%D 2D +30 B2
%D 2D
%D ren A1 A2 A3 ==> 1 c Fc
%D ren B0 B1 B2 ==> C(c,-) \Set(1,F-) F
%D
%D (( A1 A3 -> .plabel= r x'
%D A2 A3 |-> .plabel= a F
%D B0 B1 -> # .plabel= b T'
%D B1 B2 <->
%D B0 B2 -> .plabel= b α
%D A2 B1 varrownodes nil 20 nil <->
%D
%D ))
%D enddiagram
%D
%D diagram Y4-riehl-bij
%D 2Dx 100
%D 2D 100 A
%D 2D
%D 2D +40 B
%D 2D
%D ren A B ==> x∈Fc α∈\Hom(C(c,-),F)
%D
%D (( A B |-> sl_ .plabel= l \sm{α:=\\Ψ(x):=\\λd.λf.Ff(x)}
%D A B <-| sl^ .plabel= r \sm{a:=\\Φ(α):=\\α_c(1_c)}
%D ))
%D enddiagram
%D
\pu
$$\diag{Y4-riehl}
\qquad
\diag{Y4-riehl-bij}
$$
% (find-riehlccpage (+ 18 60) "Corollary 2.2.8 (Yoneda embedding)")
% (find-riehlcctext (+ 18 60) "Corollary 2.2.8 (Yoneda embedding)")
The Yoneda embeddings appear as Corollary 2.2.8 in \cite{RiehlCTIC},
in p.60. She makes this diagram:
%
%D diagram ye-riehl-orig
%D 2Dx 100 +35 +35 +35
%D 2D 100 A B a b
%D 2D
%D 2D +15 C D c d
%D 2D
%D 2D +25 E F e f
%D 2D
%D ren A B C D E F ==> 𝐬C 𝐬{Set}^{𝐬C^\op} c 𝐬C(-,c) d 𝐬C(-,d)
%D ren a b c d e f ==> 𝐬C^\op 𝐬{Set}^{𝐬C} c 𝐬C(c,-) d 𝐬C(d,-)
%D
%D (( A B `-> .plabel= a y
%D C D |->
%D C E -> .plabel= l f
%D D F -> .plabel= r f_*
%D E F |->
%D C F harrownodes nil 20 nil |->
%D
%D a b `-> .plabel= a y
%D c d |->
%D c e -> .plabel= l f
%D d f <- .plabel= r f^*
%D e f |->
%D c f harrownodes nil 20 nil |->
%D ))
%D enddiagram
%D
$$\pu
\diag{ye-riehl-orig}
$$
She uses the `$y$' with two different meanings, one in the left half
and another in the right half of her diagram. If we modify her diagram
to add some of the information from our diagrams in
sec.\ref{embeddings} and change her letters just a little bit, we get
this:
%
%D diagram ye-riehl-my
%D 2Dx 100 +35 +45 +35
%D 2D 100 A B a b
%D 2D
%D 2D +15 C D c d
%D 2D
%D 2D +35 E F e f
%D 2D
%D ren A B C D E F ==> 𝐬C 𝐬{Set}^{𝐬C^\op} b 𝐬C(-,b) c 𝐬C(-,c)
%D ren a b c d e f ==> 𝐬C^\op 𝐬{Set}^{𝐬C} b 𝐬C(b,-) c 𝐬C(c,-)
%D
%D (( A B `-> .plabel= a 𝐛y'
%D C D |->
%D C E -> .plabel= l g
%D D F -> .plabel= r \sm{g_*:=\\𝐛y'g:=\\𝐬C(-,g):=\\λa.λf.(g∘f)=\\λa.(g∘)}
%D E F |->
%D C F harrownodes nil 20 nil |->
%D
%D a b `-> .plabel= a 𝐛y
%D c d |->
%D c e -> .plabel= l g
%D d f <- .plabel= r \sm{g^*:=\\𝐛yg:=\\𝐬C(g,-):=\\λd.λh.(h∘g)=\\λd.(∘g)}
%D e f |->
%D c f harrownodes nil 20 nil |->
%D ))
%D enddiagram
%D
$$\pu
\diag{ye-riehl-my}
$$
% _ _
% / \__ _____ __| | ___ _ _
% / _ \ \ /\ / / _ \ / _` |/ _ \ | | |
% / ___ \ V V / (_) | (_| | __/ |_| |
% /_/ \_\_/\_/ \___/ \__,_|\___|\__, |
% |___/
%
% «awodey» (to ".awodey")
% (find-books "__cats/__cats.el" "awodey")
% (find-awodeyctpage (+ 10 160) "8.2 The Yoneda embedding")
% (find-awodeycttext "\n8.2 The Yoneda embedding")
% (find-awodeyctpage (+ 10 162) "8.3 The Yoneda Lemma")
% (find-awodeycttext "\n8.3 The Yoneda Lemma")
\section{Reading Awodey's ``Category Theory''}
(To do: show internal views etc of sections 8.2--8.4 of \cite{Awodey}
(pp.160--167))
\section{Related projects}
These notes are related to three, ahem, {\sl things}: a workshop
called ``Logic for Children'', a series of papers on ``Planar Heyting
Algebras for Children'' (these notes prepare the ground for the
material on presheaves, sheaves and geometric morphisms that will be
presented in the third paper), and a {\sl very} introductory course on
$λ$-calculus, logics and Categories that I am giving every semester in
my university since 2016. Links:
\url{http://angg.twu.net/logic-for-children-2018.html}
\url{http://angg.twu.net/math-b.html\#zhas-for-children-2}
\url{http://angg.twu.net/math-b.html\#lclt}
% \subsection{Universality}
\printbibliography
\end{document}
% Local Variables:
% coding: utf-8-unix
% End: