|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2020favorite-conventions.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020favorite-conventions.tex" :end))
% (defun C () (interactive) (find-LATEXSH "lualatex 2020favorite-conventions.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2020favorite-conventions.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020favorite-conventions.pdf"))
% (defun e () (interactive) (find-LATEX "2020favorite-conventions.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020favorite-conventions"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun d0 () (interactive) (find-ebuffer "2020favorite-conventions.pdf"))
% (code-eec-LATEX "2020favorite-conventions")
% (find-pdf-page "~/LATEX/2020favorite-conventions.pdf")
% (find-sh0 "cp -v ~/LATEX/2020favorite-conventions.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2020favorite-conventions.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2020favorite-conventions.pdf
% file:///tmp/2020favorite-conventions.pdf
% file:///tmp/pen/2020favorite-conventions.pdf
% http://angg.twu.net/LATEX/2020favorite-conventions.pdf
% (find-LATEX "2019.mk")
% (find-math-b-links "favorite-conventions" "2020favorite-conventions")
% (find-es "arxiv" "pdflatex")
% \ifx\pdfoutput\relax \else
% \pdfoutput=1
% \fi
% «.defs» (to "defs")
% «.defs-commaobj» (to "defs-commaobj")
% «.colors» (to "colors")
% «.title» (to "title")
% «.abstract» (to "abstract")
% «.toc» (to "toc")
% «.missing-diagrams» (to "missing-diagrams")
% «.the-conventions» (to "the-conventions")
% «.to-deserve-a-name» (to "to-deserve-a-name")
% «.freyd» (to "freyd")
% «.freyd-with-quantifiers» (to "freyd-with-quantifiers")
% «.freyd-with-functors» (to "freyd-with-functors")
% «.internal-views» (to "internal-views")
% «.reductions» (to "reductions")
% «.internal-view-functor» (to "internal-view-functor")
% «.internal-view-NT» (to "internal-view-NT")
% «.internal-view-adjunction» (to "internal-view-adjunction")
% «.teaching-adjunctions» (to "teaching-adjunctions")
% «.basic-example-as-skel» (to "basic-example-as-skel")
% «.basic-example-functors» (to "basic-example-functors")
% «.basic-example-NT» (to "basic-example-NT")
% «.basic-example-bij» (to "basic-example-bij")
% «.basic-example-full» (to "basic-example-full")
% «.extensions» (to "extensions")
% «.comma-categories» (to "comma-categories")
% «.yoneda-lemma» (to "yoneda-lemma")
% «.yoneda-embedding» (to "yoneda-embedding")
% «.opposite-categories» (to "opposite-categories")
% «.ness» (to "ness")
% «.representable-functors» (to "representable-functors")
% «.representable-functor-ex» (to "representable-functor-ex")
% «.yoneda-for-children» (to "yoneda-for-children")
% «.2-category-of-cats» (to "2-category-of-cats")
% «.kan-extensions» (to "kan-extensions")
% «.all-concepts» (to "all-concepts")
% «.kan-formula» (to "kan-formula")
% «.functors-as-objects» (to "functors-as-objects")
% «.gms-for-children» (to "gms-for-children")
% «.reading-the-elephant» (to "reading-the-elephant")
% «.how-to-name-this-language» (to "how-to-name-this-language")
% «.why-my-conventions» (to "why-my-conventions")
% «.related-and-unrelated» (to "related-and-unrelated")
% «.what-next» (to "what-next")
% «.references» (to "references")
%
% «.elisp» (to "elisp")
% «.make-for-arxiv» (to "make-for-arxiv")
% «.make» (to "make")
\documentclass[oneside,12pt]{article}
%\usepackage{hyperref} % (find-es "tex" "hyperref")
\usepackage[colorlinks,
%linkcolor=DarkRed,
citecolor=DarkRed,
urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{tocloft} % (find-es "tex" "tocloft")
\usepackage{indentfirst}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage{stmaryrd}
\usepackage{bm} % (find-es "tex" "bm")
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\usepackage{colorweb} % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (find-dednat6file "demo-write-dnt.tex")
\usepackage{ifluatex}
\ifluatex
\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrx21chars.tex % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
\else
\usepackage[utf8]{inputenc}
\input edrx21chars-d.tex % (find-LATEX "edrx21chars-d.tex")
\fi
%
\usepackage{edrx21} % (find-LATEX "edrx21.sty")
%
% (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof} % For derivation trees ("%:" lines)
\input diagxy % For 2D diagrams ("%D" lines)
\xyoption{curve} % For the ".curve=" feature in 2D diagrams
%
%\usepackage{edrx15} % (find-LATEX "edrx15.sty")
%\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
%\input edrxchars.tex % (find-LATEX "edrxchars.tex")
%\input edrx20chars.tex % (find-LATEX "edrx20chars.tex")
%\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
%\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
%\input 2017planar-has-defs.tex % (find-LATEX "2017planar-has-defs.tex")
%
% (find-es "tex" "geometry")
\usepackage[backend=biber,
style=alphabetic]{biblatex} % (find-es "tex" "biber")
\addbibresource{catsem-slides.bib} % (find-LATEX "catsem-slides.bib")
\begin{document}
%\catcode`\^^J=10
%\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
% (find-dednat6file "demo-write-dnt.tex")
\ifluatex
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}
\else
\input\jobname.dnt
\def\pu{}
\fi
% «defs» (to ".defs")
% (find-es "tex" "co")
% \co: a low-level way to typeset code; a poor man's "\verb"
\def\co#1{{%
\def\%{\char37}%
\def\\{\char92}%
\def\^{\char94}%
\def\~{\char126}%
\tt#1%
}}
\def\qco#1{`\co{#1}'}
\def\qqco#1{``\co{#1}''}
\def\ph{\phantom}
\def\respcomp{\mathsf{respcomp}}
\def\respids {\mathsf{respids}}
\def\sqcond {\mathsf{sqcond}}
\def\assoc {\mathsf{assoc}}
\def\idL {\mathsf{idL}}
\def\idR {\mathsf{idR}}
\def\univ {\mathsf{univ}}
\def\Ran {\mathsf{Ran}}
\def\sfC {\mathsf{C}}
\def\sfSet{\mathsf{Set}}
\def\Ring {\mathbf{Ring}}
\def\nameof#1{\ulcorner#1\urcorner}
\def\catK {\mathbf{K}}
\def\Dn {\Downarrow}
\def\veq{\rotatebox{90}{$=$}}
\def\liml{\underleftarrow {\lim}{}}
\def\limr{\underrightarrow{\lim}{}}
\def\veq{\rotatebox{90}{$=$}}
\def\origphi{\phi}
\def\DONE{(DONE)}
\def\DONE{}
% «defs-commaobj» (to ".defs-commaobj")
%
% «colors» (to ".colors")
% (find-angg ".emacs.papers" "xcolor")
\long\def\ColorRed #1{{\color{Red1}#1}}
\long\def\ColorViolet#1{{\color{MagentaVioletLight}#1}}
\long\def\ColorViolet#1{{\color{Violet!50!black}#1}}
\long\def\ColorGreen #1{{\color{SpringDarkHard}#1}}
\long\def\ColorGreen #1{{\color{SpringGreen4}#1}}
\long\def\ColorGreen #1{{\color{SpringGreenDark}#1}}
\long\def\ColorGray #1{{\color{GrayLight}#1}}
\long\def\ColorGray #1{{\color{black!30!white}#1}}
\long\def\ColorBrown #1{{\color{Brown}#1}}
\long\def\ColorBrown #1{{\color{brown}#1}}
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% «title» (to ".title")
\title{On my favorite conventions for drawing the missing diagrams in
Category Theory}
\author{Eduardo Ochs}
% http://angg.twu.net/math-b.html\#favco
\maketitle
% «abstract» (to ".abstract")
% (favp 1 "abstract")
% (fava "abstract")
\begin{abstract}
I used to believe that my conventions for drawing diagrams for
categorical statements could be written down in one page or less,
and that the only tricky part was the technique for reconstructing
objects ``from their names'' (sec.\ref{to-deserve-a-name})... but
then I found out that this is not so.
This is an attempt to explain, with motivations and examples, all
the conventions behind a certain diagram, called the ``Basic
Example'' in the text. Once the conventions are understood that
diagram becomes a ``skeleton'' for a certain lemma related to the
Yoneda Lemma, in the sense that both the statement and the proof of
that lemma can be reconstructed from the diagram. The last sections
discuss some simple ways to extend the conventions; we see how to
express in diagrams the (``real'') Yoneda Lemma and a corollary of
it, how to define comma categories,
%
% how to define certain limits using comma categories,
%
and how to formalize the diagram for ``geometric morphism for
children'' mentioned in sec.\ref{missing-diagrams}.
\msk
People in CT usually only share their ways of visualizing things
when their diagrams cross some threshold of mathematical relevance
--- and this usually happens when they prove new theorems with their
diagrams, or when they can show that their diagrams can translate
calculations that used to be huge into things that are much easier
to visualize. The diagrammatic language that I present here lies
below that threshold --- and so it is a ``private'' diagrammatic
language, that I am making public as an attempt to establish a
dialogue with other people who have also created their own private
diagrammatic languages.
\end{abstract}
\newpage
% _____ ___ ____
% |_ _/ _ \ / ___|
% | || | | | |
% | || |_| | |___
% |_| \___/ \____|
%
% «toc» (to ".toc")
% (favp 2 "toc")
% (fava "toc")
% (find-es "tex" "tocloft")
\renewcommand{\cfttoctitlefont}{\bfseries}
\setlength{\cftbeforesecskip}{2.5pt}
%\renewcommand{\cftsecfont}{\bfseries}
%\renewcommand{\cftsecfont}{}
% (find-es "tex" "contentsline")
%
% {\makeatletter
% \renewcommand*\l@section{\@dottedtocline{1}{1.5em}{2.3em}}
% %\renewcommand*\l@section{\@dottedtocline{1}{1.5em}{2.3em}}
% \@starttoc{toc}
% }
\tableofcontents
% __ __ _ _
% | \/ (_)___ ___(_)_ __ __ _
% | |\/| | / __/ __| | '_ \ / _` |
% | | | | \__ \__ \ | | | | (_| |
% |_| |_|_|___/___/_|_| |_|\__, |
% |___/
%
% «missing-diagrams» (to ".missing-diagrams")
% (favp 2 "missing-diagrams")
% (fava "missing-diagrams")
\section{Missing diagrams}
\label{missing-diagrams}
I need to tell a long story here.
Let me start with some quotes. This one is from Eilenberg and Steenrod
(\cite[p.ix]{EilenbergSteenrod}, but I learned it from
\cite[pp.82--83]{Kromer}):
\begin{quotation}
The diagrams incorporate a large amount of information. Their use
provides extensive savings in space and in mental effort. In the
case of many theorems, the setting up of the correct diagram is the
major part of the proof. We therefore urge that the reader stop at
the end of each theorem and attempt to construct for himself the
relevant diagram before examining the one which is given in the
text. Once this is done, the subsequent demonstration can be
followed more readily; in fact, the reader can usually supply it
himself.
\end{quotation}
I spent a {\sl lot} of my time studying Category Theory trying to
``supply the diagrams myself''. In \cite{EilenbergSteenrod} supplying
the diagrams is not very hard (I guess), but in books like
\cite{CWM2}, in which most important concepts involve several
categories, I had to rearrange my diagrams hundreds of times until I
reached ``good'' diagrams...
% (find-angg ".emacs" "idarct-preprint")
% (find-idarctpage 1 "1. Mental Space and Diagrams")
% (find-idarcttext 1 "1. Mental Space and Diagrams")
% (find-idarctpage 15 "12. Skeletons of proofs")
% (find-idarcttext 15 "12. Skeletons of proofs")
% (find-idarctpage 23 "16. Archetypal Models")
% (find-idarcttext 23 "16. Archetypal Models")
The problem is that I expected too much from ``good'' diagrams. The
next quotes are from the sections 1 and 12 of an article that I wrote
about that (\cite{IDARCT}):
\begin{quotation}
My memory is limited, and not very dependable: I often have to
rededuce results to be sure of them, and I have to make them fit in
as little ``mental space'' as possible...
Different people have different measures for ``mental space'';
someone with a good algebraic memory may feel that an expression
like $\mathsf{Frob}: Σ_f(P ∧ f^* Q) ≅ Σ_f P ∧ Q$ is easy to
remember, while I always think diagramatically, and so what I do is
that I remember this diagram,
\begin{center}
\includegraphics[height=60pt]{2020notes-yoneda-frob.pdf}
\end{center}
\noindent and I reconstruct the formula from it.
\end{quotation}
\begin{quotation}
Let's call the ``projected'' version of a mathematical object its
``skeleton''. The underlying idea in this paper is that for the
right kinds of projections, and for some kinds of mathetical
objects, it should be possible to reconstruct enough of the original
object from its skeleton and few extra clues --- just like
paleontologists can reconstruct from a fossil skeleton the look of
an animal when it was alive.
\end{quotation}
I was searching for a diagrammatic language that would let me express
the ``skeletons'' of categorical definitions and proofs. I wanted
these skeletons to be easy to remember --- partly because they would
have shapes that were easy to remember, and partly because they would
be similar to ``archetypal cases'' (\cite[section 16]{IDARCT}).
\bsk
In 2016 and 2017 I taught a seminar course for undergraduates that
covered a bit of Category Theory in the end --- see Section
\ref{teaching-adjunctions} and \cite{OchsWLD2019} --- and this forced
me to invent new techniques for working in two different styles in
parallel: a style ``for adults'', more general, abstract, and formal,
and another ``for children'', with more diagrams and examples. After
some semesters, and after writing most of the material that became
\cite{PH1}, I tried to read again some parts of Johnstone's ``Sketches
of an Elephant'', a book that always felt quite impenetrable to me,
and I found a way to present geometric morphisms in toposes to
``children''. It was based on this diagram,
%
% (jopp 23 "Set-PA")
% (joe "Set-PA")
%
%L sesw = {[" w"]="↙", [" e"]="↘"}
%
%R local Aargs, Bargs = 3/#1 #2 \, 3/ #1 \
%R | e w e | | w e |
%R \ #3 #4 / |#2 #3 |
%R | e w e |
%R | #4 #5 |
%R | e w |
%R \ #6 /
%R
%R Aargs:tozmp({def="pshAargs#1#2#3#4", scale="11pt", meta="p"}):addcells(sesw):output()
%R Bargs:tozmp({def="pshBargs#1#2#3#4#5#6", scale="11pt", meta="p"}):addcells(sesw):output()
%
%D diagram gm-for-children
%D 2Dx 100 +70
%D 2D 100 A0 A1
%D 2D
%D 2D +60 A2 A3
%D 2D
%D 2D +30 A4 A5
%D 2D
%D 2D +15 A6 A7
%D 2D
%D ren A0 A1 ==> f^*G G
%D ren A2 A3 ==> H f_*H
%D ren A0 A1 ==> \LG \G
%D ren A2 A3 ==> \H \RH
%D ren A4 A5 ==> \Set^\catA \Set^\catB
%D ren A6 A7 ==> \catA \catB
%D
%D (( A0 A1 <-|
%D A0 A2 ->
%D A1 A3 ->
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil <->
%D A4 A5 <- sl^ .plabel= a f^*
%D A4 A5 -> sl_ .plabel= b f_*
%D A6 A7 -> .plabel= a f
%D ))
%D enddiagram
%D
%D diagram gm-for-adults
%D 2Dx 100 +20
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +15 A4 A5
%D 2D
%D 2D +15 A6 A7
%D 2D
%D ren A0 A1 ==> f^*G G
%D ren A2 A3 ==> H f_*H
%D ren A4 A5 ==> \calE \calF
%D ren A6 A7 ==> \catA \catB
%D
%D (( A0 A1 <-|
%D A0 A2 ->
%D A1 A3 ->
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil <->
%D A4 A5 <- sl^ .plabel= a f^*
%D A4 A5 -> sl_ .plabel= b f_*
%D # A6 A7 -> .plabel= a f
%D ))
%D enddiagram
%D
\pu
$$
\diag{gm-for-adults}
\qquad
\def\LG{\pshAargs{G_2}{G_3}{G_4}{G_5}}
\def\G {\pshBargs{G_1}{G_2}{G_3}{G_4}{G_5}{G_6}}
\def\H {\pshAargs{H_2}{H_3}{H_4}{H_5}}
\def\RH{\pshBargs{H_2{×_{H_4}}H_3}{H_2}{H_3}{H_4}{H_5}{1}}
\scalebox{0.6}{$
\diag{gm-for-children}
$}
$$
%
that we will discuss in detail in \ref{gms-for-children}. Its left
half is a generic geometric morphism (``for adults''), and its right
half is a very specific geometric morphism (``for children'') in which
everything is easy to understand and to visualize, and that turns out
to be ``archetypal enough''.
I showed that to the few categorists with whom I had contact and the
feedback that I got was quite positive. A few of them --- the ones who
were strictly ``adults'' --- couldn't understand why I was playing
with particular cases, and even worse, with finite categories, instead
of proving things in the most general case possible, but some others
said that these ideas were very nice, that they knew a few bits about
geometric morphisms but those bits didn't connect well, and that now
they had a family of particular cases to think about, and they had
much more intuition than before.
That was the first time that my way of using diagrams yielded
something so nice! This was the excuse that I needed to organize a
workshop on diagrammatic languages and ways to use particular
cases; here's how I advertised it (from \cite{OchsLucatelli}):
%
\begin{quotation}
When we explain a theorem to children --- in the strict sense of the
term --- we focus on concrete examples, and we avoid
generalizations, abstract structures and infinite objects.
When we present something to ``children'', in a wider sense of the
term that means ``people without mathematical maturity'', or even
``people without expertise in a certain area'', we usually do
something similar: we start from a few motivating examples, and then
we generalize.
One of the aims of this workshop is to discuss techniques for {\sl
particularization} and {\sl generalization}. Particularization is
easy; substituing variables in a general statement is often enough
to do the job. Generalization is much harder, and one way to
visualize how it works is to regard particularization as a
projection: a coil projects a circle-like shadow on the ground, and
we can ask for ways to ``lift'' pieces of that circle to the coil
continously. {\sl Projections} lose dimensions and may collapse
things that were originally different; {\sl liftings} try to
reconstruct the missing information in a sensible way. There may be
several different liftings for a certain part of the circle, or
none. Finding good generalizations is somehow like finding good
liftings.
The second of our aims is to discuss {\sl diagrams}. For example, in
Category Theory statements, definitions and proofs can be often
expressed as diagrams, and if we start with a general diagram and
particularize it we get a second diagram with the same shape as the
first one, and that second diagram can be used as a version ``for
children'' of the general statement and proof. Diagrams were for a
long time considered second-class entities in CT literature
(\cite{Kromer} discusses some of the reasons), and were omitted;
readers who think very visually would feel that part of the work
involved in understanding CT papers and books would be to
reconstruct the ``missing'' diagrams from algebraic statements.
Particular cases, even when they were the motivation for the general
definition, are also treated as somewhat second-class --- and this
inspires a possible meaning for what can call ``Category Theory for
Children'': to start from the diagrams for particular cases, and
then ``lift'' them to the general case. Note that this can be done
outside Category Theory too; \cite{Jamnik} is a good example.
Our third aim is to discuss {\sl models}. A standard example is that
every topological space is a Heyting Algebra, and so a model for
Intuitionistic Predicate Logic, and this lets us explain visually
some features of IPL. Something similar can be done for some modal
and paraconsistent logics; we believe that the figures for that
should be considered more important, and be more well-known.
\end{quotation}
This is from the second announcement:
\begin{quotation}
If we say that categorical definitions are ``for adults'' - because
they may be very abstract - and that particular cases, diagrams, and
analogies are ``for children'', then our intent with this workshop
becomes easy to state. ``Children'' are willing to use ``tools for
children'' to do mathematics, even if they will have to translate
everything to a language ``for adults'' to make their results
dependable and publishable, and even if the bridge between their
tools ``for children'' and ``for adults'' is somewhat defective,
i.e., if the translation only works on simple cases...
We are interested in that {\sl bridge} between maths ``for adults''
and ``for children'' in several areas. Maths ``for children'' are
hard to publish, even informally as notes (see this thread
\msk
\centerline{\url{http://angg.twu.net/categories-2017may02.html}}
\msk
\noindent in the Categories mailing list), so often techniques are
rediscovered over and over, but kept restricted to the ``oral
culture'' of the area.
Our main intents with this workshop are:
\begin{itemize}
\item to discuss (over coffe breaks!) the techniques of the
``bridge'' that we currently use in seemingly ad-hoc ways,
\item to systematize and ``mechanize'' these techniques to make
them quicker to apply,
\item to find ways to publish those techniques --- in journals or
elsewhere,
\item to connect people in several areas working in related
ideas, and to create repositories of online resources.
\end{itemize}
\end{quotation}
In the UniLog 2018 I was able to chat with several categorists, and
they told me about the oral culture of CT and showed me that it was
not as I was guessing, and I also spent two evenings with Peter Arndt
working on factorizations of geometric morphisms ``for children'' ---
and this made me feel that I could present applications of this
diagrammatic language in conferences that were more top-level-ish in
some sense.
The following quote is from the abstract of my submission (\cite{MDE})
to the ACT2019:
%
\begin{quotation}
Imagine two category theorists, Aleks and Bob, who both think very
visually and who have exactly the same background. One day Aleks
discovers a theorem, $T_1$, and sends an e-mail, $E_1$, to Bob,
stating and proving $T_1$ in a purely algebraic way; then Bob is
able to reconstruct by himself Aleks's diagrams for $T_1$ exactly as
Aleks has thought them. We say that Bob has reconstructed the
{\it missing diagrams} in Aleks's e-mail.
Now suppose that Carol has published a paper, $P_2$, with a theorem
$T_2$. Aleks and Bob both read her paper independently, and both
pretend that she thinks diagrammatically in the same way as them.
They both ``reconstruct the missing diagrams'' in $P_2$ in the same
way, even though Carol has never used those diagrams herself.
\end{quotation}
%
and this from my submission (\cite{OchsTallinnAbs}) to Diagrams 2020:
%
\begin{quotation}
Category Theory gives the impression of being an area where most
concepts and arguments are stated and formalized via diagrams, but
this is not exactly true... in most texts almost everything is done
algebraically, and the reader is expected to be able to reconstruct
the ``missing diagrams'' by himself.
I used to believe, as an outsider, that some people who grew up
immersed the oral culture of the area would know several techniques
for ``drawing the missing diagrams''. My main intent when I
organized the workshop ``Logic for Children'' at the UniLog 2018
\cite{OchsLucatelli} was to collect some of these folklore
techniques, compare them with the ones that I had developed myself
to study CT, and formalize them all --- but what I found instead was
that everybody that I could get in touch with used their own ad-hoc
techniques, and that what I was trying to do was either totally new
to them, or at least new in its level of detail.
\end{quotation}
The story continues in the last three sections --- that also explains
why I decided to write these notes using the first person in most
places.
% and in minicourses in conferences, and this sort of forced me to
% invent new techniques for working in several levels of abstraction
% --- ``for adults'' and ``for children'' --- in parallel, and for
% translating between these styles. After that I tried to apply these
% techniques to Johnstone's ``Elephant'', a book that always made me
% think ``Help! I need a version for children of this!!!'', and they
% {\sl worked} --- I found a nice way to visualize two of its
% factorizations of geometric morphisms...
% ...and I discovered, with Peter Arndt, that if we start with toposes
% of the form $\Set^D$, where $D$ is a finite category, and a
% geometric morphism between them, we can perform these two
% factorizations by going through other toposes of the form $\Set^D$.
% From that point on I had concrete evidence that this diagrammatic
% language could be used to formulate conjectures and to obtain their
% proofs, and I had a theorem that I had obtained with it that seemed
% to be new...
% (nyop 11 "missing-diags-elephant")
% (nyo "missing-diags-elephant")
% (oxap 1 "title" "Aleks and Bob")
% (oxa "title" "Aleks and Bob")
% ____ _ _
% / ___|___ _ ____ _____ _ __ | |_(_) ___ _ __ ___
% | | / _ \| '_ \ \ / / _ \ '_ \| __| |/ _ \| '_ \/ __|
% | |__| (_) | | | \ V / __/ | | | |_| | (_) | | | \__ \
% \____\___/|_| |_|\_/ \___|_| |_|\__|_|\___/|_| |_|___/
%
% «the-conventions» (to ".the-conventions")
% (favp 8 "the-conventions")
% (fava "the-conventions")
\section{The conventions \DONE}
\label{the-conventions}
The conventions that I will present now are the ones that we need for
this diagram (called the ``Basic Example'' from here on), that is
essentially the Proposition 1 in the proof of the Yoneda Lemma in
\cite[Section III.2]{CWM2}:
%
%D diagram Basic-Example
%D 2Dx 100 +40
%D 2D 100 A1
%D 2D |
%D 2D +20 A2 |-> A3
%D 2D
%D 2D +15 B0 --> B1
%D 2D
%D 2D +15 C0 --> C1
%D 2D \ |
%D 2D +20 C2
%D 2D
%D ren A1 ==> A
%D ren A2 A3 ==> C RC
%D ren B0 B1 ==> \catB \catA
%D ren C0 C1 C2 ==> \catB(C,-) \catA(A,R-) ?
%D
%D (( A1 A3 -> .plabel= r η
%D A2 A3 |->
%D
%D B0 B1 -> .plabel= a R\phantom{mmm}
%D
%D C0 C1 -> .plabel= b T
%D # C0 C2 -> .plabel= l \sm{ψ\\\text{(iso)}}
%D # C1 C2 <->
%D
%D C0 C1 midpoint A1 A3 midpoint <-> .curve= ^15pt
%D ))
%D enddiagram
%
\pu
$$\scalebox{2.0}{$
\diag{Basic-Example}
$}
$$
\begin{itemize}
\item[(CD)] Our diagrams are made of components that are nodes and
arrows. The nodes can contain arbitrary expressions. The arrows work
as connectives, and each arrow can be interpreted as the top-level
connective in the smallest subexpression that contains it. For
example, the curved arrow in the diagram above can be interpreted
as:
%
$$(A\ton{η}RC)↔(\catB(C,-) \ton{T} \catA(A,R-)).
$$
\item[(C$→$)] Arrows that look like `$→$' (\qqco{\\to}) represent
hom-sets, or, in $\Set$, spaces of functions. When a `$→$' arrow is
named the name stands for an element of that hom-set. For example,
in $A \ton{η} RC$ we have $η:A→RC$.
\item[(C$↦$)] Arrows that look like `$↦$' (\qqco{\\mapsto}) represent
internal views of functions or functors. This has some subtleties;
see Section \ref{internal-views}.
\item[(C$↔$)] Arrows that look like `$↔$' (\qqco{\\leftrightarrow})
represent bijections or isomorphisms.
\item[(CAI)] ``Above'' usually means ``inside'', or ``internal view''.
In the diagram above the morphism $η:A→RC$ is in $\catA$ and $C$ is
an object of $\catB$. Also, the arrow $C \mapsto RC$ is above $\catB
\ton{R} \catA$, and this means that it is an internal view of the
functor $R$. Note that {\sl usually} is not {\sl always} --- and
$\catB \ton{R} \catA$ is not an internal view of $\catB(C,-) \ton{T}
\catA(A,R-)$.
\item[(CO)] When the definition of a component of our diagram is
``obvious'' in the sense of ``there is a unique natural construction
for an object with that name'', we will usually omit its definition
and {\sl pretend} that it is obvious; same for its uniqueness. See
Section \ref{to-deserve-a-name}.
\item[(CC)] Everything commutes by default, and non-commutative cells
have to be indicated explicitly. See Section \ref{freyd-notation}.
\item[(CTL)] The default ``meaning'' for a diagram is the definition
of its top-level component. There is a natural partial order on the
components of a diagram, in which $α \prec β$ iff $α$ is ``more
basic'' than $β$, or, in other words, if $α$ needs to be defined
before $β$. In the diagram above the top-level component is the
curved bijection.
\item[(CAdj)] {\sl I use shapes based on my way of drawing adjunctions
whenever possible.} I like adjunctions so much that when I want to
explain Category Theory to someone who knows just a little bit of
Maths I always start by the adjunction $({×}B)⊣(B{→})$ of Section
\ref{internal-view-adjunction}; I always draw it in a canonical way,
with the left adjoint going left, the right adjoint going right, and
the morphisms going down. In Proposition 1 of \cite[Section
III.2]{CWM2} the map $η$ is a universal arrow, and someone who
learns adjunctions first sees the unit maps $η:A→(B{→}(A{×}B))$ as
the first examples of universal arrows --- so that's why the upper
part of the diagram above is drawn in this position.
\item[(COT)] We use a notation as close to the original text as
possible, especially when we are trying to draw the missing diagrams
for some existing text. If we were drawing the missing diagrams for
the Proposition 1 of \cite[Section III.2]{CWM2} our diagram would be
this:
%
%D diagram yoneda-cwm-0-small
%D 2Dx 100 +35
%D 2D 100 A1
%D 2D |
%D 2D +20 A2 |-> A3
%D 2D
%D 2D +10 B0 --> B1
%D 2D
%D 2D +10 C0 --> C1
%D 2D \ |
%D 2D +20 C2
%D 2D
%D ren A1 ==> c
%D ren A2 A3 ==> r Sr
%D ren B0 B1 ==> D C
%D ren C0 C1 C2 ==> D(r,-) C(c,S-) ?
%D
%D (( A1 A3 -> .plabel= r u
%D A2 A3 |->
%D
%D B0 B1 -> .plabel= a S\phantom{mmm}
%D
%D C0 C1 -> .plabel= b φ
%D # C0 C2 -> .plabel= l \sm{ψ\\\text{(iso)}}
%D # C1 C2 <->
%D
%D C0 C1 midpoint A1 A3 midpoint <-> .curve= ^11pt
%D ))
%D enddiagram
%
$$\pu
\diag{yoneda-cwm-0-small}
$$
%
but I hate Mac Lane's choice of letters, so I decided to use another
notation here.
\item[(CSk)] Suppose that we have a piece of text --- say, a paragraph
$P$ --- and we want to reconstruct the ``missing diagram'' $D$ for
$P$. Ideally this $D$ should be a ``skeleton'' for $P$, in the sense
that it should be possible to reconstruct the ideas in $P$ from the
diagram $D$ using very few extra hints; see \cite[sec.12]{IDARCT}.
\item[(CFSh)] The image by a functor of a diagram $D$ is drawn with
the same shape as $D$.
\item[(CISh)] The internal view of a diagram $D$ is drawn with the
same shape as $D$, modulo duplications --- see section
\ref{internal-views}.
\item[(CPSh)] A particular case of a diagram $D$ is drawn with the
same shape as $D$.
\item[(CNSh)] A translation of a diagram $D$ to another notation is
drawn with the same shape as $D$.
\end{itemize}
% (find-books "__comp/__comp.el" "penrose")
Note that I have presented these conventions in a human-friendly way,
that is somewhat informal and admits exceptions and extensions. Some
simple examples of extensions will be discussed in Section
\ref{extensions}.
See \cite{PenroseSIGGRAPH2020} for a system that produces diagrams
from conventions and specifications and then lets the user adjust
these generated diagrams to make them clearer and more aesthetically
pleasing --- but as far as I know Penrose can only {\sl produce}
diagrams, not {\sl read} them.
% ____
% | _ \ ___ ___ ___ _ ____ _____ _ __ __ _ _ __ ___ ___
% | | | |/ _ \/ __|/ _ \ '__\ \ / / _ \ | '_ \ / _` | '_ ` _ \ / _ \
% | |_| | __/\__ \ __/ | \ V / __/ | | | | (_| | | | | | | __/
% |____/ \___||___/\___|_| \_/ \___| |_| |_|\__,_|_| |_| |_|\___|
%
% «to-deserve-a-name» (to ".to-deserve-a-name")
% (favp 11 "to-deserve-a-name")
% (fava "to-deserve-a-name")
\section{Finding ``the'' object with a given name \DONE}
\label{to-deserve-a-name}
One of the books that I tried to read when I was starting to learn
Category Theory was Mac Lane's \cite{CWM2}. It is written for readers
who know a lot of mathematics and who can follow some steps that it
treats as obvious. I was not (yet) a reader like that, but I wanted to
become one.
There is one specific thing that \cite{CWM2} does pretending that it
is obvious that I found especially fascinating. It ``defines''
functors by describing their actions on objects, and it leaves to the
reader the task of discovering their actions on morphisms. Let's see
how to find these actions on morphisms.
A functor $F:\catA→\catB$ has four components:
%
$$F=(F_0, F_1, \respids_F, \respcomp_F).$$
%
They are its action on objects, its action on morphisms, the assurance
that it takes identity maps to identity maps, and the assurance that
it respects compositions. When Mac Lane says this,
%
\begin{quote}
Fix a set $B$. Let $(×B)$ denote {\sl the} functor that takes each set
$A$ to $A×B$.
\end{quote}
%
he is saying that $(×B)_0 A = A×B$, or, more precisely, this:
%
$$(×B)_0 := λA.\,A×B$$
The ``{\sl the}'' in the expression ``Let $(×B)$ denote {\sl the}
functor...'' implies that the precise meaning of $(×B)_1$ is easy to
find, and that it is easy to prove $\respids_{(×B)}$ and
$\respcomp_{(×B)}$.
If $f:A'→A$ then $(×B)_1 f : (×B)_0 A' → (×B)_0 A$. We know the {\sl
name} of the image morphism, $(×B)_1 f$, and its {\sl type},
%
$$(×B)_1 f : A'×B → A×B,$$
%
and it is implicit that there is an ``obvious'' natural construction
for this $(×B)_1 f$ from $f$. A natural construction is ---
TA-DAAAA!!! --- a $λ$-term, so we are looking for a term of type $A'×B
→ A×B$ that can be constructed from $f:A'→A$.
In a big diagram:
%:
%:
%: [p:A'{×}B]^1
%: ------------
%: πp:A' f:A'→A [p:A'{×}B]^1
%: -------------- ------------
%: f(πp):A π'p:B
%: ----------------------
%: f:A'→A (f(πp),π'p):A{×}B
%: ==================== => -----------------------------------1
%: (×B)_1f:A'{×}B→A{×}B (λp⠆A'{×}B.(f(πp),π'p):A'{×}B→A{×}B
%:
%: ^foo1 ^foo2
%:
\pu
$$\ded{foo1} \quad ⇒ \ded{foo2}$$
A double bar in a derivation means ``there are several omitted steps
here'', and sometimes a double bar suggests that these omitted steps
are obvious. The derivation on the left says that there is an
``obvious'' way to build a $(×B)_1f:A'{×}B→A{×}B$ from a
``hypothesis'' $f:A'→A$. If we expand its double bar we get the tree
at the right, that shows that the ``precise meaning'' for $(×B)_1f$ is
$(λp⠆A'{×}B.(f(πp),π'p)$. More formally (and erasing a typing),
%
$$(×B)_1 := λf.(λp.(f(πp),π'p)).$$
The expansion of the double bar above becomes something more familiar
if we translate the trees to Logic using Curry-Howard:
%:
%:
%: [P∧R]^1
%: -------
%: P P→Q [P∧R]^1
%: ---------- -------
%: Q R
%: -----------
%: P→Q Q∧R
%: ======= => ------------1
%: P∧R→Q∧R P∧R→Q∧R
%:
%: ^foo-logic1 ^foo-logic2
%:
\pu
$$\ded{foo-logic1} \quad ⇒ \ded{foo-logic2}$$
We obtain the tree at the right by {\sl proof search}.
Let's give a name for the operation above that obtained a term of type
$A'×B→A×B$: we will call that operation {\sl term search}, or, as it
is somewhat related to type inference, {\sl term inference}.
Term search may yield several different construction and trees, and so
several non-equivalent terms of the desired type. When Mac Lane says
``{\sl the} functor $(×B)$'' he is indicating that:
\begin{itemize}
\item a term for $(×B)_1$ is easy to find (note that we use the
expression ``a {\sl precise meaning} for $(×B)_1$''),
\item all other natural constructions for something that ``deserves
the name'' $(×B)_1$ yield terms equivalent to that first, most
obvious one,
\item proving $\respids_{(×B)}$ and $\respcomp_{(×B)}$ is trivial.
\end{itemize}
In many situations we will start by just the name of a functor, as the
``$(×B)$'' in the example above, and from that name it will be easy to
find {\sl the} ``precise meaning'' for $(×B)_0$, and from that the
``precise meaning'' for $(×B)_1$, and after that proofs that
$\respids_{(×B)}$ and $\respcomp_{(×B)}$. We will use the expression
``...deserving the name...'' in this process --- terms for $(×B)_0$,
$(×B)_1$, $\respids_{(×B)}$, and $\respcomp_{(×B)}$ ``deserve their
names'' if they obey the expected constraints.
For a more thorough discussion see \cite{IDARCT}.
\msk
{\sl Note: I am not aware of any papers or books that discuss how to
(re)construct a functor from its action on objects, or from its
name. If you have any references, please let me know!}
\msk
These ideas of ``finding a precise meaning'' and ``finding (something)
deserving that name'' can also be applied to morphisms, natural
transformations, isomorphisms, and so on.
In Section \ref{basic-example-bij} we will see how to find natural
constructions for the two directions of the bijection in the Basic
Example --- or how the expand the double bars in the two derivations
here:
%:
%: γ:A→RC
%: ========================
%: T:\catB(C,-)→\catA(A,R-)
%:
%: ^bij-down
%:
%: T:\catB(C,-)→\catA(A,R-)
%: ========================
%: γ:A→RC
%:
%: ^bij-up
%:
$$\pu
\diag{Basic-Example}
\qquad
\begin{array}{c}
\ded{bij-down}
\\ \\
\ded{bij-up}
\end{array}
$$
% (find-idarctpage 8 "(Figure 4B)")
% _____ _
% | ___| __ ___ _ _ __| |
% | |_ | '__/ _ \ | | |/ _` |
% | _|| | | __/ |_| | (_| |
% |_| |_| \___|\__, |\__,_|
% |___/
%
% «freyd» (to ".freyd")
% (favp 14 "freyd")
% (fava "freyd")
\section{Freyd's diagrammatic language \DONE}
\label{freyd-notation}
In \cite{Freyd76} Peter Freyd presents a very nice diagrammatic
language that can be used to express {\sl some} definitions from
Category Theory. For example, this is the statement that a category
has all equalizers:
%
%L forths["-"] = function () pusharrow("-") end
%
%D diagram cat-has-equalizers
%D 2Dx 100 +00 +15 +20 +15 +15 +20 +20 +15 +15 +20 +20 +15 +15 +20 +20
%D 2D 100 U0 U1 U2 U3
%D 2D | | | |
%D 2D +10 | A0 | B0 | C0 | D0
%D 2D | | \ | | \ | | \ | | \
%D 2D +20 | A1 -- A2 == A3 | B1 -- B2 == B3 | C1 -- C2 == C3 | D1 -- D2 == D3
%D 2D | | | |
%D 2D +20 L0 L1 L2 L3
%D 2D
%D ren U0 L0 A0 A1 A2 A3 ==> ∀ {} X E A B
%D ren U1 L1 B0 B1 B2 B3 ==> ∃ {} X E A B
%D ren U2 L2 C0 C1 C2 C3 ==> ∀ {} X E A B
%D ren U3 L3 D0 D1 D2 D3 ==> ∃! {} X E A B
%D
%D (( U0 L0 -
%D A2 A3 -> sl^^ .plabel= a f
%D A2 A3 -> sl__ .plabel= b g
%D A2 A3 midpoint .TeX= \scriptstyle? place
%D ))
%D (( U1 L1 -
%D B2 B3 -> sl^^ .plabel= a f
%D B2 B3 -> sl__ .plabel= b g
%D B2 B3 midpoint .TeX= \scriptstyle? place
%D B1 B2 -> .plabel= b e
%D ))
%D (( U2 L2 -
%D C2 C3 -> sl^^ .plabel= a f
%D C2 C3 -> sl__ .plabel= b g
%D C2 C3 midpoint .TeX= \scriptstyle? place
%D C1 C2 -> .plabel= b e
%D C0 C2 -> .plabel= r h
%D ))
%D (( U3 L3 -
%D D2 D3 -> sl^^ .plabel= a f
%D D2 D3 -> sl__ .plabel= b g
%D D2 D3 midpoint .TeX= \scriptstyle? place
%D D1 D2 -> .plabel= b e
%D D0 D2 -> .plabel= r h
%D D0 D1 -> .plabel= l k
%D ))
%D enddiagram
%D
$$\pu
\scalebox{0.8}{$
\diag{cat-has-equalizers}
$}
$$
All cells in these diagrams commute by default, and non-commuting
cells have to be indicated with a `?'. Each vertical bar with a `$∀$'
above it means ``for all extensions of the previous diagram to this
one such that everything commutes''; a vertical bar with a `$∃!$'
above it means ``there exists a unique extension of the previous
diagram to this one such that everything commutes'', and so on. See
the scan in \cite{Freyd76} for the basic details of how to formalize
these diagrams, and the book \cite[p.28 onwards]{FreydScedrov}, for
tons of extra details, examples, and applications.
Let's call the subdiagrams of a diagram like the one above its
``stages''. Its stage 0 is empty, its stage 1 has two objects and two
arrows, its last stage has four objects and five arrows, and the
quantifiers separating the stages are $Q_1=∀$, $Q_2=∃$, $Q_3=∀$,
$Q_4=∃!$. They are structured like this:
%
%D diagram freyd-stages-1
%D 2Dx 100 +20 +20 +20 +20 +20 +20 +20 +20
%D 2D 100 SQ0 SQ1 SQ2 SQ3 SQ4
%D 2D
%D 2D 100 U0 U1 U2 U3
%D 2D
%D 2D +20 S0 S1 S2 S3 S4
%D 2D
%D 2D +20 L0 L1 L2 L3
%D 2D
%D ren U0 L0 ==> Q_1 {}
%D ren U1 L1 ==> Q_2 {}
%D ren U2 L2 ==> Q_3 {}
%D ren U3 L3 ==> Q_4 {}
%D ren S0 S1 S2 S3 S4 ==> S_0 S_1 S_2 S_3 S_4
%D ren SQ0 SQ1 SQ2 SQ3 SQ4 ==> SQ_0 SQ_1 SQ_2 SQ_3 SQ_4
%D
%D (( S0 place S1 place S2 place S3 place S4 place
%D U0 L0 -
%D U1 L1 -
%D U2 L2 -
%D U3 L3 -
%D ))
%D enddiagram
%D
%D diagram freyd-stages-2
%D 2Dx 100 +20 +20 +20 +20 +20 +20 +20 +20
%D 2D 100 SQ0 SQ1 SQ2 SQ3 SQ4
%D 2D
%D 2D +20 U0 U1 U2 U3
%D 2D
%D 2D +20 S0 S1 S2 S3 S4
%D 2D
%D 2D +20 L0 L1 L2 L3
%D 2D
%D ren U0 L0 ==> Q_1 {}
%D ren U1 L1 ==> Q_2 {}
%D ren U2 L2 ==> Q_3 {}
%D ren U3 L3 ==> Q_4 {}
%D ren S0 S1 S2 S3 S4 ==> S_0 S_1 S_2 S_3 S_4
%D ren SQ0 SQ1 SQ2 SQ3 SQ4 ==> SQ_0 SQ_1 SQ_2 SQ_3 SQ_4
%D
%D (( # SQ0 S0 .>
%D # SQ1 S1 .>
%D # SQ2 S2 .>
%D # SQ3 S3 .>
%D # SQ4 S4 .>
%D SQ0 SQ1 <--
%D SQ1 SQ2 <--
%D SQ2 SQ3 <--
%D SQ3 SQ4 <--
%D # U0 L0 -
%D # U1 L1 -
%D # U2 L2 -
%D # U3 L3 -
%D ))
%D enddiagram
%D
\pu
$$
\diag{freyd-stages-1}
$$
%$$\pu
% \diag{freyd-stages-2}
%$$
I was not very good at drawing all stages separately --- it was
boring, it took me too long, and I often got distracted and committed
errors --- so I started to play with extensions of that diagrammatic
language.
% _____ _ _ _ _ ___
% | ___| __ ___ _ _ __| | __ _(_) |_| |__ / _ \ ___
% | |_ | '__/ _ \ | | |/ _` | \ \ /\ / / | __| '_ \ | | | / __|
% | _|| | | __/ |_| | (_| | \ V V /| | |_| | | | | |_| \__ \
% |_| |_| \___|\__, |\__,_| \_/\_/ |_|\__|_| |_| \__\_\___/
% |___/
%
% «freyd-with-quantifiers» (to ".freyd-with-quantifiers")
% (favp 13 "freyd-with-quantifiers")
% (fava "freyd-with-quantifiers")
\subsection{Adding quantifiers \DONE}
\label{freyd-with-quantifiers}
Here is a simple way to draw all stages at once. We start from a
diagram for the ``last stage with quantifiers'', that we will call
$LSQ$:
%
%D diagram cat-has-equalizers-with-quants
%D 2Dx 100 +30 +30
%D 2D 100 D0
%D 2D | \
%D 2D +30 D1 -- D2 == D3
%D 2D
%D ren D0 D1 D2 D3 ==> ∀_3X ∃_2E ∀_1A ∀_1B
%D
%D (( D2 D3 -> sl^^ .plabel= a ∀_1f
%D D2 D3 -> sl__ .plabel= b ∀_1g
%D D2 D3 midpoint .TeX= \scriptstyle? place
%D D1 D2 -> .plabel= b ∃_2e
%D D0 D2 -> .plabel= r ∀_3h
%D D0 D1 -> .plabel= l ∃!_4k
%D ))
%D enddiagram
%D
$$\pu
\scalebox{1.75}{$
\diag{cat-has-equalizers-with-quants}
$}
$$
We can recover all the stages and quantifiers from it. The numbered
quantifiers in it are $∀_1$, $∃_2$, $∀_3$, and $∃!_4$. The highest
number in them 4, so we set $n=4$ ($n$ is the index of the last
stage), and we set ``stage 4 with quantifiers'', $SQ_4$, to $LSQ$. To
obtain the $SQ_3$ from $SQ_4$ we delete all nodes an arrows in $SQ_4$
that are annotated with a `$∃!_4$'; to obtain $SQ_2$ from $SQ_3$ we
delete all nodes an arrows in $SQ_3$ that are annotated with a
`$∀_3$', and so on until we get a diagram $SQ_0$, that in this example
is empty. To obtain each $S_k$ --- a stage in the original
diagrammatic language from Freyd, that doesn't have quantifiers ---
from the corresponding $SQ_k$ we treat all the quantifiers in $SQ_k$
as mere annotations, and we erase them; for example, `$∃_2e$' becomes
`$e$', and $∀_1A$ becomes $A$. To obtain the quantifiers $Q_1$, $Q_2$,
$Q_3$, $Q_4$ that are put in the vartical bars that separate the
stages, we just assign $∀_1$, $∃_2$, $∀_3$, and $∃!_4$ to them,
without the numbers in the subscripts.
Bonus convention: when the quantifiers in a diagram are just `$∀$'s
and `$∃!$'s without subscripts the `$∀$'s are to be interpreted as
`$∀_1$' and the `$∃!$'s as `$∃!_2$'s.
% _____ _ _ _ _ _____
% | ___| __ ___ _ _ __| | __ _(_) |_| |__ | ___|__
% | |_ | '__/ _ \ | | |/ _` | \ \ /\ / / | __| '_ \ | |_ / __|
% | _|| | | __/ |_| | (_| | \ V V /| | |_| | | | | _|\__ \
% |_| |_| \___|\__, |\__,_| \_/\_/ |_|\__|_| |_| |_| |___/
% |___/
%
% «freyd-with-functors» (to ".freyd-with-functors")
% (favp 16 "freyd-with-functors")
% (fava "freyd-with-functors")
\subsection{Adding functors \DONE}
\label{freyd-with-functors}
Freyd's language can't represent functors\footnote{As far as I know
--- I don't know \cite{FreydScedrov} very well.}, and I wanted to
use it to draw the missing diagrams for definitions involving
functors, so I had to extend it again.
Let me use an example to discuss this. This is the definition of
universal arrow in \cite[p.55]{CWM2}, including the original diagram,
modulo change of letters:
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 13 55) "1. Universal Arrows")
%
%D diagram univ-arrow-cwm-my-letters
%D 2Dx 100 +25 +25
%D 2D 100 A0 A1 A2
%D 2D
%D 2D +25 A3 A4 A5
%D 2D
%D ren A0 A1 A2 ==> A RB B
%D ren A3 A4 A5 ==> A RB', B'.
%D
%D (( A0 A1 -> .plabel= a η
%D A0 A3 midpoint .TeX= \veq place
%D A1 A4 .> .plabel= r Rf
%D A2 A5 .> .plabel= r f
%D A3 A4 -> .plabel= a g
%D ))
%D enddiagram
\begin{quotation}
{\bf Definition.} If $R: \catB→\catA$ is a functor and $A$ an object
of $\catA$, a universal arrow from $A$ to $R$ is a pair $(B,η)$
consisting of an object $B$ of $\catB$ and and arrow $η:A→RB$ of
$\catA$ such that to every pair $(B',g)$ with $B'$ an object of
$\catB$ and $g:A→RB'$ an arrow of $\catA$, there is a unique arrow
$f:B→B'$ of $\catB$ with $Rf∘η=g$. In other words, every arrow $h$
to $R$ factors uniquely through the universal arrow $η$, as in the
commutative diagram:
%
$$\pu
\diag{univ-arrow-cwm-my-letters}
$$
\end{quotation}
The definition itself goes only up to the ``with $Rf∘η=g$.'', so let
me ignore the part starting from ``In other words'', and draw a better
``missing diagram'' for the definition:
%
%D diagram universal-arrow-stages
%D 2Dx 100 +20 +20 +20 +20 +20 +20 +20
%D 2D 100 U0 U1
%D 2D
%D 2D +10 A1 B1 C1
%D 2D | | |
%D 2D +20 A2 A3 B2 B3 C2 C3
%D 2D | | | | | |
%D 2D +20 A4 A5 B4 B5 C4 C5
%D 2D
%D 2D +15 A6 A7 B6 B7 C6 C7
%D 2D
%D 2D +10 L0 L1
%D 2D
%D ren A1 A2 A3 A4 A5 A6 A7 ==> A B RB B' RB' \catB \catA
%D ren B1 B2 B3 B4 B5 B6 B7 ==> A B RB B' RB' \catB \catA
%D ren C1 C2 C3 C4 C5 C6 C7 ==> A B RB B' RB' \catB \catA
%D ren U0 L0 ==> ∀ {}
%D ren U1 L1 ==> ∃! {}
%D
%D (( A1 A3 -> .plabel= r η
%D A2 A3 |->
%D A6 A7 -> .plabel= a R
%D U0 L0 -
%D ))
%D (( B1 B3 -> .plabel= r η
%D B2 B3 |->
%D B4 B5 |->
%D B1 B5 -> .slide= 15pt .plabel= r g
%D B6 B7 -> .plabel= a R
%D U1 L1 -
%D ))
%D (( C1 C3 -> .plabel= r η
%D C2 C3 |->
%D C2 C4 -> .plabel= l f
%D C3 C5 -> .plabel= r Rf
%D C2 C5 harrownodes nil 20 nil |->
%D C4 C5 |->
%D C1 C5 -> .slide= 20pt .plabel= r g
%D C6 C7 -> .plabel= a R
%D ))
%D enddiagram
%D
$$\pu
\diag{universal-arrow-stages}
$$
This diagram is quite close to being a skeleton for the definition of
universal arrow. It can be interpreted as a proposition, and the only
extra hint that we need is that ``universalness'' for the arrow $η$
corresponds to the truth of that proposition. Here's how to extract
the proposition from it:
%
$$\begin{array}{rl}
\text{In a context where:}
& \catA \text{ is a category}, \\
& \catB \text{ is a category}, \\
& R:\catB \to \catA, \\
& A ∈ \catA, \\
& B ∈ \catB, \\
& η:A→RB, \\
\text{for all}
& B'∈\catB \text{ and} \\
& g:A→RB', \\
\text{there exists a unique}
& f:B→B' \text { such that} \\
& Rf∘η=g. \\
\end{array}
$$
To convert that to a definition of universalness we just have to
replace the ``for all'' by ``$(B,η)$ is a universal arrow for $A$ to
$R$ iff for all''.
The convention for quantifiers from sec.\ref{freyd-with-quantifiers}
lets us rewrite the diagram in three stages above as:
%
%D diagram universal-arrow-quants
%D 2Dx 100 +20
%D 2D 100 C1
%D 2D |
%D 2D +20 C2 C3
%D 2D | |
%D 2D +20 C4 C5
%D 2D
%D 2D +15 C6 C7
%D 2D
%D ren C1 C2 C3 C4 C5 C6 C7 ==> A B RB ∀B' RB' \catB \catA
%D
%D (( C1 C3 -> .plabel= r η
%D C2 C3 |->
%D C2 C4 -> .plabel= l ∃!f
%D C3 C5 -> .plabel= r Rf
%D C2 C5 harrownodes nil 20 nil |->
%D C4 C5 |->
%D C1 C5 -> .slide= 20pt .plabel= r ∀g
%D C6 C7 -> .plabel= a R
%D ))
%D enddiagram
%D
$$\pu
\scalebox{1.5}{$
\diag{universal-arrow-quants}
$}
$$
Also, I noticed that I could omit most typings when they could be
inferred from the diagram. I could ``formalize'' the diagram above as:
``in a context where $(\catA, \catB, R, A, B, η)$ are as in the
diagram above, we say that $(B,η)$ is a universal arrow from $A$ to
$R$ when $∀(B',g).∃!f.(Rf∘η=g)$''. This may be too loaded to be used
in public, but it's very practical for private notes --- and I can
even omit the ``$Rf∘η=g$'', as everything commutes by default.
\bsk
Note that when we erase a node or arrow we also erase everything that
depends on it. In the example above $SQ_2$ has an arrow labeled
$∃!_2f$; to obtain $SQ_1$ from $SQ_2$ we have to erase that arrow, the
arrow $Rf$, and the arrow $f \mapsto Rf$ --- and to obtain $SQ_0$ from
$SQ_1$ we have to erase the arrow $g$, the node $B'$, the node $RB'$,
and the arrow $B' \mapsto RB'$.
% (find-books "__comp/__comp.el" "penrose")
% ___ _ _ _
% |_ _|_ __ | |_ ___ _ __ _ __ __ _| | __ _(_) _____ _____
% | || '_ \| __/ _ \ '__| '_ \ / _` | | \ \ / / |/ _ \ \ /\ / / __|
% | || | | | || __/ | | | | | (_| | | \ V /| | __/\ V V /\__ \
% |___|_| |_|\__\___|_| |_| |_|\__,_|_| \_/ |_|\___| \_/\_/ |___/
%
% «internal-views» (to ".internal-views")
% (favp 19 "internal-views")
% (fava "internal-views")
\section{Internal views \DONE}
\label{internal-views}
My favorite way of introducing internal views is with the diagram
below:
%
% (nyop 19 "blob-sets")
% (nyo "blob-sets")
% (nyop 20 "blob-sets-2")
% (nyo "blob-sets-2")
% (nyop 21 "blob-cats-and-functors")
% (nyo "blob-cats-and-functors")
%
\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)}}
%
%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
$$\begin{array}{rrcl}
\sqrt{\;\;}: & \N &→& \R \\
& n &↦& \sqrt{n} \\
\end{array}
\qquad
\diag{second-blob-function}
$$
\def\longmapsto{\diagxyto/|->/}
The parts with the two blobs and `$\longmapsto$'s between them is
based on how I was taught sets and functions when I was a kid; it is
an internal view of the $\N \ton{\sqrt{\phantom{a}}} \R$ below it. Not
all elements of $\N$ are shown in the blob-view of $\N$, but the ones
that are shown are named; compare this with \cite[p.2
onwards]{LawvereRosebrugh}, in which the elements are usually dots.
The arrow $n \longmapsto \sqrt{n}$ between the blobs shows a {\sl
generic element} of $\N$ and its image, and the other
`$\longmapsto$'s are {\sl substitution instances of it}, like this:
%
$$(n \longmapsto \sqrt{n}) [n:=2] = (2 \longmapsto \sqrt{2})$$
In some cases, like $4 \longmapsto 2$, we write 2 instead of
$\sqrt{4}$ because $\sqrt{4}$ ``reduces to'' 2, as explained in the
next section.
% ____ _ _ _
% | _ \ ___ __| |_ _ ___| |_(_) ___ _ __ ___
% | |_) / _ \/ _` | | | |/ __| __| |/ _ \| '_ \/ __|
% | _ < __/ (_| | |_| | (__| |_| | (_) | | | \__ \
% |_| \_\___|\__,_|\__,_|\___|\__|_|\___/|_| |_|___/
%
% «reductions» (to ".reductions")
% (favp 19 "reductions")
% (fava "reductions")
\subsection{Reductions \DONE}
\label{reductions}
\def\squigton#1{\overset{#1}{\squigto}}
The convention (C$\mapsto$) says that an arrow $α \mapsto β$ above an
arrow $A \ton{f} B$ should be interpreted as meaning $f(α) \squigto
β$, where `$\squigto$' means ``reduces to''; the standard example is
$\sqrt{4} \squigto 2$. In a diagram:
%
%D diagram reductions-0
%D 2Dx 100 +20 +25 +40 +20 +25
%D 2D 100 A0 A1 B0
%D 2D +8 A2 A3 C0 C1 E0
%D 2D
%D 2D +15 A4 A5 C2 C3
%D 2D
%D ren A0 A1 ==> 4 2
%D ren A2 A3 ==> n \sqrt{n}
%D ren A4 A5 ==> \N \R
%D ren B0 ==> \sqrt{4}\squigto2
%D ren C0 C1 ==> α β
%D ren C2 C3 ==> A B
%D ren E0 ==> f(α)\squigtoβ
%D
%D (( A0 A1 |->
%D A2 A3 |->
%D A4 A5 -> .plabel= a \sqrt{\phantom{a}}
%D B0 place
%D C0 C1 |->
%D C2 C3 -> .plabel= a f
%D E0 place
%D ))
%D enddiagram
%D
$$\pu
\diag{reductions-0}
$$
The idea of reduction comes from $λ$-calculus. We write $α
\squigton{1} β$ to say that the term $α$ reduces to $β$ in one step,
and $α \squigton{*} γ$ to say that there is a finite sequence of
one-step reductions that reduce $α$ to $γ$. Here we are interested in
reduction in a system with constants, in which for example
$(\sqrt{\phantom{a}})(4) \squigton{1} 2$.
Here is a directed graph that shows all the one-step reductions
starting from $g(2+3)$, considering $g(a) = a·a+4$:
%
% (lam181p 5 "lambda")
% (lam181 "lambda")
%
%D diagram reduce-g
%D 2Dx 100 +30 +30 +40 +30
%D 2D 100 A ----> B
%D 2D | |
%D 2D v v
%D 2D +25 E |
%D 2D | \ |
%D 2D | v |
%D 2D +20 | F |
%D 2D | \ |
%D 2D v v v
%D 2D +20 G ----> H -> I -> J
%D 2D
%D ren A B ==> g(2+3) g(5)
%D ren E F ==> (2+3)·(2+3)+4 (2+3)·5+4
%D ren G H ==> 5·(2+3)+4 5·5+4
%D ren I J ==> 25+4 29
%D (( A B -> E F -> F H -> G H ->
%D A E -> E G -> B H -> H I -> I J ->
%D ))
%D enddiagram
%D
$$\pu
\diag{reduce-g}
$$
Note that all reductions sequences starting from $g(2+3)$ terminate at
the same term, 29 --- ``the term $g(2+3)$ is strongly normalizing''
---, and reduction sequences from $g(2+3)$ may ``diverge'' but they
``converge'' later --- this is the ``Church-Rosser Property'', a.k.a.
``confluence''.
A good place to learn about reduction in systems with constants is
\cite{SICP}.
% https://en.wikipedia.org/wiki/Confluence_(abstract_rewriting)
% (find-books "__comp/__comp.el" "abelson-sussman")
% (find-sicppage (+ 28 42) "Figure 1.3: A linear recursive process for computing 6!")
% (find-sicptext (+ 28 42) "Figure 1.3: A linear recursive process for computing 6!")
% (find-es "scheme" "sicp-pdf")
% (find-pdf-page "~/usrc/sicp-pdf/src/fig/chap1/Fig1.3c.pdf")
% \begin{center}
% \includegraphics[height=144pt]{2020favorite-conventions-frob.pdf}
% \end{center}
% _____ _
% | ___| _ _ __ ___| |_ ___ _ __ ___
% | |_ | | | | '_ \ / __| __/ _ \| '__/ __|
% | _|| |_| | | | | (__| || (_) | | \__ \
% |_| \__,_|_| |_|\___|\__\___/|_| |___/
%
% «internal-view-functor» (to ".internal-view-functor")
% (favp 20 "internal-view-functor")
% (fava "internal-view-functor")
\subsection{Functors \DONE}
\label{internal-view-functor}
% (nyop 21 "blob-cats-and-functors")
% (nyo "blob-cats-and-functors")
% (nyop 25 "convention-functors")
% (nyo "convention-functors")
By the convention (CFSh) the image of the diagram above $\catA$ in the
diagram below --- remember that {\sl above} usually means {\sl inside}
---
%
%D diagram internal-view-functor-0
%D 2Dx 100 +10 +10 +25 +12 +12
%D 2D 100 A1 ____ B1 ____
%D 2D +10 | ____ A3 | ____ B3
%D 2D +10 A2 ____ | B2 ____ |
%D 2D +10 A4 B4
%D 2D
%D 2D +15 \catA ------> \catB
%D 2D
%D ren A1 A2 A3 A4 ==> A_1 A_2 A_3 A_4
%D
%D (( A1 A2 -> .plabel= l f
%D A2 A3 -> .plabel= m g
%D A3 A4 -> .plabel= r h
%D A1 A3 -> .plabel= a k
%D A2 A4 -> .plabel= b m
%D \catA \catB -> .plabel= a F
%D ))
%D enddiagram
%D
$$\pu
\diag{internal-view-functor-0}
$$
%
is a diagram with the same shape over $\catB$. We draw it like this:
%
%D diagram internal-view-functor-1
%D 2Dx 100 +10 +10 +25 +14 +14
%D 2D 100 A1 ____ B1 ____
%D 2D +10 | ____ A3 | ____ B3
%D 2D +10 A2 ____ | B2 ____ |
%D 2D +10 A4 B4
%D 2D
%D 2D +15 \catA ------> \catB
%D 2D
%D ren A1 A2 A3 A4 ==> A_1 A_2 A_3 A_4
%D ren B1 B2 B3 B4 ==> FA_1 FA_2 FA_3 FA_4
%D
%D (( A1 A2 -> .plabel= l f
%D A2 A3 -> .plabel= m g
%D A3 A4 -> .plabel= r h
%D A1 A3 -> .plabel= a k
%D A2 A4 -> .plabel= b m
%D \catA \catB -> .plabel= a F
%D
%D B1 B2 -> .plabel= l Ff
%D B2 B3 -> .plabel= m Fg
%D B3 B4 -> .plabel= r Fh
%D B1 B3 -> .plabel= a Fk
%D B2 B4 -> .plabel= b Fm
%D ))
%D enddiagram
%D
$$\pu
\diag{internal-view-functor-1}
$$
In this case we don't draw the arrows like $A_1 \mapsto FA_1$ because
there would be too many of them --- we leave them implicit.
We say that the diagram above is {\sl an} internal view of the functor
$F$. To draw {\sl the} internal view of the functor $F: \catA → \catB$
we start with a diagram in $\catA$ that is made of two generic objects
and a generic morphism between them. We get this:
%D diagram internal-view-functor-2
%D 2Dx 100 +20
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +15 B0 B1
%D 2D
%D ren A0 A1 A2 A3 B0 B1 ==> C FC D FD \catA \catB
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l g
%D A1 A3 -> .plabel= r Fg
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil |->
%D B0 B1 -> .plabel= a F
%D ))
%D enddiagram
%D
$$\pu
\diag{internal-view-functor-2}
$$
Compare this with the diagram with blob-sets in Section
\ref{internal-views}, in which the `$n \mapsto \sqrt{n}$' says where a
generic element is taken.
Any arrow of the form $α \mapsto β$ above a functor arrow $\catA
\ton{F} \catB$ is interpreted as saying that $F$ takes $α$ to $β$, or,
in the terminology of the section \ref{reductions}, that $Fα$ reduces
to $β$. So this diagram
%
%D diagram internal-view-functor-3
%D 2Dx 100 +25
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +15 B0 B1
%D 2D
%D ren A0 A1 A2 A3 B0 B1 ==> B A{×}B C A{×}C \Set \Set
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l f
%D A1 A3 -> .plabel= r λp.(πp,f(π'p))
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil |->
%D B0 B1 -> .plabel= a (A{×})
%D ))
%D enddiagram
%D
$$\pu
\diag{internal-view-functor-3}
$$
%
defines $(A×)$ as:
%
$$\begin{array}{rcl}
(A×)_0 &:=& λB.\,A×B,\\
(A×)_1 &:=& λf.λp.(πp,f(π'p)).\\
\end{array}
$$
In this case we can also use internal views of $(A×)$ to define
$(A×)_1$:
%
%D diagram internal-view-functor-4
%D 2Dx 100 +25 +30 +35
%D 2D 100 A0 A1 C0 D0
%D 2D
%D 2D +20 A2 A3 C1 D1
%D 2D
%D 2D +15 B0 B1
%D 2D
%D ren A0 A1 A2 A3 B0 B1 ==> B A{×}B C A{×}C \Set \Set
%D ren C0 C1 ==> (a,b) (a,f(b))
%D ren D0 D1 ==> p (πp,f(π'p))
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l f
%D A1 A3 -> .plabel= r (A{×})f
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil |->
%D B0 B1 -> .plabel= a (A{×})
%D C0 C1 |->
%D D0 D1 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{internal-view-functor-4}
$$
% _ _ _____
% | \ | |_ _|__
% | \| | | |/ __|
% | |\ | | |\__ \
% |_| \_| |_||___/
%
% «internal-view-NT» (to ".internal-view-NT")
% (favp 22 "internal-view-NT")
% (fava "internal-view-NT")
\subsection{Natural transformations \DONE}
\label{internal-view-NT}
% (nyop 33 "convention-NTs")
% (nyo "convention-NTs")
% (nyop 34 "convention-NTs-2")
% (nyo "convention-NTs-2")
Suppose that we have two functors $F,G:\catA → \catB$ and a natural
transformation $T:F→G$. A first way to draw an internal view of $T$ is
this:
%
%D diagram internal-view-NT-0
%D 2Dx 100 +25
%D 2D 100 A1
%D 2D +10 A0
%D 2D +10 A2
%D 2D
%D 2D +15 B0 B1
%D 2D
%D ren A0 A1 A2 B0 B1 ==> C FC GC \catA \catB
%D
%D (( A0 A1 |->
%D A0 A2 |->
%D A1 A2 -> .plabel= r TC
%D A0 A1 A2 midpoint |->
%D B0 B1 -> sl^ .plabel= a F
%D B0 B1 -> sl_ .plabel= b G
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{internal-view-NT-0}
$$
If we start with a morphism $h:C→D$ in $\catA$, like this,
%
%D diagram NT-00
%D 2Dx 100 +25
%D 2D 100 A0
%D 2D +20 A1
%D 2D +15 D0 D1
%D 2D
%D ren A0 A1 ==> C D
%D ren D0 D1 ==> \catA \catB
%D
%D (( A0 A1 -> .plabel= l h
%D D0 D1 -> sl^ .plabel= a F
%D D0 D1 -> sl_ .plabel= b G
%D ))
%D enddiagram
%
$$\pu
\diag{NT-00}
$$
%
the convention (CFSh) would yield an image of $h$ by $F$ and another
by $G$, and we can draw the arrows $TC$ and $TD$ to obtain a commuting
square in $\catB$:
%
%D diagram NT-0
%D 2Dx 100 +20 +15 +15
%D 2D 100 A0
%D 2D +15 B0 B1
%D 2D +15 A1
%D 2D +15 B2 B3
%D 2D
%D 2D +15 C0 C1
%D 2D
%D 2D +15 D0 D1
%D 2D
%D ren A0 A1 ==> C D
%D ren B0 B1 B2 B3 ==> FC GC FD GD
%D ren C0 C1 ==> F G
%D ren D0 D1 ==> \catA \catB
%D
%D (( A0 B0 |->
%D A0 B1 |->
%D A1 B2 |->
%D A1 B3 |->
%D
%D A0 A1 -> .plabel= l h
%D B0 B1 -> .plabel= b TC
%D B0 B2 -> .plabel= r Fh
%D B1 B3 -> .plabel= r Gh
%D B2 B3 -> .plabel= b TD
%D C0 C1 -> .plabel= a T
%D D0 D1 -> sl^ .plabel= a F
%D D0 D1 -> sl_ .plabel= b G
%D ))
%D enddiagram
%
$$\pu
\diag{NT-0}
$$
This way of drawing internal views of natural transformations yields
diagrams that are too heavy, so we will usually draw them as just
this:
%
%D diagram NT-1
%D 2Dx 100 +20 +25
%D 2D 100 A0 B0 B1
%D 2D
%D 2D +25 A1 B2 B3
%D 2D +15 C0 C1
%D 2D
%D ren A0 A1 ==> C D
%D ren B0 B1 B2 B3 ==> FC GC FD GD
%D ren C0 C1 ==> F G
%D
%D (( A0 A1 -> .plabel= l h
%D B0 B1 -> .plabel= a TC
%D B0 B2 -> .plabel= l Fh
%D B1 B3 -> .plabel= r Gh
%D B2 B3 -> .plabel= b TD
%D C0 C1 -> .plabel= a T
%D ))
%D enddiagram
%
$$\pu
\diag{NT-1}
$$
%
Note that the input morphism is at the left, and above $F \ton{T} G$
we draw its images by $F$, $G$, and $T$.
When the codomain of $F$ and $G$ is $\Set$ we will sometimes also draw
at the right an internal view of the commuting square, like this:
%
%D diagram NT-2
%D 2Dx 100 +20 +30 +25 +45
%D 2D 100 A0 B0 B1 D0 D1
%D 2D +22 D3'
%D 2D +8 A1 B2 B3 D2 D3
%D 2D
%D 2D +15 C0 C1
%D 2D
%D ren A0 A1 ==> C D
%D ren B0 B1 B2 B3 ==> FC GC FD GD
%D ren C0 C1 ==> F G
%D ren D0 D1 D3' ==> x (TC)(x) (Gh∘TC)(x)
%D ren D2 D3 ==> (Fh)(x) (TD∘Ff)(x)
%D
%D (( A0 A1 -> .plabel= l h
%D B0 B1 -> .plabel= a TC
%D B0 B2 -> .plabel= l Fh
%D B1 B3 -> .plabel= r Gh
%D B2 B3 -> .plabel= a TD
%D C0 C1 -> .plabel= a T
%D D0 D1 |-> D1 D3' |-> D0 D2 |-> D2 D3 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{NT-2}
$$
%
Then the commutativity of the middle square is equivalent to
$∀x∈FC.(Gh∘TC)(x)=(TD∘Ff)(x)$. Note that in this case the square at
the right is an internal view of an internal view.
In Section \ref{to-deserve-a-name} we saw that a functor has four
components. A natural transformation has two: $T=(T_0, \sqcond_T)$,
where $T_0$ is the operation $C \mapsto TC$ and $\sqcond_T$ is the
guarantee that all the induced squares commute. Sometimes we will use
the upper line of the internal view of the internal view to define
$T_0$ --- see Section \ref{basic-example-NT} for an example of this.
% Tom Leinster has a diagram like my internal view of
% the internal view...
% (find-books "__cats/__cats.el" "leinster-basic")
% (find-leinsterbasicpage (+ 8 86) "Lemma 4.1.10")
% (find-leinsterbasictext (+ 8 86) "Lemma 4.1.10")
% _ _ _ _ _
% / \ __| |(_)_ _ _ __ ___| |_(_) ___ _ __ ___
% / _ \ / _` || | | | | '_ \ / __| __| |/ _ \| '_ \/ __|
% / ___ \ (_| || | |_| | | | | (__| |_| | (_) | | | \__ \
% /_/ \_\__,_|/ |\__,_|_| |_|\___|\__|_|\___/|_| |_|___/
% |__/
%
% «internal-view-adjunction» (to ".internal-view-adjunction")
% (favp 24 "internal-view-adjunction")
% (fava "internal-view-adjunction")
\subsection{Adjunctions \DONE}
\label{internal-view-adjunction}
% (nyop 35 "convention-adjs")
% (nyo "convention-adjs")
We will draw adjunctions like this,
%
%D diagram generic-adjunction
%D 2Dx 100 +25
%D 2D 100 LB <-| B
%D 2D | |
%D 2D v v
%D 2D +20 C |--> RC
%D 2D
%D 2D +15 E <==> F
%D 2D
%D ren LB B ==> LA A
%D ren C RC ==> B RB
%D ren E F ==> \catB \catA
%D
%D (( LB B <-| # .plabel= a L_0
%D C RC |-> # .plabel= b R_0
%D
%D LB RC harrownodes nil 20 nil <->
%D
%D LB C -> # .plabel= l \sm{g^♭\\f}
%D B RC -> # .plabel= r \sm{g\\f^♯}
%D E F <- sl^ .plabel= a L
%D E F -> sl_ .plabel= b R
%D ))
%D enddiagram
%D
$$\pu
\diag{generic-adjunction}
$$
%
with the left adjoint going left and the right adjoint going right. My
favorite names for the left and right adjoints are $L$ and $R$. The
standard notation for that adjunction is $L⊣R$.
The top-level component of the diagram above is the bijection arrow in
the middle of the square --- it says that $\Hom(LA,B) ↔ \Hom(A,RB)$.
It is implicit that we have bijections like that for all $A$ and $B$;
it is also implicit that that bijection is natural in some sense.
We will sometimes expand adjunction diagrams by adding unit and counit
maps, the unit and the unit as natural transformations, the actions of
$L$ and $R$ on morphisms, and other things. For example:
%
%D diagram generic-adjunction-with-with
%D 2Dx 100 +20 +20 +20 +20 +20
%D 2D 100 D0 D1
%D 2D +20 B0 C0 D2 D3 E0 F0
%D 2D +20 B1 C1 D4 D5 E1 F1
%D 2D +20 D6 D7
%D 2D +20 H0 H1
%D 2D
%D ren D0 D1 ==> LA' A'
%D ren B0 C0 D2 D3 E0 F0 ==> LR LRB LA A A \id_\catA
%D ren B1 C1 D4 D5 E1 F1 ==> \id_\catB B B RB RLA LR
%D ren D6 D7 ==> B' RB'
%D ren H0 H1 ==> \catB \catA
%D
%D (( B0 B1 -> .plabel= l ε
%D C0 C1 -> .plabel= l ε_B
%D
%D D0 D1 <-|
%D D0 D2 -> .plabel= l Lf
%D D1 D3 -> .plabel= r f
%D D0 D3 harrownodes nil 20 nil <-|
%D D2 D3 <-|
%D D2 D4 -> .plabel= l \sm{h^♭\\g}
%D D3 D5 -> .plabel= r \sm{h\\g^♯}
%D D2 D5 harrownodes nil 20 nil <-| sl^
%D D2 D5 harrownodes nil 20 nil |-> sl_
%D D4 D5 |->
%D D4 D6 -> .plabel= l k
%D D5 D7 -> .plabel= r Rk
%D D6 D7 |->
%D D4 D7 harrownodes nil 20 nil |->
%D
%D E0 E1 -> .plabel= r η_A
%D F0 F1 -> .plabel= r η
%D
%D H0 H1 <- sl^ .plabel= a L
%D H0 H1 -> sl_ .plabel= b R
%D ))
%D enddiagram
%D
$$\pu
\diag{generic-adjunction-with-with}
$$
We can obtain the naturality conditions by regarding $♭$ and $♯$ as
natural transformations and drawing the internal views of their
internal views:
%
%D diagram adj-nat-conditions
%D 2Dx 100 +40 +50 +45 +45
%D 2D 100 A0 B0 - B1 D0 - D1
%D 2D | | | | |
%D 2D +17 | | | D2' |
%D 2D +8 A1 B2 - B3 D2 - D3
%D 2D
%D 2D +15 A2 C0 = C1
%D 2D
%D 2D +20 E0 F0 - F1 H0 - H1
%D 2D | | | | |
%D 2D +17 | | | | H3'
%D 2D +8 E1 F2 - F3 H2 - H3
%D 2D
%D 2D +15 E2 G0 = G1
%D 2D
%D ren A0 A1 A2 ==> (A,B) (A',B') \catA^\op{×}\catB
%D ren B0 B1 D0 D1 ==> \Hom(LA,B) \Hom(A,RB) h^♭ h
%D ren D2' ==> k∘h^♭∘Lf
%D ren B2 B3 D2 D3 ==> \Hom(LA',B') \Hom(A,RB) (Rk∘h∘f)^♭ Rk∘h∘f
%D ren C0 C1 ==> \Hom(L-,-) \Hom(-,R-)
%D
%D ren E0 E1 E2 ==> (A,B) (A',B') \catA^\op{×}\catB
%D ren F0 F1 H0 H1 ==> \Hom(LA,B) \Hom(A,RB) g g^♯
%D ren H3' ==> Rk∘g^♯∘f
%D ren F2 F3 H2 H3 ==> \Hom(LA',B') \Hom(A,RB) k∘g∘Lf (k∘g∘Lf)^♯
%D ren G0 G1 ==> \Hom(L-,-) \Hom(-,R-)
%D
%D (( A0 A1 -> .plabel= l (f^\op,g)
%D # A2 place
%D B0 B1 <-
%D B0 B2 ->
%D B1 B3 ->
%D B2 B3 <-
%D C0 C1 <- .plabel= a ♭
%D D0 D1 <-|
%D D0 D2' |->
%D D1 D3 |->
%D D2 D3 <-|
%D
%D E0 E1 -> .plabel= l (f^\op,g)
%D # E2 place
%D F0 F1 ->
%D F0 F2 ->
%D F1 F3 ->
%D F2 F3 ->
%D G0 G1 -> .plabel= a ♯
%D H0 H1 |-> H1 H3' |->
%D H0 H2 |-> H2 H3 |->
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{adj-nat-conditions}
$$
% _____ _ _ _ _
% |_ _|__ __ _ ___| |__ (_)_ __ __ _ __ _ __| |(_)___
% | |/ _ \/ _` |/ __| '_ \| | '_ \ / _` | / _` |/ _` || / __|
% | | __/ (_| | (__| | | | | | | | (_| | | (_| | (_| || \__ \
% |_|\___|\__,_|\___|_| |_|_|_| |_|\__, | \__,_|\__,_|/ |___/
% |___/ |__/
%
% «teaching-adjunctions» (to ".teaching-adjunctions")
% (favp 25 "teaching-adjunctions")
% (fava "teaching-adjunctions")
\subsection{A way to teach adjunctions \DONE}
\label{teaching-adjunctions}
I mentioned in the first sections that I have tested some parts of
this language in a seminar course --- described here:
\cite{OchsWLD2019} --- and that in it I teach Categories starting by
adjunctions. Here's how: we start by the basics of $λ$-calculus and
some sections of \cite{PH1}, and then I ask the students to define
each one of the operations in the right half of the diagram below as
$λ$-terms:
%
% --- where $(C{→}D) = D^C$:
%
%D diagram generic-adjunction-big
%D 2Dx 100 +20 +25 +20
%D 2D 100 LA <-| A
%D 2D | |
%D 2D v v
%D 2D +20 G LB <-| B I
%D 2D | | | |
%D 2D v v v v
%D 2D +20 H C |--> RC J
%D 2D | |
%D 2D v v
%D 2D +20 D |--> RD
%D 2D
%D 2D +20 E <==> F
%D 2D
%D ren LA A ==> LA' A'
%D ren LB B ==> LA A
%D ren C RC ==> B RB
%D ren D RD ==> B' RB'
%D ren E F ==> \catB \catA
%D ren G H ==> LRB B
%D ren I J ==> A RLA
%D
%D (( LA A <-| # .plabel= a L_0
%D LB B <-| # .plabel= a L_0
%D C RC |-> # .plabel= b R_0
%D D RD |-> # .plabel= b R_0
%D
%D LA B harrownodes nil 20 nil <-| # sl^ .plabel= a L_1
%D LB RC harrownodes nil 20 nil <-| sl^ # .plabel= a ♭
%D LB RC harrownodes nil 20 nil |-> sl_ # .plabel= b ♯
%D C RD harrownodes nil 20 nil |-> # sl^ .plabel= b R_1
%D
%D LA LB -> # .plabel= l Lα
%D A B -> # .plabel= r α
%D LB C -> # .plabel= l \sm{g^♭\\f}
%D B RC -> # .plabel= r \sm{g\\f^♯}
%D C D -> # .plabel= l β
%D RC RD -> # .plabel= r Rβ
%D E F <- sl^ .plabel= a L
%D E F -> sl_ .plabel= b R
%D G H -> # .plabel= l εB
%D I J -> # .plabel= r ηA
%D ))
%D enddiagram
%D
%D diagram (xB)-|(B->)
%D 2Dx 100 +30 +25 +35
%D 2D 100 LA <-| A
%D 2D | |
%D 2D v v
%D 2D +20 G LB <-| B I
%D 2D | | | |
%D 2D v v v v
%D 2D +20 H C |--> RC J
%D 2D | |
%D 2D v v
%D 2D +20 D |--> RD
%D 2D
%D 2D +20 E <==> F
%D 2D
%D ren LA A ==> A{×}C A
%D ren LB B ==> B{×}C B
%D ren C RC ==> D (C{→}D)
%D ren D RD ==> E (C{→}E)
%D ren E F ==> \Set \Set
%D ren G H ==> (C{→}D){×C} D
%D ren I J ==> B (C→B{×}C)
%D ren I J ==> B (C{→}(B{×}C))
%D
%D (( LA A <-| # .plabel= a ({×}B)_0
%D LB B <-| # .plabel= a ({×}B)_0
%D C RC |-> # .plabel= b (B{→})_0
%D D RD |-> # .plabel= b (B{→})_0
%D
%D LA B harrownodes nil 20 nil <-| # sl^ .plabel= a L_1
%D LB RC harrownodes nil 20 nil <-| sl^ # .plabel= a ♭
%D LB RC harrownodes nil 20 nil |-> sl_ # .plabel= b ♯
%D C RD harrownodes nil 20 nil |-> # sl^ .plabel= b R_1
%D
%D LA LB -> # .plabel= l λp.(f(πp),π'p)
%D A B -> # .plabel= r f
%D LB C -> # .plabel= l \sm{λp.g(πp)(π'p)\\\phantom{mmmmmm}h}
%D B RC -> # .plabel= r \sm{g\phantom{mmmmm}\\λb.λc.h(b,c)}
%D C D -> # .plabel= l k
%D RC RD -> # .plabel= r λf.λc.k(fc)
%D E F <- sl^ .plabel= a ({×}C)
%D E F -> sl_ .plabel= b (C{→})
%D G H -> # .plabel= l λp.(πp)(π'p)
%D I J -> # .plabel= r λb.λc.(b,c)
%D ))
%D enddiagram
%D
$$
\pu
\diag{generic-adjunction-big}
\qquad
\diag{(xB)-|(B->)}
$$
Then we see the definition of functors, natural transformations and
adjunctions, and we check that the right half is a particular case of
the diagram for a generic adjunction in the left half. After that, and
after also checking that in the Planar Heyting Algebras of \cite{PH1}
we have an adjunction $(∧Q)⊣(Q→)$, I help the students to decypher
some excerpts of standard texts on CT --- in the last time that I gave
the course we used \cite{Awodey}, but I am planning to use \cite{CWM2}
the next time.
\msk
From the components of the generic adjunction in the diagram above it
is possible to build this big diagram:
%
%D diagram teaching-adjunctions-1
%D 2Dx 100 +20 +20 +20 +20 +20 +20 +20 +20
%D 2D 100 A0 A1
%D 2D +20 A2 A3
%D 2D +20 A4 A5
%D 2D
%D 2D +20 B0 B1 D0 D1
%D 2D +20 B2 B3 C0 D2 D3 E0 F0 F1
%D 2D +20 B4 B5 C1 D4 D5 E1 F2 F3
%D 2D +20 D6 D7 F4 F5
%D 2D
%D 2D +20 G0 G1
%D 2D +20 G2 G3
%D 2D +20 G4 G5
%D 2D
%D 2D +20 H0 H1
%D 2D
%D
%D ren A0 A1 ==> LA' A'
%D ren A3 ==> A
%D ren A4 A5 ==> LA RLA
%D
%D ren B0 B1 D0 D1 ==> LA A LA' A'
%D ren B2 B3 C0 D2 D3 E0 F1 ==> LRB RB LRB LA A A A
%D ren B4 C1 D4 D5 E1 F2 F3 ==> B B B RB RLA LA RLA
%D ren D6 D7 F4 F5 ==> B' RB' B RB
%D
%D ren G0 G1 ==> LRB RB
%D ren G2 ==> B
%D ren G4 G5 ==> B' RB'
%D
%D ren H0 H1 ==> \catB \catA
%D
%D ((
%D ))
%D (( A0 A1 <-|
%D A0 A4 -> .plabel= l Lf
%D A1 A3 -> .plabel= r f
%D A3 A5 -> .plabel= r η_A
%D A1 A5 -> .slide= -10pt
%D A0 A5 harrownodes nil 15 5 <-|
%D A4 A5 <-|
%D
%D B0 B1 <-|
%D B0 B2 -> .plabel= l Lh
%D B1 B3 -> .plabel= r h
%D B0 B3 harrownodes nil 20 nil <-|
%D B2 B3 <-|
%D B2 B4 -> .plabel= l ε_B
%D B0 B4 -> .slide= -20pt .plabel= l g
%D
%D C0 C1 -> .plabel= l ε_B
%D
%D D0 D1 <-|
%D D0 D2 -> .plabel= l Lf
%D D1 D3 -> .plabel= r f
%D D0 D3 harrownodes nil 20 nil <-|
%D D2 D3 <-|
%D D2 D4 -> .plabel= l \sm{h^♭\\g}
%D D3 D5 -> .plabel= r \sm{h\\g^♯}
%D D2 D5 harrownodes nil 20 nil <-| sl^
%D D2 D5 harrownodes nil 20 nil |-> sl_
%D D4 D5 |->
%D D4 D6 -> .plabel= l k
%D D5 D7 -> .plabel= r Rk
%D D6 D7 |->
%D D4 D7 harrownodes nil 20 nil |->
%D
%D E0 E1 -> .plabel= r η_A
%D
%D F1 F3 -> .plabel= r η_A
%D F2 F3 |->
%D F2 F4 -> .plabel= l g
%D F3 F5 -> .plabel= r Rg
%D F4 F5 |->
%D F2 F5 harrownodes nil 20 nil |->
%D F1 F5 -> .slide= 20pt .plabel= r h
%D
%D G0 G1 |->
%D G0 G2 -> .plabel= l η_B
%D G2 G4 -> .plabel= l k
%D G0 G4 -> .slide= 10pt
%D G1 G5 -> .plabel= r Rk
%D G4 G5 |->
%D G0 G5 harrownodes 5 15 nil |->
%D
%D H0 H1 <- sl^ .plabel= a L
%D H0 H1 -> sl_ .plabel= b R
%D ))
%D enddiagram
%D
$$\pu
\diag{teaching-adjunctions-1}
$$
Let's use these names for its subdiagrams: $\sm{ A \\ BCDEF \\ G \\ I}$.
% (find-riehlccpage (+ 18 124) "fully-specified adjunction")
% (find-riehlcctext (+ 18 124) "fully-specified adjunction")
A {\sl fully-specified adjunction} between categories $\catB$ and
$\catA$ has lots of components: $(L, R, ε, η, ♭, ♯, \univ(ε),
\univ(η))$, and maybe even others, but usually we define only some of
these components; there is a Big Theorem About Adjunctions (below!)
that says how to reconstruct the fully-specified adjunction from some
of its components.
Some parts of the diagram above can be interpreted as definitions,
like these:
%
$$\begin{array}{c}
Lf := (η_A∘f)^♭ \\
[5pt]
g := ε_B∘Lh
\qquad ε_B := (\id_{RB})^♭
\qquad η_A := (\id_{LA})^♯
\qquad h := Rg∘η_A \\
[5pt]
Rk := (k∘η_B)^♯ \\
\end{array}
$$
The subdiagrams $B$ and $F$ can also be interpreted in the opposite
direction, as:
%
$$\begin{array}{rclcrcl}
g^♯ &:=& (∀A.∀g.∃!h)Ag &\phantom{mmmmmm}& h^♭ &:=& (∀B.∀h.∃!g)Bh \\
&=& (\univ_{ε_B})Ag && &=& (\univ_{η_A}) Bh \\
\end{array}
$$
The notations $(∀A.∀g.∃!h)Ag$ and $(\univ_{ε_B})Ag$ are clearly abuses
of language --- but it's not hard to translate them to something
formal, and they inspire great discussions in the classroom... also,
they can help us to understand and formalize constructions like this
one,
%
%D diagram building-L_1f
%D 2Dx 100 +25 +25
%D 2D 100 A1
%D 2D
%D 2D +25 A2 A3 B1
%D 2D
%D 2D +25 B2 B3
%D 2D
%D 2D +15 C0 C1
%D 2D
%D ren A1 A2 A3 ==> A' LA' RLA'
%D ren B1 B2 B3 ==> A LA RLA
%D ren C0 C1 ==> \catB \catA
%D
%D (( A1 A3 -> .plabel= l \sm{η_{A'}\\\univ}
%D A2 A3 |->
%D B1 B3 -> .plabel= r \sm{η_A\\\univ}
%D B2 B3 |->
%D A1 B1 -> .plabel= a f
%D A2 B2 -> .plabel= l Lf
%D A3 B3 -> .plabel= m RLf
%D A2 B3 harrownodes nil 15 2 |->
%D C0 xy+= 12 0
%D C1 xy+= 12 0
%D C0 C1 -> .plabel= b R
%D ))
%D enddiagram
%D
$$\pu
Lf := (\univ_{η_A})(LA)(η_A∘f)
\qquad
\diag{building-L_1f}
$$
%
that are needed in cases like the part (ii) of the Big Theorem.
The Big Theorem About Adjunctions is this --- it's the Theorem 2 in
\cite[page 83]{CWM2}, but with letters changed to match the ones we
are using in our diagrams:
\def\ORIG#1{\msk\ColorBrown{#1}}
\def\ORIG#1{}
\newpage
\begin{quotation}
\ORIG{{\bf Theorem 2.} Each adjunction $〈F,G,φ〉: X \rightharpoonup
A$ is completely determined by the items in any one of the
following lists:}
{\bf Big Theorem About Adjunctions.} Each adjunction $〈L,R,♯〉: \catA
\rightharpoonup \catB$ is completely determined by the items in any
one of the following lists:
\ORIG{(i) Functors $F$, $G$, and a natural transformation $η: 1_X
\tnto GF$ such that each $η_x: x→GFx$ is universal to $G$ from
$x$. Then $φ$ is defined by (6).}
(i) Functors $L$, $R$, and a natural transformation $η:
\id_\catA→RL$ such that each $η_A: A→RLA$ is universal to $R$ from
$A$. Then $♯$ is defined by (6).
\ORIG{(ii) The functor $G: A → X$ and for each $x∈X$ an
object $F_0x∈A$ and a universal arrow $η_x:x→GF_0x$ from $x$
to $G$. Then the functor $F$ has object function $F_0$ and is
defined on arrows $h:x→x'$ by $GFh∘η_x = η_{x'}∘h$.}
(ii) The functor $R: \catB → \catA$ and for each $A∈\catA$ an object
$L_0A∈\catB$ and a universal arrow $η_A:A→RL_0A$ from $A$ to $R$.
Then the functor $L$ has object function $L_0$ and is defined on
arrows $f:A'→A$ by $RLf∘η_{A'} = η_A∘f$.
\ORIG{(iii) Functors $F$, $G$, and a natural transformation $ε: FG
\tnto I_A$ such that each $ε_a:FGa→a$ is universal from $F$ to
$a$. Here $φ^{-1}$ is defined by (7).}
(iii) Functors $L$, $R$, and a natural transformation $ε:
LR→\id_\catB$ such that each $ε_B:LRB→B$ is universal from $L$ to
$B$. Here $♭$ is defined by (7).
\ORIG{(iv) The functor $F:X→A$ and for each $a∈A$ an object $G_0a∈X$
and an arrow $ε_a:FG_0a→a$ universal from $F$ to $a$.}
(iv) The functor $L:\catA→\catB$ and for each $B∈\catB$ an object
$R_0B∈\catA$ and an arrow $ε_B:LR_0B→B$ universal from $L$ to $B$.
\ORIG{(v) Functors $F$, $G$ and natural transformations $η:I_x \tnto
GF$ and $ε: FG \tnto I_A$ such that both composites (8) are the
identity transformations. Here $φ$ is defined by (6) and $φ^{-1}$
by (7).}
(v) Functors $L$, $R$ and natural transformations $η:\id_\catA→RL$
and $ε:LR→\id_\catB$ such that both composites (8) are the identity
transformations. Here $♯$ is defined by (6) and $♭$ by (7).
\end{quotation}
My plan for the next incarnation of the course is to ask the students
to 1) visualize in the big diagram all the objects and constructions
in the Big Theorem, 2) take the original Theorem 2 in \cite{CWM2} and
draw the missing diagrams for it, 3) decypher some other parts of the
section about adjunctions in \cite{CWM2}.
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 13 79) "IV. Adjoints")
% (find-cwm2page (+ 13 79) "1. Adjunctions")
% (find-cwm2text (+ 13 79) "1. Adjunctions")
% (find-cwm2page (+ 13 83) "Theorem 2.")
% (find-cwm2text (+ 13 83) "Theorem 2.")
\newpage
% ____ _ _____ _ _
% | __ ) __ _ ___(_) ___ | ____|_ __ ___| | _____| |
% | _ \ / _` / __| |/ __| | _| \ \/ / / __| |/ / _ \ |
% | |_) | (_| \__ \ | (__ | |___ > < \__ \ < __/ |
% |____/ \__,_|___/_|\___| |_____/_/\_\ |___/_|\_\___|_|
%
% «basic-example-as-skel» (to ".basic-example-as-skel")
% (favp 29 "basic-example-as-skel")
% (fava "basic-example-as-skel")
\section{The Basic Example as a skeleton \DONE}
\label{basic-example-as-skel}
In the sections \ref{the-conventions} and \ref{to-deserve-a-name} I
claimed that the diagram of the Basic Example is a ``skeleton'' of a
certain theorem, in the sense that both the statement and the proof of
that theorem can be reconstructed from just the diagram and very few
extra hints. Let's see the details of this.
% ____ _ _____ __ _
% | __ ) __ _ ___(_) ___ | ____|_ __ / _|_ _ _ __ ___| |_
% | _ \ / _` / __| |/ __| | _| \ \/ / | |_| | | | '_ \ / __| __|
% | |_) | (_| \__ \ | (__ | |___ > < | _| |_| | | | | (__| |_
% |____/ \__,_|___/_|\___| |_____/_/\_\ |_| \__,_|_| |_|\___|\__|
%
% «basic-example-functors» (to ".basic-example-functors")
% (favp 26 "basic-example-functors")
% (fava "basic-example-functors")
\subsection{Reconstructing its functors \DONE}
\label{basic-example-functors}
\def\Yzero {\mathsf{Y0}}
\def\Yzeroplus{\mathsf{Y0^+}}
\def\Yone {\mathsf{Y1}}
Let's call this diagram --- the diagram of the Basic Example ---
$\Yzero$:
%
$$\Yzero \qquad := \quad \diag{Basic-Example}$$
We don't know yet the precise meaning of the functors $\catB(C,-)$ and
$\catA(A,R-)$, but if we enlarge $\Yzero$ to
%
%D diagram Basic-Example-plus
%D 2Dx 100 +40
%D 2D 100 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 2D +15 B0 --> B1
%D 2D
%D 2D +15 C0 --> C1
%D 2D \ |
%D 2D +20 C2
%D 2D
%D ren A1 ==> A
%D ren A2 A3 ==> C RC
%D ren A4 A5 ==> D RD
%D ren A6 A7 ==> E RE
%D ren B0 B1 ==> \catB \catA
%D ren C0 C1 C2 ==> \catB(C,-) \catA(A,R-) ?
%D
%D (( A1 A3 -> .plabel= r η
%D A2 A3 |->
%D A2 A4 -> .plabel= l f
%D A3 A5 -> .plabel= r Rf
%D A2 A5 harrownodes nil 20 nil |->
%D A4 A5 |->
%D A4 A6 -> .plabel= l g
%D A5 A7 -> .plabel= r Rg
%D A4 A7 harrownodes nil 20 nil |->
%D A6 A7 |->
%D A1 A5 -> .slide= 20pt .plabel= r h
%D
%D B0 B1 -> .plabel= a R
%D
%D C0 C1 -> .plabel= b T
%D # C0 C2 -> .plabel= l \sm{ψ\\\text{(iso)}}
%D # C1 C2 <->
%D
%D # C0 C1 midpoint A1 A3 midpoint <-> .curve= ^15pt
%D ))
%D enddiagram
%
$$\pu
\Yzeroplus \qquad := \quad \diag{Basic-Example-plus}
$$
%
and we draw the internal views of $\catB(C,-)$ and $\catA(A,R-)$ then
the meanings for $\catB(C,-)$ and $\catA(A,R-)$ become obvious:
%
%D diagram basic-example-obvious-functors
%D 2Dx 100 +30 +25 +30 +35 +35
%D 2D 100 A0 A1 C0 D0 D1 F0
%D 2D
%D 2D +20 A2 A3 C1 D2 D3 F1
%D 2D
%D 2D +15 B0 B1 E0 E1
%D 2D
%D ren A0 A1 C0 ==> D \catB(C,D) f
%D ren A2 A3 C1 ==> E \catB(C,E) g∘f
%D ren B0 B1 ==> \catB \Set
%D ren D0 D1 F0 ==> D \catA(A,RD) h
%D ren D2 D3 F1 ==> E \catA(A,RE) Rg∘h
%D ren E0 E1 ==> \catB \Set
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l g
%D A1 A3 -> .plabel= r \catB(C,g)
%D A2 A3 |->
%D B0 B1 -> .plabel= a \catB(C,-)
%D C0 C1 |->
%D
%D D0 D1 |->
%D D0 D2 -> .plabel= l g
%D D1 D3 -> .plabel= r \catA(A,Rg)
%D D2 D3 |->
%D E0 E1 -> .plabel= a \catA(A,R-)
%D F0 F1 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{basic-example-obvious-functors}
$$
So:
%
$$\begin{array}{rcl}
\catB(C,-) &:& \catB → \Set \\
\catB(C,-)_0 &:=& λD.\catB(C,D) \\
\catB(C,-)_1 &:=& λg.λf.g∘f \\
[5pt]
\catA(A,R-) &:& \catB → \Set \\
\catA(A,R-)_0 &:=& λD.\catA(A,RD) \\
\catA(A,R-)_1 &:=& λg.λh.Rg∘h \\
\end{array}
$$
% ____ _ _____ _ _ _____
% | __ ) __ _ ___(_) ___ | ____|_ __ | \ | |_ _|
% | _ \ / _` / __| |/ __| | _| \ \/ / | \| | | |
% | |_) | (_| \__ \ | (__ | |___ > < | |\ | | |
% |____/ \__,_|___/_|\___| |_____/_/\_\ |_| \_| |_|
%
% «basic-example-NT» (to ".basic-example-NT")
% (favp 27 "basic-example-NT")
% (fava "basic-example-NT")
\subsection{Reconstructing its natural transformation \DONE}
\label{basic-example-NT}
We also don't know --- yet --- what is the natural transformation
%
$$\catB(C,-) \ton{T} \catA(A,R-).$$
%
Its internal view is this:
%
%D diagram basic-example-obvious-NT
%D 2Dx 100 +25 +40 +30 +25
%D 2D 100 A0 B0 B1 D0 D1
%D 2D
%D 2D +25 A1 B2 B3 D2 D3
%D 2D
%D 2D +15 C0 C1
%D 2D
%D ren A0 B0 B1 D0 D1 ==> D \catB(C,D) \catA(A,RD) f h
%D ren A1 B2 B3 D2 D3 ==> E \catB(C,E) \catA(A,RE) g∘f Rg∘h
%D ren C0 C1 ==> \catB(C,-) \catA(A,R-)
%D
%D (( A0 A1 -> .plabel= l g
%D B0 B1 -> .plabel= a TD
%D B0 B2 -> .plabel= l \catB(C,g)
%D B1 B3 -> .plabel= r \catA(A,Rg)
%D B2 B3 -> .plabel= a TE
%D C0 C1 -> .plabel= a T
%D D0 D2 |->
%D D1 D3 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{basic-example-obvious-NT}
$$
%
Note that we only drew the vertical arrows of the internal view of the internal view.
If we have an arrow $η:A→RC$ then we have a natural construction for
$T_0$: $TD(f):=Rf∘η$, and we can redraw the internal view of the
internal view as:
%
%D diagram basic-example-obvious-NT-2
%D 2Dx 100 +40 +35
%D 2D 100 D0 D1 E0
%D 2D
%D 2D +17 D3' E1
%D 2D +8 D2 D3
%D 2D
%D ren D0 D1 E0 ==> f Rf∘η h
%D ren D3' E1 ==> Rg∘(Rf∘η) Rg∘h
%D ren D2 D3 ==> g∘f R(g∘f)∘η
%D
%D (( D0 D1 |->
%D D0 D2 |->
%D D1 D3' |->
%D D2 D3 |->
%D E0 E1 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{basic-example-obvious-NT-2}
$$
%
The square condition clearly holds, because:
%
$$\begin{array}{rcl}
Rg∘(Rf∘η) &=& (Rg∘Rf)∘η \\
&=& R(g∘f)∘η. \\
\end{array}
$$
So
%
$$\begin{array}{rcl}
T_0 &:=& λD.λf.Rf∘η. \\
\end{array}
$$
% ____ _ _____ _ _ _
% | __ ) __ _ ___(_) ___ | ____|_ __ | |__ (_)(_)
% | _ \ / _` / __| |/ __| | _| \ \/ / | '_ \| || |
% | |_) | (_| \__ \ | (__ | |___ > < | |_) | || |
% |____/ \__,_|___/_|\___| |_____/_/\_\ |_.__/|_|/ |
% |__/
%
% «basic-example-bij» (to ".basic-example-bij")
% (favp 31 "basic-example-bij")
% (fava "basic-example-bij")
\subsection{Reconstructing its bijection \DONE}
\label{basic-example-bij}
We can give names like `$d$' and `$u$' for the two components of the
curved bijection, like this:
%
%D diagram basic-example-bij-1
%D 2Dx 100 +55 +10 +25 +12 +25 +10
%D 2D 100 A0 B0 B1 C0 C1 D0 D1
%D 2D
%D 2D +20 A1 B2 B3 C2 C3 D2 D3
%D 2D
%D ren A0 A1 ==> \Hom(A,RC) \Hom(\catB(C,-),\catA(A,R-))
%D ren B0 B1 C0 C1 D0 D1 ==> η η η u(T) η η_T
%D ren B2 B3 C2 C3 D2 D3 ==> T T d(η) T T_η T
%D
%D (( A0 A1 -> sl_ .plabel= l d
%D A0 A1 <- sl^ .plabel= r u
%D B0 B2 |->
%D B1 B3 <-|
%D C0 C2 |->
%D C1 C3 <-|
%D D0 D2 |->
%D D1 D3 <-|
%D ))
%D enddiagram
%D
$$\pu
\diag{basic-example-bij-1}
$$
%
but the notation at the right will be clearer.
We just saw how the direction `$d$' of the bijection works:
%
$$\begin{array}{rcl}
(T_η)_0 &:=& λD.λf.Rf∘η. \\
\end{array}
$$
Here's how to find a natural construction for $u$. Suppose that we
have a natural transformation $T$. Then $TC(\id_C)$ is an element of
$\catA(A,RC)$:
%
%D diagram basic-example-bij-2
%D 2Dx 100 +25 +40 +30 +30
%D 2D 100 A0 B0 B1 D0 D1
%D 2D
%D 2D 100 A1 B2 B3 D2 D3
%D 2D
%D 2D +15 C0 C1
%D 2D
%D ren A1 B2 B3 D2 D3 ==> C \catB(C,C) \catA(A,RC) \id_C TC(\id_C)
%D ren C0 C1 ==> \catB(C,-) \catA(A,R-)
%D
%D (( A1 place
%D B2 B3 -> .plabel= a TC
%D C0 C1 -> .plabel= a T
%D D2 D3 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{basic-example-bij-2}
$$
We can define:
%
$$\begin{array}{rcl}
η_T &:=& TC(\id_C). \\
\end{array}
$$
Now we need to check that $d$ and $u$ are mutually inverse, or, in the
other notation, that the round trips $η \mapsto T_η \mapsto η_{(T_η)}$
and $T \mapsto η_T \mapsto T_{(η_T)}$ are identity maps. Here is a
good way to draw the round trips:
%
%D diagram basic-example-bij-3
%D 2Dx 100 +10 +30 +10
%D 2D 100 A0 A1 B0 B1
%D 2D | ^ | ^
%D 2D v | v |
%D 2D +20 A2 A3 B2 B3
%D 2D
%D ren A0 A1 B0 B1 ==> η η_{(T_η)} η_T η_T
%D ren A2 A3 B2 B3 ==> T_η T_η T_{(η_T)} T
%D
%D (( A0 A2 |-> A1 A3 <-|
%D B0 B2 |-> B1 B3 <-|
%D ))
%D enddiagram
%D
$$\pu
\diag{basic-example-bij-3}
$$
Checking that $η \mapsto T_η \mapsto η_{(T_η)}$ yields back the
original $η$ is easy --- we just have to start with $η_{(T_η)}$ and
reduce it as most as we can:
%
% (nyop 63 "first-yoneda-bijection-2")
% (nyo "first-yoneda-bijection-2")
%
$$\begin{array}{rcl}
η_{(T_η)} &=& T_ηC(\id_C) \\
&=& (λD.λg.(Rg∘η)) C(\id_C) \\
&=& (λg.(Rg∘η)) (\id_C) \\
&=& R(\id_C)∘η \\
&=& \id_{RC}∘η \\
&=& η \\
\end{array}
$$
Checking that the other round trip, $T \mapsto η_T \mapsto T_{(η_T)}$,
yields back the original $T$ is not trivial. In the terminology of the
convention (CSk) from Section \ref{the-conventions}, to reconstruct
that proof we need an extra hint: that at some point in the proof we
will have to use that the original $T$ obeys $\sqcond_T$, and that
we will have to ``evaluate'' $\sqcond_T$ on these inputs:
%D diagram Y0-NT-2
%D 2Dx 100 +10 +25 +15 +25 +35
%D 2D 100 A0 B0 - B1 D0 |-----> D1
%D 2D +0 | | | | D3'
%D 2D +20 A1 B2 - B3 D2 = D2' - D3
%D 2D
%D 2D +10 C0 - C1
%D 2D
%D ren A0 A1 ==> C D
%D ren B0 B1 B2 B3 ==> \catB(C,C) \catA(A,RC) \catB(C,D) \catA(A,RD)
%D ren C0 C1 ==> \catB(C,-) \catA(A,R-)
%D ren C0 C1 ==> · ·
%D ren D0 D1 D3' ==> \id_C TC(\id_C) Rf∘(TC(\id_C))
%D ren D2 D2' D3 ==> f∘\id_C f TD(f)
%D
%D (( A0 A1 -> .plabel= l f
%D C0 C1 -> .plabel= a T
%D D0 place
%D ))
%D enddiagram
%D
$$\pu
\diag{Y0-NT-2}
$$
This yields:
%
%D diagram Y0-NT-3
%D 2Dx 100 +25 +40 +30 +25 +35
%D 2D 100 A0 B0 - B1 D0 |-----> D1
%D 2D +17 | | | | D3'
%D 2D +8 A1 B2 - B3 D2 = D2' - D3
%D 2D
%D 2D +15 C0 - C1
%D 2D
%D ren A0 A1 ==> C D
%D ren B0 B1 B2 B3 ==> \catB(C,C) \catA(A,RC) \catB(C,D) \catA(A,RD)
%D ren C0 C1 ==> \catB(C,-) \catA(A,R-)
%D ren D0 D1 D3' ==> \id_C TC(\id_C) Rf∘(TC(\id_C))
%D ren D2 D2' D3 ==> f∘\id_C f TD(f)
%D
%D (( A0 A1 -> .plabel= l f
%D B0 B1 -> .plabel= a TC
%D B0 B2 -> .plabel= l \catB(C,f)
%D B1 B3 -> .plabel= r \catA(A,Rf)
%D B2 B3 -> .plabel= a TD
%D C0 C1 -> .plabel= a T
%D D0 D1 |-> D1 D3' |->
%D D0 D2 |-> D2 D2' = D2' D3 |->
%D ))
%D enddiagram
%D
$$\pu
\diag{Y0-NT-3}
$$
%
so $Rf∘(TC(\id_C)) = TD(f)$.
We want to check that for all $D$ and $f$ we have $T_{(η_T)}D(f) =
TD(f)$. We have:
%
$$\begin{array}{rcl}
T_{(η_T)}D(f) &=& (λD.λf.Rf∘η_T)D(f) \\
&=& (λf.Rf∘η_T)(f) \\
&=& Rf∘η_T \\
&=& Rf∘(TC(\id_C)) \\
&=& TD(f). \\
\end{array}
$$
It works! So we have a natural construction for the bijection $T ↔ η$,
given by:
%
$$\begin{array}{rcl}
T_0 &:=& λD.λf.Rf∘η \\
η &:=& TC(\id_C) \\
\end{array}
$$
% ____ _ _____ __ _ _
% | __ ) __ _ ___(_) ___ | ____|_ __ / _|_ _| | |
% | _ \ / _` / __| |/ __| | _| \ \/ / | |_| | | | | |
% | |_) | (_| \__ \ | (__ | |___ > < | _| |_| | | |
% |____/ \__,_|___/_|\___| |_____/_/\_\ |_| \__,_|_|_|
%
% «basic-example-full» (to ".basic-example-full")
% (favp 33 "basic-example-full")
% (fava "basic-example-full")
\subsection{The full reconstruction \DONE}
\label{basic-example-full}
We have just reconstructed all the typings and definitions for the
diagram $\Yzero$. Here is the full reconstruction, except for the
``proof terms'' like $\respids$, $\assoc$, $\idL$ and $\idR$ for each
functor, $\sqcond$ for each natural transformations, and the proofs
that both round trips in the bijections are identity maps:
%
$$\diag{Basic-Example}
\qquad
\begin{array}{rl}
& \catA \text{ is a category}, \\
& \catB \text{ is a category}, \\
& R:\catB \to \catA, \\
& A ∈ \catA, \\
& C ∈ \catB, \\
& η:A→RD, \\
[5pt]
& \catB(C,-) : \catB → \Set, \\
& \catB(C,-)_0 := λD.\catB(C,D), \\
& \catB(C,-)_1 := λg.λf.g∘f, \\
[5pt]
& \catA(A,R-) : \catA → \Set, \\
& \catA(A,R-)_0 := λD.\catA(A,RD), \\
& \catA(A,R-)_1 := λg.λh.Rg∘h, \\
[5pt]
& T : \catB(C,-) → \catA(A,R-), \\
[5pt]
& T_0 := λD.λf.Rf∘η, \\
& η := TC(\id_C). \\
\end{array}
$$
% (find-idarctpage 27 "19. The syntactical world")
% (find-idarcttext 27 "19. The syntactical world")
It shouldn't be hard --- for someone with practice --- to translate
the types and definitions at the right above to the language of some
proof assistant. I tried to do this in Idris (\cite{Brady}) using
\cite{IdrisCT2019} but I didn't go very far... I implemented the
protocategories, protofunctors and proto-NTs of \cite[section
19]{IDARCT} to be able to skip the proof terms on my first
prototypes, but I got stuck trying to implement the formalization of
$\Yzero$ as a single datatype...
\bsk
{\sl (Help would be greatly appreciated!...)}
\newpage
% _____ _ _
% | ____|_ _| |_ ___ _ __ ___(_) ___ _ __ ___
% | _| \ \/ / __/ _ \ '_ \/ __| |/ _ \| '_ \/ __|
% | |___ > <| || __/ | | \__ \ | (_) | | | \__ \
% |_____/_/\_\\__\___|_| |_|___/_|\___/|_| |_|___/
%
% «extensions» (to ".extensions")
% (favp 34 "extensions")
% (fava "extensions")
\section{Extensions to the diagrammatic language \DONE}
\label{extensions}
Our diagrammatic language and the list of conventions in Section
\ref{the-conventions} can be extended --- ``by the user'' --- in
zillions of ways. Let's see some examples of extensions.
% ____ _
% / ___|___ _ __ ___ _ __ ___ __ _ ___ __ _| |_ ___
% | | / _ \| '_ ` _ \| '_ ` _ \ / _` | / __/ _` | __/ __|
% | |__| (_) | | | | | | | | | | | (_| | | (_| (_| | |_\__ \
% \____\___/|_| |_| |_|_| |_| |_|\__,_| \___\__,_|\__|___/
%
% «comma-categories» (to ".comma-categories")
% (favp 34 "comma-categories")
% (fava "comma-categories")
\subsection{A way to define new categories \DONE}
\label{comma-categories}
We saw in the sections \ref{internal-view-functor} and
\ref{basic-example-functors} how to use diagrams to define functors,
and in sections \ref{internal-view-NT} and \ref{basic-example-NT} how
to define natural transformations. We can define new categories by
diagrams, too.
%D diagram comma-obj-0
%D 2Dx 100 +17
%D 2D 100 \A
%D 2D | \f
%D 2D v
%D 2D +15 \B |-> \FB
%D 2D
%D (( \A \FB -> .plabel= r \f
%D \B \FB |->
%D ))
%D enddiagram
\pu
\def\commaobj#1#2#3#4{{
\left( \def\A{#1}
\def\f{#4}
\def\B{#2} \def\FB{#3}
\diag{comma-obj-0}
\right)
}}
% Usage:
% %D (( A .tex= \commaobj{A}{B}{FB}{g} BOX
% %D B .tex= \commaobj{A}{B}{FB}{?} BOX
% %D A B ->
% %D ))
\def\dnAR{{(A{↓}R)}}
%D diagram defining-a-comma-category
%D 2Dx 100 +20 +50 +45
%D 2D 100 A1
%D 2D |
%D 2D +20 A2 A3 B0 C0
%D 2D | | |
%D 2D +20 A4 A5 B1 C1
%D 2D
%D 2D +15 A6 A7 B2 C2
%D 2D
%D ren A1 A2 A3 A4 A5 A6 A7 ==> A C RC D RD \catB \catA
%D ren C0 C1 B2 C2 ==> (C,η) (D,g) \dnAR \dnAR
%D
%D (( A1 A3 -> .plabel= r η
%D A2 A3 |->
%D A2 A4 -> .plabel= l f
%D A3 A5 -> .plabel= r Rf
%D A2 A5 harrownodes nil 20 nil |->
%D A4 A5 |->
%D A1 A5 -> .slide= 20pt .plabel= r g
%D A6 A7 -> .plabel= a R
%D ))
%D (( B0 xy+= 0 -23
%D B1 xy+= 0 -8
%D B0 .tex= \commaobj{A}{C}{RC}{η} BOX
%D B1 .tex= \commaobj{A}{D}{RD}{g} BOX
%D B0 B1 -> .plabel= l f
%D B2 place
%D ))
%D (( C0 C1 -> .plabel= l f
%D C2 place
%D ))
%D enddiagram
%D
$$\pu
\diag{defining-a-comma-category}
$$
\def\AProofOf #1{\llangle#1\rrangle}
\def\AllProofsOf#1{\llbracket#1\rrbracket}
My favorite way --- a syntax sugar! --- of visualizing the comma
category $\dnAR$ is the middle third of the diagram above, in which
the objects of $\dnAR$ are depicted as L-shaped diagrams. To
understand the typings and the commutativity conditions we have to
look at the left third --- it indicates that $f$ must obey $Rf∘η=g$.
The right third shows a generic morphism in $\dnAR$ without the syntax
sugar, but we still have to look at the left third to type it. We
have:
%
$$\begin{array}{rl}
\text{In a context in which}
& \catA \text{ is a category}, \\
& \catB \text{ is a category}, \\
& R : \catB → \catA, \\
& A \text{ is an object of $\catA$}, \\
\text{we define the category}
& \dnAR \text{ as follows:} \\
%
[5pt]
%
\text{An object of}
& \dnAR \\
\text{is a pair}
& (C,η) \\
\text{in which}
& C : \catB_0 \\
\text{and}
& η : \Hom_\catA(A,RC); \\
\text{so}
& (C,η) : ΣC⠆\catB_0. \Hom_\catA(A,RC) \\
\text{and}
& \dnAR_0 := ΣC⠆\catB_0. \Hom_\catA(A,RC). \\
%
[5pt]
%
\text{A morphism}
& f: (C,η) → (D,g) \text{ in $\dnAR$} \\
\text{is an}
& f: \Hom_\catB(C,D) \text{ such that $Rf∘η=g$}, \\
\text{or equivalently a pair}
& (f,\AProofOf{Rf∘η=g}); \\
\text{we have}
& (f,\AProofOf{Rf∘η=g}) : Σf⠆\Hom_\catB(C,D).\AllProofsOf{Rf∘η=g}, \\
\text{so}
& \Hom_\dnAR((C,η),(D,g)) := \\
& Σf⠆\Hom_\catB(C,D).\AllProofsOf{Rf∘η=g}.
\end{array}
$$
The notations $\AProofOf{P}$ and $\AllProofsOf{P}$ are non-standard.
For any proposition $P$ we denote by $\AllProofsOf{P}$ the set of
witnesses of $P$ (see \cite[p.18]{HOTT}) and by $\AProofOf{P}$ a
witness that $P$ is true; formally, $\AProofOf{P}$ is a variable (with
a long name!) whose type is $\AllProofsOf{P}$, and $\AllProofsOf{P}$
is a singleton when $P$ is true and the empty set when $P$ is false. A
good way to remember this notation is that $\AllProofsOf{P}$ looks
like a box and $\AProofOf{P}$ looks like something that comes in that
box.
\msk
This defines formally the first two components of the category
$\dnAR$. Remember that a category $\catC$ has seven components:
%
$$\catC = (\catC_0, \Hom_\catC, \id_\catC, ∘_\catC;
\assoc_\catC, \idL_\catC, \idR_\catC)
$$
%
We are pretending that the other components of $\dnAR$ are ``obvious''
in the sense of Section \ref{to-deserve-a-name}.
% (find-books "__logic/__logic.el" "hott")
% (find-hottpage (+ 12 18) "a witness to the provability of A")
% (find-hotttext (+ 12 18) "a witness to the provability of A")
% __ __ _
% \ \ / /__ _ __ ___ __| | __ _
% \ V / _ \| '_ \ / _ \/ _` |/ _` |
% | | (_) | | | | __/ (_| | (_| |
% |_|\___/|_| |_|\___|\__,_|\__,_|
%
% «yoneda-lemma» (to ".yoneda-lemma")
% (favp 35 "yoneda-lemma")
% (fava "yoneda-lemma")
\subsection{The Yoneda Lemma \DONE}
\label{yoneda-lemma}
The formalization of $\Yzero$ as a series of typings and definitions
in Section \ref{basic-example-full} {\sl suggests} that {\sl some}
operations from Type Theory that can be applied on the formalization
side should be translatable to the diagram side; for example,
substitution. This one clearly works: if we substitute $\catA$ by
$\Set$ and $A$ by the set 1 we get this,
%
%D diagram Basic-Example-using-Set-and-1
%D 2Dx 100 +40
%D 2D 100 A1
%D 2D |
%D 2D +20 A2 |-> A3
%D 2D
%D 2D +15 B0 --> B1
%D 2D
%D 2D +15 C0 --> C1
%D 2D \ |
%D 2D +20 C2
%D 2D
%D ren A1 ==> 1
%D ren A2 A3 ==> C RC
%D ren B0 B1 ==> \catB \Set
%D ren C0 C1 C2 ==> \catB(C,-) \Set(1,R-) ?
%D
%D (( A1 A3 -> .plabel= r η
%D A2 A3 |->
%D
%D B0 B1 -> .plabel= a R\phantom{mmm}
%D
%D C0 C1 -> .plabel= b T
%D # C0 C2 -> .plabel= l \sm{ψ\\\text{(iso)}}
%D # C1 C2 <->
%D
%D C0 C1 midpoint A1 A3 midpoint <-> .curve= ^15pt
%D ))
%D enddiagram
%
\pu
$$
\Yzero \bmat{\catA := \Set \\ A := 1}
\qquad = \quad
\diag{Basic-Example-using-Set-and-1}
$$
For each $D∈\catB$ we have a bijection $\Set(1,RD) ↔ RD$ --- and we
can use these bijections to build a natural isomorphism $\Set(1,R-) ↔
R$, that we will add to the diagram:
%D diagram Basic-Example-using-Set-and-1-and-R
%D 2Dx 100 +40
%D 2D 100 A1
%D 2D |
%D 2D +20 A2 |-> A3
%D 2D
%D 2D +15 B0 --> B1
%D 2D
%D 2D +15 C0 --> C1
%D 2D \ |
%D 2D +20 C2
%D 2D
%D ren A1 ==> 1
%D ren A2 A3 ==> C RC
%D ren B0 B1 ==> \catB \Set
%D ren C0 C1 C2 ==> \catB(C,-) \Set(1,R-) R
%D
%D (( A1 A3 -> .plabel= r η
%D A2 A3 |->
%D
%D B0 B1 -> .plabel= a R\phantom{mmm}
%D
%D C0 C1 -> .plabel= b T
%D C0 C2 -> .plabel= l T' # \sm{ψ\\\text{(iso)}}
%D C1 C2 <->
%D
%D C0 C1 midpoint A1 A3 midpoint <-> .curve= ^15pt
%D ))
%D enddiagram
%
\pu
$$
\Yone
\qquad := \qquad
\diag{Basic-Example-using-Set-and-1-and-R}
$$
We can obtain $T'$ from $T$ and vice-versa by composing them with
$\Set(1,R-) ↔ R$.
The diagram $\Yone$ ``is'' the Yoneda Lemma --- but it doesn't have a
single top-level arrow, so we can't apply the convention (CTL) to it,
and we need to specify its ``meaning'' explicitly. The statement of
the Yoneda Lemma is that there is a bijection
%
$$RC ↔ \Hom(\catB(C,-),R);$$
%
Once we know that it is easy to see that the diagram $\Yone$ shows how
we can build it by combining three bijections that we understand well:
%
$$\begin{array}{l}
RC \\
↔ \Hom(1,RC) \\
↔ \Hom(\catB(C,-),\Set(1,R-)) \\
↔ \Hom(\catB(C,-),R) \\
\end{array}
$$
%
So $\Yone$ shows a way to build the bijection $RC ↔
\Hom(\catB(C,-),R)$.
% __ __ _ _
% \ \ / /__ _ __ ___ __| | __ _ ___ _ __ ___ | |__
% \ V / _ \| '_ \ / _ \/ _` |/ _` | / _ \ '_ ` _ \| '_ \
% | | (_) | | | | __/ (_| | (_| | | __/ | | | | | |_) |
% |_|\___/|_| |_|\___|\__,_|\__,_| \___|_| |_| |_|_.__/
%
% «yoneda-embedding» (to ".yoneda-embedding")
% (favp 34 "yoneda-embedding")
% (fava "yoneda-embedding")
\subsection{The Yoneda embedding \DONE}
\label{yoneda-embedding}
Let $B$ be an object of $\catB$. If we replace the functor $R:
\catB→\Set$ in $\Yone$ by $\catB(B,-)$ and do some other renamings we
get this:
%
%D diagram Basic-Example-using-Hom(B,-)
%D 2Dx 100 +65
%D 2D 100 A1
%D 2D |
%D 2D +20 A2 |-> A3
%D 2D
%D 2D +15 B0 --> B1
%D 2D
%D 2D +15 C0 --> C1
%D 2D \ |
%D 2D +20 C2
%D 2D
%D ren A1 ==> 1
%D ren A2 A3 ==> C \catB(B,C)
%D ren B0 B1 ==> \catB \Set
%D ren C0 C1 C2 ==> \catB(C,-) \Set(1,\catB(B,-)) \catB(B,-)
%D
%D (( A1 A3 -> .plabel= r \nameof{f}
%D A2 A3 |->
%D
%D B0 B1 -> .plabel= a \phantom{mmmmm}\Hom(B,-)
%D
%D C0 C1 -> .plabel= b T'
%D C0 C2 -> .plabel= l T # \sm{ψ\\\text{(iso)}}
%D C1 C2 <->
%D
%D C0 C1 midpoint xy+= -10 0 A1 A3 midpoint <-> .curve= ^25pt
%D ))
%D enddiagram
%
\pu
$$
\Yone\bmat{
R := \catB(B,-) \\
η := \nameof{f} \\
T := T' \\
T' := T \\
}
\quad := \quad
\diag{Basic-Example-using-Hom(B,-)}
$$
We can consider that the diagram above is a skeleton for the {\sl
proof} that there is a bijection between arrows $f:B→C$ and natural
transformations $T:\catB(C,-)→\catB(B,-)$. The two directions of the
bijection are easy to define, as $T_0 := λD.λg.g∘f$ and $f :=
TC(\id_C)$, but the proof that the round trips $f \mapsto T \mapsto f$
and $T \mapsto f \mapsto T$ give back the original $f$ and $T$ are
tricky, as we saw in Section \ref{basic-example-bij}.
Usually people draw a simple diagram that just {\sl states} that the
obvious map $\catB(B,C) → \Hom(\catB(C,-),\catB(B,-)$ is a bijection,
somehow like this:
%
% (find-books "__cats/__cats.el" "riehl")
% (find-riehlccpage (+ 18 60) "Corollary 2.2.8 (Yoneda embedding)")
% (find-riehlcctext (+ 18 60) "Corollary 2.2.8 (Yoneda embedding)")
%
%D diagram Y-emb-square-only
%D 2Dx 100 +30
%D 2D 100 A0 A1
%D 2D
%D 2D +25 A2 A3
%D 2D
%D ren A0 A1 ==> B \catB(B,-)
%D ren A2 A3 ==> C \catB(C,-)
%D
%D (( A0 A1 |->
%D A0 A2 ->
%D A1 A3 <-
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
$$\pu
\diag{Y-emb-square-only}
$$
%
Compare with \cite[p.60]{Riehl}; note that our arrow in the middle of
the square is a `$↔$'.
We can draw it with more details as:
%
%D diagram Y-emb-full
%D 2Dx 100 +30 +30
%D 2D 100 A0 A1 C0
%D 2D
%D 2D +25 A2 A3 C1
%D 2D
%D 2D +15 B0'
%D 2D +8 B0 B1
%D 2D
%D ren A0 A1 C0 ==> B \catB(B,-) g∘f
%D ren A2 A3 C1 ==> C \catB(C,-) g
%D ren B0' ==> \catB
%D ren B0 B1 ==> \phantom{m}\catB^\op \Set
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l \sm{\phantom{mmm}f\\TC(\id_C)}
%D A1 A3 <- .plabel= r \sm{λg.g∘f\\T\phantom{mm}}
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil |-> sl^
%D A0 A3 harrownodes nil 20 nil <-| sl_
%D B0' place
%D B0 B1 -> .plabel= a 𝐛y
%D C0 C1 <-|
%D ))
%D enddiagram
%D
$$\pu
\diag{Y-emb-full}
$$
%
Note that it defines a {\sl contravariant} functor $𝐛y:
\catB^\op→\Set$ whose action on objects is $C \mapsto \catB(C,-)$.
We consider that the morphism $f:B→C$ in the diagram is inside
$\catB$, not inside $\catB^\op$. This is explained in the next
section.
% ___ _ _ _
% / _ \ _ __ _ __ ___ ___(_) |_ ___ ___ __ _| |_ ___
% | | | | '_ \| '_ \ / _ \/ __| | __/ _ \ / __/ _` | __/ __|
% | |_| | |_) | |_) | (_) \__ \ | || __/ | (_| (_| | |_\__ \
% \___/| .__/| .__/ \___/|___/_|\__\___| \___\__,_|\__|___/
% |_| |_|
%
% «opposite-categories» (to ".opposite-categories")
% (favp 38 "opposite-categories")
% (fava "opposite-categories")
\subsection{Opposite categories \DONE}
\label{opposite-categories}
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 13 33) "2. Contravariance and Opposites")
% (find-books "__cats/__cats.el" "abramsky-tzevelekos")
% (find-abramskyticclpage 14 "1.1.5 First Notions")
% (find-abramskyticcltext 14 "1.1.5 First Notions")
% (find-abramskyticclpage 15 "Opposite Categories and Duality")
% (find-abramskyticcltext 15 "Opposite Categories and Duality")
\def\Aop{{\catA^\op}}
Suppose that we have a diagram $A \ton{f} B \ton{g} C$ in a category
$\catA$. There are several different notations for the corresponding
diagram in $\Aop$: for example, in \cite[p.33]{CWM2} it would be
written as $A \otn{f^\op} B \otn{g^\op} C$, while in
\cite[p.15]{AbramskyTzevelekos} as $A \otn{f} B \otn{g} C$. The
convention (COT) says that the notation in our diagrams should be as
close as possible to the notation in the original text --- so let's
see how to support the notation in \cite{AbramskyTzevelekos}, that
looks a bit harder than the one in \cite{CWM2}.
We want to define a new category, $\Aop$, using tricks similar to the
ones in Section \ref{comma-categories}, but now we can't pretend that
the new composition is obvious. We will define $(\Aop)_0$,
$\Hom_\Aop$, $\id_\Aop$, and $∘_\Aop$ without any textual
explanations, with just the diagrams to convince the readed that our
definitions are reasonable.
%
%D diagram A-and-Aop
%D 2Dx 100 +35
%D 2D 100 A0 B0
%D 2D
%D 2D +10 A1 B1
%D 2D | |
%D 2D +15 A2 B2
%D 2D
%D 2D +10 A3 B3
%D 2D | |
%D 2D +15 A4 B4
%D 2D
%D 2D +10 A5 B5
%D 2D | |
%D 2D +15 A6 B6
%D 2D | |
%D 2D +15 A7 B7
%D 2D
%D 2D +15 A8 B8
%D 2D
%D ren A0 A1 A2 A3 A4 A5 A6 A7 A8 ==> A A B A A A B C \catA
%D ren B0 B1 B2 B3 B4 B5 B6 B7 B8 ==> A A B A A A B C \catA^\op
%D
%D (( A0 place
%D A1 A2 -> .plabel= r f
%D A3 A4 -> .plabel= r \id_A
%D A5 A6 -> .plabel= r f
%D A6 A7 -> .plabel= r g
%D A5 A7 -> .slide= 15pt .plabel= r g∘f
%D A8 place
%D
%D B0 place
%D B1 B2 <- .plabel= r f
%D B3 B4 <- .plabel= r \id_A
%D B5 B6 <- .plabel= r f
%D B6 B7 <- .plabel= r g
%D B5 B7 <- .slide= 15pt .plabel= r f∘g
%D B8 place
%D ))
%D enddiagram
%D
$$\pu
\diag{A-and-Aop}
\quad
\begin{array}{c}
\catA_0 =: (\Aop)_0 \\
\\
\Hom_\catA(A,B) =: \Hom_\Aop(B,A) \\
\\
\id_\catA(A) =: \id_\Aop(A) \\
\\
g ∘_\catA f =: f ∘_\Aop g \\
\\
\\
\\
\\
\\
\end{array}
$$
In the diagram below $F:\catA^\op→\catB$ is a contravariant functor,
and the $\catA$ above $\catA^\op$ indicates that $g:C→D$ is a morphism
of $\catA$, not of $\catA^\op$. I am not very happy with this trick
but I haven't found a better alternative yet.
%
%D diagram contravariant-functor
%D 2Dx 100 +20
%D 2D 100 A0 A1
%D 2D
%D 2D +20 A2 A3
%D 2D
%D 2D +12 B0'
%D 2D +8 B0 B1
%D 2D
%D ren A0 A1 ==> C FC
%D ren A2 A3 ==> D FD
%D ren B0' ==> \catA
%D ren B0 B1 ==> \phantom{m}\catA^\op \catB
%D
%D (( A0 A1 |->
%D A0 A2 -> .plabel= l g
%D A1 A3 <- .plabel= r Fg
%D A2 A3 |->
%D A0 A3 harrownodes nil 20 nil |->
%D B0' place
%D B0 B1 -> .plabel= a F
%D ))
%D enddiagram
%D
$$\pu
\diag{contravariant-functor}
$$
\msk
% _ _
% | \ | | ___ ___ ___
% | \| |/ _ \/ __/ __|
% | |\ | __/\__ \__ \
% |_| \_|\___||___/___/
%
% «ness» (to ".ness")
% (favp 39 "ness")
% (fava "ness")
\subsection{Universalness as something extra \DONE}
\label{ness}
We can consider that an universal arrow is an arrow $η:A→RC$ with an
extra property; I showed at the end of Section
\ref{freyd-with-functors} how to think of that property as being just
$∀D.∀g.∃!f$, and how to treat that as an abbreviation for something
bigger and more formal.
We can also treat a universal arrow as an arrow $η:A→RC$ plus extra
{\sl structure} --- this extra structure is an operation that returns
for each $D$ an inverse for the operation $g \mapsto Rg∘η$. For more
on properties and structure, see \cite[p.15]{BaezShulman2007}.
In any case this ``universalness'' can be treated as
something extra, and a universal arrow can be expressed as:
%
$$(η,\univ_η)$$
%
using dependent types.
Several of these ``-ness''es have standard graphical representations:
for example pullbackness is indicated by a `$\pbsymbol7$', and
monicness is indicated by a tail like this: `$\monicto$'.
\cite{FreydScedrov} defines lots of graphical representations for
``-ness''es starting on its page 37. We will use an `$:=$' to define a
new annotation that is an abbreviation for extra structure:
%
%D diagram universalness
%D 2Dx 100 +20 +50 +20
%D 2D 100 A1 C1
%D 2D
%D 2D +20 A2 A3 C2 C3
%D 2D
%D 2D +20 A4 A5 C4 C5
%D 2D
%D 2D +15 B0 B1 D0 D1
%D 2D
%D ren A1 A2 A3 B0 B1 ==> A C RC \catB \catA
%D ren C1 C2 C3 C4 C5 D0 D1 ==> A C RC D RD \catB \catA
%D
%D (( A1 A3 -> .plabel= r \sm{η\\\univ}
%D A2 A3 |->
%D B0 B1 -> .plabel= a R
%D
%D C1 C3 -> .plabel= r η
%D C2 C3 |->
%D C2 C4 -> .plabel= l ∃!f
%D C3 C5 -> .plabel= r Rf
%D C4 C5 |->
%D C1 C5 -> .slide= 15pt .plabel= r ∀g
%D D0 D1 -> .plabel= a R
%D C2 C5 harrownodes nil 20 nil |->
%D
%D A3 C4 midpoint .TeX= := place
%D ))
%D enddiagram
%D
$$\pu
\diag{universalness}
$$
This is pullbackness:
%
%D diagram pullbackness
%D 2Dx 100 100 +20 +40 +20 +20
%D 2D 100 A0 B0
%D 2D
%D 2D +20 A1 A2 B1 B2
%D 2D
%D 2D +20 A3 A4 B3 B4
%D 2D
%D ren A0 A1 A2 A3 A4 ==> ∀X A B C D
%D ren B0 B1 B2 B3 B4 ==> ∀X A B C D
%D
%D (( A1 A2 ->
%D A1 A3 ->
%D A2 A4 ->
%D A3 A4 ->
%D A1 relplace 5 5 \pbsymbol{7}
%D A2 relplace 25 5 :=
%D
%D B1 B2 ->
%D B1 B3 ->
%D B2 B4 ->
%D B3 B4 ->
%D B0 B1 -> .plabel= m ∃!
%D B0 B3 -> .plabel= l ∀
%D B0 B2 -> .plabel= a ∀
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{pullbackness}
$$
% ____ __ _
% | _ \ ___ _ __ _ __ / _|_ _ _ __ ___| |_ ___ _ __ ___
% | |_) / _ \ '_ \| '__| | |_| | | | '_ \ / __| __/ _ \| '__/ __|
% | _ < __/ |_) | | | _| |_| | | | | (__| || (_) | | \__ \
% |_| \_\___| .__/|_| |_| \__,_|_| |_|\___|\__\___/|_| |___/
% |_|
%
% «representable-functors» (to ".representable-functors")
% (favp 40 "representable-functors")
% (fava "representable-functors")
\subsection{Representable functors \DONE}
\label{representable-functors}
It is easy to see that in $\Yzero$ the universality of $η$ is
equivalent to the natural-iso-ness of $T$; in $\Yone$ the universality
of $η$ is equivalent to the natural-iso-ness of $T$, and this is
equivalent to the natural-iso-ness of $T'$. The constructions should
be evident from these diagrams:
%
%D diagram univ-arrows-univ-elts
%D 2Dx 100 +40 +50 +40
%D 2D 100 A1 D1
%D 2D | |
%D 2D +20 A2 |-> A3 D2 |-> D3
%D 2D | | | |
%D 2D +20 A4 |-> A5 D4 |-> D5
%D 2D
%D 2D +15 B0 --> B1 E0 --> E1
%D 2D
%D 2D +15 C0 --> C1 F0 --> F1
%D 2D \ | \ |
%D 2D +20 C2 F2
%D 2D
%D ren A1 ==> A
%D ren A2 A3 ==> C RC
%D ren A4 A5 ==> D RD
%D ren B0 B1 ==> \catB \catA
%D ren C0 C1 C2 ==> \catB(C,-) \catA(A,R-) ?
%D
%D ren D1 ==> 1
%D ren D2 D3 ==> C RC
%D ren D4 D5 ==> D RD
%D ren E0 E1 ==> \catB \Set
%D ren F0 F1 F2 ==> \catB(C,-) \Set(1,R-) R
%D
%D (( A1 A3 -> .plabel= r \sm{η\\\univ}
%D A2 A3 |->
%D A2 A4 -> .plabel= l f
%D A3 A5 -> .plabel= r Rf
%D A2 A5 harrownodes nil 20 nil |->
%D A4 A5 |->
%D A1 A5 -> .slide= 25pt .plabel= r h
%D
%D B0 B1 -> .plabel= a R\phantom{mmm}
%D
%D C0 C1 <-> .plabel= b T
%D C0 C1 midpoint A1 A3 midpoint <-> .curve= ^15pt
%D ))
%D (( D1 D3 -> .plabel= r \sm{η\\\univ}
%D D2 D3 |->
%D D2 D4 -> .plabel= l f
%D D3 D5 -> .plabel= r Rf
%D D2 D5 harrownodes nil 20 nil |->
%D D4 D5 |->
%D D1 D5 -> .slide= 25pt .plabel= r h
%D
%D E0 E1 -> .plabel= a R\phantom{mmm}
%D
%D F0 F1 <-> .plabel= b T
%D F0 F2 <-> .plabel= l T'
%D F1 F2 <->
%D
%D F0 F1 midpoint D1 D3 midpoint <-> .curve= ^15pt
%D ))
%D enddiagram
%
$$\pu
\diag{univ-arrows-univ-elts}
$$
The diagram at the right above can be seen as the missing diagram for
Proposition 2 in \cite[p.60]{CWM2}, that says this (I've translated
its letters to the ones I use):
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 13 60) "Definition.")
% (find-cwm2text (+ 13 60) "Definition.")
\begin{quotation}
{\bf Definition.} {\sl Let $\catB$ have small hom-sets. A
representation of a functor $R:\catB→\Set$ is a pair $〈C,T'〉$,
with $C$ an object of $\catB$ and
%
$$T':\catB(C,-)→R$$
%
a natural isomorphism. The object $C$ is called the representing
object. The functor $R$ is said to be representable when such a
representation exists.}
\msk
Up to isomorphism, a representable functor is thus just a covariant
hom-functor $\catB(C,-)$. This notion can be related to universal arrows as
follows.
\msk
{\bf Proposition 2.} Let 1 denote any one-point set and let $\catB$
have small hom-sets. If $〈C, η:1→RC〉$ is a universal arrow from $1$
to $R: \catB→\Set$, then the function $T'$ which for each object $D$
of $\catB$ sends the arrow $f:C→D$ to $(Rf)(η(*))∈RD$ is a
representation of $R$. Every representation of $R$ is obtained in
this way from exactly one such universal arrow.
\end{quotation}
The operations $T'↦η$ and $η↦T'$ can be defined as:
%
$$\begin{array}{rcl}
η &:& 1→RC \\
T' &:& \catB(C,-)→R \\
η &:=& λ*.(T'C(\id(C))) \\
T' &:=& λD.λf.(Rf)(η(*)) \\
\end{array}
$$
% _____ __ __
% |__ / | _|_ _|_ |
% / / | |\ \/ /| |
% / /_ | | > < | |
% /____| | |/_/\_\| |
% |__| |__|
%
% «representable-functor-ex» (to ".representable-functor-ex")
% (favp 42 "representable-functor-ex")
% (fava "representable-functor-ex")
\subsection{An example of a representable functor \DONE}
\label{representable-functor-ex}
% (find-books "__cats/__cats.el" "riehl")
% (find-riehlccpage (+ 18 51) "Example 2.1.5. The following covariant functors")
% (find-riehlcctext (+ 18 51) "Example 2.1.5. The following covariant functors")
Emily Riehl gives two pages of examples of representable functors in
\cite[pages 51--53]{Riehl}. Her example (iv) is:
\begin{quotation}
\begin{enumerate}
\item[(iv)] The functor $U:\Ring→\Set$ is represented by the unital
ring $\Z[x]$, the polynomial ring in one variable with integer
coefficients. A unital ring homomorphism $Z[x]→R$ is uniquely
determined by the image of $x$; put another way, $\Z[x]$ is the {\sl
free unital ring on a single generator}.
\end{enumerate}
\end{quotation}
% (find-riehlccpage (+ 18 63) "Example 2.3.4." "Z[x]")
% (find-riehlcctext (+ 18 63) "Example 2.3.4." "Z[x]")
She develops more this example in page 63, as:
\begin{quotation}
{\bf Example 2.3.4.} Recall from Example 2.1.5(iv) that the
forgetful functor $U:\Ring→\Set$ is represented by the ring $Z[x]$.
The universal element, which defines the natural isomorphism
%
$$\Ring(Z[x], R) ≅ UR,$$
%
is the element $x∈\Z[x]$. As in the proof of the Yoneda lemma, the
bijection above is implemented by evaluating a ring homomorphism
$ϕ:\Z[x]→R$ at the element $x∈\Z[x]$ to obtain an element $ϕ(x)∈R$.
\end{quotation}
Here is the ``missing diagram'' for both excerpts:
%
%D diagram 2.3.4._Z[x]
%D 2Dx 100 +55
%D 2D 100 A1
%D 2D +20 A2 A3
%D 2D +20 A4 A5
%D 2D +15 B0 B1
%D 2D +15 C1 C2
%D 2D +20 C3
%D 2D
%D ren A1 ==> 1
%D ren A2 A3 ==> \Z[x] U(\Z[x])
%D ren A4 A5 ==> R UR
%D ren B0 B1 ==> \Ring \Set
%D ren C1 C2 ==> \Ring(\Z[x],-) \Set(1,U-)
%D ren C3 ==> U
%D
%D (( A1 A3 -> .plabel= r \sm{\nameof{x}\\\univ}
%D A2 A3 |->
%D A2 A4 -> .plabel= l ϕ
%D A3 A5 -> .plabel= r Uϕ
%D A4 A5 |->
%D A1 A5 -> .slide= 25pt .plabel= r \nameof{ϕ(x)}
%D A2 A5 harrownodes nil 20 nil |->
%D B0 B1 -> .plabel= a U
%D C1 C2 <-> .plabel= b T
%D C1 C3 <-> .plabel= b T'
%D C2 C3 <->
%D ))
%D enddiagram
%D
$$\pu
\diag{2.3.4._Z[x]}
$$
That diagram may be a good starting point to explain the Yoneda Lemma
to ``children''.
% The diagram above may be a good starting point for
% __ __ _ _ _ _ _
% \ \ / /__ _ __ ___ __| | __ _ ___| |__ (_) | __| |_ __ ___ _ __
% \ V / _ \| '_ \ / _ \/ _` |/ _` | / __| '_ \| | |/ _` | '__/ _ \ '_ \
% | | (_) | | | | __/ (_| | (_| | | (__| | | | | | (_| | | | __/ | | |
% |_|\___/|_| |_|\___|\__,_|\__,_| \___|_| |_|_|_|\__,_|_| \___|_| |_|
%
% «yoneda-for-children» (to ".yoneda-for-children")
%\subsection{Yoneda for children}
%\label{yoneda-for-children}
\newpage
% ____ _ __ _
% |___ \ ___ __ _| |_ ___ / _| ___ __ _| |_ ___
% __) |____ / __/ _` | __| / _ \| |_ / __/ _` | __/ __|
% / __/_____| (_| (_| | |_ | (_) | _| | (_| (_| | |_\__ \
% |_____| \___\__,_|\__| \___/|_| \___\__,_|\__|___/
%
% «2-category-of-cats» (to ".2-category-of-cats")
% (favp 44 "2-category-of-cats")
% (fava "2-category-of-cats")
\subsection{The 2-category of categories}
\label{2-category-of-cats}
% (find-books "__cats/__cats.el" "riehl")
% (find-riehlccpage (+ 18 44) "1.7. The 2-category of categories")
\def\Dn#1{\Downarrow\scriptstyle #1}
Natural transformations are often drawn as `$⇒$'s in the middle of
``cells'' whose walls are functors. If $F,G:\catA→\catB$ are functors
and $T:F→G$ is natural transformation, then $\catA, \catB, F, G, T$
are drawn like this:
%
%D diagram 2-cat-1
%D 2Dx 100 +30
%D 2D 100 A B
%D 2D
%D ren A B ==> \catA \catB
%D
%D (( A B -> .curve= ^10pt .plabel= a F
%D A B -> .curve= _10pt .plabel= b G
%D A B midpoint .TeX= \Dn{T} place
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{2-cat-1}
$$
% (find-books "__cats/__cats.el" "power")
There are several ways to compose functors and natural transformations
--- see \cite[section 1.7]{Riehl} and \cite{PowerPasting} for the
details and the precise terminology. For example, in
%
% (riep 5 "6.1._kan-extensions")
% (rie "6.1._kan-extensions")
%
%D diagram 2-cat-2
%D 2Dx 100 +25 +25 +20 +25 +25 +20 +25 +25
%D 2D 100 A1 B1 C1
%D 2D / \ / \ / \\
%D 2D +25 A0 ---- A2 B0 ---- B2 C0 ---- C2
%D 2D
%D ren A0 A1 A2 ==> \catA \catB \catC
%D ren B0 B1 B2 ==> \catA \catB \catC
%D ren C0 C1 C2 ==> \catA \catB \catC
%D
%D ((
%D A0 A1 -> .plabel= a F
%D A1 A2 -> .curve= _10pt .plabel= m R
%D A1 A2 -> .curve= ^20pt .plabel= a G
%D A0 A2 -> .plabel= b H
%D A0 A2 midpoint relplace -4 -8 \Dn{T}
%D A1 A2 midpoint relplace 4 -2 \Dn{U}
%D
%D B0 B2 -> .curve= ^50pt .plabel= a GF
%D B0 B2 -> .curve= ^25pt .plabel= m RF
%D B0 B2 -> .plabel= b H
%D B0 B2 midpoint relplace 0 -21 \Dn{UF}
%D B0 B2 midpoint relplace 0 -7 \Dn{T}
%D
%D C0 C2 -> .curve= ^45pt .plabel= a GF
%D C0 C2 -> .plabel= b H
%D C0 C2 midpoint relplace 0 -12 \Dn{T·UF}
%D
%D A2 B0 midpoint relplace 0 -12 =
%D B2 C0 midpoint relplace 0 -12 =
%D ))
%D enddiagram
%D
$$\pu
\diag{2-cat-2}
$$
%
we used ``whiskering'' and then ``vertical composition''.
We can use internal views to lower the level of abstraction of the
diagrams above. If we draw the images of an object $A∈\catA$ by the
functors and natural transformations we get:
%
%D diagram 2-cat-2-internal-view
%D 2Dx 100 +20 +20 +30 +20 +20 +30 +20 +20
%D 2D 100 A1 B1 C1
%D 2D / |\ / |\ / |\
%D 2D +10 / \ A2 / \ B2 / \ C2
%D 2D +15 | A3 | B3 | C3
%D 2D +15 A0 ---- A4 B0 ---- B4 C0 ---- C4
%D 2D
%D ren A0 A1 A2 A3 A4 ==> A FA GFA RFA HA
%D ren B0 B1 B2 B3 B4 ==> A FA GFA RFA HA
%D ren C0 C1 C2 C3 C4 ==> A FA GFA RFA HA
%D
%D (( A0 A1 |->
%D A1 A2 |-> .curve= ^5pt
%D A1 A3 |-> .curve= _10pt
%D A0 A4 |->
%D A2 A3 -> .plabel= r UFA
%D A3 A4 -> .plabel= r TA
%D
%D B0 B2 |-> .curve= ^40pt
%D B0 B3 |-> .curve= ^20pt
%D B0 B4 |->
%D B2 B3 -> .plabel= r UFA
%D B3 B4 -> .plabel= r TA
%D
%D C0 C2 |-> .curve= ^40pt
%D C0 C4 |->
%D C2 C4 -> .plabel= r \sm{TA∘UFA\\=(T·UF)A}
%D
%D A4 B0 midpoint relplace 4 -12 =
%D B4 C0 midpoint relplace 4 -12 =
%D ))
%D enddiagram
%D
$$\pu
\diag{2-cat-2-internal-view}
$$
%
\newpage
% _ __ _
% | |/ /__ _ _ __ _____ _| |_ ___
% | ' // _` | '_ \ / _ \ \/ / __/ __|
% | . \ (_| | | | | | __/> <| |_\__ \
% |_|\_\__,_|_| |_| \___/_/\_\\__|___/
%
% «kan-extensions» (to ".kan-extensions")
% (favp 45 "kan-extensions")
% (fava "kan-extensions")
\subsection{Kan extensions}
\label{kan-extensions}
% (find-books "__cats/__cats.el" "riehl")
% (find-riehlccpage (+ 18 192) "Proposition 6.1.5")
% (find-riehlcctext (+ 18 192) "Proposition 6.1.5")
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 13 236) "3. The Kan Extension")
Kan extensions are usually drawn using 2-cells (\cite[definition
6.1.1]{Riehl}), but they can also be drawn as adjunctions
(\cite[proposition 6.1.5]{Riehl}, \cite[section X.3]{CWM2}). Let's see
how to draw them in both ways at the same time in a way that makes the
translation clear. Here is the diagram:
%
%D diagram kan-1
%D 2Dx 100 +35
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +20 A2 - A3
%D 2D |
%D 2D +20 A4
%D 2D
%D 2D +15 B0 = B1
%D 2D
%D 2D +15 C0 - C1
%D 2D
%D ren A0 A1 ==> GF ∀G
%D ren A2 A3 ==> RF R{:=}\Ran_FH
%D ren A4 ==> H
%D ren B0 B1 ==> \catC^\catA \catC^\catB
%D ren C0 C1 ==> \catA \catB
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l GU
%D A1 A3 -> .plabel= r ∃!U
%D A0 A3 harrownodes nil 20 nil <-|
%D A2 A3 <-|
%D A2 A4 -> .plabel= l T
%D A0 A4 -> .slide= -20pt .plabel= l ∀V
%D B0 B1 <- sl^ .plabel= a ∘F
%D B0 B1 -> sl_ .plabel= b \Ran_F
%D C0 C1 -> .plabel= a F
%D ))
%D enddiagram
%D
%D diagram kan-2-cells-1
%D 2Dx 100 +25 +25 +20 +25 +25 +20 +25 +25
%D 2D 100 A1 B1 C1
%D 2D / \ / \ / \\
%D 2D +25 A0 ---- A2 B0 ---- B2 C0 ---- C2
%D 2D
%D ren A0 A1 A2 ==> \catA \catB \catC
%D
%D (( A0 A1 -> .plabel= a F
%D A1 A2 -> .curve= _10pt .plabel= m R
%D A1 A2 -> .curve= ^20pt .plabel= a ∀G
%D A0 A2 -> .plabel= b H
%D A0 A2 midpoint relplace -4 -8 \Dn{T}
%D A1 A2 midpoint relplace 2 -3 \Dn{∃!U}
%D ))
%D enddiagram
%D
$$\pu
\diag{kan-1}
\qquad
\quad
\diag{kan-2-cells-1}
$$
%
We will consider right Kan extensions only.
Fix $F:\catA→\catB$ and a category $\catC$. We have a functor
$(∘F):\catC^\catB→\catC^\catA$. Suppose that it has a right adjoint,
$(∘F)⊣\Ran_F$. For each natural transformation $H:\catA→\catC$ its
image by $\Ran_f$, $R:=\Ran_FH$, is a natural transformation
$R:\catB→\catC$. We have:
%
$$\begin{array}{rcl}
\Hom_{\catC^\catA}(GF,H) &≅& \Hom_{\catC^\catB}(G,R) \\
\Hom_{\catC^\catA}(-∘F,H) &≅& \Hom_{\catC^\catB}(-,\Ran_FH), \\
\end{array}
$$
%
and if substitute $[- := \Ran_FH]$ and we transpose $\id_{\Ran_FH}$ to
the left we obtain a morphism $T:RF→H$. The pair $(R,H)$ obeys a
certain universal property, that we will call ``Ran-ness'':
%
$$∀G:\catB→\catC. \;\; ∀V:GF→H. \;\; ∃!U:G→R. \;\; (T·UF)=V.$$
The usual way of defining right Kan extensions is by starting with the
functors $F:\catA→\catB$ and $H:\catA→\catC$ and then saying that a
pair $(R,T)$ is {\sl a} right Kan extension of $H$ along $F$ iff it
obeys Ran-ness; the functor $\Ran_F$ and the adjunction come later.
See \cite{Riehl}, section 6.1.
Note that we don't draw the `$∀V:GF→H$' in the right half of the
diagram --- it would overwrite the rest.
\newpage
% _ _ _ _
% / \ | | | ___ ___ _ __ ___ ___ _ __ | |_ ___
% / _ \ | | | / __/ _ \| '_ \ / __/ _ \ '_ \| __/ __|
% / ___ \| | | | (_| (_) | | | | (_| __/ |_) | |_\__ \
% /_/ \_\_|_| \___\___/|_| |_|\___\___| .__/ \__|___/
% |_|
%
% «all-concepts» (to ".all-concepts")
\subsection{All concepts are Kan extensions}
\label{all-concepts}
Both \cite{CWM2} and \cite{Riehl} have sections called ``All concepts
are Kan extensions'' --- section X.7 in \cite{CWM2} and 6.5 in
\cite{Riehl}. Now that we have a favorite way of drawing right Kan
extensions we can use it to draw diagrams for 1) binary products in
$\Set$ are right Kan extensions, 2) limits are right Kan extensions
and 3) left adjoints are right Kan extensions.
\def\bu{{•}}
\def\bubu{{••}}
\begin{enumerate}
\item Let $\bubu$ be the discrete category with two objects, $\bu$ be
the discrete category with one object, and $!:\bubu→\bu$ be the
unique functor from $\bubu$ to $\bu$. Then:
%
%D diagram kan-binary-prods
%D 2Dx 100 +40
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +20 A2 - A3
%D 2D |
%D 2D +20 A4
%D 2D
%D 2D +15 B0 = B1
%D 2D
%D 2D +15 C0 - C1
%D 2D
%D ren A0 A1 ==> GF ∀G
%D ren A2 A3 ==> RF R{:=}\Ran_FH
%D ren A4 ==> H
%D ren B0 B1 ==> \Set^\bubu \Set^•
%D ren C0 C1 ==> \bubu •
%D
%D ren A0 A1 ==> (X,X) ∀X
%D ren A2 A3 ==> (Y{×}Z,Y{×}Z) Y{×}Z
%D ren A4 ==> (Y,Z)
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l (h,h)
%D A1 A3 -> .plabel= r ∃!h
%D A0 A3 harrownodes nil 20 nil <-|
%D A2 A3 <-|
%D A2 A4 -> .plabel= l (π,π')
%D A0 A4 -> .slide= -40pt .plabel= l ∀(f,g)
%D B0 B1 <- sl^ .plabel= a Δ:=(∘!)
%D B0 B1 -> sl_ .plabel= b \lim:=\Ran_!
%D C0 C1 -> .plabel= a !
%D ))
%D enddiagram
%D
%D diagram kan-2-cells-binary-prods
%D 2Dx 100 +30 +30
%D 2D 100 A1
%D 2D / \
%D 2D +30 A0 ---- A2
%D 2D
%D ren A0 A1 A2 ==> \catA \catB \catC
%D ren A0 A1 A2 ==> \bubu \bu \Set
%D
%D ((
%D A0 A1 -> .plabel= a !
%D A1 A2 -> .curve= _10pt .plabel= m Y×Z
%D A1 A2 -> .curve= ^20pt .plabel= a ∀X
%D A0 A2 -> .plabel= b (Y,Z)
%D A0 A2 midpoint relplace -6 -8 \Dn{(π,π')}
%D A1 A2 midpoint relplace 2 -5 \Dn{∃!h}
%D ))
%D enddiagram
%D
$$\pu
\diag{kan-binary-prods}
\qquad
\quad
\diag{kan-2-cells-binary-prods}
$$
\item Let $\catI$ be a finite index category --- for example, $\catI =
\psm{&&1 \\ &&↓ \\ 2&→&3}$ --- and let $\catC$ be a category with
finite limits. A functor $D:\catI→\catC$ is a diagram of shape
$\catI$ in $\catC$. Let's denote by $\bm1$ the discrete category
with a single object --- the name `$\bm1$' is more standard than
`$•$'. Then:
%
%D diagram kan-prods
%D 2Dx 100 +40
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +20 A2 - A3
%D 2D |
%D 2D +20 A4
%D 2D
%D 2D +15 B0 = B1
%D 2D
%D 2D +15 C0 - C1
%D 2D
%D ren A0 A1 ==> ΔC ∀C
%D ren A2 A3 ==> RF R{:=}\Ran_FH
%D ren A4 ==> H
%D ren B0 B1 ==> \catC^\catI \catC^{\bm1}
%D ren C0 C1 ==> \catI \bm1
%D
%D ren A0 A1 ==> ΔX ∀X
%D ren A2 A3 ==> Δ\lim_{\catI}D \lim_{\catI}D
%D ren A4 ==> D
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l Δf
%D A1 A3 -> .plabel= r ∃!f
%D A0 A3 harrownodes nil 20 nil <-|
%D A2 A3 <-|
%D A2 A4 -> .plabel= l ε
%D A0 A4 -> .slide= -30pt .plabel= l ∀γ
%D B0 B1 <- sl^ .plabel= a Δ:=(∘!)
%D B0 B1 -> sl_ .plabel= b \lim:=\Ran_!
%D C0 C1 -> .plabel= a !
%D ))
%D enddiagram
%D
%D diagram kan-2-cells-prods
%D 2Dx 100 +30 +30
%D 2D 100 A1
%D 2D / \
%D 2D +30 A0 ---- A2
%D 2D
%D ren A0 A1 A2 ==> \catI \bm1 \catC
%D
%D ((
%D A0 A1 -> .plabel= a !
%D A1 A2 -> .curve= _10pt .plabel= m \lim_{\catI}D
%D A1 A2 -> .curve= ^20pt .plabel= a ∀X
%D A0 A2 -> .plabel= b D
%D A0 A2 midpoint relplace -4 -8 \Dn{ε}
%D A1 A2 midpoint relplace 2 -5 \Dn{∃!f}
%D ))
%D enddiagram
%D
$$\pu
\diag{kan-prods}
\qquad
\quad
\diag{kan-2-cells-prods}
$$
\newpage
\item Left adjoints are right Kan extensions. If
%
$$\catB \two/<-`->/<200>^L_R \catA$$
%
is an adjunction, then $(L,ε)$ is a right Kan extension of $\id_\catB$
along $R$. In a more compact notation, $L:=\Ran_R \id_\catB$ --- but
in this case we only know the action of $\Ran_R$ on the object
$\id_\catB$, and we don't know if this $\Ran_R$ can be extended to a
``real'' functor whose domain is the whole of $\catB^\catB$. The
diagram is:
%
%D diagram kan-adjoints
%D 2Dx 100 +40
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +20 A2 - A3
%D 2D |
%D 2D +20 A4
%D 2D
%D 2D +15 B0 = B1
%D 2D
%D 2D +15 C0 - C1
%D 2D
%D ren A0 A1 ==> GR ∀G
%D ren A2 A3 ==> LR L{:=}\Ran_R\id_\catB
%D ren A4 ==> \id_\catB
%D ren B0 B1 ==> \catB^\catB \catB^\catA
%D ren C0 C1 ==> \catB \catA
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l UR
%D A1 A3 -> .plabel= r ∃!U
%D A0 A3 harrownodes nil 20 nil <-|
%D A2 A3 <-|
%D A2 A4 -> .plabel= l ε
%D A0 A4 -> .slide= -20pt .plabel= l ∀V
%D B0 B1 <- sl^ .plabel= a (∘R)
%D B0 B1 -> sl_ .plabel= b \Ran_R
%D C0 C1 -> .plabel= a R
%D ))
%D enddiagram
%D
%D diagram kan-2-cells-adjoints
%D 2Dx 100 +30 +30
%D 2D 100 A1
%D 2D / \
%D 2D +30 A0 ---- A2
%D 2D
%D ren A0 A1 A2 ==> \catB \catA \catB
%D
%D ((
%D A0 A1 -> .plabel= a R
%D A1 A2 -> .curve= _10pt .plabel= m L
%D A1 A2 -> .curve= ^20pt .plabel= a ∀G
%D A0 A2 -> .plabel= b \id_\catB
%D A0 A2 midpoint relplace -4 -8 \Dn{ε}
%D A1 A2 midpoint relplace 2 -5 \Dn{∃!U}
%D ))
%D enddiagram
%D
$$\pu
\diag{kan-adjoints}
\qquad
\quad
\diag{kan-2-cells-adjoints}
$$
To show that this works we have to prove that $∀V.∃!U.(ε·UR=V)$. We
will do that by ``inverting the equation $ε·UR=V$'':
%
%D diagram kan-adjoints-solving-U
%D 2Dx 100 +20 +20 +20 +25 +20 +20 +20
%D 2D _________ ____ _________ ____
%D 2D | || | | || |
%D 2D 100 A0 - A1 - A2 - A3 = B0 - B1 B2 - B3
%D 2D |__________| |__________|
%D 2D
%D 2D ||
%D 2D _________ ____
%D 2D | || |
%D 2D +50 C0 - C1 - C2 C3
%D 2D |__________|
%D 2D
%D 2D
%D ren A0 A1 A2 A3 ==> \catA \catB \catA \catB
%D ren B0 B1 B2 B3 ==> \catA \catB \catA \catB
%D ren C0 C1 C2 C3 ==> \catA \catB \catA \catB
%D
%D (( A0 A1 -> .plabel= b L
%D A1 A2 -> .plabel= b R
%D A2 A3 -> .plabel= b L
%D A0 A2 -> .curve= ^25pt .plabel= a \id_A
%D A2 A3 -> .curve= ^24pt .plabel= a G
%D A1 A3 -> .curve= _25pt .plabel= b \id_B
%D A0 A2 midpoint relplace 0 -8 \Dn{η}
%D A2 A3 midpoint relplace 0 -6 \Dn{U}
%D A1 A3 midpoint relplace 0 7 \Dn{ε}
%D
%D A3 B0 midpoint relplace 0 0 =
%D
%D B0 B1 -> .plabel= b L
%D # B1 B2 -> .plabel= b R
%D B2 B3 -> .plabel= b L
%D B0 B2 -> .curve= ^25pt .plabel= a \id_A
%D B2 B3 -> .curve= ^24pt .plabel= a G
%D B1 B3 -> .curve= _25pt .plabel= b \id_B
%D B2 B3 midpoint relplace 0 -6 \Dn{U}
%D B1 B2 midpoint relplace 1 2 \Dn{\id_L}
%D
%D B3 relplace 20 0 =\;U
%D
%D A1 C2 midpoint relplace 0 2 \veq
%D
%D C0 C1 -> .plabel= b L
%D C1 C2 -> .plabel= b R
%D # C2 C3 -> .plabel= b L
%D C0 C2 -> .curve= ^25pt .plabel= a \id_A
%D C2 C3 -> .curve= ^24pt .plabel= a G
%D C1 C3 -> .curve= _25pt .plabel= b \id_B
%D C0 C2 midpoint relplace 0 -8 \Dn{η}
%D C2 C3 midpoint relplace 0 2 \Dn{V}
%D
%D C3 relplace 25 0 =\;VL·η
%D ))
%D enddiagram
%D
$$\pu
\diag{kan-adjoints-solving-U}
$$
%
The solution in $U:=VL·Gη$.
% (riep 5 "6.1._kan-extensions")
% (rie "6.1._kan-extensions")
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 13 233) "X. Kan Extensions")
% (find-cwm2page (+ 13 248) "7. All Concepts Are Kan Extensions")
% (find-books "__cats/__cats.el" "riehl")
% (find-riehlccpage (+ 18 209) "6.5. All concepts")
\end{enumerate}
% _ __ __ _
% | |/ /__ _ _ __ / _| ___ _ __ _ __ ___ _ _| | __ _
% | ' // _` | '_ \ | |_ / _ \| '__| '_ ` _ \| | | | |/ _` |
% | . \ (_| | | | | | _| (_) | | | | | | | | |_| | | (_| |
% |_|\_\__,_|_| |_| |_| \___/|_| |_| |_| |_|\__,_|_|\__,_|
%
% «kan-formula» (to ".kan-formula")
% (favp 38 "kan-formula")
% (fava "kan-formula")
\subsection{A formula for Kan extensions}
\label{kan-formula}
% (find-books "__cats/__cats.el" "maclane")
% (find-cwm2page (+ 13 236) "3. The Kan Extension")
% (find-books "__cats/__cats.el" "riehl")
% (find-riehlccpage (+ 18 193) "6.2. A formula for Kan extensions")
\def\piAHSet {\ton{π} \catA \ton{H} \Set}
\def\piAHSetmini{\ton{H∘π} \Set}
\def\pdiag #1{\left(\diag{#1}\right)}
The sections X.3 of \cite{CWM2} and 6.2 of \cite{Riehl} discuss a
formula for calculating Kan extensions, that defines $\Ran_FH$ as the
functor whose action on objects is:
%
$$B \mapsto \Lim(B{↓}F \piAHSet),$$
%
and its action on morphisms is ``obvious'' in the sense of Section
\ref{to-deserve-a-name}. I found this formula totally impossible to
understand until I finally found a way to visualize what it ``meant''.
For each object $B∈\catB$ the functor $B{↓}F \piAHSetmini$ can be
regarded as a diagram in $\Set$ whose shape is the shape of the comma
category $B{↓}F$. If $\catA$ and $\catB$ are finite preorder categories
and $F$ is an inclusion then $B{↓}F$ can ``inherit its shape'' from
$\catA$; inclusions of preorders are ``toy examples'' ``for
children'', but they give us some intuition to start with, and they
can help us understand the formal version that can handle more general
cases.
These are the diagrams for $\Ran_F$ as a right adjoint --- note that
we use $\Set$ instead of $\catC$ to make things less abstract,
%
% (favp 45 "kan-extensions")
% (fava "kan-extensions")
%
%D diagram kan-1
%D 2Dx 100 +35
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +25 A2 - A3
%D 2D
%D 2D +15 B0 = B1
%D 2D
%D 2D +15 C0 - C1
%D 2D
%D ren A0 A1 ==> GF G
%D ren A2 A3 ==> H \Ran_FH
%D ren B0 B1 ==> \Set^\catA \Set^\catB
%D ren C0 C1 ==> \catA \catB
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l V
%D A1 A3 -> .plabel= r U
%D A0 A3 harrownodes nil 20 nil <->
%D A2 A3 |->
%D A3 relplace 20 0 =R
%D B0 B1 <- sl^ .plabel= a ∘F
%D B0 B1 -> sl_ .plabel= b \Ran_F
%D C0 C1 -> .plabel= a F
%D ))
%D enddiagram
%D
$$\pu
\diag{kan-1}
\qquad
\begin{array}{l}
RB = \\
(\Ran_FH)B = \\
\Lim(B{↓}F \piAHSet) \\
\end{array}
$$
%
and here are some diagrams to help us understand the comma category
$B{↓}F$ --- in the compact notation its objects have names like
$(A,β)$, but in the more visual notation they are L-shaped diagrams:
%
%D diagram CommaObj
%D 2Dx 100 +20
%D 2D 100 \A
%D 2D
%D 2D +15 \B \C
%D 2D
%D # ren ==>
%D
%D (( \A \C -> .plabel= r \f
%D \B \C |->
%D ))
%D enddiagram
%D
\pu
\def\CommaObj#1#2#3#4{
\def\A{#1}
\def\f{#4}
\def\B{#2} \def\C{#3}
\left(\diag{CommaObj}\right)
}
%
\def\kancommaobj#1#2#3{\psm{  \\ #2 \\}}
%
%D diagram kan-comma
%D 2Dx 100 +20 +55 +45 +30 +25
%D 2D 100 A1
%D 2D +20 A2 - A3 C0 E0 - E1 - E2
%D 2D +20 A4 - A5 C1 E3 - E4 - E5
%D 2D
%D 2D +15 B0 - B1 D0 F0 - F1 - F2
%D 2D
%D ren A1 A2 A3 A4 A5 ==> B A FA A' FA'
%D ren B0 B1 ==> \catA \catB
%D ren D0 ==> B{↓}F
%D ren E0 E1 E2 ==> (A,β) A HA
%D ren E3 E4 E5 ==> (A',β') A' HA'
%D ren F0 F1 F2 ==> B{↓}F \catA \Set
%D
%D (( A1 A3 -> .plabel= r β
%D A2 A3 |->
%D A2 A4 -> .plabel= l α
%D A3 A5 -> .plabel= r Fα
%D A2 A5 harrownodes nil 20 nil |->
%D A4 A5 |->
%D A1 A5 -> .slide= 20pt .plabel= r \sm{β'=\\Fα∘β}
%D B0 B1 -> .plabel= a F
%D
%D C0 xy+= 0 -20
%D C1 xy+= 0 -5
%D C0 .tex= \CommaObj{B}{A}{FA}{β} BOX
%D C1 .tex= \CommaObj{B}{A'}{FA'}{β'} BOX
%D C0 C1 -> .plabel= l α
%D D0 place
%D
%D E0 E1 |-> E1 E2 |->
%D E0 E3 -> .plabel= l α
%D E1 E4 -> .plabel= m α
%D E2 E5 -> .plabel= r Hα
%D E0 E4 harrownodes nil 20 nil |->
%D E1 E5 harrownodes nil 20 nil |->
%D E3 E4 |-> E4 E5 |->
%D F0 F1 -> .plabel= a π
%D F1 F2 -> .plabel= a H
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{kan-comma}
$$
\newpage
\def\kancommaobj#1#2#3{\psm{  \\ #2 \\}}
Let's see an example.
%D diagram Kan_catA
%D 2Dx 100 +15
%D 2D 100 1 2
%D 2D +15 3 4
%D 2D +15 5 6
%D 2D
%D # ren 1 2 3 4 5 6 ==> 1' 2' 3' 4' 5' 6'
%D
%D (( 2 6 ->
%D 5 6 ->
%D
%D ))
%D enddiagram
%D
%D diagram Kan_catB
%D 2Dx 100 +15
%D 2D 100 1 2
%D 2D +15 3 4
%D 2D +15 5 6
%D 2D
%D ren 1 2 3 4 5 6 ==> 1' 2' 3' 4' 5' 6'
%D
%D (( 1 2 ->
%D 1 3 -> 2 4 ->
%D 3 4 ->
%D 3 5 -> 4 6 ->
%D 5 6 ->
%D ))
%D enddiagram
%D
%D
%D
%D diagram Kan_1'_down_F
%D 2Dx 100 +30
%D 2D 100 A1
%D 2D +15
%D 2D +15 A4 A5
%D 2D
%D ren A1 ==> \kancommaobj{1'}{2}{F2}
%D ren A4 A5 ==> \kancommaobj{1'}{5}{F5} \kancommaobj{1'}{6}{F6}
%D
%D (( A1 A5 ->
%D A4 A5 ->
%D ))
%D enddiagram
%D
%D diagram Kan_3'_down_F
%D 2Dx 100 +30
%D 2D 100 A1
%D 2D +15
%D 2D +15 A4 A5
%D 2D
%D ren A1 ==> \ph{\kancommaobj{3'}{2}{F2}}
%D ren A4 A5 ==> \kancommaobj{3'}{5}{F5} \kancommaobj{3'}{6}{F6}
%D
%D (( A1 place
%D A4 A5 ->
%D ))
%D enddiagram
%D
%D
%D
%D diagram Kan_1'_H
%D 2Dx 100 +20
%D 2D 100 A1
%D 2D +15
%D 2D +15 A4 A5
%D 2D
%D ren A1 ==> H_2
%D ren A4 A5 ==> H_5 H_6
%D
%D (( A1 A5 ->
%D A4 A5 ->
%D ))
%D enddiagram
%D
%D diagram Kan_3'_H
%D 2Dx 100 +20
%D 2D 100 A1
%D 2D +15
%D 2D +15 A4 A5
%D 2D
%D ren A1 ==> \ph{H_2}
%D ren A4 A5 ==> H_5 H_6
%D
%D (( A1 place
%D A4 A5 ->
%D ))
%D enddiagram
%D
\pu
If $\catA \ton{F} \catB$ is the inclusion $\pdiag{Kan_catA} →
\pdiag{Kan_catB}$,
\msk
then
$1'{↓}F = \pdiag{Kan_1'_down_F}$ and
$3'{↓}F = \pdiag{Kan_3'_down_F}$,
\msk
and $(1'{↓}F \piAHSetmini) = \pdiag{Kan_1'_H}$
and $(3'{↓}F \piAHSetmini) = \pdiag{Kan_3'_H}$;
\msk
so $R(1') = \Lim(1'{↓}F \piAHSetmini) = H_2 ×_{H_6} H_5$,
and $R(3') = \Lim(3'{↓}F \piAHSetmini) = H_5$.
We can follow the same pattern to calculate $R(2')$, $R(4')$, $R(5')$,
$R(6')$.
The square of the adjunction becomes this, in this particular case:
%
%D diagram Kan_A-shaped
%D 2Dx 100 +20
%D 2D 100 2
%D 2D +20
%D 2D +20 5 6
%D 2D
%D ren 2 5 6 ==> \A \B \C
%D
%D (( 2 6 ->
%D 5 6 ->
%D ))
%D enddiagram
%D
%D diagram Kan_B-shaped
%D 2Dx 100 +30
%D 2D 100 1 2
%D 2D +20 3 4
%D 2D +20 5 6
%D 2D
%D ren 1 2 3 4 5 6 ==> \A \B \C \D \E \F
%D
%D (( 1 2 ->
%D 1 3 -> 2 4 ->
%D 3 4 ->
%D 3 5 -> 4 6 ->
%D 5 6 ->
%D ))
%D enddiagram
%D
\pu
\def\KanAShaped#1#2#3{
\def\A{#1}
\def\B{#2}
\def\C{#3}
\pdiag{Kan_A-shaped}
}
\def\KanBShaped#1#2#3#4#5#6{
\def\A{#1}
\def\B{#2}
\def\C{#3}
\def\D{#4}
\def\E{#5}
\def\F{#6}
\pdiag{Kan_B-shaped}
}
%
%D diagram kanadjsquare-generic
%D 2Dx 100 +25
%D 2D 100 A0 - A1
%D 2D | |
%D 2D +25 A2 - A3
%D 2D
%D 2D +15 B0 = B1
%D 2D
%D 2D +15 C0 - C1
%D 2D
%D ren A0 A1 ==> GF G
%D ren A2 A3 ==> H \Ran_FH
%D ren B0 B1 ==> \Set^\catA \Set^\catB
%D ren C0 C1 ==> \catA \catB
%D
%D (( A0 A1 <-|
%D A0 A2 -> # .plabel= l V
%D A1 A3 -> # .plabel= r U
%D A0 A3 harrownodes nil 20 nil <->
%D A2 A3 |->
%D A3 relplace 20 0 =R
%D # B0 B1 <- sl^ .plabel= a ∘F
%D # B0 B1 -> sl_ .plabel= b \Ran_F
%D # C0 C1 -> .plabel= a F
%D ))
%D enddiagram
%D
%D diagram kanadjsquare-example
%D 2Dx 100 +70
%D 2D 100 A0 A1
%D 2D
%D 2D +65 A2 A3
%D 2D
%D (( A0 .tex= \KanAShaped{G_2}{G_5}{G_6} BOX
%D A1 .tex= \KanBShaped{G_1}{G_2}{G_3}{G_4}{G_5}{G_6} BOX
%D A2 .tex= \KanAShaped{H_2}{H_5}{H_6} BOX
%D A3 .tex= \KanBShaped{H_2{×_{H_6}}H_5}{H_2}{H_5}{H_6}{H_5}{H_6} BOX
%D ))
%D (( A0 A1 <-|
%D A0 A2 ->
%D A1 A3 ->
%D A0 A3 harrownodes nil 20 nil <->
%D A2 A3 |->
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{kanadjsquare-generic}
\qquad
\diag{kanadjsquare-example}
$$
\newpage
% _____ _ _ _
% | ___| _ _ __ ___| |_ ___ _ __ ___ __ _ ___ ___ | |__ (_)___
% | |_ | | | | '_ \ / __| __/ _ \| '__/ __| / _` / __| / _ \| '_ \| / __|
% | _|| |_| | | | | (__| || (_) | | \__ \ | (_| \__ \ | (_) | |_) | \__ \
% |_| \__,_|_| |_|\___|\__\___/|_| |___/ \__,_|___/ \___/|_.__// |___/
% |__/
% «functors-as-objects» (to ".functors-as-objects")
% (favp 50 "functors-as-objects")
% (fava "functors-as-objects")
\subsection{Functors as objects \DONE}
\label{functors-as-objects}
One way to treat a diagram in $\Set$ like this
%
%D diagram evil-presheaf
%D 2Dx 100 +20 +20
%D 2D 100 A0
%D 2D / \
%D 2D +20 A1 A2
%D 2D \ /
%D 2D +20 A3
%D 2D |
%D 2D +20 A4
%D 2D
%D ren A0 A1 A2 A3 A4 ==> \{24,25\} \{1\} \{2,3\} \{1\} \{0,1\}
%D
%D (( A0 A1 ->
%D A0 A2 -> .plabel= r \sm{24↦2\\25↦2}
%D A1 A3 ->
%D A2 A3 ->
%D A3 A4 -> .plabel= r 1↦1
%D ))
%D enddiagram
%D
\pu
$$
F \qquad := \qquad \diag{evil-presheaf}
$$
%
as a functor is to think that that diagram is an abbreviation --- it
is just the upper-right part of a diagram like this,
%
%R local kite =
%R 1/ 1 \
%R |2 3|
%R | 4 |
%R \ 5 /
%R MixedPicture.__index.
%R arrows = function (mp, w) return (mp.ar or mp.zha):arrows(w) end
%R kite:tozmp({zdef="kitewitharrows", meta="p", scale="20pt"})
%R :addcells()
%R :addarrows()
%R :output()
\pu
% $$\zha{kitewitharrows}$$
%
%D diagram evil-presheaf-as-functor
%D 2Dx 100 +75
%D 2D 100 A0 A1
%D 2D
%D 2D +50 A2 A3
%D 2D
%D ren A0 ==> \zha{kitewitharrows}
%D ren A2 A3 ==> \catK \Set
%D
%D (( A1 .tex= \left(\diag{evil-presheaf}\right) BOX
%D A0 A1 |->
%D A2 A3 -> .plabel= a F
%D ))
%D enddiagram
%D
$$\pu
\diag{evil-presheaf-as-functor}
$$
%
where we add the extra hint that the index category $\catK$ is exactly
the kite-shaped preorder category drawn above the ``$\catK$''.
The convention (CFSh) says that the image by a functor of a diagram is
a diagram with the same shape, so according to that convention we have
$F(1) = \{24,25\}$, $F(4→5) = (\{1\} \ton{1↦1} \{0,1\})$, and so
on; so the upper right part of the diagram above {\sl defines} $F$.
Note that the single `$↦$' above the $\catK \ton{F} \Set$ stands for
several `$↦$'s, one for each object and one for each morphism, and
note that $F$ is an object of $\Set^\catK$.
% ____ __ __ __ _ _ _ _
% / ___| \/ |___ / _| ___ _ __ ___| |__ (_) | __| |_ __ ___ _ __
% | | _| |\/| / __| | |_ / _ \| '__| / __| '_ \| | |/ _` | '__/ _ \ '_ \
% | |_| | | | \__ \ | _| (_) | | | (__| | | | | | (_| | | | __/ | | |
% \____|_| |_|___/ |_| \___/|_| \___|_| |_|_|_|\__,_|_| \___|_| |_|
%
% «gms-for-children» (to ".gms-for-children")
% (favp 38 "gms-for-children")
% (fava "gms-for-children")
\subsection{Geometric morphisms for children \DONE}
\label{gms-for-children}
Let $\catA$ and $\catB$ be these preorder categories, and let
$f:\catA→\catB$ be the inclusion functor from $\catA$ to $\catB$:
%
$$
A := \pshAargs2345
\qquad
B := \pshBargs123456
$$
The left half of the diagram below is the standard definition of a
geometric morphism $f$ from a topos $\calE$ to a topos $\calF$. A
geometric morphism $f:\calE→\calF$ is actually an adjunction $f^*⊣f_*$
plus the guarantee that $f^*:\calE \ot \calF$ preserves limits, which
is a condition slightly weaker than requiring that $f^*$ has a left
adjoint. When that left adjoint exists it is denoted by $f^!$, and we
say that $f^!⊣f^*⊣f_*$ is an {\sl essential geometric morphism}. The
only non-standard thing about the diagram at the left below is that is
contains an internal view of the adjunction $f^*⊣f_*$.
%
$$
\diag{gm-for-adults}
\qquad
\def\LG{\pshAargs{G_2}{G_3}{G_4}{G_5}}
\def\G {\pshBargs{G_1}{G_2}{G_3}{G_4}{G_5}{G_6}}
\def\H {\pshAargs{H_2}{H_3}{H_4}{H_5}}
\def\RH{\pshBargs{H_2{×_{H_4}}H_3}{H_2}{H_3}{H_4}{H_5}{1}}
\diag{gm-for-children}
$$
The right half of the diagram is a particular case of the left half.
Its lower line, $\catA \ton{f} \catB$, does not exist in the left
half. The inclusion functor $f$ induces adjunctions $f^!⊣f^*⊣f_*$ as
this,
%
%D diagram essential-GM-small
%D 2Dx 100 +35
%D 2D 100 A B
%D 2D
%D 2D +20 A0 B0
%D 2D
%D ren A B ==> \Set^\catA \Set^\catB
%D ren A0 B0 ==> \catA \catB
%D
%D (( A B -> sl^^ .plabel= a f^!
%D A B <- .plabel= m f^*
%D A B -> sl__ .plabel= b f_*
%D A0 B0 -> .plabel= a f
%D ))
%D enddiagram
%D
$$\pu
\diag{essential-GM-small}
$$
%
where $f^*$ is easy to define and $f^!$ and $f_*$ not so much --- the
standard way to define $f^!$ and $f_*$ is by Kan extensions.
The big square in the upper part of the diagram is an internal view of
the adjunction $f^*⊣f_*$, with the functors $f^*G$, $G$, $H$, and
$f_*H$ being displayed as their internal views. We can choose the sets
$G_1, \ldots, G_6$ and the morphisms between them arbitrarily, so this
is an internal view of an arbitrary functor $G:\catB→\Set$; and the
same for $H$.
The arrow $f^*G \mapsot G$ can be read as a definition for the action
of $f^*$ on objects --- it just erases some parts of the diagram ---
and the arrow $H \mapsto f_*H$ can be read as a definition for the
action of $f_*$ on objects --- $f_*$ ``reconstructs'' $H_1$ and $H_6$
in a certain natural way. It is easy to reconstruct the actions of
$f^*$ and $f_*$ on morphisms from just what is shown, and to
reconstruct the two directions of the bijection.
The big diagram above can be used 1) to convince people that are not
hardcore toposophers that this diagrammatic language can make some
difficult categorical concepts more accessible, and 2) as a starting
point to generate diagrams ``for children'' for several parts of the
Elephant, and even to prove new theorems on toposes. For more on (1),
see \cite{OchsLucatelli} and \cite{OchsVGMS2018}; for (2), see
\cite{MDE}.
% ____ _ _ _ _ _
% | _ \ ___ __ _ __| (_)_ __ __ _ ___| | ___ _ __ | |__ __ _ _ __ | |_
% | |_) / _ \/ _` |/ _` | | '_ \ / _` | / _ \ |/ _ \ '_ \| '_ \ / _` | '_ \| __|
% | _ < __/ (_| | (_| | | | | | (_| | | __/ | __/ |_) | | | | (_| | | | | |_
% |_| \_\___|\__,_|\__,_|_|_| |_|\__, | \___|_|\___| .__/|_| |_|\__,_|_| |_|\__|
% |___/ |_|
%
% «reading-the-elephant» (to ".reading-the-elephant")
\subsection{Reading the Elephant \DONE}
\label{reading-the-elephant}
In Section \ref{teaching-adjunctions} we saw a strategy for helping
(beginner) students to read a difficult text on CT: we start with
diagrams for the most important concepts, in both a general case ``for
adults'' and a well-chosen particular case ``for children'', we give
them exercises to make sure that they understand the constructions in
the case ``for children'', we give them a few more exercises to make
sure that they understand the general case, we ask them to read
excerpts from a standard textbook in a version where the letters were
changed to match the diagrams, and then we ask them to work on the
original version of these excerpts with the original notation, and on
some other parts of the same chapter... this can be done for the
Elephant too --- here are the parts that are more relevant for our
diagrams on geometric morphisms, with the notation adjusted:
\begin{quotation}
% (find-books "__cats/__cats.el" "johnstone-elephant")
% (elep 7 "elephant-A4.1.1")
% (ele "elephant-A4.1.1")
% (find-elephanttext (+ 17 161))
% (find-elephantpage (+ 17 161) "A4 Geometric Morphisms - Basic Theory")
% (find-elephantpage (+ 17 161) "Definition 4.1.1")
{\bf Definition 4.1.1.} (a) Let $\calF$ and $\calE$ be toposes. A
geometric morphism $f: \calE → \calF$ consists of a pair of functors
$f_*: \calE → \calF$ (the direct image of f) and $f^*: \calF →
\calE$ (the inverse image of $f$) together with an adjunction ($f^*
⊣ f_*$), such that $f^*$ is cartesian (i.e. preserves finite
limits).
\msk
(...)
\msk
% (elep 7 "elephant-A4.1.4")
% (ele "elephant-A4.1.4")
% (find-elephanttext (+ 17 163))
% (find-elephantpage (+ 17 163) "Example 4.1.4")
{\bf Example 4.1.4.} Let $f: \catA → \catB$ be a functor between
small categories. Then composition with $f$ defines a functor $f^*:
\Set^\catB→\Set^\catA$, which has adjoints on both sides, the left
and right {\sl Kan extensions} along $f$: for example, the right Kan
extension $\Ran_f$ sends a functor $H: \Set^\catA$ to the functor
whose value at an object $B$ of $\catB$ is the limit of the diagram
%
% (find-es "xypic" "two-and-three")
$$ (B ↓ f) \diagxyto/->/^U \catA \diagxyto/->/^H \Set $$
%
(here $(B ↓ f)$ is the comma category whose objects are pairs
$(A,ϕ)$ with $ϕ:B→fA$ in $\catB$, and $U$ is the forgetful functor
from this category to $\catA$). Thus $f^*$ is the inverse image of a
geometric morphism $\Set^\catA → \Set^\catB$, whose direct image is
$\Ran_f$.
\msk
(...)
\msk
% (find-elephantpage (+ 17 164) "We note that the geometric morphisms")
We note that the geometric morphisms which arise as in 4.1.4, though
not as special as those of 4.1.2, still have the property that their
inverse image functors have left adjoints as well as right adjoints.
We call a geometric morphism $f$ {\it essential} if it has this
property; we normally write $f_!$ for the left adjoint of $f^*$.
With the aid of this notion, we can prove a partial converse to
4.1.4:
\ssk
% (elep 8 "elephant-A4.1.5")
% (ele "elephant-A4.1.5")
% (find-elephanttext (+ 17 164))
% (find-elephantpage (+ 17 164) "Lemma 4.1.5")
{\bf Lemma 4.1.5.} Let $\catA$ and $\catB$ be small categories such
that $\calB$ is Cauchy-complete (cf.\ 1.1.10). Then every essential
geometric morphism $f: \Set^\catA → \Set^\catB$ is induced as in
4.1.4 by a functor $\catA → \catB$.
\msk
(...)
\msk
% (elep 9 "elephant-A4.2.8")
% (ele "elephant-A4.2.8")
% (find-elephantpage (+ 17 182) "Proposition 4.2.8")
{\bf Proposition 4.2.8.} With the notation established above, the counit
$h^*h_*→1$ is an isomorphism.
(...)
A geometric morphism $h$ satisfying the condition that the counit
$h^*h_*→1$ is an isomorphism, or the equivalent condition that $h_*$
is full and faithful, is called an {\sl inclusion} (though some
authors prefer the term {\sl embedding}). We shall study inclusions
in greater detail in the next three sections; for the present, we
digress briefly to note an alternative characterization of them:
% (find-elephantpage (+ 1104 69) "General Index" "Sheafification")
% (elep 15 "elephant-A4.5.2")
% (ele "elephant-A4.5.2")
% (elep 16 "elephant-A4.6.2")
% (ele "elephant-A4.6.2")
\end{quotation}
The really interesting part would be to show that the unit $η$ of the
adjunction $f^*⊣f_*$ ``is'' a sheafification functor, and that the
geometric morphism for children of the diagram yields an example of
sheaf... but that would need lots of different fragments from several
different sections of the book.
% _ __ _ _ _ ___
% / \ _ __ __ _ _ __ ___ ___ / _| ___ _ __ | |_| |__ (_)__|__ \
% / _ \ | '_ \ / _` | '_ ` _ \ / _ \ | |_ / _ \| '__| | __| '_ \| / __|/ /
% / ___ \ | | | | (_| | | | | | | __/ | _| (_) | | | |_| | | | \__ \_|
% /_/ \_\ |_| |_|\__,_|_| |_| |_|\___| |_| \___/|_| \__|_| |_|_|___(_)
%
% «how-to-name-this-language» (to ".how-to-name-this-language")
\section{How to name this diagrammatic language \DONE}
\label{how-to-name-this-language}
{\sl I don't have any idea!...}
It can be used to produce missing diagrams, and sometimes these
missing diagrams are skeletons. We can use it to work in two styles in
parallel, ``for adults'' and ``for children''... maybe something like
``Missing Skeletons for Children''?
\msk
Suggestions welcome.
% __ ___ _ _ _ _
% \ \ / / |__ _ _ ( | )_ __ ___ _ _ ___ ___ _ ____ _____( | )
% \ \ /\ / /| '_ \| | | | V V| '_ ` _ \| | | | / __/ _ \| '_ \ \ / / __|V V
% \ V V / | | | | |_| | | | | | | | |_| | | (_| (_) | | | \ V /\__ \
% \_/\_/ |_| |_|\__, | |_| |_| |_|\__, | \___\___/|_| |_|\_/ |___/
% |___/ |___/
%
% «why-my-conventions» (to ".why-my-conventions")
% (favp 46 "why-my-conventions")
% (fava "why-my-conventions")
\section{Why ``my conventions''? \DONE}
\label{why-my-conventions}
I learned CT as an autodidact in a totally disorganized way. In the
first years I just read, or rather {\sl tried} to read, everything
that was available in my university's library, trying to locate the
parts that could be useful to my main interest at that time, that was
Non-Standard Analysis and how to do something similar to NSA but using
filter-powers instead of ultrapowers...
It was only after that that I realized that I had to learn how to {\sl
write}. I remember one time spending a whole evening on an exercise
of the beginning of \cite{LambekScott} that says just ``prove that for
categories $\catA$, $\catB$, and $\catC$ we have $\catA^{\catB×\catC}
≅ (\catA^\catB)^\catC$'' --- the full proof had lots of parts, and I
saw that I didn't know how to organize them in a neat way... also, the
proofs given in books and articles just state the main parts and
pretend that the rest is obvious, and in the case of
$\catA^{\catB×\catC} ≅ (\catA^\catB)^\catC$ there were no ``main
parts'', so I had to learn how to write down a proof in full, and this
was a new style to me...
Even now, many years after that, I still have the sensation that I had
to improvise practically everything in my ways --- both the
``algebraic'' way and the ``diagrammatic'' way --- of writing
categorical proofs, and that I still don't know even a tiny fraction
of the techniques for writing that people learn when they take CT
courses and they have opportunities to discuss exercises with other
students and with TAs and more senior people...
\msk
{\sl The ``my conventions'' in the title of this text, and my use of
the first person everywhere, are a way to stress that I still don't
know enough about other people's private languages for CT, and that
this is an attempt to gain access to other private languages,
diagrammatic or not... I am especially interested in how people
write when they turn their level-of-detail knob to a very high
position.}
% It is difficult to publish material about diagrammatic languages
% that are more for {\sl visualition} and {\sl intuition} (see
% \cite{KromerSlides}) than for {\sl proving things}. The handwritten
% notes in \cite{MacLaneNotes} for a course given by MacLane taken by
% one of his students indicate that when he wasn't constrained by what
% could be printed easily he would use several kinds of diagrams that
% are not in \cite{CWM2}. I guess that Freyd and Scedrov have
% experimented with many variants of the languages in \cite{Freyd76}
% and \cite{FreydScedrov} that they never published...
% ____ _ _ _ _
% | _ \ ___| | __ _| |_ ___ __| | __ _____ _ __| | __
% | |_) / _ \ |/ _` | __/ _ \/ _` | \ \ /\ / / _ \| '__| |/ /
% | _ < __/ | (_| | || __/ (_| | \ V V / (_) | | | <
% |_| \_\___|_|\__,_|\__\___|\__,_| \_/\_/ \___/|_| |_|\_\
%
% «related-and-unrelated» (to ".related-and-unrelated")
% (favp 47 "related-and-unrelated")
% (fava "related-and-unrelated")
\section{Related and unrelated work \DONE}
\label{related-and-unrelated}
% (find-books "__cats/__cats.el" "coecke")
% (find-books "__cats/__cats.el" "coecke-newstrup")
% (find-books "__cats/__cats.el" "marsden-ctusd")
The diagrammatic language that I described here seems to be unrelated
to the ones in \cite{CoeckePQP} and \cite{CoeckeNewStruP} --- that
describe {\sl lots} of diagrammatic languages --- and also unrelated
to \cite{MarsdenCTUSD}. We lower the level of abstraction --- see for
example Section \ref{2-category-of-cats} --- while they (usually)
raise it.
% (find-books "__cats/__cats.el" "caccamo-winskel")
I've taken an approach that is the opposite of \cite{CaccamoWinskel}
and \cite{CaccamoPhD}. Cáccamo and Winskel define a derivation system
that can only construct functors, natural transformations, etc, that
obey the expected naturality conditions, while we allow some kinds of
sloppinesses, like constructing something that looks like a functor
and pretending that it is a functor when it may not be. When I started
working on this diagrammatic language I had a companion derivation
system for it; \cite[Section 14]{IDARCT} mentions it briefly, but it
doesn't show the introduction rules that create (proto)functors and
(proto)natural transformations and that allow being sloppy (``in the
syntactical world'').
% (find-books "__phil/__phil.el" "corfield")
% (find-books "__cats/__cats.el" "kromer")
% (find-books "__cats/__cats.el" "kromer-slides")
% (find-books "__cats/__cats.el" "cheng-morally")
Some of my excuses for allowing one to pretend that a functor is a
functor and leaving the verification to a second stage come from
\cite{ChengMorally}. I learned a {\sl lot} on how mathematicians use
intuition and diagrams from \cite{Kromer} --- \cite{KromerSlides} is a
great summary --- and \cite{Corfield}, and they have helped me to
identify which characteristics of my diagrammatic language are very
unusual and may be new, and that deserve to be presented in detail.
% (find-idarctpage 19 "14. Preservations, Frobenius, Beck-Chevalley")
% (find-idarcttext 19 "14. Preservations, Frobenius, Beck-Chevalley")
Many of the first ideas for my diagrammatic language appeared when I
was reading \cite{SeelyBeck}, \cite{SeelyLCCC}, \cite{SeelyPLC},
\cite{Jacobs}, and \cite{SeelyDiff} and trying to draw the ``missing
diagrams'' in those papers in both the original notation and in the
``archetypal case'' (\cite[Section 16]{IDARCT}).
% (find-idarctpage 23 "16. Archetypal Models")
% (find-idarcttext 23 "16. Archetypal Models")
% __ ___ _ _
% \ \ / / |__ __ _| |_ _ __ _____ _| |_
% \ \ /\ / /| '_ \ / _` | __| | '_ \ / _ \ \/ / __|
% \ V V / | | | | (_| | |_ | | | | __/> <| |_
% \_/\_/ |_| |_|\__,_|\__| |_| |_|\___/_/\_\\__|
%
% «what-next» (to ".what-next")
% (favp 47 "what-next")
% (fava "what-next")
\section{What next? \DONE}
\label{what-next}
At this point I think that it is more interesting to ``implement''
more categorical definitions and proofs in this diagrammatic language
than to try to formalize it completely or try to prove meta-theorems
about it. I am doing that by (re)reading parts of several papers and
articles and drawing the missing diagrams in them; for details and
links, see:
\msk
\centerline{\url{http://angg.twu.net/math-b.html\#favorite-conventions}}
\msk
Besides this, here's what I've planned for the next steps. Most of
them can be done in parallel.
\begin{enumerate}
\item Now there are several very good books on CT for beginners with
lots of diagrams --- for example \cite{FongSpivak}, \cite{Perrone},
and \cite{MilewskiCTFPOCaml}. I want to try do draw the ``missing
diagrams'' for some of their sections, show them to some people, and
see if they find them useful.
\item I need to learn more Idris and Idris-ct --- and then 1) draw the
missing diagrams for some of the modules in the Idris-ct sources (as
a visual guide for the names of the data structures and their
fields), 2) implement some of my diagrams on Idris-ct; a column with
Idris-ct code would be a nice addition to, for example, Section
\ref{basic-example-full}.
\item The paper \cite{PH2} that I uploaded to Arxiv is a kind of
``Sheaves for Children'', and some philosopher friends of mine who
study Alain Badiou --- who uses toposes and sheaves in books like
\cite{BadiouLoW} and \cite{BadiouMoTT} --- expressed a lot of
interest in it... the first six sections of \cite{PH2} are
impeccable (I think!) but the last ones, that are the ones that
involve categories, were written in a hurry. I need to rewrite them
using techniques like the ones in Section \ref{teaching-adjunctions}
to turn them into something like a ``Let's read some sections of
\cite{Elephant1} and \cite{Riehl} --- an illustrated guide''...
until I finish that I can't advertise \cite{PH2}, I am too
embarassed by its last sections.
\end{enumerate}
% (find-books "__cats/__cats.el" "fong-spivak")
% (find-books "__cats/__cats.el" "milewski-ctfp")
% (find-books "__cats/__cats.el" "perrone")
% (find-books "__cats/__cats.el" "sobocinski")
\newpage
% (find-dednat6file "demo-write-dnt.tex")
%L write_dnt_file()
\pu
% ____ __
% | _ \ ___ / _| ___ _ __ ___ _ __ ___ ___ ___
% | |_) / _ \ |_ / _ \ '__/ _ \ '_ \ / __/ _ \/ __|
% | _ < __/ _| __/ | | __/ | | | (_| __/\__ \
% |_| \_\___|_| \___|_| \___|_| |_|\___\___||___/
%
% «references» (to ".references")
% (favp 40 "references")
% (fava "references")
%\section{references}
%\label{references}
% (find-LATEXfile "" "2020favorite-conventions.bbl")
% (find-LATEXfile "2020favorite-conventions.bbl")
\printbibliography
\end{document}
% «elisp» (to ".elisp")
(progn
(define-key eev-mode-map "\M-Z" 'eewrap-section)
(defun eewrap-section () (interactive)
(ee-this-line-wrapn 1 'ee-wrap-section))
(defun ee-wrap-section (tag)
"An internal function used by `ee-wrap-section'."
(ee-template0 (ee-tolatin1 "\
{tag}
% <{tag}>
\\section{<}{tag}{>}
\\label{<}{tag}{>}
")))
)
% __ __ _ __ _
% | \/ | __ _| | _____ / _| ___ _ __ __ _ _ ____ _(_)_ __
% | |\/| |/ _` | |/ / _ \ | |_ / _ \| '__| / _` | '__\ \/ / \ \ / /
% | | | | (_| | < __/ | _| (_) | | | (_| | | > <| |\ V /
% |_| |_|\__,_|_|\_\___| |_| \___/|_| \__,_|_| /_/\_\_| \_/
%
% «make-for-arxiv» (to ".make-for-arxiv")
% (find-build-for-arxiv-links "2020favorite-conventions")
% (find-LATEX "2020favorite-conventions.tex" "make-for-arxiv")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/LATEX/
#export PATH=/usr/local/texlive/2016/bin/x86_64-linux:$PATH
export PATH=/usr/local/texlive/2019/bin/x86_64-linux:$PATH
#export PATH=/usr/local/bin:$PATH
which biber
biber --version
make -f 2019.mk STEM=2020favorite-conventions veryclean
lualatex 2020favorite-conventions.tex
biber 2020favorite-conventions
pdflatex -record 2020favorite-conventions.tex
# (find-LATEXfile "2020favorite-conventions.fls" "biblatex/")
cd ~/LATEX/
flsfiles-zip 2020favorite-conventions.fls 2020favorite-conventions.zip
rm -rfv /tmp/2020favorite-conventions.zip
rm -rfv /tmp/edrx-latex/
cd /tmp/
cp -v ~/LATEX/2020favorite-conventions.zip .
mkdir /tmp/edrx-latex/
unzip -d /tmp/edrx-latex/ /tmp/2020favorite-conventions.zip
cd /tmp/edrx-latex/
pdflatex 2020favorite-conventions.tex
pdflatex 2020favorite-conventions.tex
cp -v 2020favorite-conventions.pdf /tmp/
# (find-fline "/tmp/edrx-latex/")
# (find-fline "/tmp/edrx-latex/2020favorite-conventions.bbl" "bbl format version")
# (find-pdf-page "/tmp/edrx-latex/2020favorite-conventions.pdf")
# (find-pdf-text "/tmp/edrx-latex/2020favorite-conventions.pdf")
# (find-fline "/tmp/2020favorite-conventions.zip")
% ----------------------------------------
% Old:
%
% (find-es "arxiv" "jop-arxiv")
% (find-es "arxiv" "biblatex-git-3.6")
% (find-es "arxiv" "biblatex-git-3.7")
% (find-es "arxiv" "biber-git-2.6")
% (find-es "arxiv" "biber-git-2.7")
% (find-es "arxiv" "biblatex-git-uninstall")
% (find-es "arxiv" "biber-git-uninstall")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/LATEX/
#export PATH=/usr/local/texlive/2016/bin/x86_64-linux:$PATH
export PATH=/usr/local/texlive/2017/bin/x86_64-linux:$PATH
#export PATH=/usr/local/bin:$PATH
biber --version
make -f 2019.mk STEM=2020favorite-conventions veryclean
make -f 2019.mk STEM=2020favorite-conventions pdf
pdflatex -record 2020favorite-conventions.tex
# (find-LATEXfile "2020favorite-conventions.fls" "biblatex/")
cd ~/LATEX/
flsfiles-zip 2020favorite-conventions.fls 2020favorite-conventions.zip
rm -rfv /tmp/2020favorite-conventions.zip
rm -rfv /tmp/edrx-latex/
cd /tmp/
cp -v ~/LATEX/2020favorite-conventions.zip .
mkdir /tmp/edrx-latex/
unzip -d /tmp/edrx-latex/ /tmp/2020favorite-conventions.zip
cd /tmp/edrx-latex/
pdflatex 2020favorite-conventions.tex
pdflatex 2020favorite-conventions.tex
# (find-fline "/tmp/edrx-latex/")
# (find-fline "/tmp/edrx-latex/2020favorite-conventions.bbl" "bbl format version")
# (find-pdf-page "/tmp/edrx-latex/2020favorite-conventions.pdf")
# (find-pdf-text "/tmp/edrx-latex/2020favorite-conventions.pdf")
# (find-fline "/tmp/2020favorite-conventions.zip")
% __ __ _
% | \/ | __ _| | _____
% | |\/| |/ _` | |/ / _ \
% | | | | (_| | < __/
% |_| |_|\__,_|_|\_\___|
%
% «make» (to ".make")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2020favorite-conventions veryclean
make -f 2019.mk STEM=2020favorite-conventions pdf
#
# optional:
pdflatex -record 2020favorite-conventions.tex
% Local Variables:
% coding: utf-8-unix
% modes: (latex-mode fundamental-mode emacs-lisp-mode)
% ee-tla: "fav"
% End: