|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% This is the `eqfibs.metatex' file of dednat4.
% Copyright 2005 Eduardo Ochs <edrx@mat.puc-rio.br>
% Author: Eduardo Ochs <edrx@mat.puc-rio.br>
% Version: 2005feb24
% License: GPL (I'll add the complete headers later)
% Latest: http://angg.twu.net/dednat4/eqfibs.metatex
% This is a "real-world" test for the diagrams feature of dednat4.
% (code-c-d "tese" "/oldfs/7/pandahome/edrx/LATEX/dout/")
% (find-tesefile "")
% (find-tesefile "tscats.metatex")
% (find-tesefile "tscats.metatex" "b=b''")
% (find-tesefile "defs-dnt.tex")
% (find-angg "LATEX/edrx.sty")
% (eebg-xdvi "/oldfs/7/pandahome/edrx/LATEX/dout/chapters.dvi")
% (eebg-xdvi "/oldfs/7/pandahome/edrx/LATEX/2002h.dvi")
% (eebg-xdvi "/oldfs/7/pandahome/edrx/LATEX/2003a.dvi")
% (eebg-xdvi "/oldfs/7/pandahome/edrx/LATEX/2003d.dvi")
% (find-tesefile "../2002h.tex")
% (find-tesefile "../2003a.tex")
% (find-tesefile "../2003d.tex")
\documentclass[oneside]{book}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{proof}
\input diagxy
\input demodefs.tex
% \xyoption{curve}
\begin{document}
\input eqfibs.dnt
\def\id{\mathrm{id}}
\def\nat{\natural}
\def\Frob{\mathrm{Frob}}
\def\BCC{\mathrm{BCC}}
\def\newpage{\vfill\break}
%L standardabbrevs()
%L require "experimental.lua"
%L forths["sl_"] = macro(".slide= -2.5pt")
%L forths["sl^"] = macro(".slide= 2.5pt")
%:*.=*{=}*
%:*&* \land *
%:*&*{\land}*
% (find-tesefile "defs-dnt.tex" "_|")
%
\def\pbsymbol#1{%
\begin{picture}(#1,#1)
\put(0,0){\line(1,0){#1}}
\put(#1,#1){\line(0,-1){#1}}
\end{picture}}
% (find-dednat "experimental.lua")
%L emitTeX = function (arrow)
%L return arrow.TeX
%L end
%L forths["relplace"] = function ()
%L local x, y = ds[1].x, ds[1].y
%L local dx, dy = getwordasluaexpr(), getwordasluaexpr()
%L local TeX = getword()
%L storearrow {special=emitTeX, TeX = format(
%L "\\place(%d,%d)[{%s}]", realx(x+dx), realy(y+dy), TeX
%L )}
%L end
%L forths["_|"] = macro "relplace 7 7 \\pbsymbol{7}"
%L
%L placetoTeX = function (arrow)
%L local node = arrow.from
%L return format("\\place(%d,%d)[{%s}]", realx(node.x), realy(node.y),
%L node.TeX)
%L end
%L forths["place"] = function ()
%L storearrow {special=placetoTeX, from=ds[1]}
%L end
%%%%%
%
% BCC and Frobenius maps in several fibrations
% (only LCCCs at the moment)
%
%%%%%
%D diagram LCCC-BCC
%D 2Dx 100 +30 +25 +30
%D 2D 100 {}d ===============> c,d{}
%D 2D - /\ - ^
%D 2D | \\ |-> | |\BCC
%D 2D v \\ v -
%D 2D +20 {}c,d <=\\=========== c,d{}{}
%D 2D /\ \\ /\
%D 2D +10 \\ d ===============> c,d{{}}
%D 2D \\ - \\ -
%D 2D \\ | <-| \\ |\id
%D 2D \\ v \\ v
%D 2D +20 c,d <============== c,d{{}}{}
%D 2D
%D 2D
%D 2D +10 a,b,c |----------> a,b
%D 2D - _| -
%D 2D \ \
%D 2D v v
%D 2D +35 a,c |--------------> a
%D 2D
%D (( {}d c,d{} # 0 1
%D {}c,d c,d{}{} # 2 3
%D d c,d{{}} # 4 5
%D c,d c,d{{}}{} # 6 7
%D @ 0 @ 1 =>
%D @ 0 @ 2 |-> @ 1 @ 3 |-> sl_ .plabel= l \natural
%D @ 1 @ 3 <-| sl^ .plabel= r \mathrm{BCC}
%D @ 0 @ 3 harrownodes nil 20 nil |->
%D @ 2 @ 3 <=
%D @ 0 @ 4 <= @ 2 @ 6 <= @ 3 @ 7 <=
%D @ 0 @ 2 midpoint @ 4 @ 6 midpoint dharrownodes nil 14 nil <-|
%D @ 4 @ 5 => @ 4 @ 6 |-> @ 5 @ 7 |-> .plabel= r \mathrm{id}
%D @ 4 @ 7 harrownodes nil 20 nil <-|
%D @ 6 @ 7 <=
%D ))
%D (( a,b,c a,b
%D a,c a
%D @ 0 @ 1 |-> @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 |->
%D @ 0 relplace 15 7 \pbsymbol{7}
%D ))
%D enddiagram
%D
% $$\diag{LCCC-BCC}$$
% (find-tesefile "NOTES" "%D diagram Frob-functional")
%D diagram Frob-functional
%D 2Dx 100 +30 +35
%D 2D 100 c =================> b,c
%D 2D ^ ----> ^
%D 2D \pi| / |\pi
%D 2D - - Frob -
%D 2D +20 c,d => b,(c,d) <--| (b,c),d
%D 2D - - |--> -
%D 2D \pi'| \ nat |\pi'
%D 2D v ------> v
%D 2D +20 d <================= d{}
%D 2D
%D 2D +15 a,b |----------------> a
%D 2D
%D (( c b,c # 0 1
%D c,d b,(c,d) (b,c),d # 2 3 4
%D d d{} # 5 6
%D @ 0 @ 1 =>
%D @ 0 @ 3 harrownodes 15 20 nil |->
%D @ 0 @ 2 <-| .plabel= l \pi @ 1 @ 3 <-| @ 1 @ 4 <-| .plabel= r \pi
%D @ 2 @ 3 =>
%D @ 3 @ 4 |-> sl_ .plabel= b \nat @ 3 @ 4 <-| sl^ .plabel= a \Frob
%D @ 2 @ 5 |-> .plabel= l \pi' @ 3 @ 6 |-> @ 4 @ 6 |-> .plabel= r \pi'
%D @ 5 @ 3 harrownodes 15 20 nil |->
%D @ 5 @ 6 <=
%D ))
%D (( a,b a |->
%D ))
%D enddiagram
%D
% $$\diag{Frob-functional}$$
$$\diag{LCCC-BCC} \qquad \diag{Frob-functional}$$
%%%%%
%
% Equality fibrations: identity, reflexivity, transitivity
% (only transitivity at the moment)
%
%%%%%
%D diagram fibeq-trans-1
%D 2Dx 100 +25 +45 +35
%D 2D 100 {b'.=b''\;\;\;\;b.=b'}
%D 2D
%D 2D +18 {b'.=b''&\,b.=b'}
%D 2D ^ -
%D 2D \nat| |Frob
%D 2D - v
%D 2D +20 b.=b' ===> b'.=b''&\,b.=b'
%D 2D - -
%D 2D id| |-> |
%D 2D v v
%D 2D +20 {}b.=b' <======== b.=b''
%D 2D /=> <=\
%D 2D // \\
%D 2D // \\
%D 2D +20 \top ============================> b=b''
%D 2D
%D 2D +15 a,b,b' |-----> a,b,b',b''
%D 2D ^ |
%D 2D / \
%D 2D |- v
%D 2D +20 a,b |---------------------------> a,b,b''
%D 2D
%D (( {b'.=b''\;\;\;\;b.=b'}
%D {b'.=b''&\,b.=b'} # 0
%D b.=b' b'.=b''&\,b.=b' # 1 2
%D {}b.=b' b.=b'' # 3 4
%D \top b=b'' # 5 6
%D # @ 1 @ 0 |-> .slide= 15pt .plabel= l \pi
%D # @ 1 @ 0 |-> .slide= -15pt .plabel= r \pi'
%D # @ 1 @ 3 <-| sl_ .plabel= l \natural
%D # @ 1 @ 3 |-> sl^ .plabel= r \mathrm{Frob}
%D @ 2 @ 3 =>
%D @ 2 @ 4 |-> .plabel= l \id @ 2 @ 5 hadjnodes |-> @ 3 @ 5 |->
%D @ 4 @ 5 <= @ 6 @ 4 => @ 4 @ 7 <= @ 5 @ 7 <= @ 6 @ 7 =>
%D ))
%D (( a,b,b' a,b,b',b'' # 0 1
%D a,b a,b,b'' # 2 3
%D @ 0 @ 1 |-> .plabel= a \delta
%D @ 2 @ 0 |-> .plabel= a \delta @ 0 @ 3 |-> .plabel= m {b'':=b} @ 1 @ 3 |->
%D @ 2 @ 3 |-> .plabel= m \delta @ 0 @ 3
%D ))
%D enddiagram
%D
$$\diag{fibeq-trans-1}$$
% (find-tesefile "tscats.metatex" "%D diagram fibeq-pairs-1\n")
\newpage
%%%%%
%
% Equality fibrations: pairs
%
%%%%%
%D diagram fibeq-pairs-1
%D 2Dx 100 +50 +30 +50
%D 2D 100 \top ==================> c_1.=c_2
%D 2D - /\ -
%D 2D | \\ |-> |
%D 2D v \\ v
%D 2D +20 (b,c).=(b,c) <======== (b_1,c_1).=(b_1,c_2)
%D 2D /\ \\ /\
%D 2D \\ \\ \\
%D 2D +10 \\ \top{} ==========> (b_1,c_1).=(b_2,c_2){}
%D 2D \\ - \\ -
%D 2D \\ | <-| \\ |\id
%D 2D \\ v \\ v
%D 2D +20 (b,c).=(b,c){} <====== (b_1,c_1).=(b_2,c_2){}{}
%D 2D
%D 2D
%D 2D +15 a,b,c |----------------> a,b_1,c_1,c_2
%D 2D - _| -
%D 2D \ \
%D 2D v v
%D 2D +30 a,(b,c) |-----------> a,(b_1,c_1),(b_2,c_2)
%D 2D
%D (( \top c_1.=c_2 # 0 1
%D (b,c).=(b,c) (b_1,c_1).=(b_1,c_2) # 2 3
%D \top{} (b_1,c_1).=(b_2,c_2){} # 4 5
%D (b,c).=(b,c){} (b_1,c_1).=(b_2,c_2){}{} # 6 7
%D @ 0 @ 1 =>
%D @ 0 @ 2 |-> @ 1 @ 3 |-> @ 0 @ 3 harrownodes nil 20 nil |->
%D @ 2 @ 3 <=
%D @ 0 @ 4 <= @ 2 @ 6 <= @ 3 @ 7 <=
%D @ 0 @ 2 midpoint @ 4 @ 6 midpoint dharrownodes nil 17 nil <-|
%D @ 4 @ 5 =>
%D @ 4 @ 6 |-> @ 5 @ 7 |-> .plabel= r \id
%D @ 4 @ 7 harrownodes nil 20 nil <-|
%D @ 6 @ 7 <=
%D ))
%D (( a,b,c a,b_1,c_1,c_2
%D a,(b,c) a,(b_1,c_1),(b_2,c_2)
%D @ 0 @ 1 |-> @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 |->
%D @ 0 relplace 23 7 \pbsymbol{7}
%D ))
%D enddiagram
%D
$$\diag{fibeq-pairs-1}$$
%D diagram fibeq-pairs-2
%D 2Dx 100 +50 +30 +50
%D 2D 100 \top ==================> b_1.=b_2
%D 2D - /\ -
%D 2D | \\ |-> |
%D 2D v \\ v
%D 2D +20 (b,c).=(b,c) <======== (b_1,c_1).=(b_2,c_1)
%D 2D /\ \\ /\
%D 2D \\ \\ \\
%D 2D +10 \\ \top{} ==========> (b_1,c_1).=(b_2,c_2){}
%D 2D \\ - \\ -
%D 2D \\ | <-| \\ |\id
%D 2D \\ v \\ v
%D 2D +20 (b,c).=(b,c){} <====== (b_1,c_1).=(b_2,c_2){}{}
%D 2D
%D 2D
%D 2D +15 a,c,b |---------------> a,c_1,b_1,b_2
%D 2D - _| -
%D 2D \ \
%D 2D v v
%D 2D +30 a,(b,c) |-----------> a,(b_1,c_1),(b_2,c_2)
%D 2D
%D (( \top b_1.=b_2 # 0 1
%D (b,c).=(b,c) (b_1,c_1).=(b_2,c_1) # 2 3
%D \top{} (b_1,c_1).=(b_2,c_2){} # 4 5
%D (b,c).=(b,c){} (b_1,c_1).=(b_2,c_2){}{} # 6 7
%D @ 0 @ 1 =>
%D @ 0 @ 2 |-> @ 1 @ 3 |-> @ 0 @ 3 harrownodes nil 20 nil |->
%D @ 2 @ 3 <=
%D @ 0 @ 4 <= @ 2 @ 6 <= @ 3 @ 7 <=
%D @ 0 @ 2 midpoint @ 4 @ 6 midpoint dharrownodes nil 17 nil <-|
%D @ 4 @ 5 =>
%D @ 4 @ 6 |-> @ 5 @ 7 |-> .plabel= r \id
%D @ 4 @ 7 harrownodes nil 20 nil <-|
%D @ 6 @ 7 <=
%D ))
%D (( a,c,b a,c_1,b_1,b_2
%D a,(b,c) a,(b_1,c_1),(b_2,c_2)
%D @ 0 @ 1 |-> @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 |->
%D @ 0 relplace 23 7 \pbsymbol{7}
%D ))
%D enddiagram
%D
$$\diag{fibeq-pairs-2}$$
%D diagram fibeq-pairs-3
%D 2Dx 100 +60 +60
%D 2D 100 b_1.=b_2&c_1.=c_2
%D 2D - - -
%D 2D / | \
%D 2D v | v
%D 2D +15 b_1.=b_2 | c_1.=c_2
%D 2D - | -
%D 2D | v |
%D 2D +10 | (b_1,c_1).=(b_2,c_1)&(b_2,c_1).=(b_2,c_2) |
%D 2D | - - - |
%D 2D | / | \ |
%D 2D v v | v v
%D 2D +15 (b_1,c_1).=(b_2,c_1) trans (b_2,c_1).=(b_2,c_2)
%D 2D |
%D 2D |
%D 2D v
%D 2D +15 (b_1,c_1).=(b_2,c_2)
%D 2D
%D 2D +15 a,b_1,c_1,b_2,c_2
%D 2D
%D (( b_1.=b_2&c_1.=c_2 # 0
%D b_1.=b_2 c_1.=c_2 # 1 2
%D (b_1,c_1).=(b_2,c_1)&(b_2,c_1).=(b_2,c_2) # 3
%D (b_1,c_1).=(b_2,c_1) (b_2,c_1).=(b_2,c_2) # 4 5
%D (b_1,c_1).=(b_2,c_2) # 6
%D a,b_1,c_1,b_2,c_2 place
%D @ 0 @ 1 |-> .plabel= b \pi @ 0 @ 2 |-> .plabel= b \pi'
%D @ 0 @ 3 |-> @ 1 @ 4 |-> @ 2 @ 5 |->
%D @ 3 @ 4 |-> .plabel= b \pi @ 3 @ 5 |-> .plabel= b \pi'
%D @ 3 @ 6 |-> .plabel= m \mathrm{trans}
%D ))
%D enddiagram
%D
$$\diag{fibeq-pairs-3}$$
% (find-eimage0 "~/IMAGES/preslim.png")
%(find-eimage0 "/tmp/screenshots/ss1.png")
\def\smallpb#1#2#3{
\begin{smallmatrix}
& & #1 \mathstrut \\
& & \downarrow \\
#2 & \to & #3 \mathstrut \\
\end{smallmatrix}
}
%D diagram preslims
%D 2Dx 100 +47 +45 +40 +40
%D 2D 100 {}a =========> aaa ===> aLaLaL <===== a^L <=========== a
%D 2D - - - - -
%D 2D | <-> | <-> | <-> | <-> |
%D 2D v v v v v
%D 2D +30 (b^R,c^R)|_{d^R} <= bRcRdR <=== bcd ===> (b,c)|_d ===> ((b,c)|_d)^R
%D 2D
%D (( {}a aaa .tex= \left(\smallpb{a}{a}{a}\right)
%D aLaLaL .tex= \left(\smallpb{a^L}{a^L}{a^L}\right) a^L a
%D (b^R,c^R)|_{d^R}
%D bRcRdR .tex= \left(\smallpb{b^R}{c^R}{d^R}\right)
%D bcd .tex= \left(\smallpb{b}{c}{d}\right) (b,c)|_d ((b,c)|_d)^R
%D @ 0 @ 1 => @ 1 @ 2 => @ 2 @ 3 <= @ 3 @ 4 <=
%D @ 0 @ 5 |-> @ 1 @ 6 |-> @ 2 @ 7 |-> @ 3 @ 8 |-> @ 4 @ 9 |->
%D @ 0 @ 6 harrownodes nil 20 nil <->
%D @ 1 @ 7 harrownodes nil 20 nil <->
%D @ 2 @ 8 harrownodes nil 20 nil <->
%D @ 3 @ 9 harrownodes nil 20 nil <->
%D @ 5 @ 6 <= @ 6 @ 7 <= @ 7 @ 8 => @ 8 @ 9 =>
%D ))
%D enddiagram
%D
$$\diag{preslims}$$
\end{document}
#####
#
# e-scripts (see http://angg.twu.net/)
#
#####
#*
mkdir /tmp/dn4/
cd /tmp/dn4/
unzip -a -o $S/ftp/ftp.math.mcgill.ca/pub/barr/diagxy.zip
cp $S/http/www.ctan.org/tex-archive/macros/latex/contrib/proof/proof.sty .
cp ~/dednat4/demodefs.tex .
cp ~/dednat4/eqfibs.metatex .
#*
# (find-node "(kpathsea)Supported file formats")
# (find-node "(kpathsea)Supported file formats" "`TEXINPUTS'; suffix `.tex'")
# (find-node "(web2c)tex invocation" "KPATHSEA_DEBUG")
cd ~/dednat4/
~/dednat4/dednat4.lua eqfibs.metatex && \
TEXINPUTS=/tmp/dn4: \
latex eqfibs.tex && \
xdvi eqfibs.dvi &
#*
% Local Variables:
% coding: raw-text-unix
% mode: latex
% End: