|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2008bcc.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008bcc.tex && latex 2008bcc.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008bcc.tex && pdflatex 2008bcc.tex"))
% (eev "cd ~/LATEX/ && Scp 2008bcc.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (defun d () (interactive) (find-dvipage "~/LATEX/2008bcc.dvi"))
% (find-dvipage "~/LATEX/2008bcc.dvi")
% (find-pspage "~/LATEX/2008bcc.pdf")
% (find-pspage "~/LATEX/2008bcc.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2008bcc.ps 2008bcc.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2008bcc.ps 2008bcc.dvi && ps2pdf 2008bcc.ps 2008bcc.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2008bcc.pdf" (ee-twupfile "LATEX/2008bcc.pdf") 'over)
% (ee-cp "~/LATEX/2008bcc.pdf" (ee-twusfile "LATEX/2008bcc.pdf") 'over)
% (find-angg ".emacs" "dnc-to-std")
% (find-angg ".emacs" "std-to-dnc")
% «.adjs-of-change-of-base» (to "adjs-of-change-of-base")
% «.new-bcc-1» (to "new-bcc-1")
% «.bcc-categorically» (to "bcc-categorically")
% «.bcc-hyperdoctrine» (to "bcc-hyperdoctrine")
% «.bcc-collapse» (to "bcc-collapse")
% «.bcc-sums-full-diag» (to "bcc-sums-full-diag")
% «.bcc-smaller-diagram» (to "bcc-smaller-diagram")
% «.bcc-smaller-diagrams» (to "bcc-smaller-diagrams")
% «.bcc-trees» (to "bcc-trees")
% «.first-preservations» (to "first-preservations")
% «.first-preservations-2» (to "first-preservations-2")
\documentclass[oneside]{book}
\usepackage[latin1]{inputenc}
\usepackage{edrx08} % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty" -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex")
\begin{document}
\input 2008bcc.dnt
%*
% (eedn4-51-bounded)
\def\Eq{\mathsf{Eq}}
%:*'**^{\prime*}*
%:*&*\&*
%:*\&*\&*
%:*b=b'*b{=}b'*
{\bf These notes are being changed!!!}
\bsk
Index of the slides:
\msk
% To update the list of slides uncomment this line:
\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")
\tocline {Adjoints to change of base} {2}
\tocline {BCC, categorically} {3}
\tocline {BCC in a hyperdoctrine} {4}
\tocline {BCC: collapsing isomorphic objects} {5}
\tocline {BCC for dependent sums: full diagram} {6}
\tocline {BCC: smaller diagram} {7}
\tocline {BCC: smaller diagrams} {8}
\tocline {BCC: trees} {9}
\tocline {First preservations} {10}
\tocline {First preservations (2)} {11}
\newpage
% --------------------
% «adjs-of-change-of-base» (to ".adjs-of-change-of-base")
% (s "Adjoints to change of base" "adjs-of-change-of-base")
\myslide {Adjoints to change of base} {adjs-of-change-of-base}
%D diagram adjs-to-change-of-base
%D 2Dx 100 +30 +30 +35 +30 +40
%D 2D 100 A0 ===> A1 B0 ===> B1 C0 ===> C1
%D 2D - - - - - -
%D 2D | <-> | | <-> | | <-> |
%D 2D v v v v v v
%D 2D +20 A2 <=== A3 B2 <=== B3 C2 <=== C3
%D 2D - - - - - -
%D 2D | <-> | | <-> | | <-> |
%D 2D v v v v v v
%D 2D +20 A4 ===> A5 B4 ===> B5 C4 ===> C5
%D 2D
%D 2D +20 a0 |--> a1 b0 |--> b1 c0 |--> c1
%D 2D
%D (( A0 .tex= Pab A1 .tex= Îb.Pab
%D A2 .tex= Qa A3 .tex= Qa
%D A4 .tex= Rab A5 .tex= ýb.Rab
%D a0 .tex= a,b a1 .tex= a
%D A0 A1 =>
%D A0 A2 |-> A1 A3 |-> A0 A3 harrownodes nil 20 nil <->
%D A2 A3 <=
%D A2 A4 |-> A3 A5 |-> A2 A5 harrownodes nil 20 nil <->
%D A4 A5 =>
%D a0 a1 |->
%D ))
%D (( B0 .tex= Pab B1 .tex= b=b'&Pabb
%D B2 .tex= Qabb B3 .tex= Qabb'
%D B4 .tex= Rab B5 .tex= b=b'⊃Rab
%D b0 .tex= a,b b1 .tex= a,b,b'
%D B0 B1 =>
%D B0 B2 |-> B1 B3 |-> B0 B3 harrownodes nil 20 nil <->
%D B2 B3 <=
%D B2 B4 |-> B3 B5 |-> B2 B5 harrownodes nil 20 nil <->
%D B4 B5 =>
%D b0 b1 |->
%D ))
%D (( C0 .tex= Pa C1 .tex= Îa.a=fb.Pb
%D C2 .tex= Qfa C3 .tex= Qb
%D C4 .tex= Ra C5 .tex= ýa.a=fb⊃Pb
%D c0 .tex= a c1 .tex= b
%D C0 C1 =>
%D C0 C2 |-> C1 C3 |-> C0 C3 harrownodes nil 20 nil <->
%D C2 C3 <=
%D C2 C4 |-> C3 C5 |-> C2 C5 harrownodes nil 20 nil <->
%D C4 C5 =>
%D c0 c1 |-> .plabel= a f
%D ))
%D enddiagram
%D
$$\diag{adjs-to-change-of-base}$$
% \end{document}
% \end{document}
\newpage
% --------------------
% «bcc-categorically» (to ".bcc-categorically")
% (s "BCC, categorically" "bcc-categorically")
\myslide {BCC, categorically} {bcc-categorically}
This is how the Beck-Chevalley condition (for dependent sums;
there is also a variation for dependent products, that we will
see soon) is usually stated:
\begin{quotation}
``If the square formed by $f,g,f',g'$ in the base category
in the diagram below is a pullback, and if $P$ is an object
over $C$, then the natural map from $\sum_{f'}g^{\prime*}P$ to $g^*\sum_{f}P$
is an isomorphism.''
\end{quotation}
The upper part of the diagram below shows how to build the map
$î: \sum_{f'}g^{\prime*}P \to g^*\sum_{f}P$.
\bsk
But what does that {\sl mean}?
%D diagram big-bcc-cat
%D 2Dx 100 +45 +45 +60 +45
%D 2D 100 B0 ======================> B1
%D 2D -/\ -
%D 2D | \\ |
%D 2D v \\ v
%D 2D +30 B2 <\> B2' <-> B2'' <===== B3
%D 2D /\ \\ /\
%D 2D +30 \\ B4 =====================> B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +30 B6 <===================== B7
%D 2D
%D 2D +20 b0 <-> b0' <-> b0'' |----> b1
%D 2D |-> |->
%D 2D +60 b2 |--------------------> b3
%D 2D
%D # g'*P |------------------> Îf'g'*P
%D # | ^ |
%D # | \ |---> |
%D # v \ v
%D # g'*f*ÎfP <\-> f'*g*ÎfP <-----| g*ÎfP
%D # /\ - ^
%D # \ P |--------------------> ÎfP
%D # \ | \ -
%D # \ | <---| \ | id
%D # - v -v
%D # f*ÎfP <------------------| ÎfP
%D #
%D # Ax_{B}C -----------------> A
%D # \ __| f' \
%D # g' \ \ g
%D # v v
%D # C ---------------------> B
%D # f
%D ((
%D B0 .tex= g'*P B1 .tex= Î_{f'}g'*P
%D B2 .tex= g'*f^*Î_fP B2' .tex= h^*Î_{f}P B2'' .tex= f'*g^*Î_fP
%D B3 .tex= g^*Î_{f}P
%D B4 .tex= P B5 .tex= Î_fP
%D B6 .tex= f^*Î_fP B7 .tex= Î_fP
%D B0 B1 |-> B0 B2 -> B0 B2' -> B0 B2'' -> B1 B3 -> .plabel= l {î}
%D B2 B2' <-> B2' B2'' <-> B2'' B3 <-|
%D B0 B4 <-| B2 B6 <-| B2' B7 <-| B3 B7 <-|
%D B4 B5 |-> B4 B6 -> B5 B7 -> .plabel= r \id B6 B7 <-|
%D B0 B2'' midpoint B1 B3 midpoint harrownodes nil 20 nil ->
%D B0 B2 midpoint B4 B6 midpoint dvarrownodes nil 18 nil <-
%D B4 B7 harrownodes nil 20 nil <-
%D ))
%D (( b0 .tex= A×_{B}C b0' .tex= A×_{B}C b0'' .tex= A×_{B}C b1 .tex= A
%D b2 .tex= C b3 .tex= B
%D b0 b0' = b0' b0'' = b0'' b1 -> .plabel= b f'
%D b0 b2 -> .plabel= l g' b0' b3 -> .plabel= l h b1 b3 -> .plabel= l g
%D b2 b3 -> .plabel= b f
%D b0 relplace 18 10 \pbsymbol{10}
%D ))
%D enddiagram
$$\defÎ{\sum}
\diag{big-bcc-cat}
$$
\newpage
% --------------------
% «bcc-hyperdoctrine» (to ".bcc-hyperdoctrine")
% (s "BCC in a hyperdoctrine" "bcc-hyperdoctrine")
\myslide {BCC in a hyperdoctrine} {bcc-hyperdoctrine}
\widemtos
In the case of a hyperdoctrine that means that from an
object $\ssst{b,c}{P}$ and a map $a \mto b$ there are two ways to
build an object that deserves the name ``$\ssst{a}{Îc.P}$''...
\msk
...and without BCC we would know a map between them
going in one direction, $î: \ssst{a}{Îc.P} \to \ssst{a}{Îc.P}'$,
but we wouldn't know that it is an iso.
%D diagram big-bcc-logical
%D 2Dx 100 +40 +40 +60 +40
%D 2D 100 B0 ======================> B1
%D 2D -/\ -
%D 2D | \\ |
%D 2D v \\ v
%D 2D +30 B2 <\> B2' <-> B2'' <===== B3
%D 2D /\ \\ /\
%D 2D +30 \\ B4 =====================> B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +30 B6 <===================== B7
%D 2D
%D 2D +20 b0 <-> b0' <-> b0'' |----> b1
%D 2D |-> |->
%D 2D +60 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= \s[a,c|P] B1 .tex= \s[a|Îc.P]
%D B2 .tex= \s[a,c|Îc.P] B2' .tex= \s[a,c|Îc.P]' B2'' .tex= \s[a,c|Îc.P]''
%D B3 .tex= \s[a|Îc.P]'
%D B4 .tex= \s[b,c|P] B5 .tex= \s[b|Îc.P]
%D B6 .tex= \s[b,c|Îc.P] B7 .tex= \s[b|Îc.P]
%D B0 B1 => B0 B2 |-> B0 B2' |-> B0 B2'' |-> B1 B3 |-> .plabel= l {î}
%D B2 B2' <-> B2' B2'' <-> B2'' B3 <=
%D B0 B4 <= B2 B6 <= B2' B7 <= B3 B7 <=
%D B4 B5 => B4 B6 |-> B5 B7 |-> .plabel= r \id B6 B7 <=
%D B0 B2'' midpoint B1 B3 midpoint harrownodes nil 20 nil |->
%D B0 B2 midpoint B4 B6 midpoint dvarrownodes nil 18 nil <-|
%D B4 B7 harrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a,c b0' .tex= a,c b0'' .tex= a,c b1 .tex= a
%D b2 .tex= b,c b0' b3 .tex= b
%D b0 b0' = b0' b0'' = b0'' b1 |->
%D b0 b2 |-> b0' b3 |-> b1 b3 |->
%D b2 b3 |->
%D b0 relplace 18 10 \pbsymbol{10}
%D ))
%D enddiagram
% BCC: full diagram (no isos hidden), in $\Sub(\Set)$.
$$\diag{big-bcc-logical}$$
\newpage
% --------------------
% «bcc-collapse» (to ".bcc-collapse")
% (s "BCC: collapsing isomorphic objects" "bcc-collapse")
\myslide {BCC: collapsing isomorphic objects} {bcc-collapse}
One trick to make the previous (big) diagram simpler to draw
is to draw the objects that are isomorphic and ``deserve the same
name'' --- but that may be different --- as a single object; these
collapsed objects (here just $\ssst{a,c}{Îc.P}$) have more than one
functor arrow pointing to them, which indicates that they have
more than one construction.
%D diagram big-bcc-logical-collapsed
%D 2Dx 100 +40 +50 +40
%D 2D 100 B0 ======================> B1
%D 2D -/\ -
%D 2D | \\ |
%D 2D v \\ v
%D 2D +30 B2 <\\==================== B3
%D 2D /\ \\ /\
%D 2D +20 \\ B4 =====================> B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +30 B6 <===================== B7
%D 2D
%D 2D +20 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +50 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= \s[a,c|P] B1 .tex= \s[a|Îc.P]
%D B2 .tex= \s[a,c|Îc.P] B3 .tex= \s[a|Îc.P]'
%D B4 .tex= \s[b,c|P] B5 .tex= \s[b|Îc.P]
%D B6 .tex= \s[b,c|Îc.P] B7 .tex= \s[b|Îc.P]
%D B0 B1 => B0 B2 |-> B1 B3 |-> .plabel= l {î}
%D B2 B3 <=
%D B0 B4 <= B2 B6 <= B3 B7 <=
%D B4 B5 => B4 B6 |-> B5 B7 |-> .plabel= r \id B6 B7 <=
%D B0 B2 midpoint B1 B3 midpoint harrownodes nil 20 nil |->
%D B0 B2 midpoint B4 B6 midpoint dvarrownodes nil 18 nil <-|
%D B4 B7 harrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a,c b1 .tex= a
%D b2 .tex= b,c b3 .tex= b
%D b0 b1 |->
%D b0 b2 |-> b1 b3 |->
%D b2 b3 |->
%D b0 relplace 18 9 \pbsymbol{9}
%D ))
%D enddiagram
% BCC: full diagram (no isos hidden), in $\Sub(\Set)$.
$$\diag{big-bcc-logical-collapsed}$$
\newpage
% --------------------
% «bcc-sums-full-diag» (to ".bcc-sums-full-diag")
% (s "BCC for dependent sums: full diagram" "bcc-sums-full-diag")
\myslide {BCC for dependent sums: full diagram} {bcc-sums-full-diag}
%D diagram big-bcc
%D 2Dx 100 +35 +35 +70 +35
%D 2D 100 B0 ======================> B1
%D 2D -/\ -
%D 2D | \\ |
%D 2D v \\ v
%D 2D +30 B2 <\> B2' <-> B2'' <===== B3
%D 2D /\ \\ /\
%D 2D +30 \\ B4 =====================> B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +30 B6 <===================== B7
%D 2D
%D 2D +20 b0 <-> b0' <-> b0'' |----> b1
%D 2D |-> |->
%D 2D +60 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= \s[a,c|d] B1 .tex= \s[a|c,d]
%D B2 .tex= \s[a,c|c,d] B2' .tex= \s[a,c|c,d]' B2'' .tex= \s[a,c|c,d]''
%D B3 .tex= \s[a|c,d]'
%D B4 .tex= \s[b,c|d] B5 .tex= \s[b|c,d]
%D B6 .tex= \s[b,c|c,d] B7 .tex= \s[b|c,d]
%D B0 B1 => B0 B2 |-> B0 B2' |-> B0 B2'' |-> B1 B3 |-> .plabel= r {î}
%D B2 B2' <-> B2' B2'' <-> B2'' B3 <=
%D B0 B4 <= B2 B6 <= B2' B7 <= B3 B7 <=
%D B4 B5 => B4 B6 |-> B5 B7 |-> .plabel= r \id B6 B7 <=
%D B0 B2'' midpoint B1 B3 midpoint harrownodes nil 20 nil |->
%D B0 B2 midpoint B4 B6 midpoint dvarrownodes nil 18 nil <-|
%D B4 B7 harrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a,c b0' .tex= a,c b0'' .tex= a,c b1 .tex= a
%D b2 .tex= b,c b0' b3 .tex= b
%D b0 b0' = b0' b0'' = b0'' b1 |->
%D b0 b2 |-> b0' b3 |-> b1 b3 |->
%D b2 b3 |->
%D ))
%D enddiagram
BCC: full diagram (no isos hidden), in $\Set^\to$.
$\diag{big-bcc}$
\newpage
% --------------------
% «bcc-smaller-diagram» (to ".bcc-smaller-diagram")
% (s "BCC: smaller diagram" "bcc-smaller-diagram")
\myslide {BCC: smaller diagram} {bcc-smaller-diagram}
%D diagram small-bcc
%D 2Dx 100 +35 +40 +35
%D 2D 100 B0 ======================> B1
%D 2D -/\ -
%D 2D | \\ |
%D 2D v \\ v
%D 2D +30 B2 <\\==================== B3
%D 2D /\ \\ /\
%D 2D +20 \\ B4 =====================> B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +30 B6 <===================== B7
%D 2D
%D 2D +20 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +50 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= \s[a,c|d] B1 .tex= \s[a|c,d]
%D B2 .tex= \s[a,c|c,d] B3 .tex= \s[a|c,d]
%D B4 .tex= \s[b,c|d] B5 .tex= \s[b|c,d]
%D B6 .tex= \s[b,c|c,d] B7 .tex= \s[b|c,d]
%D B0 B1 => B0 B2 |-> B1 B3 |-> .plabel= r {î}
%D B2 B3 <=
%D B0 B4 <= B2 B6 <= B3 B7 <=
%D B4 B5 => B4 B6 |-> B5 B7 |-> .plabel= r \id B6 B7 <=
%D B0 B2 midpoint B1 B3 midpoint harrownodes nil 20 nil |->
%D B0 B2 midpoint B4 B6 midpoint dvarrownodes nil 18 nil <-|
%D B4 B7 harrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a,c b1 .tex= a
%D b2 .tex= b,c b3 .tex= b
%D b0 b1 |->
%D b0 b2 |-> b1 b3 |->
%D b2 b3 |->
%D ))
%D enddiagram
BCC: smaller diagram.
$\diag{small-bcc}$
\newpage
% --------------------
% «bcc-smaller-diagrams» (to ".bcc-smaller-diagrams")
% (s "BCC: smaller diagrams" "bcc-smaller-diagrams")
\myslide {BCC: smaller diagrams} {bcc-smaller-diagrams}
BCC: smaller diagrams.
%D diagram smaller-bcc
%D 2Dx 100 +30 +30 +30
%D 2Dx 100 +20 +25 +20
%D 2D 100 B0 ======================> B1
%D 2D -/\ -
%D 2D | \\ |
%D 2D v \\ v
%D 2D +20 B2 <\\==================== B3
%D 2D /\ \\ /\
%D 2D +10 \\ B4 =====================> B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +20 B6 <===================== B7
%D 2D
%D 2D +10 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +30 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= d B1 .tex= c,d
%D B2 .tex= c,d B3 .tex= c,d
%D B4 .tex= d B5 .tex= c,d
%D B6 .tex= c,d B7 .tex= c,d
%D B0 B1 => B0 B2 |-> B1 B3 |-> .plabel= l {î}
%D B2 B3 <=
%D B0 B4 <= B2 B6 <= B3 B7 <=
%D B4 B5 => B4 B6 |-> B5 B7 |-> .plabel= r \id B6 B7 <=
%D B0 B2 midpoint B1 B3 midpoint harrownodes nil 20 nil |->
%D B0 B2 midpoint B4 B6 midpoint dvarrownodes nil 15 nil <-|
%D B4 B7 harrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a,c b1 .tex= a
%D b2 .tex= b,c b3 .tex= b
%D b0 b1 |->
%D b0 b2 |-> b1 b3 |->
%D b2 b3 |->
%D b0 relplace 12 7 \pbsymbol{7}
%D ))
%D enddiagram
%D diagram smaller-prod-bcc
%D 2Dx 100 +30 +30 +30
%D 2Dx 100 +20 +25 +20
%D 2D 100 B0 <====================== B1
%D 2D -/\ -
%D 2D | \\ |
%D 2D v \\ v
%D 2D +20 B2 =\\===================> B3
%D 2D /\ \\ /\
%D 2D +10 \\ B4 <===================== B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +20 B6 =====================> B7
%D 2D
%D 2D +10 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +30 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= c|->d B1 .tex= c|->d
%D B2 .tex= d B3 .tex= c|->d
%D B4 .tex= c|->d B5 .tex= c|->d
%D B6 .tex= d B7 .tex= c|->d
%D B0 B1 <= B0 B2 |-> B1 B3 |-> .plabel= l {î}
%D B2 B3 =>
%D B0 B4 <= B2 B6 <= B1 B5 <= # B3 B7 <=
%D B4 B5 <= B4 B6 |-> B5 B7 |-> .plabel= r \id B6 B7 =>
%D B0 B2 midpoint B1 B3 midpoint harrownodes nil 20 nil |->
%D B0 B2 midpoint B4 B6 midpoint dvarrownodes nil 15 nil <-|
%D B4 B7 harrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a,c b1 .tex= a
%D b2 .tex= b,c b3 .tex= b
%D b0 b1 |->
%D b0 b2 |-> b1 b3 |->
%D b2 b3 |->
%D b0 relplace 12 7 \pbsymbol{7}
%D ))
%D enddiagram
%: b,c|-D
%: -------
%: b|-Æc.D
%: --------
%: b;p|-p
%: ----------------
%: a|-b b,c;d|-\ang{c,d}
%: -----------------------
%: a,c;d|-\ang{c,d}
%: -----------------------
%: a;p|-\ang{c,d}[c,d:=p]
%:
%: ^bcc-sum-1
%:
$$\cdiag{smaller-bcc} \qquad
% \begin{matrix}
\cded{bcc-sum-1}
% \end{matrix}
$$
%: b,c|-D
%: -------
%: b|-åc.D
%: --------
%: b;f|-f
%: ---------
%: a|-b b,c;f|-fc
%: ----------------
%: a,c;f|-fc
%: ----------
%: a;f|-ðc.fc
%:
%: ^bcc-prod-1
%:
$$\cdiag{smaller-prod-bcc} \qquad
\begin{matrix}
\ded{bcc-prod-1}
\end{matrix}
$$
\newpage
% --------------------
% «bcc-trees» (to ".bcc-trees")
% (s "BCC: trees" "bcc-trees")
\myslide {BCC: trees} {bcc-trees}
%D diagram smaller-bcc-eq
%D 2Dx 100 +30 +30 +30
%D 2D 100 B0 ======================> B1
%D 2D -/\ -
%D 2D | \\ |
%D 2D v \\ v
%D 2D +20 B2 <\\==================== B3
%D 2D /\ \\ /\
%D 2D +10 \\ B4 =====================> B5
%D 2D \\ - \\ -
%D 2D \\ | \\|
%D 2D \\v \v
%D 2D +20 B6 <===================== B7
%D 2D
%D 2D +10 b0 |---------------------> b1
%D 2D |-> |->
%D 2D +30 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= d B1 .tex= (c{=}c'),d
%D B2 .tex= (c{=}c),d B3 .tex= (c{=}c'),d
%D B4 .tex= d B5 .tex= (c{=}c'),d
%D B6 .tex= (c{=}c),d B7 .tex= (c{=}c'),d
%D B0 B1 => B0 B2 |-> B1 B3 |-> .plabel= l {î}
%D B2 B3 <=
%D B0 B4 <= B2 B6 <= B3 B7 <=
%D B4 B5 => B4 B6 |-> B5 B7 |-> .plabel= r \id B6 B7 <=
%D B0 B2 midpoint B1 B3 midpoint harrownodes nil 20 nil |->
%D B0 B2 midpoint B4 B6 midpoint dvarrownodes nil 15 nil <-|
%D B4 B7 harrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a,c b1 .tex= a,c,c'
%D b2 .tex= b,c b3 .tex= b,c,c'
%D b0 b1 |->
%D b0 b2 |-> b1 b3 |->
%D b2 b3 |->
%D b0 relplace 12 7 \pbsymbol{7}
%D ))
%D enddiagram
%: b,c|-D
%: -------
%: b,c,c'|-Æ(c{=}c').D
%: ----------------------
%: b,c,c';((c{=}c'),d)|-((c{=}c').d)
%: ---------------------------------
%: a,c|-b,c b,c;d|-\ang{(c{=}c),d}
%: ---------------------------------
%: a,c;d|-\ang{(c{=}c),d}
%: -----------------------
%: a,c;((c{=}c'),d)|-\ang{(c{=}c'),d}
%:
%: ^bcc-eq-1-semi
%:
$$\cdiag{smaller-bcc-eq} \qquad
\begin{matrix}
\ded{bcc-eq-1-semi}
\end{matrix}
$$
\newpage
% --------------------
% «first-preservations» (to ".first-preservations")
% (s "First preservations" "first-preservations")
\myslide {First preservations} {first-preservations}
%D diagram cob-preserves-T-and-AND
%D 2Dx 100 +30 +30 +10 +30 +40
%D 2D 100 PP0 <=========== PP1
%D 2D ^ ^ ^
%D 2D | \ <-| |
%D 2D - - -
%D 2D +30 PT0 <== PT1 PP2 <-| PP3 <=== PP4
%D 2D - - - -
%D 2D | | / <-| |
%D 2D v v v v
%D 2D +30 PT2 PP5 <=========== PP6
%D 2D
%D 2D +20 pta |-> ptb ppa |------> ppb
%D 2D
%D (( PT0 .tex= \s[a|§] PT1 .tex= \s[b|§]
%D PT2 .tex= \s[a|§]'
%D pta .tex= a ptb .tex= b
%D PT0 PT1 <= PT0 PT2 |-> .plabel= r {î}
%D pta ptb |->
%D ))
%D (( PP0 .tex= \s[a|P] PP1 .tex= \s[b|P]
%D PP2 .tex= \s[a|P&Q]' PP3 .tex= \s[a|P&Q] PP4 .tex= \s[b|P&Q]
%D PP5 .tex= \s[a|Q] PP6 .tex= \s[b|Q]
%D ppa .tex= a ppb .tex= b
%D PP0 PP1 <=
%D PP0 PP2 <-| .plabel= r {\pi} PP0 PP3 <-|
%D PP1 PP4 <-| .plabel= r {\pi}
%D PP0 PP3 midpoint PP1 PP4 midpoint harrownodes nil 20 nil <-|
%D PP2 PP3 <-| .plabel= a {î} PP3 PP4 <=
%D PP2 PP5 |-> .plabel= r {\pi'} PP3 PP5 |->
%D PP4 PP6 |-> .plabel= r {\pi'}
%D PP3 PP5 midpoint PP4 PP6 midpoint harrownodes nil 20 nil <-|
%D PP5 PP6 <=
%D ppa ppb |->
%D ))
%D enddiagram
%D diagram cob-preserves-exp
%D 2Dx 100 +20 +20 +40 +20 +20
%D 2D 100 E0 <============= E1
%D 2D v /\ v /\
%D 2D +30 E2 <\\=========== E3 \\
%D 2D \\ \\ \\ \\
%D 2D +20 \\ E4 <============= E5
%D 2D \/ - \/ v
%D 2D +30 E6 E7
%D 2D
%D 2D +20 ea |------------> eb
%D 2D
%D (( E0 .tex= \s[a|(Q⊃R)&Q] E1 .tex= \s[b|(Q⊃R)&Q]
%D E2 .tex= \s[a|R] E3 .tex= \s[b|R]
%D E4 .tex= \s[a|Q⊃R] E5 .tex= \s[b|Q⊃R]
%D E6 .tex= \s[a|Q⊃R]' E7 .tex= \s[b|Q⊃R]
%D ea .tex= a eb .tex= b
%D E0 E1 <= E0 E2 |-> E1 E3 |-> E2 E3 <=
%D E0 E4 <= E2 E6 => E1 E5 <= E3 E7 =>
%D E4 E5 <= E4 E6 |-> .plabel= r {î} E5 E7 |-> .plabel= r \id
%D E0 E3 harrownodes nil 20 nil <-|
%D E0 E2 midpoint E4 E6 midpoint dvarrownodes nil 16 nil |->
%D E1 E3 midpoint E5 E7 midpoint dvarrownodes nil 16 nil <-|
%D ea eb |->
%D ))
%D enddiagram
Change-of-base preserves terminals and binary products:
$\diag{cob-preserves-T-and-AND}$
\medskip
Change-of-base preserves exponentials:
$\diag{cob-preserves-exp}$
\medskip
In all the diagrams above the natural morphisms marked
`$î$' are required to be isos.
\medskip
Note that in the diagram for preservation of exponentials
the object at the upper left has two constructions; in fact
it is two objects, and we are hiding the iso between them.
\newpage
% --------------------
% «first-preservations-2» (to ".first-preservations-2")
% (s "First preservations (2)" "first-preservations-2")
\myslide {First preservations (2)} {first-preservations-2}
A category with the structure above is a {\bf pre-hyperdoctrine}.
A {\bf hyperdoctrine} is a pre-hyperdoctrine that obeys certain
extra equations, like this one:
\medskip
In a pre-hyperdoctrine given $a \mton{f} b$ and two propositions $P(b)$
and $Q(b)$ over the space of `$b$'s we have two different constructions
for $P(f(a)) \& Q(f(a))$ over the space of `$a$'s, and a natural
morphism from one construction to the other one:
\medskip
$\dncdisplay[b|P\&Q] := (P(b) \& Q(b))[b:=f(a)]$
$\dncdisplay[b|P\&Q]' := P(b)[b:=f(a)] \, \& \, Q(b)[b:=f(a)]$
\medskip
%D diagram cob-preserves-AND
%D 2Dx 100 +10 +30 +40
%D 2D 100 PP0 <=========== PP1
%D 2D ^ ^ ^
%D 2D | \ <-| |
%D 2D - - -
%D 2D +30 PP2 <-| PP3 <=== PP4
%D 2D - - -
%D 2D | / <-| |
%D 2D v v v
%D 2D +30 PP5 <=========== PP6
%D 2D
%D 2D +20 ppa |------> ppb
%D 2D
%D (( PP0 .tex= \s[a|P] PP1 .tex= \s[b|P]
%D PP2 .tex= \s[a|P&Q]' PP3 .tex= \s[a|P&Q] PP4 .tex= \s[b|P&Q]
%D PP5 .tex= \s[a|Q] PP6 .tex= \s[b|Q]
%D ppa .tex= a ppb .tex= b
%D PP0 PP1 <=
%D PP0 PP2 <-| .plabel= r {\pi} PP0 PP3 <-| .plabel= r {f^*\pi}
%D PP1 PP4 <-| .plabel= r {\pi}
%D PP0 PP3 midpoint PP1 PP4 midpoint harrownodes nil 20 nil <-|
%D PP2 PP3 <-| .plabel= a {î} PP3 PP4 <=
%D PP2 PP5 |-> .plabel= r {\pi'} PP3 PP5 |-> .plabel= r {f^*\pi'}
%D PP4 PP6 |-> .plabel= r {\pi'}
%D PP3 PP5 midpoint PP4 PP6 midpoint harrownodes nil 20 nil <-|
%D PP5 PP6 <=
%D ppa ppb |-> .plabel= a {f}
%D ))
%D enddiagram
$\diag{cob-preserves-AND}$
\medskip
we want these two constructions to be equivalent, so in the
definition of hyperdoctrine we include a condition that says
that the morphism `$î$' is an iso, i.e., that it has an inverse.
%*
\end{document}
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: