% (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:
