|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2008topos-str.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008topos-str.tex && latex 2008topos-str.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008topos-str.tex && pdflatex 2008topos-str.tex"))
% (eev "cd ~/LATEX/ && Scp 2008topos-str.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (find-dvipage "~/LATEX/2008topos-str.dvi")
% (find-pspage "~/LATEX/2008topos-str.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2008topos-str.ps 2008topos-str.dvi")
% (find-pspage "~/LATEX/2008topos-str.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% «.biccc-and classifier» (to "biccc-and classifier")
% «.pre-hyperdoctrine» (to "pre-hyperdoctrine")
% «.topos-ccompc» (to "topos-ccompc")
% «.nnos-basic-constructions» (to "nnos-basic-constructions")
% «.nnos-p-prime» (to "nnos-p-prime")
\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 2008topos-str.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 {The BiCCC structure and the classifier axiom} {2}
\tocline {The pre-hyperdoctrine structure} {3}
\tocline {Two CCompC structures in a topos} {4}
\tocline {Basic constructions with NNOs} {5}
\tocline {NNOs: the morphism $\kappa $} {6}
%:*&*\&*
\newpage
% --------------------
% «biccc-and classifier» (to ".biccc-and classifier")
% (s "The BiCCC structure and the classifier axiom" "biccc-and classifier")
\myslide {The BiCCC structure and the classifier axiom} {biccc-and classifier}
%D diagram CCC
%D 2Dx 100 +25 +25 +15 +20 +25
%D 2D 100 --| p0 |- t0 a0 <==== a1
%D 2D / - \ - - -
%D 2D / | \ | | <--> |
%D 2D v v v v v v
%D 2D +25 p1 <--| p2 |--> p3 t1 a2 ====> a3
%D 2D
%D 2D +15 c0 |--> c1 <--| c2 i0
%D 2D / - \ -
%D 2D \ | / |
%D 2D \ v / v
%D 2D +25 --> c3 <- i1
%D 2D
%D (( p0 .tex= a
%D p1 .tex= b p2 .tex= b,c p3 .tex= c
%D @ 0 @ 1 |-> @ 0 @ 2 |-> @ 0 @ 3 |->
%D @ 1 @ 2 <-| @ 2 @ 3 |->
%D ))
%D (( c0 .tex= a c1 .tex= a÷b c2 .tex= b
%D c3 .tex= c
%D @ 0 @ 1 |-> @ 1 @ 2 <-|
%D @ 0 @ 3 |-> @ 1 @ 3 |-> @ 2 @ 3 |->
%D ))
%D (( t0 .tex= a t1 .tex= *
%D @ 0 @ 1 |->
%D ))
%D (( i0 .tex= ® i1 .tex= a
%D @ 0 @ 1 |->
%D ))
%D (( a0 .tex= a,b a1 .tex= a
%D a2 .tex= c a3 .tex= b|->c
%D @ 0 @ 1 <= @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D diagram HA
%D 2Dx 100 +25 +25 +15 +20 +25
%D 2D 100 --| p0 |- t0 a0 <==== a1
%D 2D / - \ - - -
%D 2D / | \ | | <--> |
%D 2D v v v v v v
%D 2D +25 p1 <--| p2 |--> p3 t1 a2 ====> a3
%D 2D
%D 2D +15 c0 |--> c1 <--| c2 i0
%D 2D / - \ -
%D 2D \ | / |
%D 2D \ v / v
%D 2D +25 --> c3 <- i1
%D 2D
%D (( p0 .tex= P
%D p1 .tex= Q p2 .tex= Q&R p3 .tex= R
%D @ 0 @ 1 |-> @ 0 @ 2 |-> @ 0 @ 3 |->
%D @ 1 @ 2 <-| @ 2 @ 3 |->
%D ))
%D (( c0 .tex= P c1 .tex= P∨Q c2 .tex= Q
%D c3 .tex= R
%D @ 0 @ 1 |-> @ 1 @ 2 <-|
%D @ 0 @ 3 |-> @ 1 @ 3 |-> @ 2 @ 3 |->
%D ))
%D (( t0 .tex= P t1 .tex= {§}
%D @ 0 @ 1 |->
%D ))
%D (( i0 .tex= ® i1 .tex= P
%D @ 0 @ 1 |->
%D ))
%D (( a0 .tex= P&Q a1 .tex= P
%D a2 .tex= R a3 .tex= Q⊃R
%D @ 0 @ 1 <= @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D diagram Topos
%D 2Dx 100 +25 +20 +25
%D 2D 100 pb0 |---> pb1 cl0 |---> cl1
%D 2D - __| - v __| v
%D 2D | | | --\ |
%D 2D v v v v v
%D 2D +25 pb2 |---> pb3 cl2 |---> cl3
%D 2D
%D (( pb0 .tex= (a,b)|_c pb1 .tex= b
%D pb2 .tex= a pb3 .tex= c
%D @ 0 @ 1 |-> @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 |->
%D # @ 0 _|
%D @ 0 relplace 8 8 \pbsymbol{7}
%D ))
%D (( cl0 .tex= a|_P cl1 .tex= *
%D cl2 .tex= a cl3 .tex= Ï
%D @ 0 @ 1 |-> @ 0 @ 2 >-> @ 1 @ 3 >-> .plabel= r § @ 2 @ 3 |-> .plabel= a P
%D # @ 0 _|
%D @ 0 relplace 8 8 \pbsymbol{7}
%D ))
%D enddiagram
CCC:
$\diag{CCC}$
\medskip
HA:
$\diag{HA}$
\medskip
Topos:
\smallskip
$\diag{Topos}$
\newpage
% --------------------
% «pre-hyperdoctrine» (to ".pre-hyperdoctrine")
% (s "The pre-hyperdoctrine structure" "pre-hyperdoctrine")
\myslide {The pre-hyperdoctrine structure} {pre-hyperdoctrine}
%D diagram Hyperdoctrine
%D 2Dx 100 +30 +30 +45 +35 +40
%D 2D 100 eq0 =====> eq1 aw0 =====> aw1
%D 2D - - - -
%D 2D | <--> | | <--> |
%D 2D |---> v v v v
%D 2D +30 s0 <==== s1 eq2 <===== eq3 aw2 <===== aw3
%D 2D - -
%D 2D | <--> |
%D 2D v v
%D 2D +30 aw4 =====> aw5
%D 2D
%D 2D +20 s2 |---> s3 eq4 |----> eq5 aw6 |----> aw7
%D
%D (( s0 .tex= \s[a|P] s1 .tex= \s[b|P]
%D @ 0 @ 1 <= sl_ @ 0 @ 1 |-> sl^ .plabel= a {ñ}
%D ))
%D (( s2 .tex= a s3 .tex= b
%D @ 0 @ 1 |->
%D ))
%D (( eq0 .tex= \s[a,b|P] eq1 .tex= \s[a,b,b'|b{=}b'&P]
%D eq2 .tex= \s[a,b|{Q[b,b]}] eq3 .tex= \s[a,b,b'|{Q[b,b']}]
%D @ 0 @ 1 => sl_ @ 0 @ 1 |-> sl^ .plabel= a \co{ñ}
%D @ 2 @ 3 <= sl_ @ 2 @ 3 |-> sl^ .plabel= a {ñ}
%D @ 0 @ 2 |-> @ 1 @ 3 |-> @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D (( eq4 .tex= a,b eq5 .tex= a,b,b'
%D @ 0 @ 1 |->
%D ))
%D (( aw0 .tex= \s[a,b|P] aw1 .tex= \s[a|Îb.P]
%D aw2 .tex= \s[a,b|Q] aw3 .tex= \s[a|Q]
%D aw4 .tex= \s[a,b|R] aw5 .tex= \s[a|ýb.R]
%D @ 0 @ 1 => sl_ @ 0 @ 1 |-> sl^ .plabel= a \co{ñ}
%D @ 2 @ 3 <= sl_ @ 2 @ 3 |-> sl^ .plabel= a {ñ}
%D @ 4 @ 5 =>
%D @ 0 @ 2 |-> @ 1 @ 3 |-> @ 0 @ 3 harrownodes nil 20 nil <->
%D @ 2 @ 4 |-> @ 3 @ 5 |-> @ 2 @ 5 harrownodes nil 20 nil <->
%D ))
%D (( aw6 .tex= a,b aw7 .tex= a
%D @ 0 @ 1 |->
%D ))
%D enddiagram
%D diagram LCCC
%D 2Dx 100 +30 +30 +45 +35 +40
%D 2D 100 eq0 =====> eq1 aw0 =====> aw1
%D 2D - - - -
%D 2D | <--> | | <--> |
%D 2D |---> v v v v
%D 2D +30 s0 <==== s1 eq2 <===== eq3 aw2 <===== aw3
%D 2D - -
%D 2D | <--> |
%D 2D v v
%D 2D +30 aw4 =====> aw5
%D 2D
%D 2D +20 s2 |---> s3 eq4 |----> eq5 aw6 |----> aw7
%D
%D (( s0 .tex= \s[a|c] s1 .tex= \s[b|c]
%D @ 0 @ 1 <= sl_ @ 0 @ 1 |-> sl^ .plabel= a {ñ}
%D ))
%D (( s2 .tex= a s3 .tex= b
%D @ 0 @ 1 |->
%D ))
%D (( eq0 .tex= \s[a,b|c] eq1 .tex= \s[a,b,b'|(b{=}b'),c]
%D eq2 .tex= \s[a,b|d] eq3 .tex= \s[a,b,b'|d]
%D @ 0 @ 1 => sl_ @ 0 @ 1 |-> sl^ .plabel= a \co{ñ}
%D @ 2 @ 3 <= sl_ @ 2 @ 3 |-> sl^ .plabel= a {ñ}
%D @ 0 @ 2 |-> @ 1 @ 3 |-> @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D (( eq4 .tex= a,b eq5 .tex= a,b,b'
%D @ 0 @ 1 |->
%D ))
%D (( aw0 .tex= \s[a,b|c] aw1 .tex= \s[a|b,c]
%D aw2 .tex= \s[a,b|d] aw3 .tex= \s[a|d]
%D aw4 .tex= \s[a,b|e] aw5 .tex= \s[a|{b|->e}]
%D @ 0 @ 1 => sl_ @ 0 @ 1 |-> sl^ .plabel= a \co{ñ}
%D @ 2 @ 3 <= sl_ @ 2 @ 3 |-> sl^ .plabel= a {ñ}
%D @ 4 @ 5 =>
%D @ 0 @ 2 |-> @ 1 @ 3 |-> @ 0 @ 3 harrownodes nil 20 nil <->
%D @ 2 @ 4 |-> @ 3 @ 5 |-> @ 2 @ 5 harrownodes nil 20 nil <->
%D ))
%D (( aw6 .tex= a,b aw7 .tex= a
%D @ 0 @ 1 |->
%D ))
%D enddiagram
Hyperdoctrine:
\smallskip
$\diag{Hyperdoctrine}$
\medskip
LCCC:
\smallskip
$\diag{LCCC}$
\newpage
% --------------------
% «topos-ccompc» (to ".topos-ccompc")
% (s "Two CCompC structures in a topos" "topos-ccompc")
\myslide {Two CCompC structures in a topos} {topos-ccompc}
The two CCompC structures in a topos:
%D diagram CCompHyp
%D 2Dx 100 +30 +30
%D 2D 100 a0 |---> a1 |---> a2
%D 2D || ^ /\ ^ ||
%D 2D || | || | ||
%D 2D \/ v || v \/
%D 2D +30 a3 |---> a4 |---> a5
%D 2D
%D (( a0 .tex= \s[a|P] a1 .tex= \s[b|§] a2 .tex= \s[c|Q]
%D a3 .tex= a a4 .tex= b a5 .tex= c|_Q
%D @ 0 @ 1 |-> @ 1 @ 2 |->
%D @ 0 @ 3 => @ 1 @ 4 <= @ 2 @ 5 =>
%D @ 0 @ 4 varrownodes nil 20 nil <->
%D @ 1 @ 5 varrownodes nil 20 nil <->
%D @ 3 @ 4 |-> @ 4 @ 5 |->
%D ))
%D enddiagram
%D diagram CCompLCCC
%D 2Dx 100 +30 +30
%D 2D 100 a0 |---> a1 |---> a2
%D 2D || ^ /\ ^ ||
%D 2D || | || | ||
%D 2D \/ v || v \/
%D 2D +30 a3 |---> a4 |---> a5
%D 2D
%D (( a0 .tex= \s[a|b] a1 .tex= \s[c|*] a2 .tex= \s[d|e]
%D a3 .tex= a a4 .tex= c a5 .tex= d,e
%D @ 0 @ 1 |-> @ 1 @ 2 |->
%D @ 0 @ 3 => @ 1 @ 4 <= @ 2 @ 5 =>
%D @ 0 @ 4 varrownodes nil 20 nil <->
%D @ 1 @ 5 varrownodes nil 20 nil <->
%D @ 3 @ 4 |-> @ 4 @ 5 |->
%D ))
%D enddiagram
%D
$$\diag{CCompHyp} \qquad \diag{CCompLCCC}$$
\medskip
Cartesian morphisms project into pullbacks:
%D diagram display1
%D 2Dx 100 +30 +30 +30 +30 +30 +30 +45 +45
%D 2D 100 a0 / q0 / e0 /
%D 2D // || /\ \ // || \\ \ // || \\ \
%D 2D // || \\ v // || \\ v // || \\ v
%D 2D \/ \/ \\ \/ \/ \/ \/ \/ \/
%D 2D +30 a2 |--> a3 a1 q2 |--> q3 q1 e2 |--> e3 e1
%D 2D / / // || / / // || / / // ||
%D 2D \ // || \ // || \ // ||
%D 2D v \/ v \/ v \/ v \/ v \/ v \/
%D 2D +30 a4 |--> a5 q4 |--> q5 e4 |--> e5
%D 2D
%D (( a0 .tex= \s[a|P] a1 .tex= \s[b|P]
%D a2 .tex= a|_P a3 .tex= a
%D a4 .tex= b|_P a5 .tex= b
%D @ 0 @ 1 <= sl_ @ 0 @ 1 |-> sl^ .plabel= a {ñ}
%D @ 0 @ 2 => @ 0 @ 3 => @ 1 @ 4 => @ 1 @ 5 =>
%D @ 2 @ 3 |-> @ 2 @ 4 |-> @ 3 @ 5 |-> @ 4 @ 5 |->
%D @ 2 relplace 16 6 \pbsymbol{7}
%D ))
%D enddiagram
%D diagram displayLCCC1
%D 2Dx 100 +30 +30 +30 +30 +30 +30 +45 +45
%D 2D 100 a0 / q0 / e0 /
%D 2D // || /\ \ // || \\ \ // || \\ \
%D 2D // || \\ v // || \\ v // || \\ v
%D 2D \/ \/ \\ \/ \/ \/ \/ \/ \/
%D 2D +30 a2 |--> a3 a1 q2 |--> q3 q1 e2 |--> e3 e1
%D 2D / / // || / / // || / / // ||
%D 2D \ // || \ // || \ // ||
%D 2D v \/ v \/ v \/ v \/ v \/ v \/
%D 2D +30 a4 |--> a5 q4 |--> q5 e4 |--> e5
%D 2D
%D (( a0 .tex= \s[a|c] a1 .tex= \s[b|c]
%D a2 .tex= a,c a3 .tex= a
%D a4 .tex= b,c a5 .tex= b
%D @ 0 @ 1 <= sl_ @ 0 @ 1 |-> sl^ .plabel= a {ñ}
%D @ 0 @ 2 => @ 0 @ 3 => @ 1 @ 4 => @ 1 @ 5 =>
%D @ 2 @ 3 |-> @ 2 @ 4 |-> @ 3 @ 5 |-> @ 4 @ 5 |->
%D @ 2 relplace 16 6 \pbsymbol{7}
%D ))
%D enddiagram
$$\diag{display1} \qquad \diag{displayLCCC1}$$
\medskip
%D diagram display2
%D 2Dx 100 +30 +30 +30 +30 +30 +30 +45 +45
%D 2D 100 a0 / q0 / e0 /
%D 2D // || /\ \ // || \\ \ // || \\ \
%D 2D // || \\ v // || \\ v // || \\ v
%D 2D \/ \/ \\ \/ \/ \/ \/ \/ \/
%D 2D +30 a2 |--> a3 a1 q2 |--> q3 q1 e2 |--> e3 e1
%D 2D / / // || / / // || / / // ||
%D 2D \ // || \ // || \ // ||
%D 2D v \/ v \/ v \/ v \/ v \/ v \/
%D 2D +30 a4 |--> a5 q4 |--> q5 e4 |--> e5
%D 2D
%D (( q0 .tex= \s[a,b|P] q1 .tex= \s[a|Îb.P]
%D q2 .tex= a,b|_P q3 .tex= a,b
%D q4 .tex= a|_{Îb.P} q5 .tex= a
%D @ 0 @ 1 => sl_ @ 0 @ 1 |-> sl^ .plabel= a \co{ñ}
%D @ 0 @ 2 => @ 0 @ 3 => @ 1 @ 4 => @ 1 @ 5 =>
%D @ 2 @ 3 |-> @ 2 @ 4 |->> @ 3 @ 5 |-> @ 4 @ 5 |->
%D ))
%D (( e0 .tex= \s[a,b|P] e1 .tex= \s[a|b{=}b'&P]
%D e2 .tex= a,b|_P e3 .tex= a,b
%D e4 .tex= a,b,b'|_{b{=}b'&P} e5 .tex= a,b,b'
%D @ 0 @ 1 => sl_ @ 0 @ 1 |-> sl^ .plabel= a \co{ñ}
%D @ 0 @ 2 => @ 0 @ 3 => @ 1 @ 4 => @ 1 @ 5 =>
%D @ 2 @ 3 |-> @ 2 @ 4 <-> @ 3 @ 5 `-> @ 4 @ 5 |->
%D ))
%D enddiagram
%D diagram displayLCCC2
%D 2Dx 100 +30 +30 +30 +30 +30 +30 +45 +45
%D 2D 100 a0 / q0 / e0 /
%D 2D // || /\ \ // || \\ \ // || \\ \
%D 2D // || \\ v // || \\ v // || \\ v
%D 2D \/ \/ \\ \/ \/ \/ \/ \/ \/
%D 2D +30 a2 |--> a3 a1 q2 |--> q3 q1 e2 |--> e3 e1
%D 2D / / // || / / // || / / // ||
%D 2D \ // || \ // || \ // ||
%D 2D v \/ v \/ v \/ v \/ v \/ v \/
%D 2D +30 a4 |--> a5 q4 |--> q5 e4 |--> e5
%D 2D
%D (( q0 .tex= \s[a,b|c] q1 .tex= \s[a|b,c]
%D q2 .tex= (a,b),c q3 .tex= a,b
%D q4 .tex= a,(b,c) q5 .tex= a
%D @ 0 @ 1 => sl_ @ 0 @ 1 |-> sl^ .plabel= a \co{ñ}
%D @ 0 @ 2 => @ 0 @ 3 => @ 1 @ 4 => @ 1 @ 5 =>
%D @ 2 @ 3 |-> @ 2 @ 4 <-> @ 3 @ 5 |-> @ 4 @ 5 |->
%D ))
%D (( e0 .tex= \s[a,b|c] e1 .tex= \s[a|(b{=}b'),c]
%D e2 .tex= a,b,c e3 .tex= a,b
%D e4 .tex= a,b,b',(b{=}b'),c e5 .tex= a,b,b'
%D @ 0 @ 1 => sl_ @ 0 @ 1 |-> sl^ .plabel= a \co{ñ}
%D @ 0 @ 2 => @ 0 @ 3 => @ 1 @ 4 => @ 1 @ 5 =>
%D @ 2 @ 3 |-> @ 2 @ 4 <-> @ 3 @ 5 `-> @ 4 @ 5 |->
%D ))
%D enddiagram
%D
Cocartesian morphisms induce isos and epis:
$$\diag{display2}$$
$$\diag{displayLCCC2}$$
\newpage
% --------------------
% «nnos-basic-constructions» (to ".nnos-basic-constructions")
% (s "Basic constructions with NNOs" "nnos-basic-constructions")
\myslide {Basic constructions with NNOs} {nnos-basic-constructions}
% (find-eoutput '(insert 8760))
%:*-.*{\overset{.}{-}}*
\widemtos
%D diagram NNO+
%D 2Dx 100 +40 +45 +45 +45
%D 2D 100 * |--> 0 |--> 1 |--> 2 m
%D 2D / - - - -
%D 2D \ | | | |
%D 2D v v v v v
%D 2D +30 a0 |-> a1 |-> a2 am
%D 2D
%D (( a0 .tex= (n|->n) a1 .tex= (n|->n{+}1) a2 .tex= (n|->n{+}2)
%D am .tex= n|->n{+}m
%D * 0 |-> 0 1 |-> 1 2 |->
%D * a0 |-> a0 a1 |-> a1 a2 |->
%D 0 a0 |-> 1 a1 |-> 2 a2 |-> m am |->
%D ))
%D enddiagram
%D
$$\diag{NNO+}$$
%D diagram NNO*
%D 2Dx 100 +40 +45 +45 +45
%D 2D 100 * |--> 0 |--> 1 |--> 2 m
%D 2D / - - - -
%D 2D \ | | | |
%D 2D v v v v v
%D 2D +30 a0 |-> a1 |-> a2 am
%D 2D
%D (( a0 .tex= (n|->0) a1 .tex= (n|->n) a2 .tex= (n|->2n)
%D am .tex= n|->mn
%D * 0 |-> 0 1 |-> 1 2 |->
%D * a0 |-> a0 a1 |-> a1 a2 |->
%D 0 a0 |-> 1 a1 |-> 2 a2 |-> m am |->
%D ))
%D enddiagram
%D
$$\diag{NNO*}$$
%D diagram NNOexp
%D 2Dx 100 +40 +45 +45 +45
%D 2D 100 * |--> 0 |--> 1 |--> 2 m
%D 2D / - - - -
%D 2D \ | | | |
%D 2D v v v v v
%D 2D +30 a0 |-> a1 |-> a2 am
%D 2D
%D (( a0 .tex= (n|->1) a1 .tex= (n|->n) a2 .tex= (n|->n^2)
%D am .tex= n|->n^m
%D * 0 |-> 0 1 |-> 1 2 |->
%D * a0 |-> a0 a1 |-> a1 a2 |->
%D 0 a0 |-> 1 a1 |-> 2 a2 |-> m am |->
%D ))
%D enddiagram
%D
$$\diag{NNOexp}$$
%D diagram NNO-
%D 2Dx 100 +40 +45 +45 +45
%D 2D 100 * |--> 0 |--> 1 |--> 2 m
%D 2D / - - - -
%D 2D \ | | | |
%D 2D v v v v v
%D 2D +30 a0 |-> a1 |-> a2 am
%D 2D
%D (( a0 .tex= (n|->n) a1 .tex= (n|->n-.1) a2 .tex= (n|->n-.2)
%D am .tex= n|->n-.m
%D * 0 |-> 0 1 |-> 1 2 |->
%D * a0 |-> a0 a1 |-> a1 a2 |->
%D 0 a0 |-> 1 a1 |-> 2 a2 |-> m am |->
%D ))
%D enddiagram
%D
$$\diag{NNO-}$$
\newpage
% --------------------
% «nnos-p-prime» (to ".nnos-p-prime")
% (s "NNOs: the morphism $p'$" "nnos-p-prime")
\myslide {NNOs: the morphism $p'$} {nnos-p-prime}
\def\kk{\kappa}
%:*+*{+}*
Fact: in a topos with NNO the map $[0,s]: 1{+}N \to N$ is an iso.
\msk
First we need to define the arrow $s': 1{+}N \to 1{+}N$,
using a factorization through a coproduct.
Note that $s'$ takes the `$*$' in `$*÷n$' to 0, not to $*'$.
$s' := [0;\kk',s;\kk']$.
%D diagram NNO-sprime
%D 2Dx 100 +20 +20 +20 +20
%D 2D 100 a0 ---> a2 <--- a4
%D 2D \ | /
%D 2D v | v
%D 2D +20 b1 | b3
%D 2D \ | /
%D 2D vv v
%D 2D +20 c2
%D 2D
%D (( a0 .tex= 1 a2 .tex= 1+N a4 .tex= N
%D b1 .tex= N b3 .tex= N
%D c2 .tex= 1+N
%D a0 a2 -> .plabel= a \kk a2 a4 <- .plabel= a \kk'
%D a0 b1 -> .plabel= l 0 b1 c2 -> .plabel= l \kk'
%D a2 c2 -> .plabel= m s'
%D a4 b3 -> .plabel= r s
%D b3 c2 -> .plabel= r \kk'
%D ))
%D enddiagram
%D
%D diagram NNO-sprime-dnc
%D 2Dx 100 +20 +20 +20 +20
%D 2D 100 a0 ---> a2 <--- a4
%D 2D \ | /
%D 2D v | v
%D 2D +20 b1 | b3
%D 2D \ | /
%D 2D vv v
%D 2D +20 c2
%D 2D
%D (( a0 .tex= * a2 .tex= *÷n a4 .tex= n
%D b1 .tex= 0 b3 .tex= n+1
%D c2 .tex= *'÷n+1
%D a0 a2 -> a2 a4 <-
%D a0 b1 -> b1 c2 -> a2 c2 -> a4 b3 -> b3 c2 ->
%D ))
%D enddiagram
\msk
$\diag{NNO-sprime} \qquad \diag{NNO-sprime-dnc}$
\bsk
Now we can define $p': N \to 1+N$ by factoring $(\kk, s')$ through the NNO.
It is possible to show that $p'$ and $[0,s]$ are inverses.
%D diagram NNO+1
%D 2Dx 100 +30 +30 +30 +30
%D 2D 100 a0 ---> a1 ----> a2 ---> a3 a4
%D 2D | \ | | | |
%D 2D | \ | | | |
%D 2D | \ v v v v
%D 2D +20 \ -> b1 ----> b2 ---> b3 b4
%D 2D \ | | | |
%D 2D \ | | | |
%D 2D \ v v v v
%D 2D +20 -> c1 ----> c2 ---> c3 c4
%D 2D
%D (( a0 .tex= 1 a1 .tex= N a2 .tex= N a3 .tex= N a4 .tex= N
%D b1 .tex= 1+N b2 .tex= 1+N b3 .tex= 1+N b4 .tex= 1+N
%D c1 .tex= N c2 .tex= N c3 .tex= N c4 .tex= N
%D a0 a1 -> .plabel= a 0
%D a1 a2 -> .plabel= a s a2 a3 -> .plabel= a s
%D b1 b2 -> .plabel= a s' b2 b3 -> .plabel= a s'
%D c1 c2 -> .plabel= a s c2 c3 -> .plabel= a s
%D a0 b1 -> .plabel= m \kk
%D a1 b1 -> .plabel= r p'
%D a2 b2 -> .plabel= r p'
%D a3 b3 -> .plabel= r p'
%D a4 b4 -> .plabel= r p'
%D a0 c1 -> .plabel= l 0
%D b1 c1 -> .plabel= r [0,s]
%D b2 c2 -> .plabel= r [0,s]
%D b3 c3 -> .plabel= r [0,s]
%D b4 c4 -> .plabel= r [0,s]
%D ))
%D enddiagram
%D
$$\diag{NNO+1}$$
%D diagram NNO+1-dnc
%D 2Dx 100 +30 +30 +30 +30
%D 2D 100 a0 ---> a1 ----> a2 ---> a3 a4
%D 2D | \ | | | |
%D 2D | \ | | | |
%D 2D | \ v v v v
%D 2D +20 \ -> b1 ----> b2 ---> b3 b4
%D 2D \ | | | |
%D 2D \ | | | |
%D 2D \ v v v v
%D 2D +20 -> c1 ----> c2 ---> c3 c4
%D 2D
%D (( a0 .tex= * a1 .tex= 0 a2 .tex= 1 a3 .tex= 2 a4 .tex= n
%D b1 .tex= *÷0' b2 .tex= *'÷1' b3 .tex= *''÷2' b4 .tex= *÷n{-}1
%D c1 .tex= 0 c2 .tex= 1 c3 .tex= 2 c4 .tex= n
%D a0 a1 -> a1 a2 -> a2 a3 ->
%D b1 b2 -> b2 b3 ->
%D c1 c2 -> c2 c3 ->
%D a0 b1 -> a1 b1 -> a2 b2 -> a3 b3 -> a4 b4 ->
%D a0 c1 -> b1 c1 -> b2 c2 -> b3 c3 -> b4 c4 ->
%D ))
%D enddiagram
%D
$$\diag{NNO+1-dnc}$$
\msk
\def\dotminus{\overset{.}{-}}
%:*-.*{\dotminus}*
Define $n \mto n {\dotminus} 1$ as $p';[0,\id]$,
The arrow $m \mto (n \dotminus m)$ of the previous page
% (find-dn4ex "edrx08.sty")
% (find-dn4 "experimental.lua")
%*
\end{document}
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: