|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2020riehl.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020riehl.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2020riehl.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020riehl.pdf"))
% (defun e () (interactive) (find-LATEX "2020riehl.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020riehl"))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (find-pdf-page "~/LATEX/2020riehl.pdf")
% (find-sh0 "cp -v ~/LATEX/2020riehl.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2020riehl.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2020riehl.pdf
% file:///tmp/2020riehl.pdf
% file:///tmp/pen/2020riehl.pdf
% http://anggtwu.net/LATEX/2020riehl.pdf
% (find-LATEX "2019.mk")
% «.title» (to "title")
% «.2.2.9._matrices» (to "2.2.9._matrices")
% «.2.3._univ-props-and-elts» (to "2.3._univ-props-and-elts")
% «.2.3.4._example-Zx» (to "2.3.4._example-Zx")
% «.2.3.7._example-bilin» (to "2.3.7._example-bilin")
% «.2.4._cat-of-elements» (to "2.4._cat-of-elements")
% «.4._adjunctions» (to "4._adjunctions")
% «.4.5.2._RAPL» (to "4.5.2._RAPL")
% «.6.1._kan-extensions» (to "6.1._kan-extensions")
\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\usepackage{colorweb} % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof} % For derivation trees ("%:" lines)
\input diagxy % For 2D diagrams ("%D" lines)
\xyoption{curve} % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx15} % (find-LATEX "edrx15.sty")
\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
%
% (find-es "tex" "geometry")
%\usepackage[a4paper,landscape]{geometry}
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
\def\Lan{\text{Lan}}
\def\Ran{\text{Ran}}
\def\sfC{\mathsf{C}}
\def\sfD{\mathsf{D}}
\def\sfE{\mathsf{E}}
\def\sfSet{\mathsf{Set}}
\def\Dn{\Downarrow}
\def\nameof#1{\ulcorner#1\urcorner}
% «title» (to ".title")
{\setlength{\parindent}{0em}
\footnotesize
Notes on Emily Riehl's ``Categories in Context'' (2016):
\url{http://www.math.jhu.edu/~eriehl/}
\url{http://www.math.jhu.edu/~eriehl/context/}
\url{http://www.math.jhu.edu/~eriehl/context.pdf}
\ssk
These notes are at:
\url{http://anggtwu.net/LATEX/2020riehl.pdf}
\ssk
See:
\url{http://anggtwu.net/LATEX/2020favorite-conventions.pdf}
\url{http://anggtwu.net/math-b.html\#favorite-conventions}
I wrote these notes mostly to test if the conventions above
are good enough.
}
\newpage
% (find-books "__cats/__cats.el" "riehl")
% (find-riehlccpage (+ 18 36) "1.6. The art of the diagram chase")
% (find-riehlccpage (+ 18 40) "equational reasoning")
% (find-riehlccpage (+ 18 44) "1.7. The 2-category of categories")
% (find-riehlcctext (+ 18 44) "1.7. The 2-category of categories")
% (find-riehlccpage (+ 18 55) "2.2. The Yoneda lemma")
% (find-riehlcctext (+ 18 55) "2.2. The Yoneda lemma")
% (find-riehlccpage (+ 18 57) "Theorem 2.2.4 (Yoneda lemma)")
% (find-riehlcctext (+ 18 57) "Theorem 2.2.4 (Yoneda lemma)")
\section*{2.2. The Yoneda Lemma}
% __ __ _ _
% | \/ | __ _| |_ _ __(_) ___ ___ ___
% | |\/| |/ _` | __| '__| |/ __/ _ \/ __|
% | | | | (_| | |_| | | | (_| __/\__ \
% |_| |_|\__,_|\__|_| |_|\___\___||___/
%
% «2.2.9._matrices» (to ".2.2.9._matrices")
% (riep 2 "2.2.9._matrices")
% (rie "2.2.9._matrices")
\subsection*{2.2.9. Corollary: matrices}
% (find-books "__cats/__cats.el" "riehl-matrices")
% (find-riehlmatricespage)
% (find-riehlccpage (+ 18 60) "Corollary 2.2.9. Every row operation")
% (find-riehlcctext (+ 18 60) "Corollary 2.2.9. Every row operation")
(Page 60)
Corollary 2.2.9. Every row operation on matrices with n rows is
defined by left multiplication by some $n×n$ matrix, namely the
matrix obtained by performing the row operation on the identity
matrix.
\msk
She gave a presentation about this in the Tutorial Day of the ACT2020:
\url{http://www.math.jhu.edu/~eriehl/matrices.pdf}
\url{https://www.youtube.com/watch?v=SsgEvrDFJsM}
\def\Vect{\mathbf{Vect}}
\def\Mat {\mathsf{Mat}}
\def\Objs{\mathsf{Objs}}
\def\matrices#1#2{\{\,\text{$#1×#2$ -matrices}\,\}}
\msk
Let $\Mat$ be the category that has:
$\Objs(\Mat) = \{1,2,3,\ldots\}$,
$\Hom_\Mat(k,m) = \Mat(k,m) = \matrices m k$,
and composition like this:
%
%D diagram yoneda-matrices-comp
%D 2Dx 100 +20 +20 +20 +20 +20
%D 2D 100 A0 A1 A2 B0 B1 B2
%D 2D
%D 2D +20
%D 2D
%D ren A0 A1 A2 ==> n m k
%D ren B0 B1 B2 ==> 4 3 2
%D
%D (( A0 A1 <- .plabel= a A
%D A1 A2 <- .plabel= a B
%D A0 A2 <- .slide= -10pt .plabel= b A∘B=AB
%D
%D B0 B1 <- .plabel= a \psm{·&·&·\\·&·&·\\·&·&·\\·&·&·\\}
%D B1 B2 <- .plabel= a \psm{·&·\\·&·\\·&·\\}
%D B0 B2 <- .slide= -10pt .plabel= b \psm{·&·\\·&·\\·&·\\·&·\\}
%D
%D ))
%D enddiagram
%D
$\pu
\cdiag{yoneda-matrices-comp}
$
The main diagram is:
%
%D diagram yoneda-matrices
%D 2Dx 100 +60
%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 ==> k \Mat(j,k)
%D ren A4 A5 ==> n \Mat(j,n)
%D ren B0 B1 ==> \Mat \sfSet
%D ren C1 C2 ==> h_k=\Mat(k,-) \sfSet(1,\Mat(j,-))
%D ren C3 ==> h_j=\Mat(j,-)
%D
%D (( A1 A3 -> .plabel= r \nameof{α_k(I_k)}
%D A2 A3 |->
%D A2 A4 -> # .plabel= l ϕ
%D A3 A5 -> # .plabel= r ·
%D A4 A5 |->
%D # A1 A5 -> .slide= 35pt .plabel= r ·
%D A2 A5 harrownodes nil 20 nil |->
%D B0 B1 -> .plabel= a \Mat(j,-)
%D C1 C2 -> # .plabel= b T
%D C1 C3 -> .plabel= b α
%D C2 C3 <->
%D ))
%D enddiagram
%D
$$\pu
\diag{yoneda-matrices}
$$
\newpage
% «2.3._univ-props-and-elts» (to ".2.3._univ-props-and-elts")
% (riep 1 "2.3._univ-props-and-elts")
% (rie "2.3._univ-props-and-elts")
% (find-riehlccpage (+ 18 62) "2.3. Universal properties and universal elements")
% (find-riehlcctext (+ 18 62) "2.3. Universal properties and universal elements")
\section*{2.3. Universal properties and universal elements}
(Page 62):
% «2.3.4._example-Zx» (to ".2.3.4._example-Zx")
% (riep 1 "2.3.4._example-Zx")
% (rie "2.3.4._example-Zx")
% (find-riehlccpage (+ 18 63) "Example 2.3.4." "Z[x]")
% (find-riehlcctext (+ 18 63) "Example 2.3.4." "Z[x]")
(Page 63):
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 (2.3.5) is implemented by evaluating a ring homomorphism $φ:
\Z[x] → R$ at the element $x∈Z[x]$ to obtain an element $φ(x)∈R$.
%
%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}\\\text{univ}}
%D A2 A3 |->
%D A2 A4 -> .plabel= l φ
%D A3 A5 ->
%D A4 A5 |->
%D A1 A5 -> .slide= 20pt .plabel= r \nameof{φ(x)}
%D B0 B1 |-> .plabel= a U
%D C1 C2 <->
%D C1 C3 <->
%D C2 C3 <->
%D
%D ))
%D enddiagram
%D
$$\pu
\diag{2.3.4._Z[x]}
$$
% «2.3.7._example-bilin» (to ".2.3.7._example-bilin")
% (riep 1 "2.3.7._example-bilin")
% (rie "2.3.7._example-bilin")
% (find-riehlccpage (+ 18 63) "Example 2.3.7.")
% (find-riehlcctext (+ 18 63) "Example 2.3.7.")
Example 2.3.7.
%
%D diagram 2.3.4._Bilin
%D 2Dx 100 +70
%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 ==> V⊗_{\k}W 𝐬{Bilin}(V,W;V⊗_{\k}W)
%D ren A4 A5 ==> U 𝐬{Bilin}(V,W;U)
%D ren B0 B1 ==> 𝐬{Vect}_\k 𝐬{Set}
%D ren C1 C2 ==> 𝐬{Vect}(V⊗_{\k}W,-) 𝐬{Set}(1,𝐬{Bilin}(V,W;-))
%D ren C3 ==> 𝐬{Bilin}(V,W;-)
%D
%D (( A1 A3 -> .plabel= r \sm{\nameof{⊗}\\\text{univ}}
%D A2 A3 |->
%D A2 A4 -> .plabel= l \ovl{f}
%D A3 A5 ->
%D A4 A5 |->
%D A1 A5 -> .slide= 55pt .plabel= r \nameof{f}
%D B0 B1 |-> .plabel= a U
%D C1 C2 <->
%D C1 C3 <->
%D C2 C3 <->
%D
%D ))
%D enddiagram
%D
$$\pu
\def\k{k}
\diag{2.3.4._Bilin}
$$
% ____ _ _ _____ _ _
% |___ \ | || | | ____| | |_ ___
% __) | | || |_ | _| | | __/ __|
% / __/ _ |__ _| | |___| | |_\__ \
% |_____| (_) |_| |_____|_|\__|___/
%
% «2.4._cat-of-elements» (to ".2.4._cat-of-elements")
% (find-books "__cats/__cats.el" "riehl")
% (find-riehlccpage (+ 18 66) "2.4. The category of elements")
\section*{2.4 The category of elements}
(Page 66):
2.4.1: Covariant:
%
%D diagram elts-covariant
%D 2Dx 100 +20 +40 +25
%D 2D 100 A1
%D 2D
%D 2D +20 A2 A3 C0 C1
%D 2D
%D 2D +20 A4 A5 C2 C3
%D 2D
%D 2D +20 B0 B1 D0 D1
%D 2D
%D ren A1 A2 A3 A4 A5 B0 B1 ==> 1 c Fc c' Fc' \sfC \sfSet
%D ren C0 C1 C2 C3 D0 D1 ==> (c,x) c (c',x') c' ∫F \sfC
%D
%D (( A1 A3 -> .plabel= r \nameof{x}
%D A2 A3 |->
%D A2 A4 -> .plabel= l f
%D A3 A5 -> .plabel= r Ff
%D A4 A5 |->
%D A1 A5 -> .plabel= r \nameof{x'} .slide= 20pt
%D B0 B1 -> .plabel= a F
%D A2 A5 harrownodes nil 20 nil |->
%D
%D C0 C1 |->
%D C0 C2 -> .plabel= l f
%D C1 C3 -> .plabel= r f
%D C2 C3 |->
%D C0 C3 harrownodes nil 20 nil |->
%D D0 D1 -> .plabel= a Π
%D ))
%D enddiagram
%D
$$\pu
\diag{elts-covariant}
$$
2.4.2: Contravariant:
%
%D diagram elts-contravariant
%D 2Dx 100 +20 +40 +25
%D 2D 100 A1
%D 2D
%D 2D +20 A2 A3 C0 C1
%D 2D
%D 2D +20 A4 A5 C2 C3
%D 2D
%D 2D +20 B0 B1 D0 D1
%D 2D
%D ren A1 A2 A3 A4 A5 B0 B1 ==> 1 c' Fc' c Fc \sfC^\op \sfSet
%D ren C0 C1 C2 C3 D0 D1 ==> (c',x') c' (c,x) c ∫F \sfC
%D
%D (( A1 A3 -> .plabel= r \nameof{x'}
%D A2 A3 |->
%D A2 A4 <- .plabel= l f
%D A3 A5 -> .plabel= r Ff
%D A4 A5 |->
%D A1 A5 -> .plabel= r \nameof{x} .slide= 20pt
%D B0 B1 -> .plabel= a F
%D A2 A5 harrownodes nil 20 nil |->
%D
%D C0 C1 |->
%D C0 C2 <- .plabel= l f
%D C1 C3 <- .plabel= r f
%D C2 C3 |->
%D C0 C3 harrownodes nil 20 nil |->
%D D0 D1 -> .plabel= a Π
%D ))
%D enddiagram
%D
$$\pu
\diag{elts-contravariant}
$$
% _ _ _ _ _ _ _
% | || | / \ __| |(_)_ _ _ __ ___| |_(_) ___ _ __ ___
% | || |_ / _ \ / _` || | | | | '_ \ / __| __| |/ _ \| '_ \/ __|
% |__ _| / ___ \ (_| || | |_| | | | | (__| |_| | (_) | | | \__ \
% |_| /_/ \_\__,_|/ |\__,_|_| |_|\___|\__|_|\___/|_| |_|___/
% |__/
%
% «4._adjunctions» (to ".4._adjunctions")
% (find-riehlccpage 134 "4.1. Adjoint functors")
% (find-riehlcctext 134 "4.1. Adjoint functors")
% (find-riehlccpage 134 "Definition 4.1.1 (adjunctions I)")
% (find-riehlcctext 134 "Definition 4.1.1 (adjunctions I)")
% (find-riehlccpage 140 "4.2. The unit and counit as universal arrows")
% (find-riehlcctext 140 "4.2. The unit and counit as universal arrows")
% (find-riehlccpage (+ 18 123) "Definition 4.2.5 (adjunction II)")
% (find-riehlcctext (+ 18 123) "Definition 4.2.5 (adjunction II)")
% (find-riehlccpage (+ 18 124) "fully-specified adjunction")
% (find-riehlcctext (+ 18 124) "fully-specified adjunction")
\section*{4. Adjunctions}
% «4.5.2._RAPL» (to ".4.5.2._RAPL")
% (riep 5 "4.5.2._RAPL")
% (rie "4.5.2._RAPL")
\subsection*{4.5.2. Right adjoints preserve limits}
(Page 136):
% (find-riehlccpage (+ 18 136) "Theorem 4.5.2 (RAPL)")
% (find-riehlcctext (+ 18 136) "Theorem 4.5.2 (RAPL)")
%D diagram RAPL-1
%D 2Dx 100 +40 +40 +40
%D 2D 100 A0 <--| A1
%D 2D +20 A2 |--> A3
%D 2D +10 A4 <--| A5
%D 2D +20 A6 A7' A7
%D 2D
%D 2D +20 B0 <==> B1
%D 2D +30 B2 <==> B3
%D 2D
%D ren A0 A1 ==> (LA\;LA) (A\;A)
%D ren A2 A3 ==> (B_1\;B_2) (RB_1\;RB_2)
%D ren A4 A5 ==> LA A
%D ren A6 A7' A7 ==> B_1{×}B_2 R(B_1{×}B_2) RB_1{×}RB_2
%D ren B0 B1 ==> \catB^{••} \catA^{••}
%D ren B2 B3 ==> \catB \catA
%D
%D (( A7' xy+= 5 0
%D
%D # Horizontal arrows:
%D A0 A1 <-|
%D A2 A3 |->
%D A4 A5 <-|
%D A6 A7' |->
%D B0 B1 <- sl^ .plabel= a L^{••}
%D B0 B1 -> sl_ .plabel= b R^{••}
%D B2 B3 <- sl^ .plabel= a L
%D B2 B3 -> sl_ .plabel= b R
%D
%D # Vertical arrows:
%D A0 A2 ->
%D A1 A3 ->
%D A4 A6 ->
%D A5 A7 ->
%D A5 A7' ->
%D
%D # Diagonal arrows:
%D A0 A4 <-|
%D A1 A5 <-|
%D A2 A6 |->
%D A3 A7 |->
%D B0 B2 <- sl^ .plabel= a Δ
%D B0 B2 -> sl_ .plabel= b \lim
%D B1 B3 <- sl^ .plabel= a Δ
%D B1 B3 -> sl_ .plabel= b \lim
%D ))
%D enddiagram
%D
$$\pu
\diag{RAPL-1}
$$
%D diagram RAPL-2
%D 2Dx 100 +40 +40 +40
%D 2D 100 A0 <--| A1
%D 2D +20 A2 |--> A3
%D 2D +10 A4 <--| A5
%D 2D +20 A6 A7' A7
%D 2D
%D 2D +20 B0 <==> B1
%D 2D +30 B2 <==> B3
%D 2D
%D ren A0 A1 ==> ΔLA=L^\catIΔA ΔA
%D ren A2 A3 ==> D R^{\catI}D
%D ren A4 A5 ==> LA A
%D ren A6 A7' A7 ==> \lim\,D R(\lim\,D) \lim(R^\catI\,D)
%D ren B0 B1 ==> \catB^\catI \catA^\catI
%D ren B2 B3 ==> \catB \catA
%D
%D (( A7' xy+= 5 0
%D
%D # Horizontal arrows:
%D A0 A1 <-|
%D A2 A3 |->
%D A4 A5 <-|
%D A6 A7' |->
%D B0 B1 <- sl^ .plabel= a L^\catI
%D B0 B1 -> sl_ .plabel= b R^\catI
%D B2 B3 <- sl^ .plabel= a L
%D B2 B3 -> sl_ .plabel= b R
%D
%D # Vertical arrows:
%D A0 A2 ->
%D A1 A3 ->
%D A4 A6 ->
%D A5 A7 ->
%D A5 A7' ->
%D
%D # Diagonal arrows:
%D A0 A4 <-|
%D A1 A5 <-|
%D A2 A6 |->
%D A3 A7 |->
%D B0 B2 <- sl^ .plabel= a Δ
%D B0 B2 -> sl_ .plabel= b \lim
%D B1 B3 <- sl^ .plabel= a Δ
%D B1 B3 -> sl_ .plabel= b \lim
%D ))
%D enddiagram
%D
$$\pu
\diag{RAPL-2}
$$
\newpage
% __ _ _ __
% / /_ / | | |/ /__ _ _ __
% | '_ \ | | | ' // _` | '_ \
% | (_) | _ | | | . \ (_| | | | |
% \___/ (_) |_| |_|\_\__,_|_| |_|
%
% «6.1._kan-extensions» (to ".6.1._kan-extensions")
% (riep 5 "6.1._kan-extensions")
% (rie "6.1._kan-extensions")
\section*{6.1. Kan Extensions}
(Page 190):
Definition 6.1.1 (second half). Given functors $F$ and $K$ a right kan
extension of $F$ along $K$ is a pair $(R,ε)$ such that
$∀G.∀δ.∃!β. \; δ=ε·βK$.
Lower half: internal view --- $δ=ε·βK$ becomes $∀c. \; δc=εc∘βKc$.
% From [PH1]:
%
% Look at Figure \ref{fig:internal-external}; let's name its
% subdiagrams as $A$, $B$, and $C$, like this: $\sm{A \; B \\ C}$.
% Each one of $A$, $B$, $C$ has an {\sl internal view} above and an
% {\sl external view} below.
% (find-riehlccpage (+ 18 44) "1.7. The 2-category of categories")
% (find-riehlcctext (+ 18 44) "1.7. The 2-category of categories")
% (find-riehlccpage (+ 18 46) "whiskering")
% (find-riehlcctext (+ 18 46) "whiskering")
% (find-riehlccpage (+ 18 190) "6.1. Kan extensions")
% (find-riehlcctext (+ 18 190) "6.1. Kan extensions")
%D diagram Ran-cells
%D 2Dx 100 +30 +30 +20 +30 +30 +20 +30 +30
%D 2D 100 A1 B1 C1
%D 2D / \ / \ / \\
%D 2D +30 A0 ---- A2 B0 ---- B2 C0 ---- C2
%D 2D
%D 2D +20 D1 E1 F1
%D 2D +10 / \ / E2 / F2
%D 2D +15 / D3 / | / F3
%D 2D +15 D0 ---- D4 E0 ---- E4 F0 ---- F4
%D 2D
%D ren A0 A1 A2 ==> \sfC \sfD \sfE
%D ren B0 B1 B2 ==> \sfC \sfD \sfE
%D ren C0 C1 C2 ==> \sfC \sfD \sfE
%D ren D0 D1 D3 D4 ==> c Kc RKc Fc
%D ren E0 E1 E2 E4 ==> c Kc GKc Fc
%D ren F0 F1 F2 F3 F4 ==> c Kc GKc RKc Fc
%D
%D (( A0 A1 -> .plabel= a K
%D A1 A2 -> .curve= _10pt .plabel= a R
%D A0 A2 -> .plabel= b F
%D A0 A2 midpoint relplace -5 -10 \Dnε
%D
%D B0 B1 -> .plabel= a K
%D B1 B2 -> .curve= ^20pt .plabel= a ∀G
%D B0 B2 -> .plabel= b F
%D B0 B2 midpoint relplace 10 -15 \Dn∀δ
%D
%D C0 C1 -> .plabel= a K
%D C1 C2 -> .curve= _10pt .plabel= m R
%D C1 C2 -> .curve= ^20pt .plabel= a G
%D C0 C2 -> .plabel= b F
%D C1 C2 midpoint relplace 5 0 \Dn∃!β
%D C0 C2 midpoint relplace -5 -10 \Dnε
%D
%D D0 D1 |->
%D D1 D3 |-> .curve= _10pt
%D D0 D4 |->
%D D3 D4 -> .plabel= r εc
%D
%D E0 E1 |->
%D E1 E2 |-> .curve= ^10pt
%D E0 E4 |->
%D E2 E4 -> .plabel= r δc
%D
%D F0 F1 |->
%D F1 F2 |-> .curve= ^10pt
%D F1 F3 |-> .curve= _10pt
%D F0 F4 |->
%D F2 F3 -> .plabel= r βKc
%D F3 F4 -> .plabel= r εc
%D F2 F4 -> .slide= 25pt .plabel= r δc
%D
%D ))
%D enddiagram
%D
$$\pu
\def\Dn{{\Downarrow}}
\diag{Ran-cells}
$$
% (find-riehlccpage (+ 18 192) "Proposition 6.1.5")
% (find-riehlcctext (+ 18 192) "Proposition 6.1.5")
(Page 192):
Proposition 6.1.5 (right Kan only). Fix $K$ and suppose that we have
an operation $F ↦ (\Ran_KF,ε)$ that returns right Kan extensions. We
can use that to build an adjunction $K^*⊣\Ran_K$, where $K^*$ is
pre-composition with $K$.
%D diagram Ran-adjunction
%D 2Dx 100 +25 +40 +20 +25 +20 +20
%D 2D 100 A0 - A1 B0 C0 - C1
%D 2D | | | | |
%D 2D +20 A2 - A3 B1 C2 - C3
%D 2D |
%D 2D +20 A4 D0 - D1
%D 2D
%D 2D +20 E0 - E1
%D 2D
%D ren A0 A1 A2 A3 A4 ==> K^*G ∀G K^*R R F
%D ren B0 B1 ==> K^*R F
%D ren C0 C1 C2 C3 ==> K^*G G F \Ran_KF
%D ren D0 D1 ==> \sfE^\sfC \sfE^\sfD
%D ren E0 E1 ==> \sfC \sfD
%D
%D (( A0 A1 <-|
%D A0 A2 -> .plabel= l K^*β
%D A1 A3 -> .plabel= r ∃!β
%D A2 A3 <-|
%D A2 A4 -> .plabel= l ε
%D A0 A4 -> .slide= -25pt .plabel= l ∀δ
%D
%D B0 B1 -> .plabel= l ε
%D
%D C0 C1 <-|
%D C0 C2 -> .plabel= l δ
%D C1 C3 -> .plabel= r β
%D C2 C3 |->
%D C3 relplace 20 0 =R
%D
%D D0 D1 <- sl^ .plabel= a K^*
%D D0 D1 -> sl_ .plabel= b \Ran_K
%D E0 E1 -> .plabel= a K
%D ))
%D enddiagram
%D
$$\pu
\diag{Ran-adjunction}
$$
% (find-riehlccpage (+ 18 190) "6.1. Kan extensions")
% (find-riehlcctext (+ 18 190) "6.1. Kan extensions")
%
% Definition 6.1.1 (second half). Given functors $F:\sfC → \sfE$,
% $K:\sfC→\sfD$, a right Kan extension of $F$ along $K$ is a functor
% $\Ran_K F: \sfD → \sfE$ together with a natural transformation $ε:
% \Ran_K F · K ⇒ F$ such that for any $(G: \sfD → \sfE, δ: GK ⇒ F)$,
% factors uniquely through as illustrated.
% (find-riehlccpage (+ 18 192) "Proposition 6.1.5")
% (find-riehlcctext (+ 18 192) "Proposition 6.1.5")
%
% Proposition 6.1.5. If, for fixed $K: \sfC → \sfD$ and $E$, the right
% Kan extensions of any functor $F: \sfC → \sfE$ along $K$ exist, then
% it defines right adjoints to the pre-composition functor $K^* :
% \sfE^\sfD → \sfE^\sfC$.
\newpage
\def\pdiag#1{\left(\diag{#1}\right)}
\def\Po#1#2{\psm{ & #1 \\ #2 & F#2}}
\def\po#1#2{\phantom{\Po#1#2}}
\section*{6.2 A formula for Kan extensions}
% (find-riehlccpage (+ 18 193) "6.2. A formula for Kan extensions")
% (find-riehlcctext (+ 18 193) "6.2. A formula for Kan extensions")
% (find-riehlccpage (+ 18 194) "Theorem 6.2.1.")
% (find-riehlcctext (+ 18 194) "Theorem 6.2.1.")
Riehl's formula for $\Ran_K F (d)$ is:
$\Ran_K F(d) = \lim(d↓K \ton{Π_d} \sfC \ton{F} \sfE)$
I'll change the notation by
$\bsm{
\sfC := \catA \\
\sfD := \catB \\
\sfE := \Set \\
K := F \\
F := H \\
d := B \\
}
$
$F_*H(B) = \Ran_F H(B) = \lim(B↓F \ton{π_o} \catA \ton{F} \Set)$
%D diagram A
%D 2Dx 100 +15
%D 2D 100 A1 A2
%D 2D +15 A3 A4
%D 2D +15 A5 A6
%D 2D
%D ren A1 A2 A3 A4 A5 A6 ==> · 2 · · 5 6
%D
%D (( A2 A6 -> A5 A6 ->
%D
%D ))
%D enddiagram
%D
%D diagram B
%D 2Dx 100 +15
%D 2D 100 A1 A2
%D 2D +15 A3 A4
%D 2D +15 A5 A6
%D 2D
%D ren A1 A2 A3 A4 A5 A6 ==> 1' 2' 3' 4' 5' 6'
%D
%D (( A1 A2 -> A1 A3 -> A2 A4 ->
%D A3 A4 -> A3 A5 -> A4 A6 -> A5 A6 ->
%D ))
%D enddiagram
%D
$$\pu
F:\catA→\catB
\qquad \text{is} \qquad
\pdiag{A}
\diagxyto/->/<200>^F
\pdiag{B}
$$
%D diagram ??
%D 2Dx 100 +30
%D 2D 100 A1 A2
%D 2D +30 A3 A4
%D 2D +30 A5 A6
%D 2D
%D ren A1 A2 A3 A4 A5 A6 ==> · \Po26 · · \Po56 \Po66
%D
%D (( A2 A6 -> A5 A6 ->
%D ))
%D enddiagram
%D
$$\pu
\pdiag{??}
$$
\newpage
\end{document}
% __ __ _
% | \/ | __ _| | _____
% | |\/| |/ _` | |/ / _ \
% | | | | (_| | < __/
% |_| |_|\__,_|_|\_\___|
%
% <make>
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2020riehl veryclean
make -f 2019.mk STEM=2020riehl pdf
% Local Variables:
% coding: utf-8-unix
% ee-tla: "rie"
% End: