|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2008quotypes.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008quotypes.tex && latex 2008quotypes.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008quotypes.tex && pdflatex 2008quotypes.tex"))
% (eev "cd ~/LATEX/ && Scp 2008quotypes.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (find-dvipage "~/LATEX/2008quotypes.dvi")
% (find-pspage "~/LATEX/2008quotypes.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -P pk -D 300 -o 2008quotypes.ps 2008quotypes.dvi")
% (find-pspage "~/LATEX/2008quotypes.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -P pk -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2008quotypes.pdf" (ee-twupfile "LATEX/2008quotypes.pdf") 'over)
% (ee-cp "~/LATEX/2008quotypes.pdf" (ee-twusfile "LATEX/2008quotypes.pdf") 'over)
% «.lemma-4.8.2» (to "lemma-4.8.2")
% «.quotient-types» (to "quotient-types")
% «.eq-on-morphisms» (to "eq-on-morphisms")
% «.eq-on-morphisms-2» (to "eq-on-morphisms-2")
% «.adjunctions» (to "adjunctions")
\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 2008quotypes.dnt
%*
% (eedn4-51-bounded)
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 {Lemma 4.8.2} {2}
\tocline {Quotient types} {3}
\tocline {How the `Eq' functor acts on morphisms} {4}
\tocline {How the `Eq' functor acts on morphisms (2)} {5}
\def\byR{_{\!/\!R}}
\def\ovl{\overline}
\def\Eq{¯{Eq}}
\def\Ker{¯{Ker}}
%:*§_*§\!_*
\newpage
% --------------------
% «lemma-4.8.2» (to ".lemma-4.8.2")
% (s "Lemma 4.8.2" "lemma-4.8.2")
\myslide {Lemma 4.8.2} {lemma-4.8.2}
(Jacobs, p.292)
% (find-jacobspage (+ 19 292) "4.8.2. Lemma")
%D diagram ??
%D 2Dx 100 +40 +60
%D 2D 100 A0 |------------\
%D 2D v v
%D 2D +20 A1 |-> A2 A3
%D 2D v v ^
%D 2D +20 A4 |-> A5 |-----/
%D 2D
%D 2D +15 B0 |------------> B1
%D 2D |-> |----->
%D 2D +20 B2
%D 2D
%D (( A0 .tex= Raa'
%D A1 .tex= \oa{=}\oa' A2 .tex= \oa{=}\oa' A3 .tex= b{=}b'
%D A4 .tex= b{=}b' A5 .tex= b{=}b'
%D B0 .tex= a;a' B1 .tex= b;b'
%D B2 .tex= \oa;\oa'
%D A0 A1 |-> A0 A3 |->
%D A1 A2 |-> .plabel= a {ñ}
%D A1 A4 |-> A2 A5 |->
%D A4 A5 |-> .plabel= a {ñ} A5 A3 |-> .plabel= a {ñ}
%D ))
%D (( A0 B2 => A3 B1 <=
%D ))
%D (( B0 B1 |->
%D B0 B2 |-> B2 B1 |->
%D ))
%D enddiagram
%D
$$\def\oa{\ovl{a}}
\diag{??}
$$
%D diagram ???
%D 2Dx 100 +40 +60
%D 2D 100 A0 |------------\
%D 2D v v
%D 2D +20 A1 |-> A2 A3
%D 2D v v ^
%D 2D +20 A4 |-> A5 |-----/
%D 2D
%D 2D +15 B0 |------------> B1
%D 2D |-> |----->
%D 2D +20 B2
%D 2D
%D (( A0 .tex= R
%D A1 .tex= \Ker(c_R) A2 .tex= \Eq(I/R) A3 .tex= \Eq(J)
%D A4 .tex= \Ker(u) A5 .tex= \Ker(v)
%D B0 .tex= I B1 .tex= J
%D B2 .tex= I/R
%D A0 A1 -> A0 A3 ->
%D A1 A2 -> .plabel= a {ñ}
%D A1 A4 -> A2 A5 ->
%D A4 A5 -> .plabel= a {ñ} A5 A3 -> .plabel= a {ñ}
%D ))
%D (( A0 B2 |-> A3 B1 <-|
%D ))
%D (( B0 B1 -> .plabel= a u
%D B0 B2 -> .plabel= b c_R B2 B1 -> .plabel= b v
%D ))
%D enddiagram
%D
$$\def\oa{\ovl{a}}
\diag{???}
$$
% \end{document}
\newpage
% --------------------
% «quotient-types» (to ".quotient-types")
% (s "Quotient types" "quotient-types")
\myslide {Quotient types} {quotient-types}
(Jacobs, p.282/290)
% (find-jacobspage (+ 19 282) "4.7_ Quotient types")
% (find-jacobspage (+ 19 290) "4.7_ Quotient types, categorically")
%D diagram quo1
%D 2Dx 100 +35 +35
%D 2D 100 Raa' b{=}b'
%D 2D
%D 2D +20 R^*aa'
%D 2D
%D 2D +25 a;a' a\byR;{a'}\byR b;b'
%D 2D
%D (( Raa' b{=}b' # 0 1
%D R^*aa' # 2
%D a;a' a\byR;{a'}\byR b;b' # 3 4 5
%D @ 0 @ 1 |->
%D @ 0 @ 2 |-> @ 0 @ 4 => @ 1 @ 5 <=
%D @ 2 @ 3 =>
%D @ 2 @ 4 =>
%D @ 3 @ 4 |-> @ 4 @ 5 |->
%D @ 1 @ 4 varrownodes nil 22 nil <->
%D ))
%D enddiagram
%D
$$\diag{quo1}$$
%D diagram quo2
%D 2Dx 100 +40 +55
%D 2D 100 \ovl{R}aa' a\byR{=}{a'}\byR
%D 2D
%D 2D +20 Raa' b{=}b'
%D 2D
%D 2D +30 a\byR;{a'}\byR
%D 2D
%D 2D +20 a;a' b;b'
%D 2D
%D (( \ovl{R}aa' a\byR{=}{a'}\byR # 0 1
%D Raa' b{=}b' # 2 3
%D a\byR;{a'}\byR # 4
%D a;a' b;b' # 5 6
%D @ 0 @ 1 <= sl_ @ 0 @ 1 |-> sl^ .plabel= a ñ
%D @ 0 @ 2 <-| @ 1 @ 4 <= @ 1 @ 3 |->
%D @ 2 @ 5 => @ 2 @ 4 => @ 2 @ 3 |-> @ 3 @ 6 <=
%D @ 5 @ 4 |-> @ 4 @ 6 |-> @ 5 @ 6 |->
%D ))
%D enddiagram
%D
$$\diag{quo2}$$
\bsk
%:
%: a,a'|-Ï[Raa'] a|-b a|-b a|-b'
%: -------------Q --------QI ----------------------QI=
%: |-A/R a|-b\byR a,Rbb'|-b\byR={b'}\byR
%:
%: ^Q ^QI ^QI=
%:
%:
%: a,b|-c_b a,b,b',Rbb'|-c_b=c_{b'} a|-b a|-b'
%: ---------------------------------QE ------------------------Qeff
%: a,b\byR|-c_{b\byR} a,b\byR{=}{b'}\byR|-Rbb'
%:
%: ^QE ^Qeff
%:
$$\ded{Q} \qquad \ded{QI} \qquad \ded{QI=}$$
$$\ded{QE} \qquad \ded{Qeff}$$
\newpage
% --------------------
% «eq-on-morphisms» (to ".eq-on-morphisms")
% (s "How the `Eq' functor acts on morphisms" "eq-on-morphisms")
\myslide {How the `Eq' functor acts on morphisms} {eq-on-morphisms}
% (find-jacobspage (+ 19 291) "\"equality relation\" functor")
(Jacobs, p.291)
% (find-LATEX "2008hyp.tex" "dep-eq-from-simple-eq")
%D diagram QEq1-dnc
%D 2Dx 100 +45 +55 +45
%D 2Dx 100 +55 +60 +55
%D 2D 100 B0 <==> B0' <============= B1
%D 2D -\\ - -\\
%D 2D | \\ | <--| | \\
%D 2D v \\ v v \\
%D 2D +20 B2 <\\> B2' <============= B3 \\
%D 2D /\ \/ /\ \/
%D 2D +15 \\ 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 +35 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= § B0' .tex= § x+= -3 B1 .tex= a{=}a
%D B2 .tex= b{=}b B2' .tex= b{=}b x+= -3 B3 .tex= b{=}b
%D B4 .tex= a{=}a' B5 .tex= b{=}b'
%D B6 .tex= b{=}b' B7 .tex= b{=}b'
%D # B0 B0' <-| sl^ .plabel= a î
%D B0 B0' |-> .plabel= a ÐP§
%D B0 B2 |-> B0' B2' |-> B2 B2' <-|
%D B1 B3 |-> B0' B1 <= B2' B3 <=
%D B0 B4 => B1 B5 =>
%D B2 B6 <= B3 B7 <=
%D B6 B7 <= B6 B7 |-> sl^^ .plabel= a {ñ}
%D B5 B7 |-> .plabel= r \id
%D B4 B6 |->
%D # B4 B6 <-| sl^ .plabel= r Ð{BCC}Î
%D B0 B2 midpoint B0' B2' midpoint harrownodes 7 17 nil <-|
%D B0' B2' midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes nil 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= a b1 .tex= b b2 .tex= a,a' b3 .tex= b,b'
%D b0 b1 |-> b0 b2 |-> b1 b3 |-> b2 b3 |->
%D # b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{QEq1-dnc}$$
%D diagram QEq1-std
%D 2Dx 100 +55 +60 +55
%D 2D 100 B0 <==> B0' <============= B1
%D 2D -\\ - -\\
%D 2D | \\ | <--| | \\
%D 2D v \\ v v \\
%D 2D +20 B2 <\\> B2' <============= B3 \\
%D 2D /\ \/ /\ \/
%D 2D +15 \\ 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 +35 b2 |--------------------> b3
%D 2D
%D ((
%D B0 .tex= §_I B0' .tex= u^*§_J x+= 3 B1 .tex= §_J
%D B2 .tex= _I^*(u{×}u)^*\Eq_J§_J B2' .tex= u^*_J^*\Eq_J§_J x+= 3 B3 .tex= _J^*\Eq_J§_J
%D B4 .tex= \Eq_I§_I B5 .tex= \Eq_J§_J
%D B6 .tex= (u{×}u)^*\Eq_J§_J B7 .tex= \Eq_J§_J
%D # B0 B0' <- sl^ .plabel= a î
%D B0 B0' -> .plabel= a ÐP§
%D B0 B2 -> B0' B2' -> B2 B2' <-
%D B1 B3 -> B0' B1 <-| B2' B3 <-|
%D B0 B4 |-> B1 B5 |->
%D B2 B6 <-| B3 B7 <-|
%D B6 B7 <-| B6 B7 -> sl^^ .PLABEL= ^(0.5) {ñ}
%D B5 B7 -> .plabel= r \id
%D B4 B6 ->
%D # B4 B6 <- sl^ .plabel= r Ð{BCC}Î
%D B0 B2 midpoint B0' B2' midpoint harrownodes 7 17 nil <-|
%D B0' B2' midpoint B1 B3 midpoint harrownodes nil 20 nil <-|
%D B0 B2 midpoint B4 B6 midpoint dharrownodes 5 20 nil |->
%D B1 B3 midpoint B5 B7 midpoint dharrownodes nil 20 nil <-|
%D ))
%D (( b0 .tex= I b1 .tex= J b2 .tex= I×I b3 .tex= J×J
%D b0 b1 -> .plabel= b u
%D b0 b2 -> .plabel= l _I
%D b1 b3 -> .plabel= b _J
%D b2 b3 -> .plabel= r u×u
%D # b0 relplace 20 7 \pbsymbol{7}
%D ))
%D enddiagram
%
$$\diag{QEq1-std}$$
\newpage
% --------------------
% «eq-on-morphisms-2» (to ".eq-on-morphisms-2")
% (s "How the `Eq' functor acts on morphisms (2)" "eq-on-morphisms-2")
\myslide {How the `Eq' functor acts on morphisms (2)} {eq-on-morphisms-2}
% (find-jacobspage (+ 19 291) "\"equality relation\" functor")
(Jacobs, p.291)
%: u;(J)=(I);u×u \Eq_J(§(J))
%: ----------------------------------------------
%: u^*(J)^*\Eq_J(§(J))->(I)^*(u×u)^*\Eq_J(§(J))
%:
%: ^Eq1a
%:
%: \Eq_J(§(J))->\Eq_J(§(J))
%: ------------------------
%: u §(J)->(J)^*\Eq_J(§(J))
%: -------------------------------
%: §(I) u §(J) u^*(§(J))->u^*(J)^*\Eq_J(§(J)) u;(J)=(I);u×u
%: ---------------ÐP§ ----------------------------------------------------
%: §(I)->u^*(§(J)) u^*(§(J))->(I)^*(u×u)^*\Eq_J(§(J))
%: -------------------------------------------------------------------
%: §(I)->(I)^*(u×u)^*\Eq_J(§(J))
%: ------------------------------
%: \Eq_I(§(I))->(u×u)^*\Eq_J(§(J))
%:
%: ^Eq1b
%:
%: u×u \Eq_J(§(J))
%: ------------------------------{ñ}
%: \Eq_I(§(I))->(u×u)^*\Eq_J(§(J)) (u×u)^*\Eq_J(§(J))->\Eq_J(§(J))
%: ------------------------------------------------------------------
%: \Eq_I(§(I))->\Eq_J(§(J))
%:
%: ^Eq1c
%:
$$\ded{Eq1a}$$
$$\ded{Eq1b}$$
$$\ded{Eq1c}$$
\msk
%: (a|->b|->b,b')=(a|->a,a'|->b,b') \ssst{b,b'}{b{=}b'}
%: ------------------------------------------------------
%: a||b{=}b|-b{=}b
%:
%: ^Eq1a-dnc
%:
%: b,b'||b{=}b'|-b{=}b'
%: -------------------
%: a|->b b||§|-b{=}b
%: ----------------------
%: \ssst{a}{§} a|->b \ssst{b}{§} a||§|-b{=}b (a|->b|->b,b')=(a|->a,a'|->b,b)
%: ------------------------------- ----------------------------------------------
%: a||§|-§ a||§|-b{=}b
%: ---------------------------------------------------------
%: a||§|-b{=}b
%: -------------------
%: a,a'||a{=}a'|-b{=}b'
%:
%: ^Eq1b-dnc
%:
%: a,a'|->b,b' \ssst{b,b'}{b{=}b'}
%: ---------------------------------------
%: a,a'||a{=}a'|-b{=}b' (a,a'\,||\,b{=}b')|->(b,b'\,||\,b{=}b')
%: --------------------------------------------------------------
%: (a,a'\,||\,a{=}a')|->(b,b'\,||\,b{=}b')
%:
%: ^Eq1c-dnc
%:
$$\ded{Eq1a-dnc}$$
$$\ded{Eq1b-dnc}$$
$$\ded{Eq1c-dnc}$$
\newpage
% --------------------
% «adjunctions» (to ".adjunctions")
% (s "Adjunctions" "adjunctions")
\myslide {Adjunctions} {adjunctions}
% (find-LATEX "2008comprcat.tex" "ccw1")
% (find-jacobspage (+ 19 294) "4.8.3. Theorem")
(Jacobs, p.294)
%D diagram ??
%D 2Dx 100 +20 +20 +20 +20
%D 2D 100 § ======> a=a'
%D 2D v v
%D 2D +20 {}Rbb <==== Rbb'{}
%D 2D <== <==
%D 2D +20 a |-----> a,a'
%D 2D +10 Rbb <====== Rbb'
%D 2D <-| |-> |->
%D 2D +20 b|_{Rbb} `---> b |------> b,b'
%D 2D
%D 2D
%D (( § a=a' # 0 1
%D {}Rbb Rbb'{} # 2 3
%D Rbb Rbb' # 4 5
%D @ 0 @ 1 =>
%D @ 0 @ 2 |-> @ 1 @ 3 |->
%D @ 2 @ 3 <=
%D @ 2 @ 4 <= @ 3 @ 5 <=
%D @ 4 @ 5 <=
%D ))
%D (( a a,a' # 0 1
%D b|_{Rbb} b b,b' # 2 3 4
%D @ 0 @ 1 |-> @ 0 @ 2 <-| @ 0 @ 3 |-> @ 1 @ 4 |->
%D @ 2 @ 3 `-> @ 3 @ 4 |->
%D ))
%D (( Rbb b|_{Rbb} =>
%D Rbb b =>
%D ))
%D enddiagram
%D
$$\diag{??}$$
%D diagram 4.8.3
%D 2Dx 100 +40 +40 +40 +40
%D 2D 100 Raa' |-----------------> b=b' |----------------> Scc'
%D 2D || \\ /\ // ||
%D 2D || \\ || // ||
%D 2D \/ \/ || \/ \/
%D 2D +20 a;a' |-->> a/R;a'/R |--> b;b' |--> c|S;c'|S `--> c;c'
%D 2D
%D (( Raa' b=b' Scc' # 0 1 2
%D a;a' a/R;a'/R b;b' c|S;c'|S c;c' # 3 4 5 6 7
%D c|S;c'|S .tex= c|_{Scc},c'|_{Sc'c'}
%D @ 0 @ 1 |-> @ 1 @ 2 |->
%D @ 0 @ 3 => @ 0 @ 4 => @ 1 @ 5 <= @ 2 @ 6 => @ 2 @ 7 =>
%D @ 3 @ 4 |->> @ 4 @ 5 |-> @ 5 @ 6 |-> @ 6 @ 7 `->
%D ))
%D enddiagram
%D
$$\diag{4.8.3}$$
%*
\end{document}
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: