|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2008dclosed.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008dclosed.tex && latex 2008dclosed.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008dclosed.tex && pdflatex 2008dclosed.tex"))
% (eev "cd ~/LATEX/ && Scp 2008dclosed.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (find-dvipage "~/LATEX/2008dclosed.dvi")
% (find-pspage "~/LATEX/2008dclosed.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2008dclosed.ps 2008dclosed.dvi")
% (find-pspage "~/LATEX/2008dclosed.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2008dclosed.pdf" (ee-twupfile "LATEX/2008dclosed.pdf") 'over)
% (ee-cp "~/LATEX/2008dclosed.pdf" (ee-twusfile "LATEX/2008dclosed.pdf") 'over)
% «.why-slides» (to "why-slides")
% «.mod-induces-dclosed» (to "mod-induces-dclosed")
% «.mod-induces-dclosed-2» (to "mod-induces-dclosed-2")
% «.dncing-dense-closed» (to "dncing-dense-closed")
% «.dncing-dense-closed-2» (to "dncing-dense-closed-2")
% «.etc» (to "etc")
\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 2008dclosed.dnt
%*
% (eedn4-51-bounded)
Notes about factorization systems -
esp.\ the dense/closed factorizations for monics.
\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 {Why slides} {2}
\tocline {A modality induces a dense/close factorization} {3}
\tocline {A modality induces a dense/close factorization (2)} {4}
\tocline {Downcasing dense and closed maps} {5}
\tocline {Downcasing dense and closed maps (2)} {6}
\tocline {etc} {7}
%:*>->*\monicto *
%:*<-<*\monicot *
%L forths[">.>"] = function () pusharrow(" >.>") end
%L forths["<.<"] = function () pusharrow(" <.<") end
%L forths["`.>"] = function () pusharrow("^{ (}.>") end
%L forths["|-"] = function () pusharrow("|-") end
%L forths["-|"] = function () pusharrow("-|") end
\def\j{¦j}
\def\sm#1{\begin{smallmatrix}#1\end{smallmatrix}}
\newpage
% --------------------
% «why-slides» (to ".why-slides")
% (s "Why slides" "why-slides")
\myslide {Why slides} {why-slides}
% (find-es "tex" "smash")
\def\mysmash#1{{\setbox0\hbox{#1}%
\wd0=0pt\ht0=0pt\dp0=0pt%
\box0}}
\def\tl#1{\begin{tabular}{l}#1\end{tabular}}
%D diagram ??
%D 2Dx 100 +60
%D 2D 100 \boxrps \boxcts
%D 2D
%D 2D +40 \boxssl \boxlpp
%D 2D
%D 2D +40 \boxips \boxstu
%D 2D
%D (( \boxrps \boxcts
%D \boxssl \boxlpp
%D \boxips \boxstu
%D @ 0 @ 1 ->
%D @ 0 @ 3 -> @ 2 @ 1 ->
%D @ 2 @ 3 ->
%D @ 2 @ 5 -> @ 4 @ 3 ->
%D @ 4 @ 5 ->
%D ))
%D enddiagram
%D
$$
\def\boxcts{\tl{Category \\ Theorists}}
\def\boxlpp{\tl{local alge\mysmash{braic} \\ geometers / \\ logicians / \\ CS people}}
\def\boxstu{\tl{students}}
\def\boxrps{\tl{``real'' \\ papers}}
\def\boxssl{\tl{seminars, \\ slides}}
\def\boxips{\tl{introductory \\ papers}}
\diag{??}
$$
moral proofs, intuition, archetypal examples
new language, with translation (not as formal as C/H)
private devices
lifting and generalization
Several kinds of brownie points (cite Simmons)
Translation of notations in several articles
A new language, vs.\ a new truth.
Draw the mnemonics for
Sometimes I think that this may look like an autistic exercise - too
much energy spent on just rephrasing two well-known papers into a new
notation.
{\sl How does one work the standard, ``algebraic'' notation?} I've
spent
Even after working with it for years, the standard, ``algebraic''
notation,
However, the downcased notation reflects exactly how I think about
certain problems, and I still find - even after many years - the usual
(I'll call it ``standard'') algebraic notation hard to follow.
This is probably because I don't know the tricks.
What are the mnemonics/skeletons?
Social effects:
few people around me know category theory
some people to whom I've shown this have found it very nice (maybe
they were just being polite?)
there's a gap between not knowing and knowing CT
\bsk
Truth vs. translation
Making things obvious, tautological; zooming into proofs
I will try to describe it in linguistical terms.
Native speaker
\msk
A new language, vs.\ a new truth.
Only one real ``theorem'' --- about filter-powers. It needs sheaves.
The big metatheorems ahead involve parametricity (and polymorphism and hyperdoctrines).
Another possibility: Property-Like Structures.
\msk
I do not want the brownie points now [Simmons].
Sheaves: I learned a lot from Simmons course notes.
Actually there are several ways to get brownie points - seminars,
talks in conferences, introductory papers,
I'm looking for coauthors (and energy)
Translate the notation in several important books
\msk
Barr: *-Autonomous Cats
Bierman/dePaiva: S4
Cheng: Mathematics, Morally
Corfield: [Towards a Philosophy of Real Mathematics]
Freyd: Algebraic categories
Jacobs: Tijolão
Jacobs: Comprehension Cats
Joyal/Street: On the Geometry of Tensor Calculus
Kelly/Lack: On Property-Like Structures
Kock: A simple axiomatics for differentiation
Lawvere (easy book): external/internal view
MacLane: CWM
Pitts: Polymorphism is Set-Theoretic, constructively
Reyes/Zolfaghari: Topos-theoretic approaches to modality
Reynolds: Polymorphism is notCategorical Semantics for Higher Order Polymorphic Lambda Calculus Set-Theoretic
Seely: Hyperdoctrines
Seely: Categorical Semantics for Higher Order Polymorphic Lambda Calculus
Seely: Differential Cats
Wadler: The Girard/Reynods iso
Wadler: Theorems for Free
\newpage
% --------------------
% «mod-induces-dclosed» (to ".mod-induces-dclosed")
% (s "A modality induces a dense/close factorization" "mod-induces-dclosed")
\myslide {A modality induces a dense/close factorization} {mod-induces-dclosed}
Any map $j:Ø \to Ø$ induces ``the right half'' of a factorization
for the monics of a topos, in a way that is stable by pullbacks:
any diagram $A \to B \monicot P$ induces the bigger diagram below,
%D diagram mod-ind-fact
%D 2Dx 100 +20 +20 +20 +40 +20 +20
%D 2D 100 AP BP 1
%D 2D
%D 2D +30 AP* BP* 1*
%D 2D
%D 2D +30 A B Ø Ø*
%D 2D
%D (( AP .tex= A×_BP BP .tex= P
%D AP* .tex= A×_BP^* BP* .tex= P^* 1* .tex= 1
%D Ø* .tex= Ø
%D BP* .tex= \j_BP
%D AP* .tex= \sm{\j_A(A×_BP)\,\cong\\A×_B(\j_BP)}
%D ))
%D (( AP BP -> BP 1 ->
%D AP AP* >.> AP* A >-> AP A >->
%D BP BP* >.> BP* B >-> BP B >->
%D AP* BP* -> BP* 1* ->
%D A B -> .plabel= b f B Ø -> .plabel= b p Ø Ø* -> .plabel= b j
%D 1 Ø -> 1* Ø* ->
%D AP _| BP _|
%D AP* relplace 15 6 \pbsymbol{7}
%D BP* relplace 11 5 \pbsymbol{7}
%D ))
%D enddiagram
%D
$$\diag{mod-ind-fact}$$
where the `$\j_BP$'s are constructed as this:
%: P>->B
%: ------
%: p:B->Ø j:Ø->Ø
%: --------------
%: (p;j):B->Ø
%: ----------
%: \j_BP>->B
%:
%: ^jBP-construction
%:
$$\ded{jBP-construction}$$
$\j_A(A×_BP) \monicto A$ is classified by $(f;p);j$ and
$A×_B(\j_BP) \monicto A$ is classified by $f;(p;j)$,
so they are isomorphic.
\msk
If $j$ is ``inflationary'' then the dotted monics above exist.
This becomes easier to understand if we use a more logical language:
%
%D diagram P-to-jBP
%D 2Dx 100 +35 +30 +45
%D 2D 100 A0 A1 a0 a1
%D 2D
%D 2D +30 A2 A3 a2 a3
%D 2D
%D (( A0 .tex= \j_BP×_BP A1 .tex= P
%D A2 .tex= \j_BP A3 .tex= B
%D A0 A1 <->
%D A0 A2 >-> A1 A2 >.> A1 A3 >->
%D A2 A3 >->
%D ))
%D (( a0 .tex= \sst{b}{P^*{∧}P} a1 .tex= \sst{b}{P}
%D a2 .tex= \sst{b}{P^*} a3 .tex= B
%D a0 a1 <->
%D a0 a2 >-> a1 a2 >.> a1 a3 >->
%D a2 a3 >->
%D ))
%D enddiagram
%:
%: P|-P^*
%: ==========
%: P∧P|-P^*∧P
%: ==========
%: P|-P^*∧P
%:
%: ^P-to-jBP
%:
$$\cdiag{P-to-jBP} \qquad \cded{P-to-jBP}$$
\msk
By one of the standard lemmas on glueing pullbacks,
the square with the dotted monics in the top diagram is a pullback.
\newpage
% --------------------
% «mod-induces-dclosed-2» (to ".mod-induces-dclosed-2")
% (s "A modality induces a dense/close factorization (2)" "mod-induces-dclosed-2")
\myslide {A modality induces a dense/close factorization (2)} {mod-induces-dclosed-2}
Any inflationary map $j:Ø \to Ø$ induces a ``factorization''
for the monics of a topos, in a way that is stable by pullbacks...
any diagram $A \to B \monicot P$ induces the diagram below,
%D diagram mod-ind-fact-2
%D 2Dx 100 +20 +20 +20 +40 +20 +20
%D 2D 100 AP BP 1
%D 2D
%D 2D +30 AP* BP* 1*
%D 2D
%D 2D +30 A B Ø Ø*
%D 2D
%D (( AP .tex= A×_BP BP .tex= P
%D AP* .tex= A×_BP^* BP* .tex= P^* 1* .tex= 1
%D Ø* .tex= Ø
%D BP* .tex= \j_BP
%D AP* .tex= \sm{\j_A(A×_BP)\,\cong\\A×_B(\j_BP)}
%D ))
%D (( AP BP -> BP 1 ->
%D AP AP* >-> AP* A >->
%D BP BP* >-> BP* B >->
%D AP* BP* -> BP* 1* ->
%D A B -> .plabel= b f B Ø -> .plabel= b p Ø Ø* -> .plabel= b j
%D 1 Ø -> .plabel= m \hbox{\phantom{p}} 1* Ø* ->
%D AP _| BP _|
%D AP* relplace 14 7 \pbsymbol{7}
%D BP* relplace 7 7 \pbsymbol{7}
%D ))
%D enddiagram
%D
$$\diag{mod-ind-fact-2}$$
In the more logical notation, this becomes:
%D diagram mod-ind-fact-3
%D 2Dx 100 +20 +50 +40 +20 +20
%D 2D 100 AP BP 1
%D 2D
%D 2D +30 AP* BP* 1*
%D 2D
%D 2D +30 A B Ø Ø*
%D 2D
%D (( AP .tex= \sst{a}{P(fa)} BP .tex= \sst{b}{P(b)}
%D 1* .tex= 1
%D Ø* .tex= Ø
%D BP* .tex= \sst{a}{P^*(b)}
%D AP* .tex= \sm{\sst{a}{(P¢f)^*(a)}\\\cong\,\sst{a}{P^*(fa)}}
%D ))
%D (( AP BP -> BP 1 ->
%D AP AP* >-> AP* A >->
%D BP BP* >-> BP* B >->
%D AP* BP* -> BP* 1* ->
%D A B -> .plabel= b f B Ø -> .plabel= b p Ø Ø* -> .plabel= b j
%D 1 Ø -> .plabel= m \hbox{\phantom{p}} 1* Ø* ->
%D AP relplace 8 8 \pbsymbol{7}
%D BP relplace 8 8 \pbsymbol{7}
%D AP* relplace 14 10 \pbsymbol{7}
%D BP* relplace 9 8 \pbsymbol{7}
%D ))
%D enddiagram
%D
$$\diag{mod-ind-fact-3}$$
We will usually omit the parameter - as in `$P(fa)$' $\mto$ `$P$' -
and the `1's and `$Ø$'s when we downcase this.
The case where $A \to B$ is a monic ($\equiv \; b|_Q \mto b$)
is especially interesting - then the left column is formed
by adding `$∧Q$'s.
%D diagram mod-ind-fact-4
%D 2Dx 100 +35 +40 +35
%D 2D 100 a0 a1 b0 b1
%D 2D
%D 2D +30 a2 a3 b2 b3
%D 2D
%D 2D +30 a4 a5 b4 b5
%D 2D
%D (( a0 .tex= a|_P a1 .tex= b|_P
%D a2 .tex= a|_{P^*} a3 .tex= b|_{P^*}
%D a4 .tex= a a5 .tex= b
%D a0 a1 `->
%D a0 a2 `-> a1 a3 `->
%D a2 a3 `->
%D a2 a4 `-> a3 a5 `->
%D a4 a5 `->
%D a0 _| a2 _|
%D ))
%D (( b0 .tex= b|_{P∧Q} b1 .tex= b|_P
%D b2 .tex= b|_{P^*{∧}Q} b3 .tex= b|_{P^*}
%D b4 .tex= b|_{Q} b5 .tex= b
%D b0 b1 `->
%D b0 b2 `-> b1 b3 `->
%D b2 b3 `->
%D b2 b4 `-> b3 b5 `->
%D b4 b5 `->
%D b0 _| b2 _|
%D ))
%D enddiagram
%D
$$\diag{mod-ind-fact-4}$$
{\bf Crucial fact:}
every dense map is of the form $b|_{P∧Q} \ito b|_{P^*{∧}Q}$, and
every closed map is of the form $b|_{P^*{∧}Q} \ito b|_Q$!
\newpage
% --------------------
% «dncing-dense-closed» (to ".dncing-dense-closed")
% (s "Downcasing dense and closed maps" "dncing-dense-closed")
\myslide {Downcasing dense and closed maps} {dncing-dense-closed}
% (find-LATEX "2008hyp.tex" "adj-functors-as-seq-rules")
%D diagram foo
%D 2Dx 100 +60
%D 2D 100 P∧Q R
%D 2D - |b> -
%D 2D | |
%D 2D v <#| v
%D 2D +30 P^*∧Q S
%D 2D - <b| -
%D 2D | |
%D 2D v |#> v
%D 2D +30 Q T
%D 2D
%D (( P∧Q R P^*∧Q S Q T
%D @ 0 @ 2 |-
%D @ 1 @ 3 |-
%D @ 2 @ 4 |-
%D @ 3 @ 5 |-
%D @ 0 @ 3 harrownodes nil 20 nil -> sl^ .plabel= a R:=P∧Q,\;S:=P^*∧Q
%D @ 0 @ 3 harrownodes nil 20 nil <- sl_ .plabel= b P':=R,\;Q':=S
%D @ 2 @ 5 harrownodes nil 20 nil -> sl^ .plabel= a S:=P^*∧Q,\;T:=Q
%D @ 2 @ 5 harrownodes nil 20 nil <- sl_ .plabel= b P':=S,\;Q':=T
%D ))
%D enddiagram
$$\diag{foo}$$
\widemtos
The composites
$(P∧Q \vdash P^*∧Q) \mto (R \vdash S) \mto (P'∧Q' \vdash P'^*∧Q')$
and
$(P^*∧Q \vdash Q) \mto (S \vdash T) \mto (P'^*∧Q' \vdash Q')$
are identity maps:
\ssk
in the first one,
$(P'∧Q' \vdash P'^*∧Q') =$
$(R∧S \vdash R^*∧S) =$
$((P∧Q)∧(P^*∧Q) \vdash (P∧Q)^*∧(P^*∧Q)) =$
$(P∧Q \vdash P^*∧Q)$;
\ssk
in the second one,
$(P'^*∧Q' \vdash Q') =$
$(S^*∧T \vdash T) =$
$((P^*∧Q)^*∧Q \vdash Q) =$
$(P^*∧Q \vdash Q)$.
\newpage
% --------------------
% «dncing-dense-closed-2» (to ".dncing-dense-closed-2")
% (s "Downcasing dense and closed maps (2)" "dncing-dense-closed-2")
\myslide {Downcasing dense and closed maps (2)} {dncing-dense-closed-2}
%D diagram foo2
%D 2Dx 100 +60
%D 2D 100 P∧Q R
%D 2D - |b> -
%D 2D | |
%D 2D v <#| v
%D 2D +30 P^*∧Q S
%D 2D - <b| -
%D 2D | |
%D 2D v |#> v
%D 2D +30 Q T
%D 2D
%D (( P∧Q R P^*∧Q S Q T
%D @ 0 @ 2 |-
%D @ 1 @ 3 |-
%D @ 2 @ 4 |-
%D @ 3 @ 5 |-
%D @ 0 @ 3 harrownodes nil 20 nil -> sl^ .plabel= a R':=P∧Q,\;S':=P^*∧Q
%D @ 0 @ 3 harrownodes nil 20 nil <- sl_ .plabel= b P:=R,\;Q:=S
%D @ 2 @ 5 harrownodes nil 20 nil -> sl^ .plabel= a S':=P^*∧Q,\;T':=Q
%D @ 2 @ 5 harrownodes nil 20 nil <- sl_ .plabel= b P:=S,\;Q:=T
%D ))
%D enddiagram
$$\diag{foo2}$$
The other two composites,
$(R \vdash S) \mto (P∧Q \vdash P^*∧Q) \mto (R' \vdash S')$
and
$(S \vdash T) \mto (P^*∧Q \vdash Q) \mto (S' \vdash T')$,
should be identities iff $R \vdash S$ is dense and $S \vdash T$ is closed...
\ssk
Let's check. In the first one,
$(R' \vdash S') =$
$(P∧Q \vdash P^*∧Q) =$
$(R∧S \vdash R^*∧S) =$
$(R \vdash R^*∧S)$,
\ssk
and in the second one,
$(S' \vdash T') =$
$(P^*∧Q \vdash Q) =$
$(S^*∧T \vdash T)$;
\ssk
so what we need to prove is:
$R \vdash S$ is dense iff $S = R^*∧S$,
$S \vdash T$ is closed iff $S = S^*∧T$.
As $R^*∧S \vdash S$ and $S^*∧T \vdash T$, we just need to prove
$R \vdash S$ is dense iff $S \vdash R^*$,
$S \vdash T$ is closed iff $S \vdash S^*∧T$.
\newpage
% --------------------
% «etc» (to ".etc")
% (s "etc" "etc")
\myslide {etc} {etc}
%:*P**P^**
%:*Q**Q^**
\def\arr#1#2{\begin{array}{#1}#2\end{array}}
%L -- (find-dn4file "dednat4.lua")
%L forths[".dp="] = function ()
%L ds[1].placement = getword()
%L ds[1].label = "(d)"
%L end
%L forths[".cp="] = function ()
%L ds[1].placement = getword()
%L ds[1].label = "(c)"
%L end
%D diagram perm1
%D 2Dx 100 +35 +35 +40 +50 +45
%D 2D 100 a|_{P} a|_{P*} a A×_BC A×_Bj_BC A
%D 2D
%D 2D +30 b|_{P} b|_{P*} b C j_BC B
%D 2D
%D (( a|_{P} a|_{P*} a
%D b|_{P} b|_{P*} b
%D @ 0 @ 1 `-> .dp= a @ 1 @ 2 `-> .cp= a
%D @ 3 @ 4 `-> .dp= a @ 4 @ 5 `-> .cp= a
%D @ 0 @ 3 |-> @ 1 @ 4 |-> @ 2 @ 5 |->
%D @ 0 _| @ 1 _|
%D ))
%D (( A×_BC A×_Bj_BC A
%D C j_BC B
%D A×_Bj_BC .tex= \arr{c}{j_A{A×_BC}\\{\cong}A×_Bj_BC}
%D @ 0 @ 1 >-> .dp= a @ 1 @ 2 >-> .cp= a
%D @ 3 @ 4 >-> .dp= a @ 4 @ 5 >-> .cp= a
%D @ 0 @ 3 -> @ 1 @ 4 -> @ 2 @ 5 ->
%D @ 0 _| @ 1 _|
%D ))
%D enddiagram
%D
$$\diag{perm1}$$
%D diagram permanence2
%D 2Dx 100 +40 +35 +35 +45 +35
%D 2D 100 a|_{P∧Q} a|_{P*∧Q} a|_{Q} A×_BC j_C(A×_BC) C
%D 2D
%D 2D +30 a|_{P∧Q*} a|_{P*∧Q*} a|_{Q*} j_B(A×_BC) M j_AC
%D 2D
%D 2D +30 a|_{P} a|_{P*} a B j_AB A
%D 2D
%D (( a|_{P∧Q} a|_{P*∧Q} a|_{Q}
%D a|_{P∧Q*} a|_{P*∧Q*} a|_{Q*}
%D a|_{P} a|_{P*} a
%D @ 0 @ 1 `-> .dp= a @ 1 @ 2 `-> .cp= a
%D @ 0 @ 3 `-> .dp= l @ 1 @ 4 `-> .dp= l @ 2 @ 5 `-> .dp= l
%D @ 3 @ 4 `-> .dp= a @ 4 @ 5 `-> .cp= a
%D @ 3 @ 6 `-> .cp= l @ 4 @ 7 `-> .cp= l @ 5 @ 8 `-> .cp= l
%D @ 6 @ 7 `-> .dp= a @ 7 @ 8 `-> .cp= a
%D @ 0 _| @ 1 _| @ 3 _| @ 4 _|
%D ))
%D (( A×_BC j_C(A×_BC) C
%D j_B(A×_BC) M j_AC
%D B j_AB A
%D @ 0 @ 1 >-> .dp= a @ 1 @ 2 >-> .cp= a
%D @ 0 @ 3 >-> .dp= l @ 1 @ 4 >-> .dp= l @ 2 @ 5 >-> .dp= l
%D @ 3 @ 4 >-> .dp= a @ 4 @ 5 >-> .cp= a
%D @ 3 @ 6 >-> .cp= l @ 4 @ 7 >-> .cp= l @ 5 @ 8 >-> .cp= l
%D @ 6 @ 7 >-> .dp= a @ 7 @ 8 >-> .cp= a
%D @ 0 _| @ 1 _| @ 3 _| @ 4 _|
%D ))
%D enddiagram
%D
$$\diag{permanence2}$$
%D diagram permanence3
%D 2Dx 100 +35 +35 +35 +35 +35
%D 2D 100 a|_{P∧Q} C
%D 2D
%D 2D +30 a|_{P∧Q*} a|_{P*∧Q*} j_BC j_AC
%D 2D
%D 2D +30 a|_{P} a|_{P*} a B j_AB A
%D 2D
%D (( a|_{P∧Q}
%D a|_{P∧Q*} a|_{P*∧Q*}
%D a|_{P} a|_{P*} a
%D @ 0 @ 1 `-> .dp= l @ 0 @ 2 `-> .dp= r
%D @ 1 @ 2 `-> .dp= b
%D @ 1 @ 3 `-> .cp= l @ 2 @ 4 `-> .cp= l @ 2 @ 5 `-> .cp= r
%D @ 3 @ 4 `-> .dp= b @ 4 @ 5 `-> .cp= b
%D ))
%D (( C
%D j_BC j_AC
%D B j_AB A
%D @ 0 @ 1 >-> .dp= l @ 0 @ 2 >-> .dp= r
%D @ 1 @ 2 >-> .dp= b
%D @ 1 @ 3 >-> .cp= l @ 2 @ 4 >-> .cp= l @ 2 @ 5 >-> .cp= r
%D @ 3 @ 4 >-> .dp= b @ 4 @ 5 >-> .cp= b
%D ))
%D enddiagram
%D
$$\diag{permanence3}$$
%D diagram permanence4
%D 2Dx 100 +35 +35 +25 +0 +35 +35 +25
%D 2D 100 a|_{P} a|_{R} B D
%D 2D
%D 2D +30 a|_{Q} a|_{Q∨R} C C∨D
%D 2D
%D 2D +25 a|_{P*} a j_AB A
%D 2D
%D (( a|_{P} a|_{R}
%D a|_{Q} a|_{Q∨R}
%D a|_{P*} a
%D @ 0 @ 1 `-> .dp= a
%D @ 0 @ 2 `-> .dp= l @ 1 @ 3 `-> .dp= l @ 1 @ 4 `-> .dp= r
%D @ 2 @ 3 `-> .dp= a
%D @ 2 @ 4 `-> .dp= b @ 3 @ 4 `-> .dp= m @ 4 @ 5 `-> .cp= a
%D ))
%D (( B D
%D C C∨D
%D j_AB A
%D @ 0 @ 1 >-> .dp= a
%D @ 0 @ 2 >-> .dp= l @ 1 @ 3 >-> .dp= l @ 1 @ 4 >-> .dp= r
%D @ 2 @ 3 >-> .dp= a
%D @ 2 @ 4 >-> .dp= b @ 3 @ 4 >-> .dp= m @ 4 @ 5 >-> .cp= a
%D ))
%D enddiagram
%D
$$\diag{permanence4}$$
\def\calU{{\mathcal{U}}}
\def\calV{{\mathcal{V}}}
\def\calW{{\mathcal{W}}}
An open set $U$ is above and to the right of a point $\cc$ when $\cc Ý U$.
An open set $U$ is straight above a point $\aa$ when $\aa$ generates $U$.
A cover $\calU$ is above and to right of $W$ when $\bigcup \calU = W$.
A cover $\calU$ is straight above $U$ when $\bigcup \calU = U$.
% $\sst{a}{P(a)}$
%*
\end{document}
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: