% This file: (find-LATEX "2019J-ops-kan.tex")
%       See: (find-LATEX "2020J-ops-new.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019J-ops-kan.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019J-ops-kan.pdf"))
% (defun e () (interactive) (find-LATEX "2019J-ops-kan.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019J-ops-kan"))
% (find-pdf-page   "~/LATEX/2019J-ops-kan.pdf")
% (find-sh0 "cp -v  ~/LATEX/2019J-ops-kan.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2019J-ops-kan.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2019J-ops-kan.pdf
%               file:///tmp/2019J-ops-kan.pdf
%           file:///tmp/pen/2019J-ops-kan.pdf
% http://angg.twu.net/LATEX/2019J-ops-kan.pdf
% (find-LATEX "2019.mk")

% «.kan-extensions»	(to "kan-extensions")



\directlua{tf_push("2019J-ops-kan.tex")}


%  _  __                       _       
% | |/ /__ _ _ __     _____  _| |_ ___ 
% | ' // _` | '_ \   / _ \ \/ / __/ __|
% | . \ (_| | | | | |  __/>  <| |_\__ \
% |_|\_\__,_|_| |_|  \___/_/\_\\__|___/
%                                      
% «kan-extensions»  (to ".kan-extensions")
% (jonp 36 "kan-extensions")
% (jop     "kan-extensions")
% (favp 45 "kan-extensions")
% (fav     "kan-extensions")
\subsection{Kan extensions}
\label     {kan-extensions}

\def\Lan{\text{Lan}}
\def\Ran{\text{Ran}}
\def\sfC{\mathsf{C}}
\def\sfD{\mathsf{D}}
\def\sfE{\mathsf{E}}



% (find-books "__cats/__cats.el" "riehl")
% (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  45) "Lemma 1.7.4 (horizontal composition)")
% (find-riehlcctext (+ 18  45) "Lemma 1.7.4 (horizontal composition)")
% (find-riehlccpage (+ 18  46) "whiskering")
% (find-riehlcctext (+ 18  46) "whiskering")
% (find-riehlccpage (+ 18 189) "6. All Concepts are Kan Extensions")
% (find-riehlccpage (+ 18 190) "6.1. Kan extensions")
% (find-riehlccpage (+ 18 190) "Dually, a right Kan")
% (find-riehlcctext (+ 18 190) "Dually, a right Kan")



In \cite{Riehl}, sec.6.1, right Kan extensions are explained using the
two diagrams below. The notation of cells is explained in sec.1.7 of
the book, and modulo the types --- that can be inferred from the
diagrams --- a right Kan extension of $K$ along $K$ is a pair $(\Ran_K
F,ε)$ such that for all $(G,α)$ there is a unique $β$ making
everything commute.
%
%D diagram riehl-ran-1
%D 2Dx     100 +40 +40
%D 2D  100 A0 ---> A2
%D 2D        ->  ->
%D 2D  +40     A1
%D 2D
%D ren A0 A1 A2 ==> \mathsf{C} \mathsf{D} \mathsf{E}
%D
%D (( A0 A2 -> .plabel= a F
%D    A0 A1 -> .plabel= l K
%D    A1 A2 -> .plabel= r G    .curve= _25pt
%D    A1 A2 varrownodes nil 17 nil <= .slide= -5pt .plabel= r δ
%D ))
%D enddiagram
%D
%D diagram riehl-ran-factored
%D 2Dx     100 +40 +40
%D 2D  100 A0 ---> A2
%D 2D        ->  -> ^
%D 2D  +40     A1 -/
%D 2D
%D ren A0 A1 A2 ==> \mathsf{C} \mathsf{D} \mathsf{E}
%D
%D (( A0 A2 -> .plabel= a F
%D    A0 A1 -> .plabel= l K
%D    A1 A2 -> .plabel= m \Ran_KF
%D    A1 A2 -> .plabel= r G    .curve= _25pt
%D    A0 A2 varrownodes 35 17 nil <=              .plabel= l ε
%D    A1 A2 varrownodes 20 17 nil <= .slide=  5pt .plabel= r β
%D ))
%D enddiagram
%D
$$\pu
  \diag{riehl-ran-1}
  \quad
  \diag{riehl-ran-factored}
$$

If we specialize $\sfE$ to $\Set$ and do some renamings, the diagram
becomes:
%
%D diagram my-ran-1
%D 2Dx     100 +40 +40
%D 2D  100 A0      A2
%D 2D
%D 2D  +40     A1
%D 2D
%D ren A0 A1 A2 ==> \catA \catB \Set
%D
%D (( A0 A2 -> .plabel= a D
%D    A0 A1 -> .plabel= l f
%D    A1 A2 -> .plabel= r C    .curve= _25pt
%D    A1 A2 varrownodes nil 17 nil <= .slide= -5pt .plabel= r α
%D ))
%D enddiagram
%D
%D diagram my-ran-2
%D 2Dx     100 +40 +40
%D 2D  100 A0      A2
%D 2D
%D 2D  +40     A1
%D 2D
%D ren A0 A1 A2 ==> \catA \catB \Set
%D
%D (( A0 A2 -> .plabel= a D
%D    A0 A1 -> .plabel= l f
%D    A1 A2 -> .plabel= m \Ran_fD
%D    A1 A2 -> .plabel= r C    .curve= _25pt
%D    A0 A2 varrownodes 35 17 nil <=              .plabel= l ε
%D    A1 A2 varrownodes 20 17 nil <= .slide=  5pt .plabel= r β
%D ))
%D enddiagram
%D
$$\pu
  \diag{my-ran-1}
  \quad
  \diag{my-ran-2}
$$
%
and if we change its {\sl shape} to stress that $ε$ ``looks like'' a
counit map and $\Ran_f$ ``looks like'' the right adjoint to the
functor $f^*$, we get this:
%
%D diagram geo-morph
%D 2Dx     100     +30 +35   +30     
%D 2D  100 L0      C0  C1    R1
%D 2D                          
%D 2D  +35 L2      C2  C3    R3
%D 2D                          
%D 2D  +20         C4  C5      
%D 2D
%D 2D  +20         C6  C7
%D 2D
%D ren C0 C1 C2 C3 C4 C5 ==> f^*C C D \Ran_fD \Set^\catA  \Set^\catB
%D ren C6 C7 ==> \catA \catB
%D ren L0 L2 ==> f^*\Ran_fD D
%D ren R1 R3 ==> C \Ran_ff^*C
%D
%D (( C0 C1 <-|
%D    C0 C2 -> .plabel= l \sm{β^\fl\\α}
%D    C1 C3 -> .plabel= r \sm{β\\α^♯}
%D    C2 C3 |->
%D    C0 C3 harrownodes nil 20 nil <-| sl^
%D    C0 C3 harrownodes nil 20 nil |-> sl_
%D
%D    C4 C5 <- sl^ .plabel= a f^*
%D    C4 C5 -> sl_ .plabel= b \Ran_f
%D
%D    C6 C7 -> .plabel= a f
%D    L0 L2 -> .plabel= l ε
%D    R1 R3 -> .plabel= r d
%D ))
%D enddiagram
%D
$$\pu
  \diag{geo-morph}
$$

When the categories $\catA$ and $\catB$ are finite posets we get:

\begin{itemize}

\item $\Set^\catA$ and $\Set^\catB$ are toposes (we saw this in
  sec.\ref{Set-PA}),
  %
  % (jopp 23 "Set-PA")
  % (joe     "Set-PA")

\item the functor $f^*$ is ``precomposition with $f$'', in this sense:
  if $C$ is an object of $\Set^B$ and $A∈\catA$ then $(f^*C)(A)$ is
  $C(f(A))$,

\item the left and right Kan extensions $\Lan_f$ and $\Ran_f$ and can be
  defined and calculated by the formulas in sec.6.2 of \cite{Riehl},
  %
  % (elep 7 "elephant-A4.1.4")
  % (ele    "elephant-A4.1.4")
  % (find-books "__cats/__cats.el" "riehl")
  % (find-riehlccpage (+ 18 193) "6.2. A formula for Kan extensions")

\item we have adjunctions $\Lan_f ⊣ f^* ⊣ \Ran_f$, and so the structure
  $(\Lan_f ⊣ f^* ⊣ \Ran_f)$ can be seen as an essential geometric
  morphism $f:\Set^\catA → \Set^\catB$ (\cite{EA}, A4.1.4); as $f^*$
  is a right adjoint it preserves limits (\cite{Riehl}, sec.4.5,
  and \cite{Awodey}, sec.9.6), and so $(f^* ⊣ \Ran_f)$ is a geometric
  morphism $f:\Set^\catA → \Set^\catB$. We usually rename $(\Lan_f ⊣
  f^* ⊣ \Ran_f)$ to $(f^! ⊣ f^* ⊣ f_*)$

\item when $f:\catA→\catB$ is something very simple we can find $\Ran_f D$
  ``by hand'' --- for example, in the example below, discussed
  in \cite{OchsACT2019}:
  %
% (oxap 5 "fig:internal-gms")
% (oxa    "fig:internal-gms")
%
%R sesw = {[" w"]="↙",  [" e"]="↘"}
%R
%R local zcB, zpBC, zpBRD
%R  = 3/       1             \, 3/      C_1            \, 3/      !Dt            \
%R     |    w     e          |   |    w     e          |   |    w     e          |
%R     | 2           3       |   |C_2         C_3      |   |D_2         D_3      |
%R     |    e     w     e    |   |    e     w     e    |   |    e     w     e    |
%R     |       4           5 |   |      C_4         C_5|   |      D_4         D_5|
%R     |          e     w    |   |          e     w    |   |          e     w    |
%R     \             6       /   \            C_6      /   \             1       /
%R
%R local zpBRLC
%R  =                           3/      !Ct            \
%R                               |    w     e          |
%R                               |C_2         C_3      |
%R                               |    e     w     e    |
%R                               |      C_4         C_5|
%R                               |          e     w    |
%R                               \             1       /
%R
%R local zcA, zpALC, zpAD
%R  = 3/ 2           3       \, 3/C_2         C_3      \, 3/D_2         D_3      \
%R     |    e     w     e    |   |    e     w     e    |   |    e     w     e    |
%R     \       4           5 /   \      C_4         C_5/   \      D_4         D_5/
%R                
%R zcB   :tozmp({def="zcB",    scale="7pt", meta="s p"}):addcells(sesw):output()
%R zpBC  :tozmp({def="zpBC",   scale="7pt", meta="s p"}):addcells(sesw):output()
%R zpBRD :tozmp({def="zpBRD" , scale="7pt", meta="s p"}):addcells(sesw):output()
%R zpBRLC:tozmp({def="zpBRLC", scale="7pt", meta="s p"}):addcells(sesw):output()
%R zcA   :tozmp({def="zcA",    scale="7pt", meta="s p"}):addcells(sesw):output()
%R zpALC :tozmp({def="zpALC",  scale="7pt", meta="s p"}):addcells(sesw):output()
%R zpAD  :tozmp({def="zpAD",   scale="7pt", meta="s p"}):addcells(sesw):output()
%
%D diagram internal-zgm-particular-case
%D 2Dx     100 +50    +60 +55
%D 2D  100 A1  B1 <-| B2  C1
%D 2D      |   |       |   |
%D 2D      |   |  <->  |   |
%D 2D      v   v       v   v
%D 2D  +50 A2  B3 |-> B4  C2
%D 2D
%D 2D  +30     D1 <=> D2
%D 2D
%D 2D  +20     E1 --> E2
%D 2D
%D 2D  +30     F1     F2
%D 2D
%D ren A1 B1 B2 C1 ==> \zpALC  \zpALC \zpBC   \zpBC
%D ren A2 B3 B4 C2 ==> \zpAD   \zpAD  \zpBRD  \zpBRLC
%D ren D1 D2 ==> \Set^\catA \Set^\catB
%D ren E1 E2 ==> \Set^\catA \Set^\catB
%D ren F1 F2 ==> \catA \catB
%D ren F1 F2 ==> \zcA \zcB
%D
%D (( A1 A2 -> .plabel= l εD
%D    C1 C2 -> .plabel= r ηC
%D
%D    B1 B2 <-|
%D    B1 B3 -> B2 B4 ->
%D    B3 B4 |->
%D    B1 B4 harrownodes nil 20 nil <->
%D
%D    D1 D2 <- sl^ .plabel= a f^*
%D    D1 D2 -> sl_ .plabel= b f_*
%D    E1 E2 -> .plabel= a f
%D    
%D    F1 F2 -> .plabel= a f
%D ))
%D enddiagram
%D
%
$$\pu
  \def\Ct{C_2 {×_{C_4}} C_3}
  \def\Dt{D_2 {×_{D_4}} D_3}
  \diag{internal-zgm-particular-case}
$$

\end{itemize}

\bsk

Every situation in which the category $\catB$ is a $(P,A)$ and the
category $\catA$ is the full subcategory of $(P,A)$ whose objects are
$P∖Q$ yields a situation like the one in the diagram above, in which
the maps $εD$ are isos, the geometric morphism $f$ is an ``inclusion''
and the functor that takes each $C$ to $f_*f^*C$ is a sheafification
functor. A diagram with an example fully worked out will be included
in the next version of this paper at the Arxiv.




% (find-books "__cats/__cats.el" "riehl")
% (find-riehlccpage (+ 18 136) "4.5. Adjunctions, limits, and colimits")
% (find-books "__cats/__cats.el" "awodey")
% (find-awodeyctpage (+ 10 197) "9.6 RAPL")



\newpage




\directlua{tf_pop()}




% Local Variables:
% coding: utf-8-unix
% ee-tla: "jok"
% End:
