% (find-LATEX "2020barrwellsctcs.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020barrwellsctcs.tex" :end))
% (defun d () (interactive) (find-pdf-page      "~/LATEX/2020barrwellsctcs.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020barrwellsctcs.pdf"))
% (defun e () (interactive) (find-LATEX "2020barrwellsctcs.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020barrwellsctcs"))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (find-pdf-page   "~/LATEX/2020barrwellsctcs.pdf")
% (find-sh0 "cp -v  ~/LATEX/2020barrwellsctcs.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2020barrwellsctcs.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2020barrwellsctcs.pdf
%               file:///tmp/2020barrwellsctcs.pdf
%           file:///tmp/pen/2020barrwellsctcs.pdf
% http://angg.twu.net/LATEX/2020barrwellsctcs.pdf
% (find-LATEX "2019.mk")

\documentclass[oneside,11pt]{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")
\begin{document}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

% %L dofile "edrxtikz.lua"  -- (find-LATEX "edrxtikz.lua")
% %L dofile "edrxpict.lua"  -- (find-LATEX "edrxpict.lua")
% \pu


{\setlength{\parindent}{0em}
\footnotesize

Notes on Michael Barr and Charles Wells's

``Category Theory for Computing Science'':

\url{http://www.tac.mta.ca/tac/reprints/articles/22/tr22.pdf}

\url{http://www.tac.mta.ca/tac/reprints/articles/22/tr22abs.html}

\ssk

These notes are at:

\url{http://angg.twu.net/LATEX/2020barrwellsctcs.pdf}

}


% (find-books "__cats/__cats.el" "barr-wells-ctcs")
% (find-barrwellsctcspage (+ 20 331) "12 Fibrations")
% (find-barrwellsctcspage (+ 20 331) "12.1.1" "cartesian")

\section*{12. Fibrations}

12.1.1. Fibrations and opfibrations (page 331):

$u$ is cartesian (for $f$ and $Y$) when:

%D diagram cartesian
%D 2Dx     100 +20 +20 +20
%D 2D  100     A0
%D 2D
%D 2D  +20 L0      A1  A2
%D 2D
%D 2D  +20     B0
%D 2D
%D 2D  +20 L1      B1  B2
%D 2D
%D ren A0 A1 A2 ==> ∀Z X Y
%D ren B0 B1 B2 ==> P(Z) C D
%D ren L0 L1    ==> \calE \calC
%D
%D (( A0 A1 -> .plabel= l ∃!w
%D    A1 A2 -> .plabel= b u
%D    A0 A2 -> .plabel= a ∀v
%D
%D    B0 B1 -> .plabel= l h
%D    B1 B2 -> .plabel= b f
%D    B0 B2 -> .plabel= a P(v)
%D
%D    L0 xy+= 0 -5
%D    L1 xy+= 0 -5
%D    L0 L1 -> .plabel= l P
%D ))
%D enddiagram
%D
$$\pu
  \diag{cartesian}
$$

% (find-barrwellsctcspage (+ 20 332) "opcartesian")

$u$ is opcartesian (for $f$ and $X$):

%D diagram opcartesian
%D 2Dx     100 +20 +20 +20
%D 2D  100             A2
%D 2D
%D 2D  +20 L0  A0  A1
%D 2D
%D 2D  +20             B2
%D 2D
%D 2D  +20 L1  B0  B1
%D 2D
%D ren A0 A1 A2 ==> X Y ∀Z
%D ren B0 B1 B2 ==> C D P(Z)
%D ren L0 L1    ==> \calE \calC
%D
%D (( A0 A1 -> .plabel= b u
%D    A1 A2 -> .plabel= r ∃!w
%D    A0 A2 -> .plabel= a ∀v
%D
%D    B0 B1 -> .plabel= b f
%D    B1 B2 -> .plabel= r ∀k
%D    B0 B2 -> .plabel= a P(v)
%D
%D    L0 xy+= 0 -5
%D    L1 xy+= 0 -5
%D    L0 L1 -> .plabel= l P
%D ))
%D enddiagram
%D
$$\pu
  \diag{opcartesian}
$$

12.1.4. Example:
%
%D diagram Example-12.1.4
%D 2Dx     100 +20 +20 +60
%D 2D  100     A0
%D 2D
%D 2D  +20 L0      A1  A2
%D 2D
%D 2D  +20     B0
%D 2D
%D 2D  +20 L1      B1  B2
%D 2D
%D ren A0 A1 A2 ==> ∀(A',C'') (A,C) Y=(A',C)
%D ren B0 B1 B2 ==> C'' C C'
%D ren L0 L1    ==> \calA×\calC \calC
%D
%D (( A0 A1 -> .plabel= l (g,u)
%D    A1 A2 -> .plabel= b γ(f,v)=(\id_A,f)
%D    A0 A2 -> .plabel= a ∀(g,h)
%D
%D    B0 B1 -> .plabel= l ∀u
%D    B1 B2 -> .plabel= b f
%D    B0 B2 -> .plabel= a h
%D
%D    L0 xy+= 0 -5
%D    L1 xy+= 0 -5
%D    L0 L1 -> .plabel= l P
%D ))
%D enddiagram
%D
$$\pu
  \diag{Example-12.1.4}
$$


% (find-barrwellsctcspage (+ 20 334) "12.1.7 Cleavages induce functors")
% (find-barrwellsctcstext (+ 20 334) "12.1.7 Cleavages induce functors")
% (find-barrwellsctcspage (+ 20 334) "12.1.8 Proposition")
% (find-barrwellsctcstext (+ 20 334) "12.1.8 Proposition")

{\bf 12.1.7 Cleavages induce functors} (page 334)

Let $P: \calE → \calC$ be an opfibration with opcleavage $κ$. Define
$F: \calC → \Cat$ by...
%
%D diagram opcleavage-induce-functor
%D 2Dx     100 +20 +40
%D 2D  100     A0  A1
%D 2D
%D 2D  +25     A2  A3
%D 2D
%D 2D  +25 L0  A4  A5
%D 2D
%D 2D  +20 L1  B0  B1
%D 2D
%D ren A0 A1 ==> X   Ff(X)
%D ren A2 A3 ==> X'  Ff(X')
%D ren A4 A5 ==> X'' Ff(X'')
%D ren B0 B1 ==> C D
%D ren L0 L1 ==> \calE \calC
%D
%D (( A0 A1 -> .plabel= a κ(f,X)
%D
%D    A0 A2 -> .plabel= l u
%D    A1 A3 -> .plabel= r ∃!Ff(u)
%D    A0 A3 -> .plabel= m \phantom{a}
%D    A0 A3 harrownodes nil 20 nil |->
%D
%D    A2 A3 -> .plabel= a κ(f,X')
%D
%D    A2 A4 -> .plabel= l v
%D    A3 A5 -> .plabel= r ∃!Ff(v)
%D    A2 A5 -> .plabel= m \phantom{a}
%D    A2 A5 harrownodes nil 20 nil |->
%D
%D    A4 A5 -> .plabel= a κ(f,X'')
%D
%D    B0 B1 -> .plabel= a f
%D
%D    L0 L1 -> .plabel= l P
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{opcleavage-induce-functor}
$$


% (find-barrwellsctcspage (+ 20 335) "In a similar way, split fibrations")
% (find-barrwellsctcstext (+ 20 335) "In a similar way, split fibrations")

In a similar way, split fibrations give functors $\calC^\op → \Cat$.
Let $P: \calE → \calC$ be a fibration with cleavage $γ$. Define $F:
\calC^\op → \Cat$ by
%
%D diagram cleavage-induce-functor
%D 2Dx     100 +20 +40
%D 2D  100     A0  A1
%D 2D
%D 2D  +25     A2  A3
%D 2D
%D 2D  +25 L0  A4  A5
%D 2D
%D 2D  +20 L1  B0  B1
%D 2D
%D ren A0 A1 ==> Ff(Y)   Y
%D ren A2 A3 ==> Ff(Y')  Y'
%D ren A4 A5 ==> Ff(Y'') Y''
%D ren B0 B1 ==> C D
%D ren L0 L1 ==> \calE \calC
%D
%D (( A0 A1 -> .plabel= a γ(f,Y)
%D
%D    A0 A2 -> .plabel= l ∃!Ff(u)
%D    A1 A3 -> .plabel= r u
%D    A0 A3 -> .plabel= m \phantom{a}
%D    A0 A3 harrownodes nil 20 nil <-|
%D
%D    A2 A3 -> .plabel= a γ(f,Y')
%D
%D    A2 A4 -> .plabel= l ∃!Ff(v)
%D    A3 A5 -> .plabel= r v
%D    A2 A5 -> .plabel= m \phantom{a}
%D    A2 A5 harrownodes nil 20 nil <-|
%D
%D    A4 A5 -> .plabel= a γ(f,Y'')
%D
%D    B0 B1 -> .plabel= a f
%D
%D    L0 L1 -> .plabel= l P
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{cleavage-induce-functor}
$$

\newpage


% (find-barrwellsctcspage (+ 20 336) "12.2 The Grothendieck construction")
% (find-barrwellsctcstext (+ 20 336) "12.2 The Grothendieck construction")
% (find-barrwellsctcspage (+ 20 339) "12.2.8 Given a functor")
% (find-barrwellsctcstext (+ 20 339) "12.2.8 Given a functor")

\section*{12.2 The Grothendieck construction}

{\bf 12.2.8} and {\bf 12.2.9}: Given a functor $F: \calC → \Cat$ (...)
the Grothendieck construction in this more general setting constructs
the opfibration induced by $F$, a category $𝐛G(\calC, F)$ defined as
follows:
%
%D diagram 12.2.8-and-12.2.9
%D 2Dx     100 +20    +30    +45  +30 +25   +35   +35
%D 2D  100     D1 |-> D2 |-> D3
%D 2D                 |       |
%D 2D                 v       v
%D 2D  +20            D5 |-> D6
%D 2D                         |
%D 2D                         v
%D 2D  +20                   D9
%D 2D
%D 2D  +10 A0  B0 --> B1 --> B2   E0  F0 -> F1 -> F2
%D 2D      ^                      |
%D 2D      |                      v
%D 2D  +20 A1  C0 --> C1 --> C2   E1  G0 -> G1 -> G2
%D 2D
%D ren A0 A1    ==> \Cat \calC
%D ren B0 B1 B2 ==> F(C) F(C') F(C'')
%D ren C0 C1 C2 ==>   C    C'    C''
%D ren D1 D2 D3 ==> x (Ff)(x) (Fg)((Ff)(x))
%D ren    D5 D6 ==>        x' (Fg)(x')
%D ren       D9 ==>               x''
%D ren E0 E1    ==> 𝐛G(\calC,F) \calC
%D ren F0 F1 F2 ==> (x,C) (x',C') (x'',C'')
%D ren G0 G1 G2 ==>    C      C'       C''
%D
%D (( A0 A1 <- .plabel= l F
%D    B0 B1 -> .plabel= a Ff
%D    B1 B2 -> .plabel= a Fg
%D    C0 C1 -> .plabel= a f
%D    C1 C2 -> .plabel= a g
%D
%D    D1 D2 |-> D2 D3 |-> D5 D6 |->
%D    D2 D5 -> .plabel= l u
%D    D3 D6 -> .plabel= r (Fg)(u)
%D    D6 D9 -> .plabel= r v
%D
%D    E0 E1 -> .plabel= l P
%D    F0 F1 -> .plabel= a (u,f)
%D    F1 F2 -> .plabel= a (v,g)
%D    G0 G1 -> .plabel= a  f
%D    G1 G2 -> .plabel= a  g
%D ))
%D enddiagram
%D
$$\pu
  \diag{12.2.8-and-12.2.9}
$$

\msk

% (find-barrwellsctcspage (+ 20 341) "12.2.10 An analogous construction")
% (find-barrwellsctcstext (+ 20 341) "12.2.10 An analogous construction")

{\bf 12.2.10} An analogous construction, also called the Grothendieck
construction (in fact this is the original one), produces a split
fibration $𝐛F(\calC, G)$ given a functor $G: \calC^\op → \Cat$:
%
%D diagram 12.2.10
%D 2Dx     100 +20    +50    +30  +30 +25   +35   +35
%D 2D  100     D1
%D 2D          |
%D 2D          v
%D 2D  +20     D4 <-| D5
%D 2D          |       |
%D 2D          v       v
%D 2D  +20     D7 <-| D8 <-| D9
%D 2D
%D 2D  +15 A0  B0 <-- B1 <-- B2   E0  F0 -> F1 -> F2
%D 2D      ^                      |
%D 2D      |                      v
%D 2D  +20 A1  C0 --> C1 --> C2   E1  G0 -> G1 -> G2
%D 2D
%D ren A0 A1    ==> \Cat \calC^\op
%D ren B0 B1 B2 ==> G(C) G(C') G(C'')
%D ren C0 C1 C2 ==>   C    C'    C''
%D ren D1       ==> x
%D ren D4 D5    ==> (Gf)(x') x'
%D ren D7 D8 D9 ==> (Gf)((Gg)(x'')) (Gg)(x'') x''
%D ren E0 E1    ==> 𝐛F(\calC,G) \calC
%D ren F0 F1 F2 ==> (C,x) (C',x') (C'',x'')
%D ren G0 G1 G2 ==>    C      C'       C''
%D
%D (( A0 A1 <- .plabel= l G
%D    B0 B1 <- .plabel= a Gf
%D    B1 B2 <- .plabel= a Gg
%D    C0 C1 -> .plabel= a f
%D    C1 C2 -> .plabel= a g
%D
%D    D4 D5 <-| D7 D8 <-| D8 D9 <-|
%D    D1 D4 -> .plabel= l u
%D    D4 D7 -> .plabel= l (Gf)(v)
%D    D5 D8 -> .plabel= r v
%D
%D    E0 E1 -> .plabel= l P
%D    F0 F1 -> .plabel= a (f,u)
%D    F1 F2 -> .plabel= a (g,v)
%D    G0 G1 -> .plabel= a  f
%D    G1 G2 -> .plabel= a  g
%D ))
%D enddiagram
%D
$$\pu
  \diag{12.2.10}
$$







\end{document}

%  __  __       _        
% |  \/  | __ _| | _____ 
% | |\/| |/ _` | |/ / _ \
% | |  | | (_| |   <  __/
% |_|  |_|\__,_|_|\_\___|
%                        
% <make>

 (eepitch-shell)
 (eepitch-kill)
 (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2020barrwellsctcs veryclean
make -f 2019.mk STEM=2020barrwellsctcs pdf

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

