|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2017planar-has-deleted.tex")
% (find-angg "LATEX/2017planar-has.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2017planar-has-deleted.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2017planar-has-deleted.pdf"))
% (defun e () (interactive) (find-LATEX "2017planar-has-deleted.tex"))
% (defun u () (interactive) (find-latex-upload-links "2017planar-has-deleted"))
% (find-xpdfpage "~/LATEX/2017planar-has-deleted.pdf")
% (find-sh0 "cp -v ~/LATEX/2017planar-has-deleted.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2017planar-has-deleted.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2017planar-has-deleted.pdf
% file:///tmp/2017planar-has-deleted.pdf
% file:///tmp/pen/2017planar-has-deleted.pdf
% http://angg.twu.net/LATEX/2017planar-has-deleted.pdf
% An improvised index with links to pages:
% (find-LATEXsh "grep phap 2017planar-has.tex")
% (find-LATEXsh "grep phap 2017planar-has-deleted.tex")
% (phai)
% «.picturedots» (to "picturedots")
% «.title» (to "title")
% «.introduction» (to "introduction")
%
% «.positional» (to "positional")
% «.ZDAGs» (to "ZDAGs")
% «.LR-coords» (to "LR-coords")
% «.ZHAs» (to "ZHAs")
% «.two-conventions» (to "two-conventions")
% «.prop-calc» (to "prop-calc")
% «.prop-calc-ZHA» (to "prop-calc-ZHA")
% «.HAs» (to "HAs")
% «.implication-formally» (to "implication-formally")
% «.logic-in-HAs» (to "logic-in-HAs")
% «.derived-rules» (to "derived-rules")
% «.topologies» (to "topologies")
% «.topologies-on-ZSets» (to "topologies-on-ZSets")
% «.topologies-as-partial-orders» (to "topologies-as-partial-orders")
% «.2CGs» (to "2CGs")
% «.topologies-on-2CGs» (to "topologies-on-2CGs")
% «.converting-ZHAs-2CAGs» (to "converting-ZHAs-2CAGs")
%
% «.piccs-and-slashings» (to "piccs-and-slashings")
% «.slash-partitions» (to "slash-partitions")
% «.slash-max» (to "slash-max")
% «.cuts-stopping-midway» (to "cuts-stopping-midway")
% «.slash-ops» (to "slash-ops")
% «.slash-ops-property» (to "slash-ops-property")
% «.slash-regions-and-ops» (to "slash-regions-and-ops")
% «.J-ops-and-regions» (to "J-ops-and-regions")
% «.no-Y-cuts-no-L-cuts» (to "no-Y-cuts-no-L-cuts")
% «.J-ops-and-connectives» (to "J-ops-and-connectives")
% «.J-cubes-as-partial-orders» (to "J-cubes-as-partial-orders")
% «.valuations-induce-POs» (to "valuations-induce-POs")
% «.comparing-partial-orders» (to "comparing-partial-orders")
% «.lindenbaum-fragments» (to "lindenbaum-fragments")
% «.polynomial-J-ops» (to "polynomial-J-ops")
% «.algebra-of-J-ops» (to "algebra-of-J-ops")
%
% «.question-marks-new» (to "question-marks-new")
% «.question-marks» (to "question-marks")
% «.rectangular-ZHAs» (to "rectangular-ZHAs")
% «.on-intervals-and-interiors» (to "on-intervals-and-interiors")
% «.how-J-ops-act-on-2CGs» (to "how-J-ops-act-on-2CGs")
% «.2017jun05» (to "2017jun05")
% «.2017jun06» (to "2017jun06")
% «.2017jun11» (to "2017jun11")
% «.rectangular-1» (to "rectangular-1")
%
% «.children» (to "children")
% «.comprehension» (to "comprehension")
\documentclass[oneside]{article}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage{color} % (find-LATEX "edrx15.sty" "colors")
\usepackage{colorweb} % (find-es "tex" "colorweb")
\usepackage{tikz}
\usepackage{proof} % (find-dn6 "preamble6.lua" "preamble0")
\input diagxy % (find-dn6 "preamble6.lua" "preamble0")
%
\usepackage{edrx15} % (find-angg "LATEX/edrx15.sty")
\input edrxaccents.tex % (find-angg "LATEX/edrxaccents.tex")
\input edrxchars.tex % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex")
%\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
%
\begin{document}
\catcode`\^^J=10
\directlua{dednat6dir = "dednat6/"}
\directlua{dofile(dednat6dir.."dednat6.lua")}
\directlua{texfile(tex.jobname)}
\directlua{verbose()}
\directlua{output(preamble1)}
\def\expr#1{\directlua{output(tostring(#1))}}
\def\eval#1{\directlua{#1}}
\def\pu{\directlua{pu()}}
\directlua{dofile "edrxtikz.lua"} % (find-LATEX "edrxtikz.lua")
\directlua{dofile "edrxpict.lua"} % (find-LATEX "edrxpict.lua")
%L V.__tostring = function (v) return format("(%.3f,%.3f)", v[1], v[2]) end
% «picturedots» (to ".picturedots")
% (find-LATEX "2016-2-GA-algebra.tex" "picturedots")
% (find-LATEX "2016-2-GA-algebra.tex" "comprehension-gab")
% (gaap 5)
%
\def\beginpicture(#1,#2)(#3,#4){\expr{beginpicture(v(#1,#2),v(#3,#4))}}
\def\pictaxes{\expr{pictaxes()}}
\def\pictdots#1{\expr{pictdots("#1")}}
\def\picturedotsa(#1,#2)(#3,#4)#5{%
\vcenter{\hbox{%
\beginpicture(#1,#2)(#3,#4)%
\pictaxes%
\pictdots{#5}%
\end{picture}%
}}%
}
\def\picturedots(#1,#2)(#3,#4)#5{%
\vcenter{\hbox{%
\beginpicture(#1,#2)(#3,#4)%
%\pictaxes%
\pictdots{#5}%
\end{picture}%
}}%
}
\def\sa{\rightsquigarrow}
\def\BPM{\mathsf{BPM}}
\def\WPM{\mathsf{WPM}}
\def\ZHAG{\mathsf{ZHAG}}
\def\catTwo{\mathbf{2}}
%\def\Pts{\mathcal{P}}
\def\calS{\mathcal{S}}
\def\und#1#2{\underbrace{#1}_{#2}}
\def\subst#1{\left[\begin{array}{rcl}#1\end{array}\right]}
\def\subst{\bsm}
% (find-LATEXfile "2015planar-has.tex" "\\def\\Mop")
\def\MP{\mathsf{MP}}
\def\J {\mathsf{J}}
\def\Mo {\mathsf{Mo}}
\def\Mop {\mathsf{Mop}}
\def\Sand{\mathsf{Sand}}
\def\ECa {\mathsf{EC}{\&}}
\def\ECv {\mathsf{EC}{∨}}
\def\ECS {\mathsf{ECS}}
\def\pdiag#1{\left(\diag{#1}\right)}
\def\ltor#1#2{#1\_{\to}\_#2}
\def\lotr#1#2{#1\_{\ot}\_#2}
\def\Int{{\operatorname{int}}}
\def\coInt{{\operatorname{\mathsf{coint}}}}
\def\propagate{\operatorname{\mathsf{prp}}}
%
\def\NoLcuts{\mathsf{No}λ\mathsf{cuts}}
\def\NoYcuts{\mathsf{NoYcuts}}
\def\astarcube{{\&}^*\mathsf{Cube}}
\def\ostarcube{{∨}^*\mathsf{Cube}}
\def\istarcube{{→}^*\mathsf{Cube}}
\def\acz{{\&}^*\mathsf{C}_0}
\def\ocz{{∨}^*\mathsf{C}_0}
\def\icz{{→}^*\mathsf{C}_0}
%
\def\astarcuben{{\&}^*\mathsf{Cube}_\mathsf{n}}
\def\ostarcuben{{∨}^*\mathsf{Cube}_\mathsf{n}}
\def\istarcuben{{→}^*\mathsf{Cube}_\mathsf{n}}
\def\astarcubev{{\&}^*\mathsf{Cube}_\mathsf{v}}
\def\ostarcubev{{∨}^*\mathsf{Cube}_\mathsf{v}}
\def\istarcubev{{→}^*\mathsf{Cube}_\mathsf{v}}
%
%\catcode`∧=13 \def∧{\mathop{\&}}
\def\biggest {\mathsf{biggest}}
\def\smallest{\mathsf{smallest}}
\def\Cuts {\mathsf{Cuts}}
\def\OPENS{\operatorname{\mathsf{Opens}}}
\def\OPENSPABD{\OPENS(\Opens_A(P),B,D)}
\def\OPENSPABD{\OPENS((P,A),B,D)}
\def\relevant {\operatorname{\mathsf{relev}}}
\def\qmarks {\operatorname{\mathsf{qmarks}}}
\def\forget {\operatorname{\mathsf{forget}}}
\def\propagate{\operatorname{\mathsf{prpgt}}}
\def\propagate{\operatorname{\mathsf{prp}}}
\def\biggest{\mathsf{biggest}}
\def\ess{\mathsf{ess}}
\def\calS{\mathcal{S}}
\def\calI{\mathcal{I}}
\def\calK{\mathcal{K}}
\def\calV{\mathcal{V}}
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
% (find-LATEX "idarct/idarct-preprint.tex")
% «title» (to ".title")
\title{Planar Heyting Algebras for Children - Deleted Parts}
\author{Eduardo Ochs}
% \begin{abstract}
% Not yet
% \end{abstract}
\maketitle
% ___ _ _ _ _
% |_ _|_ __ | |_ ___ __| |_ _ ___| |_(_) ___ _ __
% | || '_ \| __/ _ \ / _` | | | |/ __| __| |/ _ \| '_ \
% | || | | | || (_) | (_| | |_| | (__| |_| | (_) | | | |
% |___|_| |_|\__\___/ \__,_|\__,_|\___|\__|_|\___/|_| |_|
%
% «introduction» (to ".introduction")
This paper shows a way to interpret (propositional) intuitionistic
logic {\sl visually} (see section \ref{prop-calc-ZHA}).
The ``for children'' in the title has a precise, but somewhat unusual,
meaning, that is explained in sec.\ref{children}.
% \nopagebreak % (find-es "tex" "pagebreak")
% ____ _ _ _ _
% | _ \ ___ ___(_) |_(_) ___ _ __ __ _| |
% | |_) / _ \/ __| | __| |/ _ \| '_ \ / _` | |
% | __/ (_) \__ \ | |_| | (_) | | | | (_| | |
% |_| \___/|___/_|\__|_|\___/|_| |_|\__,_|_|
%
% «positional» (to ".positional")
\section{Positional notations}
\label {positional}
% Good (phap 1 "positional")
% (laq 2)
% (laq 3)
% (gaap 5)
% (to "picturedots")
\unitlength=8pt \def\closeddot{\circle*{0.4}}
\def\closeddot{\circle*{0.5}}
%L kite = ".1.|2.3|.4.|.5."
%L house = ".1.|2.3|4.5"
%L W = "1.2.3|.4.5."
%L guill = ".1.2|3.4.|.5.6"
%L hex = ".1.2.|3.4.5|.6.7."
%L mp = MixedPicture.new({def="dagKite", meta="s", scale="5pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagKite", meta="t", scale="4pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagHouse", meta="s", scale="5pt"}, z):zfunction(house):output()
%L mp = MixedPicture.new({def="dagW", meta="s", scale="4pt"}, z):zfunction(W):output()
%L mp = MixedPicture.new({def="dagGuill", meta="s", scale="4pt"}, z):zfunction(guill):output()
%L mp = MixedPicture.new({def="dagHex", meta="s", scale="4pt"}, z):zfunction(hex):output()
\pu
% _________ _ ____
% |__ / _ \ / \ / ___|___
% / /| | | |/ _ \| | _/ __|
% / /_| |_| / ___ \ |_| \__ \
% /____|____/_/ \_\____|___/
%
% «ZDAGs» (to ".ZDAGs")
\section{ZDAGs}
\label {ZDAGs}
% Good (phap 2 "ZDAGs")
% _ ____ _ _ _
% | | | _ \ ___ ___ ___ _ __ __| (_)_ __ __ _| |_ ___ ___
% | | | |_) | / __/ _ \ / _ \| '__/ _` | | '_ \ / _` | __/ _ \/ __|
% | |___| _ < | (_| (_) | (_) | | | (_| | | | | | (_| | || __/\__ \
% |_____|_| \_\ \___\___/ \___/|_| \__,_|_|_| |_|\__,_|\__\___||___/
%
% «LR-coords» (to ".LR-coords")
\section{LR-coordinates}
\label {LR-coords}
% Good (phap 3 "LR-coords")
\def\LR{\mathbb{LR}}
% ______ _ _
% |__ / | | | / \ ___
% / /| |_| | / _ \ / __|
% / /_| _ |/ ___ \\__ \
% /____|_| |_/_/ \_\___/
%
% «ZHAs» (to ".ZHAs")
\section{ZHAs}
\label {ZHAs}
% Good (phap 4 "ZHAs")
% _____ _ _
% |_ _|_ _____ ___ ___ _ ____ _____ _ __ | |_(_) ___ _ __ ___
% | | \ \ /\ / / _ \ / __/ _ \| '_ \ \ / / _ \ '_ \| __| |/ _ \| '_ \/ __|
% | | \ V V / (_) | | (_| (_) | | | \ V / __/ | | | |_| | (_) | | | \__ \
% |_| \_/\_/ \___/ \___\___/|_| |_|\_/ \___|_| |_|\__|_|\___/|_| |_|___/
%
% «two-conventions» (to ".two-conventions")
\section{Conventions on diagrams without axes}
\label {two-conventions}
% Good (phap 5 "two-conventions")
% ____ _
% | _ \ _ __ ___ _ __ ___ __ _| | ___
% | |_) | '__/ _ \| '_ \ / __/ _` | |/ __|
% | __/| | | (_) | |_) | | (_| (_| | | (__
% |_| |_| \___/| .__/ \___\__,_|_|\___|
% |_|
%
% «prop-calc» (to ".prop-calc")
\section{Propositional calculus}
\label {prop-calc}
% Good (phap 5 "prop-calc")
% ____ _ ______ _ _
% | _ \ _ __ ___ _ __ ___ __ _| | ___ |__ / | | | / \
% | |_) | '__/ _ \| '_ \ / __/ _` | |/ __| / /| |_| | / _ \
% | __/| | | (_) | |_) | | (_| (_| | | (__ / /_| _ |/ ___ \
% |_| |_| \___/| .__/ \___\__,_|_|\___| /____|_| |_/_/ \_\
% |_|
%
% «prop-calc-ZHA» (to ".prop-calc-ZHA")
\section{Propositional calculus in a ZHA}
\label {prop-calc-ZHA}
% Good (phap 7 "prop-calc-ZHA")
% _ _ _
% | | | | / \ ___
% | |_| | / _ \ / __|
% | _ |/ ___ \\__ \
% |_| |_/_/ \_\___/
%
% «HAs» (to ".HAs")
% Good (phap 7 "HAs")
\section{Heyting Algebras}
\label{HAs}
% __ __ _ _
% \ \ / _| ___ _ __ _ __ ___ __ _| | |_ _
% _____\ \ | |_ / _ \| '__| '_ ` _ \ / _` | | | | | |
% |_____/ / | _| (_) | | | | | | | | (_| | | | |_| |
% /_( ) |_| \___/|_| |_| |_| |_|\__,_|_|_|\__, |
% |/ |___/
%
% «implication-formally» (to ".implication-formally")
% Bad (phap 10 "implication-formally")
\section{Implication, formally}
\label {implication-formally}
{
\def\impen{\ton{\text{en}}}
\def\impeq{\ton{\text{eq}}}
\def\o#1{\mathop{\mathsf{#1}}}
\def\o#1{\mathbin{\mathsf{#1}}}
\def\a#1#2{\ang{#1,#2}}
\def\ab{\a ab}
\def\cd{\a cd}
\def\ef{\a ef}
\def\ab{ab}
\def\cd{cd}
\def\ef{ef}
\def\wh{\widehat}
The definition of `$→$' in sec.\ref{prop-calc-ZHA} is easy to state in
English and easy to calculate; the definition from sec.\ref{HAs} is
hard to calculate, but it is easy to check that it obeys the expected
equation. Let's refer to them as `$\impen$' and `$\impeq$'. If we
write $P=ab$, $Q=cd$, $R=ef$, we have:
%
$$\begin{array}{rcl}
\cd \impen \ef &:=& \begin{array}[t]{llll}
\o{if} & \cd \o{below} \ef & \o{then} & ⊤ \\
\o{elseif} & \cd \o{leftof} \ef & \o{then} & \o{ne}(\cd∧\ef) \\
\o{elseif} & \cd \o{rightof} \ef & \o{then} & \o{nw}(\cd∧\ef) \\
\o{elseif} & \cd \o{above} \ef & \o{then} & \ef \\
\o{end}
\end{array} \\
\end{array}
$$
$$(ab ≤ (cd \impeq ef)) ↔ ((ab ∧ cd) ≤ ef)$$
We want to check that $cd \impen ef$ obeys the same equation, i.e.,
%
$$(ab ≤ (cd \impen ef)) ↔ ((ab ∧ cd) ≤ ef)$$
%
and so `$\impen$' and `$\impeq$' are equivalent.
In `$\impen$' the order of the cases is very important. For example,
if $cd=21$ and $ef=23$ then both ``$\cd \o{below} \ef$'' and ``$\cd
\o{leftof} \ef$'' are true, but ``$\cd \o{below} \ef$'' takes
precedence and so $\cd \impen \ef = ⊤$. It easy to check that we can
redefine `$\impen$' as this:
%
$$\begin{array}{rcl}
\cd \impen \ef &=& \begin{array}[t]{llll}
\o{if} & c≤e∧d≤f & \o{then} & ⊤ \\
\o{elseif} & c>e∧d≤f & \o{then} & \o{ne}(\cd∧\ef) \\
\o{elseif} & c≤e∧d>f & \o{then} & \o{nw}(\cd∧\ef) \\
\o{elseif} & c>e∧d>f & \o{then} & \ef \\
\o{end},
\end{array} \\
\end{array}
$$
%
and now the four cases are disjoint.
Let's introduce a notation: a ``$\widehat{a}$'' means ``make this
digit as big possible without leaving the ZHA''. So,
%
%L mpnew({def="foo"}, "123RL232L1"):addlrs():output()
$$\pu
\text{in} \qquad \foo \qquad \text{we have} \qquad
\begin{array}{rclcl}
\wh1\wh2 &=& 54 &=& ⊤, \\
1\wh2 &=& 13 &=& \o{ne}(12), \\
\wh12 &=& 42 &=& \o{nw}(12); \\
\end{array}
% \quad ;
$$
%
it turns out that we can get rid of the `$\o{ne}$' and the `$\o{nw}$',
rewriting the definition of `$\impen$' as:
%
$$\begin{array}{rcl}
\cd \impen \ef &=& \begin{array}[t]{llll}
\o{if} & c≤e∧d≤f & \o{then} & \wh{e}\wh{f} \\
\o{elseif} & c>e∧d≤f & \o{then} & e\wh{f} \\
\o{elseif} & c≤e∧d>f & \o{then} & \wh{e}f \\
\o{elseif} & c>e∧d>f & \o{then} & \ef \\
\o{end},
\end{array} \\
\end{array}
$$
%
and ``$(ab ≤ (cd \impen ef)) ↔ ((ab ∧ cd) ≤ ef)$'' is equivalent to
the conjunction of these four statements:
%
\def\abcdef{ab ≤ (\cd \impen \ef)}
\def\abcdeF{ab ∧ \cd ≤ \ef}
\def\abcdem{\min(a,c)≤e ∧ \min(b,d)≤f}
\def\p{\phantom}
%
$$\begin{array}[t]{lllllllll}
c≤e∧d≤f &→& (\abcdef &↔& \abcdeF) \\
c>e∧d≤f &→& (\abcdef &↔& \abcdeF) \\
c≤e∧d>f &→& (\abcdef &↔& \abcdeF) \\
c>e∧d>f &→& (\abcdef &↔& \abcdeF) \\
\end{array} \\
$$
%
If we replace each `$cd \impen ef$' by $\wh{e}\wh{f}$, $e\wh{f}$,
$\wh{e}f$, $ef$ depending on in which case we are, and we replace each
`$\abcdeF$' by `$\min(a,c)≤e ∧ \min(b,d)≤f$', we get:
%
$$\begin{array}[t]{lllllllll}
c≤e∧d≤f &→& (ab≤\wh{e}\wh{f} &↔& \abcdem) \\
c>e∧d≤f &→& (ab≤e\wh{f} &↔& \abcdem) \\
c≤e∧d>f &→& (ab≤\wh{e}f &↔& \abcdem) \\
c>e∧d>f &→& (ab≤\ef &↔& \abcdem) \\
\end{array} \\
$$
%
Let's see how to prove the second implication. The third one is
similar to the second, and the first and the fourth are very easy. We
have
%
$$ab≤e\wh{f} \;\;↔\;\; a≤e∧b≤\wh{f} \;\;↔\;\; a≤e,$$
%
and when $c>e∧d≤f$ when have:
%
$$\abcdem \;\;↔\;\; a≤e∧⊤ \;\;↔\;\; a≤e.$$
}
% _ _ _ _ _ _
% | | ___ __ _(_) ___ (_)_ __ | | | | / \ ___
% | | / _ \ / _` | |/ __| | | '_ \ | |_| | / _ \ / __|
% | |__| (_) | (_| | | (__ | | | | | | _ |/ ___ \\__ \
% |_____\___/ \__, |_|\___| |_|_| |_| |_| |_/_/ \_\___/
% |___/
%
% «logic-in-HAs» (to ".logic-in-HAs")
% Good (phap 12 "logic-in-HAs")
\section{Logic in a Heyting Algebra}
\label {logic-in-HAs}
% ____ _ _ _
% | _ \ ___ _ __(_)_ _____ __| | _ __ _ _| | ___ ___
% | | | |/ _ \ '__| \ \ / / _ \/ _` | | '__| | | | |/ _ \/ __|
% | |_| | __/ | | |\ V / __/ (_| | | | | |_| | | __/\__ \
% |____/ \___|_| |_| \_/ \___|\__,_| |_| \__,_|_|\___||___/
%
% «derived-rules» (to ".derived-rules")
% Bad (phap 14 "derived-rules")
\subsection{Derived rules}
\label {derived-rules}
\def\HAness{\mathsf{HA-ness}}
\def\HAness{\textsf{HA-ness}}
% _____ _ _
% |_ _|__ _ __ ___ | | ___ __ _(_) ___ ___
% | |/ _ \| '_ \ / _ \| |/ _ \ / _` | |/ _ \/ __|
% | | (_) | |_) | (_) | | (_) | (_| | | __/\__ \
% |_|\___/| .__/ \___/|_|\___/ \__, |_|\___||___/
% |_| |___/
%
% «topologies» (to ".topologies")
\section{Topologies}
\label {topologies}
% Good (phap 18 "topologies")
% _____ _________ _
% |_ _|__ _ __ ___ ___ _ __ |__ / ___| ___| |_ ___
% | |/ _ \| '_ \/ __| / _ \| '_ \ / /\___ \ / _ \ __/ __|
% | | (_) | |_) \__ \ | (_) | | | | / /_ ___) | __/ |_\__ \
% |_|\___/| .__/|___/ \___/|_| |_| /____|____/ \___|\__|___/
% |_|
%
% «topologies-on-ZSets» (to ".topologies-on-ZSets")
\section{The default topology on a ZSet}
\label {topologies-on-ZSets}
% Good (phap 19 "topologies-on-ZSets")
% _____ _
% |_ _|__ _ __ ___ __ _ ___ ___ _ __ __| | ___ _ __ ___
% | |/ _ \| '_ \/ __| / _` / __| / _ \| '__/ _` |/ _ \ '__/ __|
% | | (_) | |_) \__ \ | (_| \__ \ | (_) | | | (_| | __/ | \__ \
% |_|\___/| .__/|___/ \__,_|___/ \___/|_| \__,_|\___|_| |___/
% |_|
%
% «topologies-as-partial-orders» (to ".topologies-as-partial-orders")
\section{Topologies as partial orders}
\label {topologies-as-partial-orders}
% Good (phap 19 "topologies-as-partial-orders")
% ____ ____ ____
% |___ \ / ___/ ___|___
% __) | | | | _/ __|
% / __/| |__| |_| \__ \
% |_____|\____\____|___/
%
% «2CGs» (to ".2CGs")
\section{2-Column Graphs}
\label {2CGs}
% Good (phap 22 "2CGs")
\def\LC {\mathsf{LC}}
\def\RC {\mathsf{RC}}
\def\TCG{\mathsf{2CG}}
\def\pile{\mathsf{pile}}
\def\l#1{#1\_}
\def\r#1{\_#1}
\def\ltor#1#2{#1\_{\to}\_#2}
\def\lotr#1#2{#1\_{\ot}\_#2}
\def\ltol#1#2{#1\_{\to}#2\_}
\def\rtor#1#2{\_#1{\to}\_#2}
%L -- (find-LATEX "edrxpict.lua" "TCG")
%L
%L tcg_big = {scale="10pt", meta="p", dv=2, dh=3, ev=0.32, eh=0.2}
%L tcg_medium = {scale= "8pt", meta="p s", dv=1, dh=2, ev=0.32, eh=0.25}
%L tcgnew = function (opts, def, str)
%L return TCG.new(opts, def, unpack(split(str, "[ %d]+")))
%L end
%L tcgbig = function (def, spec) return tcgnew(tcg_big, def, spec or tcg_spec) end
%L tcgmed = function (def, spec) return tcgnew(tcg_medium, def, spec or tcg_spec) end
%L
%L tcg = TCG.new(tcg_big, "foo", 3, 4, "34 23", "22 12"):lrs():vs():hs():output()
%L tcg_spec = "3, 4; 34 23, 22 12"
%L tcgmed("foo"):lrs():hs():output()
%L tcgmed("bar"):bus():hs():output()
%L tcg_spec = "4, 3; 32, 32"
%L tcgbig("foo"):lrs():vs():hs():output()
%L tcg_spec = "3, 4; 14, 32"
%L tcgbig("bar"):lrs():vs():hs():output()
% _____ ____ ____ ____
% |_ _|__ _ __ ___ ___ _ __ |___ \ / ___/ ___|___
% | |/ _ \| '_ \/ __| / _ \| '_ \ __) | | | | _/ __|
% | | (_) | |_) \__ \ | (_) | | | | / __/| |__| |_| \__ \
% |_|\___/| .__/|___/ \___/|_| |_| |_____|\____\____|___/
% |_|
%
% «topologies-on-2CGs» (to ".topologies-on-2CGs")
\section{Topologies on 2CGs}
\label {topologies-on-2CGs}
% Good (phap 23 "topologies-on-2CGs")
\catcode`↓=13 \def↓{\dnto}
\catcode`↓=13 \def↓{{\dnto}}
% ______ _ _ __ __ ____ ____ _ ____
% |__ / | | | / \ ___ / / \ \ |___ \ / ___| / \ / ___|___
% / /| |_| | / _ \ / __| / /_____\ \ __) | | / _ \| | _/ __|
% / /_| _ |/ ___ \\__ \ \ \_____/ / / __/| |___ / ___ \ |_| \__ \
% /____|_| |_/_/ \_\___/ \_\ /_/ |_____|\____/_/ \_\____|___/
%
% «converting-ZHAs-2CAGs» (to ".converting-ZHAs-2CAGs")
\section{Converting between ZHAs and 2CAGs}
\label {converting-ZHAs-2CAGs}
% Good (phap 25 "converting-ZHAs-2CAGs")
% ____ _
% | _ \(_) ___ ___ ___
% | |_) | |/ __/ __/ __|
% | __/| | (_| (__\__ \
% |_| |_|\___\___|___/
%
% «piccs-and-slashings» (to ".piccs-and-slashings")
\section{Piccs and slashings}
\label {piccs-and-slashings}
% Good (phap 28 "piccs-and-slashings")
\def\eqP{\underset{P}{\sim}}
\def\eqJ{\underset{J}{\sim}}
\def\eqP{\underset{\scriptscriptstyle P}{\sim}}
\def\eqJ{\underset{\scriptscriptstyle J}{\sim}}
\def\eqP{\sim_P}
\def\eqJ{\sim_J}
\def\eqL{\sim_L}
\def\eqR{\sim_R}
\def\eqS{\sim_S}
\def\eqF{\sim_F}
\def\eqQ{\sim_Q}
%L -- local putl, putr, cutl, cutr
%L -- mp = MixedPicture.new {scale="7pt", def="foo"}
%L -- putl = function (n) mp:put(v((n+1).."0"), n.."", n.."") end
%L -- putr = function (n) mp:put(v("0"..(n+1)), n.."", n.."") end
%L -- cutl = function (n) mp:addcuts(format("%d0w-%d0n", n+1, n+1)) end
%L -- cutr = function (n) mp:addcuts(format("0%dn-0%de", n+1, n+1)) end
%L -- putl(0); putl(1); putl(2); putl(3); putl(4)
%L -- putr(0); putr(1); putr(2); putr(3); putr(4); putr(5); putr(6)
%L -- cutl(0)
%L -- cutr(3); cutr(5)
%L -- mp:print():output()
%L
%L -- (find-LATEX "dednat6/zhas.lua" "VCuts-tests")
%L local vc = VCuts.new({scale="7pt", def="foo"}, 4, 6)
%L vc:cutl(0)
%L vc:cutr(3):cutr(5)
%L vc:output()
%L
%L mp = mpnew({def="ZQuot"}, "12345RR4321"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="ZQuotients"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp:print()
%
% / \
% 46
% / \ \
% 45 36
% \ \ \
% 35 26
% / \ /
% 34 25
% \ /
% 24
% / \ \
% 23 14
% / \ / \
% 22 13 04
% \ / \ /
% 12 03
% / / /
% 11 02
% \ / /
% 01
% / /
% 00
% 4321/0 \ / 0123\45\6
%
%$$\pu
% \foo
% \qquad
% \ZQuot
% \qquad
% \ZQuotients
%$$
\pagebreak[0] % (find-es "tex" "pagebreak")
% ____ _ _ _
% / ___|| | __ _ ___| |__ _ __ __ _ _ __| |_
% \___ \| |/ _` / __| '_ \ _____| '_ \ / _` | '__| __|
% ___) | | (_| \__ \ | | |_____| |_) | (_| | | | |_
% |____/|_|\__,_|___/_| |_| | .__/ \__,_|_| \__|
% |_|
% «slash-partitions» (to ".slash-partitions")
\section{From slash-partitions back to slashings}
\label {slash-partitions}
% Good (phap 29 "slash-partitions")
%
\def\nem#1#2{\psm{ &\!#2\\ #1& \\}}
\def\nwm#1#2{\psm{ #2& \\ &\!#1\\}}
\def\nem#1#2{\sm{ &&\!#2\\ &\!\nearrow&\\ #1& \\}}
\def\nwm#1#2{\sm{ #2&\\&\!\nwarrow&\\ &&\!#1\\}}
\def\neyes#1#2#3#4{\nem{#1#2}{#3#4}: #1#2 { \eqS} #3#4 \;⇒\; #2 { \eqR} #4 \;⇒\; #2 #4 }
\def\neno #1#2#3#4{\nem{#1#2}{#3#4}: #1#2 {\not\eqS} #3#4 \;⇒\; #2 {\not\eqR} #4 \;⇒\; #2\bsl#4 }
\def\nwyes#1#2#3#4{\nwm{#1#2}{#3#4}: #1#2 { \eqS} #3#4 \;⇒\; #1 { \eqL} #3 \;⇒\; #3 #1 }
\def\nwno #1#2#3#4{\nwm{#1#2}{#3#4}: #1#2 {\not\eqS} #3#4 \;⇒\; #1 {\not\eqL} #3 \;⇒\; #3/#1 }
% ____ _ _
% / ___|| | __ _ ___| |__ _ __ ___ __ ___ __
% \___ \| |/ _` / __| '_ \ _____| '_ ` _ \ / _` \ \/ /
% ___) | | (_| \__ \ | | |_____| | | | | | (_| |> <
% |____/|_|\__,_|___/_| |_| |_| |_| |_|\__,_/_/\_\
%
% «slash-max» (to ".slash-max")
\section{Slash-regions have maximal elements}
\label {slash-max}
% Good (phap 30 "slash-max")
% ____ _ _ _
% / ___| _| |_ ___ ___| |_ ___ _ __ _ __ (_)_ __ __ _
% | | | | | | __/ __| / __| __/ _ \| '_ \| '_ \| | '_ \ / _` |
% | |__| |_| | |_\__ \ \__ \ || (_) | |_) | |_) | | | | | (_| |
% \____\__,_|\__|___/ |___/\__\___/| .__/| .__/|_|_| |_|\__, |
% |_| |_| |___/
%
% «cuts-stopping-midway» (to ".cuts-stopping-midway")
\section{Cuts stopping midway}
\label {cuts-stopping-midway}
% Good (phap 31 "cuts-stopping-midway")
\def\undtrue #1{\und{#1}{\text{true}}}
\def\undfalse#1{\und{#1}{\text{false}}}
\def\undfrown#1{\und{#1}{=(}}
\def\iff{\;\;↔\;\;}
\def\notiff{\;\not↔\;}
% ____ _ _
% / ___|| | __ _ ___| |__ ___ _ __ ___
% \___ \| |/ _` / __| '_ \ _____ / _ \| '_ \/ __|
% ___) | | (_| \__ \ | | |_____| (_) | |_) \__ \
% |____/|_|\__,_|___/_| |_| \___/| .__/|___/
% |_|
% «slash-ops» (to ".slash-ops")
\section{Slash-operators}
\label {slash-ops}
% Good (phap 32 "slash-ops")
% ____ _ _ _
% / ___|| | __ _ ___| |__ _ __ _ __ ___ _ __ ___ _ __| |_ _ _
% \___ \| |/ _` / __| '_ \ | '_ \| '__/ _ \| '_ \ / _ \ '__| __| | | |
% ___) | | (_| \__ \ | | | | |_) | | | (_) | |_) | __/ | | |_| |_| |
% |____/|_|\__,_|___/_| |_| | .__/|_| \___/| .__/ \___|_| \__|\__, |
% |_| |_| |___/
%
% «slash-ops-property» (to ".slash-ops-property")
\section{Slash-operators: a property}
\label {slash-ops-property}
% Good (phap 33 "slash-ops-property")
% _
% | | ___ _ __ ___
% _ | |_____ / _ \| '_ \/ __|
% | |_| |_____| (_) | |_) \__ \
% \___/ \___/| .__/|___/
% |_|
%
% «J-ops-and-regions» (to ".J-ops-and-regions")
% J-regions and J-operators
\section{J-operators and J-regions}
\label {J-ops-and-regions}
% Good (phap 35 "J-ops-and-regions")
% _ _ __ __ _
% | \ | | ___ \ \ / / ___ _ _| |_ ___
% | \| |/ _ \ \ V / / __| | | | __/ __|
% | |\ | (_) | | | | (__| |_| | |_\__ \
% |_| \_|\___/ |_| \___|\__,_|\__|___/
%
% «no-Y-cuts-no-L-cuts» (to ".no-Y-cuts-no-L-cuts")
\section{The are no Y-cuts and no $\lambda$-cuts}
\label {no-Y-cuts-no-L-cuts}
% Good (phap 37 "no-Y-cuts-no-L-cuts")
% _ _
% | | __ _ _ __ __| | ___ ___ _ __ _ __ ___
% _ | | / _` | '_ \ / _` | / __/ _ \| '_ \| '_ \/ __|
% | |_| | | (_| | | | | (_| | | (_| (_) | | | | | | \__ \
% \___/ \__,_|_| |_|\__,_| \___\___/|_| |_|_| |_|___/
%
% «J-ops-and-connectives» (to ".J-ops-and-connectives")
\section{How J-operators interact with connectives}
\label {J-ops-and-connectives}
% (find-LATEX "2015planar-has.tex" "J-connectives")
% (find-planarhaspage 16 "How J-operators interact with the connectives")
% (find-planarhastext 16 "How J-operators interact with the connectives")
%D diagram cube-and*-obvious
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (P^*{∧}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{∧}Q)^* P^*{∧}Q^* (P{∧}Q^*)^*
%D ren A1 A4 A2 ==> P^*{∧}Q (P{∧}Q)^* P{∧}Q^*
%D ren A0 ==> P{∧}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 -> A6 A7 ->
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%D diagram cube-and*-full
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (P^*{∧}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{∧}Q)^* P^*{∧}Q^* (P{∧}Q^*)^*
%D ren A1 A4 A2 ==> P^*{∧}Q (P{∧}Q)^* P{∧}Q^*
%D ren A0 ==> P{∧}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 =
%D ))
%D enddiagram
%
%D diagram cube-or*-obvious
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (P^*{∨}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{∨}Q)^* P^*{∨}Q^* (P{∨}Q^*)^*
%D ren A1 A4 A2 ==> P^*{∨}Q (P{∨}Q)^* P{∨}Q^*
%D ren A0 ==> P{∨}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 -> A6 A7 ->
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%D diagram cube-or*-full
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (P^*{∨}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{∨}Q)^* P^*{∨}Q^* (P{∨}Q^*)^*
%D ren A1 A4 A2 ==> P^*{∨}Q (P{∨}Q)^* P{∨}Q^*
%D ren A0 ==> P{∨}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%D diagram cube-imp*-obvious
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (P^*{→}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{→}Q)^* P^*{→}Q^* (P{→}Q^*)^*
%D ren A1 A4 A2 ==> P^*{→}Q (P{→}Q)^* P{→}Q^*
%D ren A0 ==> P{→}Q
%D
%D (( A0 A1 <- A2 A3 <- A4 A5 <- A6 A7 <-
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
%D diagram cube-imp*-full
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> (P^*{→}Q^*)^*
%D ren A5 A3 A6 ==> (P^*{→}Q)^* P^*{→}Q^* (P{→}Q^*)^*
%D ren A1 A4 A2 ==> P^*{→}Q (P{→}Q)^* P{→}Q^*
%D ren A0 ==> P{→}Q
%D
%D (( A0 A1 <- A2 A3 = A4 A5 <- A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 -> A5 A7 ->
%D A0 A4 -> A1 A5 -> A2 A6 = A3 A7 =
%D ))
%D enddiagram
%
\pu
%$$
% \begin{array}{rcl}
% \diag{cube-and*-obvious} && \diag{cube-and*-full} \\ \\
% \diag{cube-or*-obvious} && \diag{cube-or*-full} \\ \\
% \diag{cube-imp*-obvious} && \diag{cube-imp*-full} \\
% \end{array}
%$$
% _ _ ____ ___
% | | ___ _ _| |__ ___ ___ __ _ ___ | _ \ / _ \ ___
% _ | |_____ / __| | | | '_ \ / _ \/ __| / _` / __| | |_) | | | / __|
% | |_| |_____| (__| |_| | |_) | __/\__ \ | (_| \__ \ | __/| |_| \__ \
% \___/ \___|\__,_|_.__/ \___||___/ \__,_|___/ |_| \___/|___/
%
% «J-cubes-as-partial-orders» (to ".J-cubes-as-partial-orders")
\section{J-cubes as partial orders}
\label {J-cubes-as-partial-orders}
% Good (phap 40 "J-cubes-as-partial-orders")
% __ __ _ _ _ __ ____ ___
% \ \ / /_ _| |_ _ __ _| |_(_) ___ _ __ ___ \ \ | _ \ / _ \ ___
% \ \ / / _` | | | | |/ _` | __| |/ _ \| '_ \/ __| _____\ \ | |_) | | | / __|
% \ V / (_| | | |_| | (_| | |_| | (_) | | | \__ \ |_____/ / | __/| |_| \__ \
% \_/ \__,_|_|\__,_|\__,_|\__|_|\___/|_| |_|___/ /_/ |_| \___/|___/
%
% «valuations-induce-POs» (to ".valuations-induce-POs")
\section{Valuations induce partial orders}
\label {valuations-induce-partial-orders}
% Good (phap 42 "valuations-induce-POs")
\def\V#1{v(#1)}
\def\VV#1{v((∨)_#1)}
%D diagram cube-or*-0v
%D 2Dx 100 +20 +20
%D 2D 100 A7
%D 2D +15 A5 A3 A6
%D 2D +15 A1 A4 A2
%D 2D +15 A0
%D 2D
%D ren A7 ==> (P^*∨Q^*)^*
%D ren A5 A3 A6 ==> (P∨Q^*)^* P^*∨Q^* (P^*∨Q)^*
%D ren A1 A4 A2 ==> P∨Q^* (P∨Q)^* P^*∨Q
%D ren A0 ==> P∨Q
%D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D ren A7 ==> 22
%D ren A5 A3 A6 ==> 22 22 22
%D ren A1 A4 A2 ==> 21 22 12
%D ren A0 ==> 11
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 =
%D ))
%D enddiagram
%
%D diagram cube-or*-0vn
%D 2Dx 100 +20 +20
%D 2D 100 A7
%D 2D +15 A5 A3 A6
%D 2D +15 A1 A4 A2
%D 2D +15 A0
%D 2D
%D ren A7 ==> (P^*∨Q^*)^*
%D ren A5 A3 A6 ==> (P∨Q^*)^* P^*∨Q^* (P^*∨Q)^*
%D ren A1 A4 A2 ==> P∨Q^* (P∨Q)^* P^*∨Q
%D ren A0 ==> P∨Q
%D
%D ren A7 ==> 22
%D ren A5 A3 A6 ==> 22 22 22
%D ren A1 A4 A2 ==> 21 22 12
%D ren A0 ==> 11
%D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 =
%D ))
%D enddiagram
%
%R local fooor =
%R 2/1 1 1 1 1 1 1 1 \
%R |1 1 1 1 1 1 1 1 |
%R |1 1 1 1 1 1 1 1 |
%R |1 1 1 1 1 1 1 1 |
%R |1 1 1 1 0 0 0 0 |
%R |1 0 1 0 0 0 0 0 |
%R |1 1 0 0 0 0 0 0 |
%R \1 0 0 0 0 0 0 0 /
%R
%R fooor:tomp({def="fooor", scale="7pt", meta="s"}):addcells():output()
%L mp = mpnew({def="orCube", scale="11pt"}, "12321"):addcuts("c 21/0 0|12")
%L mp:put(v"10", "P"):put(v"20", "P*", "P^*")
%L mp:put(v"01", "Q"):put(v"02", "Q*", "Q^*")
%L mp:output()
%
%D diagram cube-or*-a
%D 2Dx 100 +20 +20
%D 2D 100 A7
%D 2D +15 A5 A3 A6
%D 2D +15 A1 A4 A2
%D 2D +15 A0
%D 2D
%D ren A7 ==> 7
%D ren A5 A3 A6 ==> 5 3 6
%D ren A1 A4 A2 ==> 1 4 2
%D ren A0 ==> 0
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 =
%D ))
%D enddiagram
%
%D diagram cube-or*-b
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> (P^*{∨}Q^*)^*
%D ren A5 A3 A6 ==> (P{∨}Q^*)^* P^*{∨}Q^* (P^*{∨}Q)^*
%D ren A1 A4 A2 ==> P{∨}Q^* (P{∨}Q)^* P^*{∨}Q
%D ren A0 ==> P{∨}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 =
%D ))
%D enddiagram
%L mp = mpnew({def="orCubeTen", scale="11pt"}, "12321L"):addcuts("c 321/0 0|12")
%L mp:put(v"10", "P"):put(v"20", "P*", "P^*")
%L mp:put(v"01", "Q"):put(v"02", "Q*", "Q^*")
%L mp:output()
%
%D diagram cube-or*-c
%D 2Dx 100 +30 +30
%D 2D 100 A7
%D 2D +20 A5 A3 A6
%D 2D +20 A1 A4 A2
%D 2D +20 A0
%D 2D
%D ren A7 ==> (P^*{∨}Q^*)^*
%D ren A5 A3 A6 ==> (P{∨}Q^*)^* P^*{∨}Q^* (P^*{∨}Q)^*
%D ren A1 A4 A2 ==> P{∨}Q^* (P{∨}Q)^* P^*{∨}Q
%D ren A0 ==> P{∨}Q
%D
%D (( A0 A1 -> A2 A3 -> A4 A5 = A6 A7 =
%D A0 A2 -> A1 A3 -> A4 A6 = A5 A7 =
%D A0 A4 -> A1 A5 -> A2 A6 -> A3 A7 ->
%D ))
%D enddiagram
%
% ____ _ ____ ___
% / ___|___ _ __ ___ _ __ __ _ _ __(_)_ __ __ _ | _ \ / _ \ ___
% | | / _ \| '_ ` _ \| '_ \ / _` | '__| | '_ \ / _` | | |_) | | | / __|
% | |__| (_) | | | | | | |_) | (_| | | | | | | | (_| | | __/| |_| \__ \
% \____\___/|_| |_| |_| .__/ \__,_|_| |_|_| |_|\__, | |_| \___/|___/
% |_| |___/
%
% «comparing-partial-orders» (to ".comparing-partial-orders")
\section{Comparing partial orders}
\label {comparing-partial-orders}
% Rewrite (phap 44 "comparing-partial-orders")
\def\ptab#1{\left(\begin{tabular}{c}#1\end{tabular}\right)}
% _ _ _ _
% | | (_)_ __ __| | ___ _ __ | |__ __ _ _ _ _ __ ___
% | | | | '_ \ / _` |/ _ \ '_ \| '_ \ / _` | | | | '_ ` _ \
% | |___| | | | | (_| | __/ | | | |_) | (_| | |_| | | | | | |
% |_____|_|_| |_|\__,_|\___|_| |_|_.__/ \__,_|\__,_|_| |_| |_|
%
% «lindenbaum-fragments» (to ".lindenbaum-fragments")
\section{Fragments of Lindenbaum Algebras}
\label {lindenbaum-fragments}
% Bad (phap 47 "lindenbaum-fragments")
% ____ _ _
% | _ \ ___ | |_ _ | | ___ _ __ ___
% | |_) / _ \| | | | | _ | |_____ / _ \| '_ \/ __|
% | __/ (_) | | |_| | | |_| |_____| (_) | |_) \__ \
% |_| \___/|_|\__, | \___/ \___/| .__/|___/
% |___/ |_|
%
% «polynomial-J-ops» (to ".polynomial-J-ops")
\section{Polynomial J-operators}
\label {polynomial-J-ops}
% Bad (phap 47 "polynomial-J-ops")
% (phop 22)
% (pho "J-examples")
% (find-books "__cats/__cats.el" "fourman")
% (find-slnm0753page (+ 14 331) "polynomial")
\def\JiiR {{({→→}R)}}
\def\JoQ {{(∨Q)}}
\def\JiR {{({→}R)}}
\def\JfoQR{{(∨Q∧{→}R)}}
\def\JmiQ {({→→}Q∧{→}Q)}
% _ _ _
% | | ___ _ __ ___ __ _| | __ _ ___| |__ _ __ __ _
% _ | |_____ / _ \| '_ \/ __| / _` | |/ _` |/ _ \ '_ \| '__/ _` |
% | |_| |_____| (_) | |_) \__ \ | (_| | | (_| | __/ |_) | | | (_| |
% \___/ \___/| .__/|___/ \__,_|_|\__, |\___|_.__/|_| \__,_|
% |_| |___/
%
% «algebra-of-J-ops» (to ".algebra-of-J-ops")
\section{An algebra of J-operators}
\label {algebra-of-J-ops}
% Bad (phap 49 "algebra-of-J-ops")
% (pho "algebra-of-piccs")
% (phop 25 "algebra-of-piccs")
%
%L partitiongraph = function (opts, spec, ylabel)
%L local mp = MixedPicture.new(opts)
%L for y=0,5 do mp:put(v(-1, y), y.."") end
%L for x=0,5 do mp:put(v(x, -1), x.."") end
%L for a=0,5 do local aP = spec:sub(a+1, a+1)+0; mp:put(v(a, aP), "*") end
%L mp.lp:addlineorvector(v(0, 0), v(6, 0), "vector")
%L mp.lp:addlineorvector(v(0, 0), v(0, 6.5), "vector")
%L mp:put(v(7, 0), "a")
%L mp:put(v(0, 7), "aP", ylabel)
%L return mp
%L end
%L pg = function (def, spec, ylabel)
%L return partitiongraph({def=def, scale="5pt", meta="s"}, spec, ylabel)
%L end
%L
%L pg("grapha", "012345", "a^P" ):output()
%L pg("graphb", "113355", "a^{P'}" ):output()
%L pg("graphc", "115555", "a^{P''}" ):output()
%L pg("graphd", "555555", "a^{P'''}"):output()
%L
%
% a^P a^P a^P a^P
% ^ ^ ^ ^
% 5 | * 5 | * * 5 | * * * * 5 * * * * * *
% 4 | * 4 | 4 | 4 |
% 3 | * <= 3 | * * <= 3 | <= 3 |
% 2 | * 2 | 2 | 2 |
% 1 | * 1 * * 1 * * 1 |
% 0 *----------> a 0 +----------> a 0 +----------> a 0 +----------> a
% 0 1 2 3 4 5 0 1 2 3 4 5 0 1 2 3 4 5 0 1 2 3 4 5
%
% 0|1|2|3|4|5 <= 01|23|45 <= 01|2345 012345
%
% ___ _ _ _ ____
% / _ \ _ _ ___ ___| |_(_) ___ _ __ _ __ ___ _ __| | _____ |___ \
% | | | | | | |/ _ \/ __| __| |/ _ \| '_ \ | '_ ` _ \| '__| |/ / __| __) |
% | |_| | |_| | __/\__ \ |_| | (_) | | | | | | | | | | | | <\__ \ / __/
% \__\_\\__,_|\___||___/\__|_|\___/|_| |_| |_| |_| |_|_| |_|\_\___/ |_____|
%
% «question-marks-new» (to ".question-marks-new")
\section{Question marks (new)}
\label {question-marks-new}
\section{How J-operators act on 2CGs}
\label {how-J-ops-act-on-2CGs}
We saw in sec.\ref{piccs-and-slashings} (and
sec.\ref{J-ops-and-regions}) that a J-operator $J$ on a ZHA $H$ can be
represented a pair $(L,R)$ of piccs, that we drew in a V-shaped
diagram; let's write $S$ for the set of numbers above the cuts in the
V-shaped diagram, converting them to the notation for elements of the
left and the right columns of 2-column graphs:
%
%L -- (find-LATEX "dednat6/zhas.lua" "VCuts-tests")
%L local vc = VCuts.new({scale="7pt", def="vcuts"}, 4, 6)
%L vc:cutl(0)
%L vc:cutr(3):cutr(5)
%L vc:output()
%L
%L mp = mpnew({def="ZQuot"}, "12345RR4321"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="ZQuotients"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp:print()
%
$$\pu
J = \ZQuotients
\qquad
(L,R) = \vcuts
\qquad
S = \{1\_, \; \_4, \_6\}
$$
Let $\mathsf{S}$ be the operation that obtains the set $S$ for a
J-operator $J$: $\mathsf{S}(J) = \{1\_, \; \_4, \_6\}$ for the $J$
above.
\msk
The ZHA $H$ above is generated by the 2CG $(P,A)$ below; we will
sometimes need the 2CG $(P,A')$ that is obtained by $(P,A)$ by
deleting the intercolumn arrows,
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgbig("foo"):lrs():hs():vs():output()
%L tcg_spec = "4, 6; , "
%L tcgbig("bar"):lrs():hs():vs():output()
%
$$
\pu
(P,A) = \foo
\qquad
(P,A') = \bar
$$
%
and we will need the ``rectangular versions'' of $H$ and $J$, that we
will call $H'$ and $J'$:
%
%L mp = mpnew({def="Hprime"}, "12345RR4321"):addlrs() :output()
%L mp = mpnew({def="Jprime"}, "12345RR4321"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%
$$\pu
H' = \Hprime
\qquad
J' = \Jprime
$$
Note that $S⊆P$.
\msk
The J-operator $J$ acts on $H$, but we can transfer its action to
$\Opens_A(P)$ using the bijection $\pile:H→\Opens_A(P)$ described in
sec.\ref{2CGs}, and obtain a function $J':\Opens_A(P)→\Opens_A(P)$.
Note that $J'=\pile∘J∘\pile^{-1}$ and $J=\pile^{-1}∘J'∘\pile$.
\def\dro{\mathsf{dro}}
\def\rec{\mathsf{rec}}
The main theme of this section is that the action of $J'$ is
equivalent to {\sl dropping information} and then {\sl reconstructing
it back in the ``biggest'' way possible}. More formally, for a
$U∈\Opens_A(P)$ we have $J'(U) = \rec(\dro(U))$, where $\dro(U) = U∩S$
and $\rec(V) = (V∪(P\bsl S))^\Int$. In a diagram, with a parallel
diagram at the right showing the particular case that we will discuss:
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgC"):strs(split("1 0 0 0"), split("1 1 0 0 0 0")):hs():output()
%L tcgmed("tcgD"):strs(split("1 1 0 0"), split("1 1 1 0 0 0")):hs():output()
%L tcgmed("tcgE"):strs(split("1 · · ·"), split("· · · 0 · 0")):hs():output()
%L tcgmed("tcgF"):strs(split("1 1 1 1"), split("1 1 1 0 0 0")) :output()
%L
%D diagram dro-rec
%D 2Dx 100 +40 +40 +35 +40 +40
%D 2D 100 A ----> B a ----> b
%D 2D | | | |
%D 2D v v v v
%D 2D +35 C ----> D c ----> d
%D 2D \ ^ ^ \ ^ ^
%D 2D v / | v / |
%D 2D +50 E > F e > f
%D 2D
%D ren A B ==> H H
%D ren C D ==> \Opens_A(P) \Opens_A(P)
%D ren E F ==> \Opens_{A|_S}(S) \Opens_{A'}(P')
%D ren a b ==> 12 23
%D ren c d ==> \tcgC \tcgD
%D ren e f ==> \tcgE \tcgF
%D (( A B -> .plabel= a J
%D A C -> .plabel= l \pile B D -> .plabel= r \pile
%D C D -> .plabel= a J'
%D C E -> .plabel= l \dro
%D E D -> .plabel= r \rec
%D F D -> .plabel= r \Int
%D E F -> .plabel= b \rec'
%D
%D a b |->
%D a c |-> b d |->
%D c d |->
%D c e |-> e d |-> f d |->
%D e f |->
%D ))
%D enddiagram
%D
$$\pu
\diag{dro-rec}
$$
The extra step at the bottom left of the diagram will simplify a part
of the proof. The function $\rec'$ acts like $\rec$, but takes the
interior relative to the topology of $(P',A')$, and the vertical arrow
saying `$\Int$' takes the interior relative to $(P,A)$.
\bsk
There is a bijection between $H$ and $\Opens_A(P)$ --- we saw it in
sec.\ref{topologies-on-2CGs}, it was given by the function
$\pile:H→\Opens_A(P)$. We can transfer the action of $J:H→H$ to
$\Opens_A(P)$; let's call it $J':\Opens_A(P)→\Opens_A(P)$ --- we have
$J'=\pile∘J∘\pile^{-1}$.
Let $U$ be any element of $\Opens_A(P)$. Now look at $U∩S$; the
operation $U↦U∩S$ ``drops information'', roughly in this way:
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgbig("before"):lrs():hs():vs():output()
%L tcgbig("after"):strs(split("1\\_ · · ·"), split("· · · \\_4 · \\_6")):hs():vs():output()
$$\pu
\before
\qquad
\squigto
\after
$$
There are several ways to reconstruct from $U∩S$ the information that
was dropped. This one yields the biggest element of $\Opens_A(P)$
whose intersection with $S$ is $U∩S$: 1) add the complement of $S$, 2)
take the interior (in $\Opens_A(P)$) of the result. Formally, this is:
%
$$\begin{array}{rcl}
↑_S(U) &:=& ((U∩S)∪(P \bsl S))^\Int \\
&=& (U∪(P \bsl S))^\Int \\
\end{array}
$$
%L tcgmed("tcgU") :strs(split("1 0 0 0"), split("1 1 0 0 0 0")):hs():output()
%L tcgmed("tcgPS"):strs(split("0 1 1 1"), split("1 1 1 0 1 0")):hs():output()
%L tcgmed("tcgUB"):strs(split("1 1 1 1"), split("1 1 1 0 1 0")):hs():output()
%L tcgmed("tcgI") :strs(split("1 1 0 0"), split("1 1 1 0 0 0")):hs():output()
If $U=\pile(12)$, then:
%
$$\pu ↑_S \tcgU = \left(\tcgU ∪ \tcgPS\right)^\Int = \tcgUB^\Int = \tcgI$$
%
note that $↑_S(\pile(12)) = \pile(23)$, and $J(12)=23$.
\msk
{\sl Theorem:} for every $ab∈H$ we have $↑_S(\pile(ab)) =
\pile(J(ab))$, i.e., $↑_S=J'$.
\msk
It is easier to sketch a proof of the theorem above if we use another
notation, in which we write a `?' for each element of $P$ that is not
in $S$, and where we write `$\biggest(\ldots)$' for the biggest open
set of a given form. The result of the operation $↑_S(U) = (U∪(P \bsl
S))^\Int$ is clearly equivalent to the following series of operations:
1) let $U'$ be $U$ with a `?'s in each positions that is not in $S$,
2) looking at each column separately, replace each `?' that is above a
`0' with a `0' and each `?' that is below a `1' with a `1' and call
the result $U''$, 4) take the biggest open set of the form $U''$.
%L tcgmed("tcgU"):strs(split("1 0 0 0"), split("1 1 0 0 0 0")):hs():output()
%L tcgmed("tcgA"):strs(split("1 ? ? ?"), split("? ? ? 0 ? 0")):hs():output()
%L tcgmed("tcgB"):strs(split("1 ? ? ?"), split("? ? ? 0 0 0")):hs():output()
%L tcgmed("tcgC"):strs(split("1 1 1 1"), split("1 1 1 0 0 0")):hs():output()
%L tcgmed("tcgD"):strs(split("1 1 0 0"), split("1 1 1 0 0 0")):hs():output()
$$\pu \tcgU \tcgA \tcgB \tcgC \tcgD$$
% In section ??? we saw that a description for a 2-column graph (a
% ``D2CG'') is 4-uple $(l,r,R,L)$, and a 2-column graph (a ``2CG'') is a
% pair $(P,A)$. The operation $\TCG$
% %
% $$\begin{array}{rcl}
% \TCG(l,r,R,L) &:=& \left(\LC(l)∪\RC(r),
% \csm{\{\ltol{l}{(l-1)}, \;\ldots, \;\ltol21\}∪ \\
% \{\rtor{r}{(r-1)}, \;\ldots, \;\rtor21\}∪ \\
% R∪L
% }
% \right)
% \end{array}
% $$
% %
% converts a D2CG into a 2CG; and in section ??? we saw an operation
% $\pile(ab)$ that returns subsets of $\LC(l)∪\RC(r)$; $\pile(ab)$ was
% an open set of $(P,A)$ exactly when $ab$ was an element of the ZHA
% generated by the 2CG.
% ___ _ _ _
% / _ \ _ _ ___ ___| |_(_) ___ _ __ _ __ ___ __ _ _ __| | _____
% | | | | | | |/ _ \/ __| __| |/ _ \| '_ \ | '_ ` _ \ / _` | '__| |/ / __|
% | |_| | |_| | __/\__ \ |_| | (_) | | | | | | | | | | (_| | | | <\__ \
% \__\_\\__,_|\___||___/\__|_|\___/|_| |_| |_| |_| |_|\__,_|_| |_|\_\___/
%
% «question-marks» (to ".question-marks")
\section{Question marks}
\label {question-marks}
% Bad (phap 53 "question-marks")
% ZHA taken from:
% (find-LATEX "2017planar-has.tex" "slash-partitions")
% 2-piles taken from:
% (find-LATEX "2017planar-has.tex" "topologies-on-2CGs")
Let's now see a second way in which a J-operator on a ZHA $H$ induces
a slashing on $H$. Let's work on a specific example: $H$ is ZHA below,
and $J$ (a.k.a. `${}^*$') is J-operator that takes each element in $H$
to the top element of its equivalence class.
%L mp = mpnew({def="foo"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
$$\pu
H = \;\;\foo
\qquad
\begin{array}{rcl}
12^* &=& 23 \\\relax
[12]^J &=& \{11,12,23,22,33\} \\
12 &\eqJ& 22 \\
12 &\not\eqJ& 04 \\
\end{array}
$$
We have $12 \eqJ 13$; in 2CG notation, this is
%
%L tcg_spec = "4, 6; 11 22 34 45, 26"
%L tcgmed("foo"):lrs():hs():output()
%L tcgmed("bara"):cs("1000", "100000"):hs():output()
%L tcgmed("barb"):cs("1000", "110000"):hs():output()
%L tcgmed("barc"):cs("1000", "111000"):hs():output()
%L tcgmed("bard"):cs("1100", "110000"):hs():output()
%L tcgmed("bare"):cs("1100", "111000"):hs():output()
%L tcgmed("barq"):cs("1?00", "1??000"):hs():output()
%
\pu
$$
12 \;\;=\;\; \barb \;\;\eqJ\;\; \barc \;\;=\;\; 13,
$$
%
i.e., $\{1\_, \_1, \_2\} \eqJ \{1\_, \_1, \_2, \_3\}$. This {\sl
suggests} that modulo J-equivalence classes the presence or not of
the element $\_3$ does not matter.
Let's introduce several notations with `?'s in the places that ``don't
matter when we look modulo J-equivalence''. The first notation uses
`0's, `1's and `?'s. The equivalence class of 23 is $[23]^J = \{11,
12, 13, 22, 23\}$, which is:
%
$$% [12]^J \;\;=\;\;
\cmat{
\bara, \;
\barb, \;
\barc, \;
\bard, \;
\bare
}
$$
%
or all open sets between
%
$$\bara
\quad\text{and}\quad
\bare;
$$
%
the notation
%
$$\barq
$$
%
will mean
%
$$\text{all open sets of the form} \quad \barq,
$$
%
or sometimes ``all open sets of the form ... belong to the same
J-equivalence class''.
\msk
The J-equivalence classes of the ZHA $H$ above are:
%
%L tcgmed("barqa"):cs("0000", "???000"):hs():output()
%L tcgmed("barqb"):cs("0000", "111100"):hs():output()
%L tcgmed("barqc"):cs("1?00", "1??000"):hs():output()
%L tcgmed("barqd"):cs("1???", "1111?0"):hs():output()
%L tcgmed("barqe"):cs("11??", "111111"):hs():output()
%L tcgmed("barqs"):cq("L???", "???R?R"):hs():output()
%L tcgmed("barQb"):cs("1???", "???0?0"):hs():output()
%L tcgmed("barQb"):cs("1???", "???0?0"):hs():output()
\pu
$$
\begin{array}{rrr}
{} [11]^J=[23]^J=\barqc &
{} [14]^J=[45]^J=\barqd &
{} [26]^J=[46]^J=\barqd \\\\
{} [00]^J=[03]^J=\barqa &
{} [04]^J=\barqb \\
\end{array}
$$
If we transfer the `?'s above to the 2CG, we get this:
%
$$\barqs$$
%
where now each `?' means ``this point does not matter in {\sl at least
one} J-equivalence class''. Let's define formally what is the
diagram above. A {\sl 2-column graph with question marks} (a ``2CGQ'')
is a pair made of a 2CG $(P,A)$ and a subset $P'⊆P$, where $P'$ is the
set of points of $P$ that are not displayed as question marks; in the
example above, $P'=\{1\_, \_4, \_6\}$.
Each 2CGQ $Q=((P,A), P')$ induces two operations, $\biggest_Q$ and
$\smallest_Q$, from $\Opens_A(P)$ to $\Opens_A(P)$:
%
%$$\biggest_Q\barb \quad := \quad (\text{the biggest open set in $\barqb$})$$
%
$$\begin{array}{rcrcl}
\biggest _Q\barb &:=& \text{the biggest open set of the form $\barQb$} &=& \bare \\\\
\smallest_Q\barb &:=& \text{the smallest open set of the form $\barQb$} &=& \bara \\
\end{array}
$$
\msk
{\sl Theorem:} $\biggest_Q$ coincides with $J$, and $\smallest_Q$
coincides with the operation that takes each element of $H$ to the
smallest element in its J-equivalence class mentioned in
secs.\ref{slash-ops} and \ref{J-ops-and-regions}.
The proof is non-trivial: the equivalence class $[11]^J=[23]^J$
described in the beginning of the section had three `?'s, but now we
are working with diagrams with six `?'s... however, we can reduce the
number of `?'s by replacing `$?→0$'s with `$0→0$'s and `$1→?$'s with
`$1→1$'s, both in vertical arrows and in intercolumn arrows:
%
%L tcgmed("barQb"):cs("1???", "???0?0"):hs():output()
%L tcgmed("barQc"):cs("1???", "???000"):hs():output()
%L tcgmed("barQd"):cs("1?00", "???000"):hs():output()
%L tcgmed("barQe"):cs("1?00", "1??000"):hs():output()
%L tcgmed("barQf"):cs("1???", "???000"):hs():output()
\pu
$$\barQb = \barQc = \barQd = \barQe$$
$$\biggest _Q(12) = \biggest _Q \barQb = \biggest _Q \barQe = \bare = 23$$
$$\smallest_Q(12) = \smallest_Q \barQb = \smallest_Q \barQe = \bara = 11$$
We only saw a particular case, but this works in general.
\msk
A {\sl formal} proof can be done like this. We start with a diagram
with all the `?'s from the 2CGQ --- six `?'s in the examples that we
are using. Then replace the `$?→0$'s in it with `$0→0$'s, and the
`$1→?$'s with `$1→1$'s, {\sl only along the vertical arrows}; we get a
new diagram in which in each column we have '0's at the top, followed
by '?'s and then `1's. In the example:
%
$$\barQb = \barQf$$
The open sets in
%
$$\barQf$$
%
are exactly the open sets between
%
%L tcgmed("barSbelow"):cs("1000", "000000"):hs():output()
%L tcgmed("barSabove"):cs("1111", "111000"):hs():output()
$$\pu
\barSbelow = 10 \quad\text{and}\quad \barSbelow = 43
$$
%
where 10 and 43 are not (necessarily) open, but are the extremities of
a slash-equivalence class; compare with sec.\ref{piccs-and-slashings},
where we saw that the same slashing, $S=(4321/0,\, 0123\bsl45\bsl6)$,
could act on two different ZHAs,
%
%L mp = mpnew({def="foo"}, "12345RR4321"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="bar"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
$$\pu
[00,46] = \foo \qquad H = \bar
$$
%
and we have $[10,43]∩H = [12]^J = \{11, 12, 13, 22, 23\}$.
\newpage
\def\OPENS{\operatorname{\mathsf{Opens}}}
\def\OPENSPABC{\OPENS_{PABC}}
\def\dro{\mathsf{dro}}
\def\rec{\mathsf{rec}}
\def\ess{\mathsf{ess}}
\def\puq{\operatorname{\mathsf{puq}}}
\def\rqo{\operatorname{\mathsf{rq1}}}
% _ ____ ____ ____
% | | ___ _ __ ___ ___ _ __ |___ \ / ___/ ___|___
% _ | |_____ / _ \| '_ \/ __| / _ \| '_ \ __) | | | | _/ __|
% | |_| |_____| (_) | |_) \__ \ | (_) | | | | / __/| |__| |_| \__ \
% \___/ \___/| .__/|___/ \___/|_| |_| |_____|\____\____|___/
% |_|
%
% «how-J-ops-act-on-2CGs» (to ".how-J-ops-act-on-2CGs")
\section{How J-operators act on 2CGs}
\label {how-J-ops-act-on-2CGs}
% (phap 52 "how-J-ops-act-on-2CGs")
% (phap)
The main theme of this section is that the action of $J$ is equivalent
to {\sl dropping information} (about the points in $Q$) and then {\sl
reconstructing it back in the ``biggest'' way possible} (by setting
these points to 1 and then taking the interior of the result). For
example:
%
%L tcg_spec = "4, 6; , "
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgA"):strs(split("1 0 0 0"), split("1 1 0 0 0 0")):hs():output()
%L tcgmed("tcgB"):strs(split("1 ? ? ?"), split("? ? ? 0 ? 0")):hs():output()
%L tcgmed("tcgC"):strs(split("1 1 1 1"), split("1 1 1 0 1 0")):hs():output()
%L tcgmed("tcgD"):strs(split("1 1 0 0"), split("1 1 1 0 0 0")):hs():output()
%
$$\pu
12
\;\;\;\mton{\pile}\;\;\;
\tcgA
\;\;\mton{\puq}\;\;
\tcgB
\;\;\mton{\rqo}\;\;
\tcgC
\;\;\mton{\Int}\;\;
\tcgD
\;\;\;\mton{\pile^{-1}}\;\;\;
23
$$
%
We write `$\puq$' is the operation that puts question marks at the
points of $Q$, and `$\rqo$' for the operation that replaces each
question mark by a `1'; `$\Int$' is the interior relative to the
topology $\Opens_A(P)$.
If we start with $ab∈H$, the sequence of steps above acts as:
%
$$\begin{array}{rcl}
ab & \mton{\pile} & \pile(ab) \\
& \mton{\puq} & ((P,A), \pile(ab)∩S, \pile(ab)∪Q) \\
& \mton{\rqo} & \pile(ab)∪Q \\
& \mton{\Int} & (\pile(ab)∪Q)^\Int \\
& \mton{\pile^{-1}} & \pile^{-1}((\pile(ab)∪Q)^\Int) \\
\end{array}
$$
\hrule
We will need three other topologies, coming from the 2-column graphs
$(P,A')$, $(S, A|_S)$ and $(S, A'|_S)$, where the last two are new;
the operations of taking the interior relative to each of them will be
called $\Int'$, $\Int|_S$, $\Int'|_S$. The 2CGs $(S, A|_S)$ and $(S,
A'|_S)$ are obtained from $(P, A)$ and $(P, A')$ by restricting the
points to $S$:
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgbig("tcgSA") :strs(split("1\\_ · · ·"), split("· · · \\_4 · \\_6")):hs():vs():output()
%L tcg_spec = "4, 6; , 16"
%L tcgbig("tcgSAr") :strs(split("1\\_ · · ·"), split("· · · \\_4 · \\_6")):hs():vs():output()
%L tcg_spec = "4, 6; , "
%L tcgbig("tcgSAp"):strs(split("1\\_ · · ·"), split("· · · \\_4 · \\_6")):hs():vs():output()
%
$$
\pu
(S,A|_S) = \tcgSA = \tcgSAr
\qquad
(S,A'|_S) = \tcgSAp
$$
Referring to their arrows as $A|_S$ and $A'|_S$ is an abuse of
language; the correct way to do that is to {\sl define} $A|_S$ as
$(A^*∩(S×S))^\ess$, and similarly for $A'|_S$: we take the
transitive-reflexive closure of $A$, $A^*$, to make it into a partial
order, then we restrict that to $S$, then we take only the essential
arrows. A really honest drawing for $(S,A|_S)$ would have only one
vertical arrow, $\_6→\_4$, ond only one intercolumn arrow, $1\_←\_6$
--- but we will draw the arrows in the restriction as in the original
2CG, even though some arrows may look as coming from or going to
nonexistent points.
\bsk
\bsk
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Deleted stuff}
\def\OPENSXBC{\OPENS'_{XBC}}
\def\OPENSPABC{\OPENS_{PABC}}
Theorem: take a 2CG $(P,A)$, and draw an open set $V∈\Opens_A(P)$ as
the 2CG with the points replaced by `0's and `1's. Replace some of
these `0's and `1's with `?'s; this yields a 2CGQ $((P,A),B,C)$. Then
$V⊆\bigcup\OPENSPABC=C^\Int⊆C$.
Here is an example of how we will use that theorem:
%
%L tcg_spec = "6, 6; 45, "
%L tcgmed("tcgA"):strs(split("1 1 0 0 0 0"), split("1 1 1 0 0 0")):hs():output()
%L tcgmed("tcgB"):strs(split("? 1 ? ? 0 ?"), split("? 1 ? ? 0 ?")):hs():output()
%L tcgmed("tcgb"):strs(split("1 1 ? ? 0 0"), split("1 1 ? ? 0 0")):hs():output()
%L tcgmed("tcgC"):strs(split("1 1 1 1 0 1"), split("1 1 1 1 0 1")):hs():output()
%L tcgmed("tcgD"):strs(split("1 1 1 0 0 0"), split("1 1 1 1 0 0")):hs():output()
%
%L tcgmed("tcgn"):strs(split("1 1 ? ? 0 0"), split("1 1 ? ? 0 0")):hs():output()
%R mpnew({def="Zfoo", scale="7pt", meta="s"}, "12345654321"):addlrs():output()
%R mpnew({def="Zbar", scale="5pt", meta="t"}, "1234RRRLLL321"):addlrs():output() -- 43
%R mpnew({def="Zbar", scale="5pt", meta="t"}, "1234RRR32LLL1"):addlrs():output() -- 45
\pu
$$\OPENS\tcgB = \OPENS\tcgb = \; [22,44] ∩ \; \Zbar$$
$$
23 =
\tcgA \text{ is open}
\quad⇒\quad
\sup\OPENS\tcgB = \tcgC^{\!\Int} \! = \tcgD = 34
$$
A set of the form $\OPENSPABC$ is always an interval in a ZHA.
If we start with an open set $V=\pile(ab)$ in a ZHA $H$, change some
of the `0's and `1's in $V$ to `?' and look for the biggest open set
of that form,
%
%L tcg_spec = "6, 6; , "
%L tcgmed("tcgA"):strs(split("? 1 ? ? 0 ?"), split("? 1 ? ? 0 ?")):hs():output()
%L tcgmed("tcgB"):strs(split("1 1 ? ? 0 0"), split("1 1 ? ? 0 0")):hs():output()
%L tcg_spec = "6, 6; 44, "
%L tcgmed("tcgC"):strs(split("? 1 ? ? 0 ?"), split("? 1 ? ? 0 ?")):hs():output()
%L tcgmed("tcgD"):strs(split("1 1 ? ? 0 0"), split("1 1 ? ? 0 0")):hs():output()
%L tcgmed("tcgE"):lrs() :hs():output()
%
{\bf Garbage:}
More formally, for a $U∈\Opens_A(P)$ we have $J'(U) = \rec(\dro(U))$,
where $\dro(U) = U∩S$ and $\rec(V) = (V∪(P∖S))^\Int$. In a
diagram, with a parallel diagram at the right showing the particular
case that we will discuss:
Note that $S⊆P$ and that $S$ has this property: take any $Q∈H'$ and
replace the points not in $S$ in $\pile(Q)$ by `?'s; the set of open
sets of that form is exactly --- modulo $\pile$ --- the region in $J'$
containing $Q$. For example:
%
%L tcg_spec = "4, 6; , "
%L tcgmed("tcgA"):strs(split("1 1 0 0"), split("1 1 1 1 0 0")):hs():output()
%L tcgmed("tcgB"):strs(split("1 ? ? ?"), split("? ? ? 1 ? 0")):hs():output()
%L tcgmed("tcgC"):strs(split("1 ? ? ?"), split("1 1 1 1 ? 0")):hs():output()
$$\pu
24
\quad\squigto\quad
\tcgA
\quad\squigto\quad
\OPENS\tcgB =
\OPENS\tcgC = [14, 45]
% \quad\squigto\quad
$$
\bsk
\msk
The J-operator $J$ acts on $H$, but we can transfer its action to
$\Opens_A(P)$ using the bijection $\pile:H→\Opens_A(P)$ described in
sec.\ref{2CGs}, and obtain a function $J':\Opens_A(P)→\Opens_A(P)$.
Note that $J'=\pile∘J∘\pile^{-1}$ and $J=\pile^{-1}∘J'∘\pile$.
\msk
The main theme of this section is that the action of $J'$ is
equivalent to {\sl dropping information} and then {\sl reconstructing
it back in the ``biggest'' way possible}. More formally, for a
$U∈\Opens_A(P)$ we have $J'(U) = \rec(\dro(U))$, where $\dro(U) = U∩S$
and $\rec(V) = (V∪(P∖S))^\Int$. In a diagram, with a parallel diagram
at the right showing the particular case that we will discuss:
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgC"):strs(split("1 0 0 0"), split("1 1 0 0 0 0")):hs():output()
%L tcgmed("tcgD"):strs(split("1 1 0 0"), split("1 1 1 0 0 0")):hs():output()
%L tcgmed("tcgE"):strs(split("1 · · ·"), split("· · · 0 · 0")):hs():output()
%L tcgmed("tcgF"):strs(split("1 1 1 1"), split("1 1 1 0 0 0")) :output()
%L
%D diagram dro-rec
%D 2Dx 100 +40 +40 +35 +40 +40
%D 2D 100 A ----> B a ----> b
%D 2D | | | |
%D 2D v v v v
%D 2D +35 C ----> D c ----> d
%D 2D \ ^ ^ \ ^ ^
%D 2D v / | v / |
%D 2D +50 E > F e > f
%D 2D
%D ren A B ==> H H
%D ren C D ==> \Opens_A(P) \Opens_A(P)
%D ren E F ==> \Opens_{A|_S}(S) \Opens_{A'}(P')
%D ren a b ==> 12 23
%D ren c d ==> \tcgC \tcgD
%D ren e f ==> \tcgE \tcgF
%D (( A B -> .plabel= a J
%D A C -> .plabel= l \pile B D -> .plabel= r \pile
%D C D -> .plabel= a J'
%D C E -> .plabel= l \dro
%D E D -> .plabel= r \rec
%D F D -> .plabel= r \Int
%D E F -> .plabel= b \rec'
%D
%D a b |->
%D a c |-> b d |->
%D c d |->
%D c e |-> e d |-> f d |->
%D e f |->
%D ))
%D enddiagram
%D
$$\pu
\diag{dro-rec}
$$
The extra step at the bottom right of the diagram is a trick that will
simplify a part of the proof later. The function $\rec'$ acts like
$\rec$, but takes the interior relative to the topology of $(P',A')$,
and the vertical arrow saying `$\Int$' takes the interior relative to
$(P,A)$. The 2-column graph in the bottom middle has fewer points in
each column than the original $(P,A)$, and the right way to calculate
the intercolumn arrows in it would to turn $(P,A)$ into a partial
order $(P,A^*)$, and then restrict that to a partial order
$(S,A^*∩(S×S))$ and drop the superfluous arrows as we did in
sec.\ref{converting-ZHAs-2CAGs}; the result would be this:
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgE"):strs(split("1 · · ·"), split("· · · 0 · 0")):hs():output()
%L tcg_spec = "4, 6; , 14"
%L tcgmed("tcgF"):strs(split("1 · · ·"), split("· · · 0 · 0")):hs():output()
%
$$\pu
(S, (A^*∩(S×S))^\ess) = \tcgF
$$
The ``restriction of $A$ to $S$'', $A|_S$, is formally the set of
``essential arrows'' in $(A^*∩(S×S))$, $(A^*∩(S×S))^\ess$, but we
prefer to draw its intercolumn arrows as a copy of the intercolumn
arrows in $(P,A)$, even though some of the arrows may look as coming
from or going to nonexistent points.
\bsk
{\sl Theorem.} For any $Q∈H$ the diagram above becomes
%
%D diagram dro-rec-2
%D 2Dx 100 +45 +45 +35 +40 +40
%D 2D 100 A ----> B a ----> b
%D 2D | | | |
%D 2D v v v v
%D 2D +30 C ----> D c ----> d
%D 2D \ ^ ^ \ ^ ^
%D 2D v / | v / |
%D 2D +30 E > F e > f
%D 2D
%D ren A B ==> Q J(Q)
%D ren C D ==> \pile(Q) \pile(J(Q))
%D ren E F ==> \pile(Q)∩S \pile(J'(Q))
%D (( A B |->
%D A C |-> B D |->
%D C D |->
%D C E |-> E D |-> F D |->
%D E F |->
%D ))
%D enddiagram
%D
$$\pu
\diag{dro-rec-2}
$$
%
and:
a) for $R'∈H'$ we have $\pile(R')∩S = \pile(Q)∩S$ iff $R'∈[Q]_{J'}$.
b) for $R∈H$ we have $\pile(R)∩S = \pile(Q)∩S$ iff $R∈[Q]_J$,
\bsk
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgH") :strs(split("1 ? ? ?"), split("? ? ? 0 ? 0")):hs():output()
%L tcg_spec = "4, 6; , "
%L tcgmed("tcgHp"):strs(split("1 ? ? ?"), split("? ? ? 0 ? 0")):hs():output()
\pu
$$\pile(R') \quad\text{is an open set of the form}\quad \tcgHp \iff R'∈[12]_{J'}$$
$$\pile(R) \quad\text{is an open set of the form}\quad \tcgH \iff R∈[12]_J$$
\bsk
\bsk
\bsk
Let's write
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgO"):strs(split("1 ? ? ?"), split("? ? ? 0 ? 0")):hs():output()
%L tcgmed("tcgB"):strs(split("1 ? ? ?"), split("? ? ? 0 ? 0")):hs():output()
$$\pu
\OPENS \tcgO \qquad \text{and} \qquad \biggest \tcgB
$$
%
for the set of all opens sets of the given form and for the biggest
open set of the given form.
\bsk
{\sl (Incomplete)}
% ____ ___ _ _____ _ ___ ____
% |___ \ / _ \/ |___ (_)_ _ _ __ / _ \| ___|
% __) | | | | | / /| | | | | '_ \| | | |___ \
% / __/| |_| | | / / | | |_| | | | | |_| |___) |
% |_____|\___/|_|/_/ _/ |\__,_|_| |_|\___/|____/
% |__/
%
% «2017jun05» (to ".2017jun05")
\section{2017jun05}
\label{2017jun05}
The next theorem applies these ideas to the case where the $I$ of the
previous theorem is a J-equivalence (or slash-equivalence) class.
{\sl Theorem 4.} Suppose the conditions of Theorem 3 plus a J-operator
$J:H→H$. Then:
a) if $ab$ and $ef$ are the minimal and maximal elements of a
J-equivalence class then $I = H∩[ab,ef] = [ab]^J = [ef]^J$,
b) if $\pile(cd)∈\OPENS(G)$ (i.e., $cd∈H$) and $ab = \co J(cd)$ and
$ef = J(cd)$ then $ab$ and $ef$ are the minimal and maximal elements
of $I = H∩[ab,ef] = [ab]^J = [ef]^J = [cd]^J$.
\bsk
Let's allow the notation $\OPENS(\calU, B, D)$ for all
open sets in $\calU$ between $B$ and $D$; we always have $\Int(S) =
\sup(\OPENS(\calU, ∅, S)) = ⋃ \OPENS(\calU, ∅, S)$, and in finite
topologies such as the ones we've been working on we also have
$\coInt(S) = \inf(\OPENS(\calU, S, P)) = ⋂ \OPENS(\calU, S, P)$.
The expression ``$B$ and $D$ are the extremities of $\calU$'' will
mean: $B = \inf(\calU) = ⋂\calU$, $D = \sup(\calU) = ⋃\calU$, and
$B,D∈\calU$.
The operations of propagating only the `1's or only the `0's as
described above are called `$\propagate_1$', `$\propagate_0$' and
respectively; note that $\OPENS(G) = \OPENS(\propagate_1(G)) =
\OPENS(\propagate_0(G))$, and that `$\propagate_1$' enlarges $P_1$ and
shrinks $P_?$, and `$\propagate_0$' enlarges $P_0$ and shrinks $P_?$.
In other words, `$\propagate_1$' enlarges $B$ and keeps $D$ unchanged,
and `$\propagate_0$' shrinks $D$ and keeps $B$ unchanged,
\msk
In other words: suppose that $G=((P,A),B,D)$ and $\OPENS(G)≠∅$. Then
the extremities of $\OPENS(\propagate(G))$ are $\coInt(B)$ and
$\Int(D)$ --- which are open sets, so they are piles, and so there
exist $ab$ and $ef$ such that $B'=\pile(ab)$ and $C'=\pile(ef)$. Each
element of $\OPENS(G)$ is a pile between $ab$ and $ef$, and, moreover,
a pile that is open in $(P,A)$... this lets us rephrase Theorem 1 into
the language of ZHAs:
\msk
{\sl Theorem 2.} Suppose that $\OPENS(G)≠∅$. Let $B' = \coInt(B)$, $D'
= \Int(D)$, $ab = \pile^{-1}(B')$, $ef = \pile^{-1}(D')$. Then $B'$
and $D'$ are the extremities of $\OPENS(G)$, and $\OPENS(G)$
corresponds to $[ab,ef]∩H$, where $H = \TCG(P,A)$.
\msk
An example:
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgG" ):strs("1 ? ? ?", "? ? ? 0 ? 0"):hs():output()
%L tcgmed("tcgGG" ):strs("1 ? ? ?", "? ? ? 0 0 0"):hs():output()
%L tcgmed("tcgGGG"):strs("1 ? 0 0", "1 ? ? 0 0 0"):hs():output()
%
%L tcg_spec = "4, 6; , "
%L tcgmed("tcgGG" ):strs("1 ? ? ?", "? ? ? 0 0 0"):hs():output()
%
%L mp = mpnew({def="foo", meta="s", scale="7pt"}, "1R2R3212RL1"):addlrs():output()
%
$$\pu
\begin{array}{c}
G = \tcgG
\qquad
G' = \propagate(G) = \tcgGGG = ((P,A), \pile(11), \pile(23))
\\
\OPENS(G) = \OPENS(G')
\quad
\two/<-`->/<300>^{\pile}_{\pile^{-1}}
\quad
[11,23]∩\;\;\foo \\
\end{array}
$$
% ____ ___ _ _____ _ ___ __
% |___ \ / _ \/ |___ (_)_ _ _ __ / _ \ / /_
% __) | | | | | / /| | | | | '_ \| | | | '_ \
% / __/| |_| | | / / | | |_| | | | | |_| | (_) |
% |_____|\___/|_|/_/ _/ |\__,_|_| |_|\___/ \___/
% |__/
%
% «2017jun06» (to ".2017jun06")
\section{2017jun06}
\label{2017jun06}
\bsk
\bsk
\bsk
Choose an element $cd∈H$. Let $Q=\qmarks(J)$, $C=\pile(cd)$,
$G=((P,A'), C∖Q, C∪Q)$, $G = \propagate(G) = ((P,A'),B',C') =
((P,A'),\pile(ab), \pile(ef))$. For example, if $cd=12$ we have:
%
%L tcg_spec = "4, 6; , "
%L tcgmed("tcgGF" ):strs("1 ? ? ?", "? ? ? 0 ? 0"):hs():output()
%L tcgmed("tcgGR" ):strs("1 ? ? ?", "? ? ? 0 0 0"):hs():output()
%
$$\pu
\begin{array}{c}
\forget_{(P,A'),Q}(\pile(12)) = \tcgGF \\
\propagate(\forget_{(P,A'),Q}(\pile(12))) = \tcgGR = ((P,A), \pile(10), \pile(43)) \\
\end{array}
$$
Each column of a $\forget_{(P,A'),Q}(\pile(cd))$ is made of blocks of
consecutive `?'s separated from the other ones by `0's and `1's, and
$\propagate$ acts homogeneously on each block --- a block below a `1'
is replaced by `1's, a block above a `0' is replaced by `0's, and
there's at most one block of consecutive `?'s in each column that
keeps its `?'s. Applying `$\OPENS$' on that yields exactly the
$J'$-equivalence class of $cd$.
\def\PA{{(P,A)}}
\def\PA{{}}
\def\PAP{{(P,A')}}
The bottom and the top points of the $J'$-equivalence class of $cd$
can be calculated as $\co J'(cd)$ and $J'(cd)$, and also as
$\coInt_\PAP(\pile(cd)∖Q)$ and $\Int_\PAP(\pile(cd)∪Q)$.
\msk
{\sl Theorem.} For any $cd∈H'$ we have:
a) $\pile(J'(cd)) = \Int_\PAP(\pile(cd)∪Q)$,
b) $\pile(\co J'(cd)) = \coInt_\PAP(\pile(cd)∖Q)$.
% ____ ___ _ _____ _ _ _
% |___ \ / _ \/ |___ (_)_ _ _ __ / / |
% __) | | | | | / /| | | | | '_ \| | |
% / __/| |_| | | / / | | |_| | | | | | |
% |_____|\___/|_|/_/ _/ |\__,_|_| |_|_|_|
% |__/
%
% «2017jun11» (to ".2017jun11")
\section{2017jun11}
\bsk
Fix a ZHA $H$ and a J-operator $J$ on it, and from that produce
$(P,A)$, $\calU=\Opens_A(P)$, $S$, $Q$, etc. Let's define the
functions:
%
$$\begin{array}{lll}
f: S→P && \text{(inclusion)} \\
f^!: \Opens(S)→\Opens(P) && f^!(W) = \coInt(W∖Q) \\
f^*: \Opens(P)→\Opens(S) && f^*(V) = V∩Q \\
f_*: \Opens(S)→\Opens(P) && f_*(U) = \Int(U∪Q) \\
\end{array}
$$
%
where the $\coInt$ and $\Int$ are in the topology $\Opens(P)$. The
functions $f^!$, $f^*$, $f_*$ are clearly (the actions on objects of)
functors, and we will see that we have adjunctions $f^! ⊣ f^* ⊣ f_*$.
Using a notation similar to figures 6 and 7 in \cite{OchsIDARCT}, we
can draw the ``external view'' and the ``external view'' of $f^! ⊣ f^*
⊣ f_*$ as:
%
%D diagram foo
%D 2Dx 100 +40 +30 +35
%D 2D 100 U --> U_*
%D 2D ^ ^
%D 2D | <--> |
%D 2D | |
%D 2D +25 O(S) :::: O(P) V^* <-- V
%D 2D ^ ^
%D 2D | <--> |
%D 2D | |
%D 2D +25 W --> W^!
%D 2D
%D 2D +20 S0 -----> P0 S ---> P
%D 2D
%D ren O(S) O(P) ==> \Opens(S) \Opens(P)
%D ren S0 P0 ==> S P
%D
%D ren W^! ==> f^!(W)
%D ren V^* ==> f^*(V)
%D ren U_* ==> f_*(U)
%D ren S P ==> s f(s){=}s
%D
%D (( O(S) O(P) -> sl__ .plabel= b f^!
%D O(S) O(P) <- .plabel= m f^*
%D O(S) O(P) -> sl^^ .plabel= a f_*
%D S0 P0 -> .plabel= a f
%D ))
%D
%D (( W W^! |->
%D V^* V <-|
%D U U_* |->
%D W V^* -> W^! V ->
%D W V harrownodes nil 20 nil <->
%D V^* U -> V U_* ->
%D V U harrownodes nil 20 nil <->
%D S P |->
%D ))
%D enddiagram
%D
$$\pu
\diag{foo}
$$
The vertical arrows at the right are inclusions, and the
`$\diagxyto/<->/<150>$'s mean that the inclusion at the left is true
if and only if the inclusion at the right is true, i.e., for any
choices of $W,U∈\Opens(S)$ and $V∈\Opens(P)$ we have:
a) $f^*(V)⊆U$ iff $V⊆f_*(U)$
b) $W⊆f^*(V)$ iff $f^!(W)⊆V$
\msk
We will prove (a) and (b) soon, but let's first clarify what the
diagram above ``means''. Expanding $f^!$, $f^*$ and $f_*$ and making
some intermediate steps explicit, the diagram becomes this:
%
%D diagram foo
%D 2Dx 100 +30 +40
%D 2D 100 U0 --> U1 --> U2
%D 2D ^ ^
%D 2D | <--> |
%D 2D | |
%D 2D +25 V2 <--------- V0
%D 2D ^ ^
%D 2D | <--> |
%D 2D | |
%D 2D +25 W0 --> W1 --> W2
%D 2D
%D 2D +20 OS PP OP
%D
%D ren U0 U1 U2 ==> U U∪Q \Int(U∪Q)
%D ren V0 V2 ==> V V∩S
%D ren W0 W1 W2 ==> W W \coInt(W)
%D ren OS PP OP ==> \Opens(S) \Pts(P) \Opens(P)
%D
%D (( U0 U1 |-> U1 U2 |->
%D V2 V0 <-|
%D W0 W1 |-> W1 W2 |->
%D
%D U0 V2 <- U2 V0 <-
%D V2 W0 <- V0 W2 <-
%D U0 V0 harrownodes nil 25 nil <->
%D V0 W0 harrownodes nil 25 nil <->
%D
%D OS PP -> PP OP -> OS OP <- sl__
%D ))
%D enddiagram
%D
$$\pu
\diag{foo}
$$
Every $V∈\Opens(P)$ is of the form $\pile(cd)$ for some $cd∈H$, and
all opens sets $U,W∈\Opens(S)$ are restrictions by `$∩S$' of sets
$\pile(ab)$ and $\pile(ef)$ where $ab,ef∈H$, so we can rewrite the
diagram as:
%
%D diagram foo
%D 2Dx 100 +60 +75
%D 2D 100 U0 --> U1 --> U2
%D 2D ^ ^
%D 2D | <--> |
%D 2D | |
%D 2D +25 V2 <--------- V0
%D 2D ^ ^
%D 2D | <--> |
%D 2D | |
%D 2D +25 W0 --> W1 --> W2
%D 2D
%D 2D +20 OS PP OP
%D
%D ren U0 U1 U2 ==> \pile(ef)∩S (\pile(ef)∩S)∪Q \Int((\pile(ef)∩S)∪Q)
%D ren V0 V2 ==> \pile(cd) \pile(cd)∩S
%D ren W0 W1 W2 ==> \pile(ab)∩S \pile(ab)∩S \coInt(\pile(ab)∩S)
%D ren OS PP OP ==> \Opens(S) \Pts(P) \Opens(P)
%D
%D (( U0 U1 |-> U1 U2 |->
%D V2 V0 <-|
%D W0 W1 |-> W1 W2 |->
%D
%D U0 V2 <- U2 V0 <-
%D V2 W0 <- V0 W2 <-
%D U0 V0 harrownodes nil 30 nil <->
%D V0 W0 harrownodes nil 30 nil <->
%D
%D OS PP -> PP OP -> OS OP <- sl__
%D ))
%D enddiagram
%D
$$\pu
\diag{foo}
$$
We know that:
c) $(\pile(ef)∩S)∪Q = \pile(ef)∪Q$,
d) $\Int(\pile(ef)∪Q) = \pile(J(ef))$,
e) $\coInt(\pile(ab)∩S) = \pile(\co J(ab))$,
so the diagram can be rewritten as:
%
%D diagram foo
%D 2Dx 100 +50 +55
%D 2D 100 U0 --> U1 --> U2
%D 2D ^ ^
%D 2D | <--> |
%D 2D | |
%D 2D +25 V2 <--------- V0
%D 2D ^ ^
%D 2D | <--> |
%D 2D | |
%D 2D +25 W0 --> W1 --> W2
%D 2D
%D 2D +20 OS PP OP
%D
%D ren U0 U1 U2 ==> \pile(ef)∩S \pile(ef)∪Q \pile(J(ef))
%D ren V0 V2 ==> \pile(cd) \pile(cd)∩S
%D ren W0 W1 W2 ==> \pile(ab)∩S \pile(ab)∩S \pile(\co{J}(ab))
%D ren OS PP OP ==> \Opens(S) \Pts(P) \Opens(P)
%D
%D (( U0 U1 |-> U1 U2 |->
%D V2 V0 <-|
%D W0 W1 |-> W1 W2 |->
%D
%D U0 V2 <- U2 V0 <-
%D V2 W0 <- V0 W2 <-
%D U0 V0 harrownodes nil 25 nil <->
%D V0 W0 harrownodes nil 25 nil <->
%D
%D OS PP -> PP OP -> OS OP <- sl__
%D ))
%D enddiagram
%D
$$\pu
\diag{foo}
$$
We can rewrite (a) and (b) as:
\ssk
a') $\pile(cd)∩S ⊆ \pile(ef)∩S$ iff $\pile(cd) ⊆ \pile(J(ef))$
b') $\pile(ab)∩S ⊆ \pile(cd)∩S$ iff $\pile(\co J(ab)) ⊆ \pile(cd)$
\ssk
and we know that:
\ssk
g) $\pile(cd)∩S ⊆ \pile(ef)∩S$ iff $J(cd) ≤ J(ef)$
h) $\pile(ab)∩S ⊆ \pile(cd)∩S$ iff $\co J(ab)) ≤ \co J(cd)$
\ssk
so we can rewrite (a') and (b') into:
\ssk
a'') $ J(cd) ≤ J(ef)$ iff $cd ≤ J(ef)$
b'') $\co J(ab)) ≤ \co J(cd)$ iff $\co J(ab) ≤ cd$,
\ssk
and (a'') and (b'') are very easy to prove.
\msk
Note that our last diagram is also very easy to {\sl visualize}. If we
take $ab=cd=ef=12$ and use the $H$, $J$ and $(P,A)$ that we are using
in most examples in the last sections, it becomes:
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgL" ):strs("1 · · ·", "· · · 0 · 0"):hs():output()
%L tcgmed("tcgUB"):strs("1 1 1 1", "1 1 1 0 1 0"):hs():output() -- U1
%L tcgmed("tcgWB"):strs("1 0 0 0", "0 0 0 0 0 0"):hs():output() -- W1
%L tcgmed("tcgUC"):strs("1 1 0 0", "1 1 1 0 0 0"):hs():output() -- U2 = 23
%L tcgmed("tcgVA"):strs("1 0 0 0", "1 1 0 0 0 0"):hs():output() -- V0 = 12
%L tcgmed("tcgWC"):strs("1 0 0 0", "1 0 0 0 0 0"):hs():output() -- W2 = 11
%
%D diagram foo
%D 2Dx 100 +45 +45
%D 2D 100 U0 --> U1 --> U2
%D 2D ^ ^
%D 2D | <--> |
%D 2D | |
%D 2D +50 V2 <--------- V0
%D 2D ^ ^
%D 2D | <--> |
%D 2D | |
%D 2D +50 W0 --> W1 --> W2
%D 2D
%D 2D +35 OS PP OP
%D
%D ren U0 U1 U2 ==> \tcgL \tcgUB \tcgUC
%D ren V2 V0 ==> \tcgL \tcgVA
%D ren W0 W1 W2 ==> \tcgL \tcgWB \tcgWC
%D ren OS PP OP ==> \Opens(S) \Pts(P) \Opens(P)
%D
%D (( U0 U1 |-> U1 U2 |->
%D V2 V0 <-|
%D W0 W1 |-> W1 W2 |->
%D
%D U0 V2 <- U2 V0 <-
%D V2 W0 <- V0 W2 <-
%D U0 V0 harrownodes nil 30 nil <->
%D V0 W0 harrownodes nil 30 nil <->
%D
%D OS PP -> PP OP -> OS OP <- sl__
%D ))
%D enddiagram
%D
$$\pu
\diag{foo}
$$
\bsk
\bsk
{\sl Lemma.} The operations corresponding to the horizontal arrows
above --- $U ↦ U∪Q ↦ \Int(U∪Q)$, \; $V ↦ V∩S$, \; $W ↦ W ↦ \coInt(W)$
--- never change the Q-equivalence class.
% ____ _ _ _
% | _ \ ___ ___| |_ __ _ _ __ __ _ _ _| | __ _ _ __ / |
% | |_) / _ \/ __| __/ _` | '_ \ / _` | | | | |/ _` | '__| | |
% | _ < __/ (__| || (_| | | | | (_| | |_| | | (_| | | | |
% |_| \_\___|\___|\__\__,_|_| |_|\__, |\__,_|_|\__,_|_| |_|
% |___/
%
% «rectangular-1» (to ".rectangular-1")
\section{Rectangular 1}
Also, note that $J(ab)=J(cd)$ is equivalent to $\co J(ab)=\co J(cd)$
(see sec.\ref{slash-ops}).
\msk
Let's say that $ab$ and $cd$ are ``$Q$-equivalent'', for some $Q⊆P$
that is clear from the context (notation: $ab\eqQ cd$) when
$\pile(ab)$ and $\pile(cd)$ are equal modulo question marks:
$\pile(ab)∖Q = \pile(cd)∖Q$. This is equivalent to saying that
$\pile(ab)$ and $\pile(cd)$ are equal on the relevant points, i.e.,
that $\pile(ab)∩S = \pile(cd)∩S$.
\msk
{\sl Theorem}. $J(ab)=J(cd)$ if and only if $ab,cd$ are $Q$-equivalent
for $Q=\qmarks(J)$.
{\sl Proof}: omitted, but the main idea is that $J(ab)=J(cd)$ if and
only if $a\eqL c$ and $b\eqR d$, and $a\eqL c$ happens if and only if
$\pile(ab)∖Q$ and $\pile(cd)∖Q$ are equal in the left column; same for
$a\eqR c$ and the right column.
\msk
In the next sections we will see ways to calculate the maximal and
minimal elements of each J-equivalence class --- i.e., $J(ab)$ and
$\co J(ab)$ --- using the set of relevant points of $J$ and the
topology.
% ____ _ _ ____
% | _ \ ___ ___| |_ __ _ _ __ __ _ _ _| | __ _ _ __ |___ \
% | |_) / _ \/ __| __/ _` | '_ \ / _` | | | | |/ _` | '__| __) |
% | _ < __/ (__| || (_| | | | | (_| | |_| | | (_| | | / __/
% |_| \_\___|\___|\__\__,_|_| |_|\__, |\__,_|_|\__,_|_| |_____|
% |___/
%
\section{Rectangular 2}
The following assumptions will hold for the rest of this section. Let
$G=((P,A),B,D)$ and suppose that $\OPENS(G)≠∅$. Let $G'$ be the 2CGQ
obtained by deleting the intercolumn arrows and applying $\propagate$
to that; let $G''$ be the 2CGQ obtained from $G'$ by adding the
intercolumn arrows back and applying $\propagate$ to that, and let
$G''':=\propagate(G)$. Formally,
%
$$\begin{array}{rclcl}
G' &=& ((P,A'),B',D') &:=& \propagate((P,A'),B,D) \\
G'' &=& ((P,A),B'',D'') &:=& \propagate((P,A),B',D') \\
G''' &=& ((P,A),B''',D''') &:=& \propagate((P,A),B,D) \\
\end{array}
$$
\def\PA{{(P,A)}}
\def\PA{{}}
\def\PAP{{(P,A')}}
{\sl Theorem 3.}
a) $B''=B'''$ and
b) $D''=D'''$, so
c) $G''=G'''$;
d) $B'' = \coInt_\PA(B') = \coInt_\PA(\coInt_\PAP(B))$ and
e) $B''' = \coInt_\PA(B)$, so $\coInt_\PA(B) = \coInt_\PA(\coInt_\PAP(B))$,
f) $D'' = \Int_\PA(D') = \Int_\PA(\Int_\PAP(D))$ and
g) $D''' = \Int_\PA(D)$, so $\Int_\PA(D) = \Int_\PA(\Int_\PAP(D))$,
\msk
Here is a motivating example for Theorem 3:
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgG" ):strs("1 ? ? ?", "? ? ? 0 ? 0"):hs():output()
%L tcgmed("tcgGG" ):strs("1 ? ? ?", "? ? ? 0 0 0"):hs():output()
%L tcgmed("tcgGGG"):strs("1 ? 0 0", "1 ? ? 0 0 0"):hs():output()
%
%L tcg_spec = "4, 6; , "
%L tcgmed("tcgGG" ):strs("1 ? ? ?", "? ? ? 0 0 0"):hs():output()
%
$$\pu
G = \tcgG
\qquad
G' = \tcgGG
\qquad
G'' = G''' = \tcgGGG
$$
Omitting the `$\pile$'s and `$\pile^{-1}$'s to make the main ideas
clearer. Note that $B'$ and $D'$ are the extremities of a rectangular
region, and that $B''$ and $D''$
\msk
Now suppose that $C∈\OPENS(G)$; we will omit the `$\pile$'s and
`$\pile^{-1}$'s to make the argument clearer. Note that $B'$ and $D'$
are the extremities of a rectangular region, and that $B''$ and $D''$
are the extremities of $[B',D']∩H$, and that $C∈[B',D']∩H$. Suppose
also that we have a J-operator $J$, and that $B'$ and $D'$ are the
extremities of the $J'$-equivalence class of $C$. Then we have
something like this:
%
%L mp = mpnew({def="ZRect", meta="s", scale="7pt"}, "12345RR4321"):addcuts("c 4321/0 0123|45|6")
%L mp:put(v"12", "C"):put(v"10", "B'") :put(v"43", "D'") :output()
%L mp = mpnew({def="ZOrig", meta="s", scale="7pt"}, "1R2R3212RL1"):addcuts("c 4321/0 0123|45|6")
%L mp:put(v"12", "C"):put(v"11", "B''"):put(v"23", "D''") :output()
%L mp = mpnew({def="ZHAJR", meta="s", scale="7pt"}, "12345RR4321"):addcuts("c 4321/0 0123|45|6")
%L mp:addlrs():output()
%L mp = mpnew({def="ZHAJ", meta="s", scale="7pt"}, "1R2R3212RL1"):addcuts("c 4321/0 0123|45|6")
%L mp:addlrs():output()
%
$$\pu
J=\ZHAJ
\quad
J'=\ZHAJR
\quad
\ZRect
\quad
\ZOrig
$$
{\sl Theorem 4.} With the conditions above, if $B'=\co J'(C)$ and
$D'=J'(C)$ then $B''=\co J(C)$ and $D''=J(C)$.
\bsk
$B'=10$, $C'=43$, $B''=B'''=11$, $C''=C'''=23$, $\OPENS(G')=[10,43]$.
%
where $C=12$, $B=C∖\qmarks(J)$, $D=C∪\qmarks(J)$, $B'=10$, $D'=43$,
$B''=11$, $D''=23$; note that $(B{⊆⊆}D)$ yields all subsets of $P$ that
\bsk
When there are no intercolumn arrows the set of open sets is
a rectangular region (possibly empty).
We will see in sec.\ref{relevant-points} that each of the
slash-regions of the ZHA at the left below corresponds to a set of the
form at the right,
%
%L mp = mpnew({def="ZRect", meta="s", scale="7pt"}, "12345RR4321"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="ZFavo"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L tcg_spec = "4, 6; , "
%L tcgmed("tcgQ"):strs(split("a ? ? ?"), split("? ? ? b ? c")):hs():output()
$$\pu \ZRect \qquad \diagxyto/<-->/<350> \qquad \OPENS\tcgQ
$$
%
for the right choice of $a,b,c∈\{0,1\}$; for example:
%
%L tcg_spec = "4, 6; , "
%L tcgmed("tcgA"):strs(split("1 ? ? ?"), split("? ? ? 0 ? 0")):hs():output()
%L tcgmed("tcga"):strs(split("1 ? ? ?"), split("? ? ? 0 0 0")):hs():output()
%L tcgmed("tcgB"):strs(split("0 ? ? ?"), split("? ? ? 1 ? 0")):hs():output()
%L tcgmed("tcgb"):strs(split("0 0 0 0"), split("1 1 1 1 ? 0")):hs():output()
%
$$\pu
\begin{array}{l}
[10,43] = \OPENS\tcgA = \OPENS\tcga, \\ \\\relax
[04,05] = \OPENS\tcgB = \OPENS\tcgb
\end{array}
$$
Note that question marks above `0's inside an $\OPENS(\ldots)$ can be
replaced by `0's and question marks below `1's can be replaced by `1's
without changing the resulting set, because no open set can have a `1'
above a `0'; also,
% Also, every $\OPENSPABD$ is the intersection of a rectangular region
% with $\Opens_A(P)$. Writing $\pile(ab)$ as just $ab$ to make the
% notation lighter, we have:
% %
% %L tcg_spec = "6, 6; 43, "
% %L tcgmed("tcgG"):lrs() :hs():output()
% %L tcgmed("tcgQ"):strs(split("? 1 ? ? 0 ?"), split("? 1 ? ? 0 ?")):hs():output()
% %L tcgmed("tcgN"):strs(split("1 1 ? ? 0 0"), split("1 1 ? ? 0 0")):hs():output()
% %L tcgmed("tcgA"):strs(split("0 1 0 0 0 0"), split("0 1 0 0 0 0")):hs():output()
% %L tcgmed("tcgB"):strs(split("1 1 1 1 0 1"), split("1 1 1 1 0 1")):hs():output()
% %L tcg_spec = "6, 6; , "
% %L tcgmed("tcgn"):strs(split("1 1 ? ? 0 0"), split("1 1 ? ? 0 0")):hs():output()
% %L mpnew({def="Zfoo", scale="7pt", meta="s"}, "12345654321"):addlrs():output()
% %L mpnew({def="Zbar", scale="5pt", meta="t"}, "1234RRR32LLL1"):addlrs():output() -- 45
% %L mpnew({def="Zbar", scale="5pt", meta="t"}, "1234RRRLLL321"):addlrs():output() -- 43
% %
% $$\pu
% \OPENS\tcgN
% \;\;=\;\;
% [22,44]∩\Opens\tcgG
% \;\;=\;\;
% [22,44]∩\Zbar
% \;\; ,
% $$
% _____ _ _ _ _
% | ____|_ _| |_ _ __ ___ _ __ ___ (_) |_(_) ___ ___
% | _| \ \/ / __| '__/ _ \ '_ ` _ \| | __| |/ _ \/ __|
% | |___ > <| |_| | | __/ | | | | | | |_| | __/\__ \
% |_____/_/\_\\__|_| \___|_| |_| |_|_|\__|_|\___||___/
%
% «extremities» (to ".extremities")
% (phap 54 "extremities")
\section{Extremities}
\label {extremities}
\def\ul#1{\underline{#1}}
\def\ol#1{\overline {#1}}
\def\UBC{\calU_B^C}
The sets $\OPENSPABD$ of sec.\ref{question-marks} are closed by unions
and intersections; let's prove a theorem about them that holds in a
more general situation. {\sl We will only deal with finite objects},
so we will not need to distinguish between ``closed by {\sl finite}
unions and intersections'' and ``closed by {\sl arbitrary} unions and
intersections''. Two abbreviations: CUAI means ``closed by unions and
intersections'' and CUAINE means ``CUAI and not-empty''; finiteness is
implied everywhere.
Every topology is CUAINE. The intersection of two sets that are CUAI
is also CUAI.
The expression ``$B$ and $C$ are the extremities of $\calS$'' will
mean: $\calS$ is CUAINE and $B=\inf(\calS)=⋂\calS$ and
$C=\sup(\calS)=⋃\calS$.
\msk
{\sl Theorem 1.} If $\calS$ is CUAINE then it has a minimal and a
maximal elements, and they can be calculated as $\inf(\calS)=⋂\calS$
and $\sup(\calS)=⋃\calS$.
{\sl Proof.} It is easy to check that $⋂\calS$ and that $⋃\calS$
belong to $\calS$, and that for any $D∈\calS$ we have
$⋂\calS⊆D⊆⋃\calS$; so the minimal and the maximal elements of $\calS$
are $⋂\calS$ and $⋃\calS$.
\msk
Let $\calU$ be a topology on a set $P$. Remember that the {\sl
interior} of an $S⊆P$ is the union of all open sets in $\calU$
contained in $S$, and the {\sl cointerior} of an $S⊆P$ is the
intersection of all open sets in $\calU$ containing $S$. We will write
the interior of $S$ as $\Int_\calU(S)$, $\Int(S)$, $S^\Int$ or
$\ul{S}$, and the cointerior as $\coInt_\calU(S)$, $\coInt(S)$,
$S^\coInt$ or $\ol{S}$; we always have $∅ ⊆ \ul{S} ⊆ S ⊆ \ol{S} ⊆ P$.
As our topologies are finite, when $U∈\calU$ we have not only
$\Int(U)=U$ but also $U=\coInt(U)$ --- i.e., $\ul{U} = U = \ol{U}$
instead of just $\ul{U} = U ⊆ \ol{U}$.
If $B⊆D⊆P$, we write $(B{⊆⊆}D)$ for $\setofst{S⊆P}{B⊆S⊆D}$; a
$(B{⊆⊆}D)$ is always CUAINE.
% There's a nice way to calculate the intersection of a $(B{⊆⊆}D)$
% with a topology on $P$ when that intersection is non-empty.
\msk
{\sl Theorem 2.} If $\calU$ is a topology on $P$ and $(B{⊆⊆}D)∩\calU$
is non-empty then all things below happen. Letting $C$ be an element
of $(B{⊆⊆}D)∩\calU$, we
have:
% and abbreviating $(B{⊆⊆}D)∩\calU$ as $\UBC$,
a) $B⊆C⊆D$ and so $\ul{B}⊆\ul{C}⊆\ul{D}$ and $\ol{B}⊆\ol{C}⊆\ol{D}$,
b) $\ul{B}⊆B⊆\ol{B}$, $\ul{C}⊆C⊆\ol{C}$, $\ul{D}⊆D⊆\ol{D}$,
c) $C$ is open, so $\ul{C}=C=\ol{C}$,
d) combining (a), (b), (c) above we get:
%
%D diagram BCD
%D 2Dx 100 +15 +15 +15 +15
%D 2D 100 D3
%D 2D +15 D2 C3
%D 2D +15 D1 C2 B3
%D 2D +15 C1 B2
%D 2D +15 B1
%D 2D
%D ren D1 D2 D3 ==> \ul{D} D \ol{D}
%D ren C1 C2 C3 ==> \ul{C} C \ol{C}
%D ren B1 B2 B3 ==> \ul{B} B \ol{B}
%D (( D1 D2 -> D2 D3 ->
%D C1 C2 = C2 C3 =
%D B1 B2 -> B2 B3 ->
%D
%D B1 C1 -> C1 D1 ->
%D B2 C2 -> C2 D2 ->
%D B3 C3 -> C3 D3 ->
%D ))
%D enddiagram
%D
$$\pu
\diag{BCD}
$$
and so $\ul{B}⊆B⊆\ol{B} ⊆ \ul{C}=C=\ol{C} ⊆ \ul{D}⊆D⊆\ol{D}$;
e) $B ⊆ \ol{B} ⊆ \ul{D} ⊆ D$;
f) $\ol{B} ⊆ C ⊆ \ul{D}$ holds for any open set $C ∈ (B{⊆⊆}D)∩\calU$,
g) $\ol{B}$ and $\ul{D}$ are open sets between $B$ and $C$,
h) $\ol{B}$ and $\ul{D}$ are the minimal and maximal opens sets between $B$ and $C$,
i) $(B{⊆⊆}D)∩\calU = (\ol{B}{⊆⊆}\ul{D})∩\calU$,
j) $(B{⊆⊆}D)∩\calU$ is CUAINE with extremities $\ol{B}$ and $\ul{D}$,
k) $\sup((B{⊆⊆}D)∩\calU) = ⋃((B{⊆⊆}D)∩\calU) = \ul{D} = \Int(D)$,
l) $\inf((B{⊆⊆}D)∩\calU) = ⋂((B{⊆⊆}D)∩\calU) = \ol{B} = \coInt(B)$.
\msk
Here is an application of Theorem 2. Let $\calU=\Opens_A(P)$. Then
%
$$\begin{array}{rcl}
\OPENSPABD & = & (B{⊆⊆}D)∩\Opens_A(P) \\
& = & (B{⊆⊆}D)∩\calU \\
& = & (\ol{B}{⊆⊆}\ul{D})∩\calU \\
& = & \OPENS((P,A),\ol{B},\ul{D}) \\
\end{array}
$$
%
two particular cases:
%
%L tcg_spec = "6, 6; 43, "
%L tcg_spec = "6, 6; , "
%L tcgmed("tcgA"):strs(split("? 1 ? ? 0 ?"), split("? 1 ? ? 0 ?")):hs():output()
%L tcgmed("tcgB"):strs(split("1 1 ? ? 0 0"), split("1 1 ? ? 0 0")):hs():output()
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgL" ):strs("1 ? ? ?", "? ? ? 0 ? 0"):hs():output()
%L tcgmed("tcgR" ):strs("1 ? 0 0", "1 ? ? 0 0 0"):hs():output()
%
$$
\pu
\OPENS\tcgA = \OPENS\tcgB
\qquad
\OPENS\tcgL = \OPENS\tcgR
$$
% _ _ _ _ _____
% | | __ _ _ __ __| | ___ ___ | | (_)_ __ |___ /
% _ | | / _` | '_ \ / _` | / __/ _ \ _ | | | | '_ \ |_ \
% | |_| | | (_| | | | | (_| | | (_| (_) | |_| | | | | | | ___) |
% \___/ \__,_|_| |_|\__,_| \___\___/ \___/ |_|_| |_| |____/
%
% «J-and-coJ-in-three-steps» (to ".J-and-coJ-in-three-steps")
% (phap 56 "J-and-coJ-in-three-steps")
\section{Calculating $J$ and $\co J$ in three steps}
\label{J-and-coJ-in-three-steps}
Fix a ZHA $H$, a J-operator $J$ on it, and an element $C∈H$. Let
$(P,A)$ be the 2CG for $H$, let $A'$ be $A$ minus its intercolumn
arrows, let $H'$ be the (rectangular) ZHA associated to $(P,A')$, and
let $J':H'→H'$ be the J-operator on $H'$ that has the same cuts as
$J$. We will consistently omit the `$\pile$'s in this section to make
the argument less cluttered, and our motivating example will be this,
%L mp = mpnew({def="ZRect", meta="s", scale="7pt"}, "12345RR4321"):addcuts("c 4321/0 0123|45|6")
%L mp:put(v"12", "C"):put(v"10", "B'") :put(v"43", "D'") :output()
%L mp = mpnew({def="ZOrig", meta="s", scale="7pt"}, "1R2R3212RL1"):addcuts("c 4321/0 0123|45|6")
%L mp:put(v"12", "C"):put(v"11", "B''"):put(v"23", "D''") :output()
%L mp = mpnew({def="ZHAJR", meta="s", scale="7pt"}, "12345RR4321"):addcuts("c 4321/0 0123|45|6")
%L mp:addlrs():output()
%L mp = mpnew({def="ZHAJ", meta="s", scale="7pt"}, "1R2R3212RL1"):addcuts("c 4321/0 0123|45|6")
%L mp:addlrs():output()
%
$$\pu
J=\ZHAJ
\quad
J'=\ZHAJR
\quad
\ZRect
\quad
\ZOrig
$$
%
where $C=12$, $B=C∖\qmarks(J)$, $D=C∪\qmarks(J)$, $B'=10$, $D'=43$,
$B''=11$, $D''=23$; note that $(B{⊆⊆}D)$ yields all subsets of $P$ that
are Q-equivalent to $C$, $(B'{⊆⊆}D')∩\Opens_{A'}(P)$ yields the
J-equivalence class of $C$ by $J'$, and $(B''{⊆⊆}D'')∩\Opens_{A}(P)$
yields the J-equivalence class of $C$ by $J$.
\msk
Let's return to the general case. We define
a) $\calU=\Pts(P)$, $\calU'=\Opens_{A'}(P)$, $\calU''=\Opens_{A}(P)$
(so $\calU⊇\calU'⊇\calU''$),
b) $B=C∖\qmarks(J)$, $D=C∪\qmarks(J)$ (so $B,D∈\calU$)
c) $B'$ and $C'$ are the extremities of $(B{⊆⊆}D)∩\calU'$ (so $B',D'∈\calU'$)
d) $B''$ and $C''$ are the extremities of $(B'{⊆⊆}D')∩\calU''$ (so $B'',D''∈\calU'$)
e) $\calI_0 = \calI = (B{⊆⊆}D)$, $\calU_0 = \calU$,
f) $\calI_1 = \calI' = (B'{⊆⊆}D')$, $\calU_1 = \calU'$,
g) $\calI_2 = \calI'' = (B''{⊆⊆}D'')$, $\calU_2 = \calU''$,
h) $\calV_{ij} = \calI_i ∩ \calU_j$.
\msk
\def \IntU#1{ \Int_{\calU#1}}
\def\coIntU#1{\coInt_{\calU#1}}
{\sl Lemma.} For all $X⊆P$ we have
i) $\IntU{''}(\IntU{'}(X)) = \IntU{''}(X)$ and
j) $\coIntU{''}(\coIntU{'}(X)) = \coIntU{''}(X)$.
\msk
{\sl Theorem.} The partial order between the sets $\calV{ij}$ above is
given by the diagram below; the non-trivial parts in it are
$\calV_{01} = \calV{11}$ and $\calV_{02} = \calV{12} = \calV{22}$.
%
%D diagram foo
%D 2Dx 100 +15 +15 +15 +15 +15 +15
%D 2D 100 I0 U0
%D 2D
%D 2D +15 I1 V00 U1
%D 2D
%D 2D +15 I2 V10 V01 U2
%D 2D
%D 2D +15 V20 V11 V02
%D 2D
%D 2D +15 V21 V12
%D 2D
%D 2D +15 V22
%D 2D
%D ren I0 I1 I2 ==> \calI_0 \calI_1 \calI_2
%D ren U0 U1 U2 ==> \calU_0 \calU_1 \calU_2
%D ren V00 V01 V02 ==> \calV_{00} \calV_{01} \calV_{02}
%D ren V10 V11 V12 ==> \calV_{10} \calV_{11} \calV_{12}
%D ren V20 V21 V22 ==> \calV_{20} \calV_{21} \calV_{22}
%D
%D (( I2 I1 -> I1 I0 ->
%D U2 U1 -> U1 U0 ->
%D
%D V20 V10 -> V10 V00 ->
%D V21 V11 -> V11 V01 =
%D V22 V12 = V12 V02 =
%D
%D V02 V01 -> V01 V00 ->
%D V12 V11 -> V11 V10 ->
%D V22 V21 -> V21 V20 ->
%D ))
%D enddiagram
%D
$$\pu
\diag{foo}
$$
\def \IntU#1{ \Int_{\calU#1}}
\def\coIntU#1{\coInt_{\calU#1}}
{\sl Proof.} Applying the theorems of sec.\ref{extremities} two times
we get:
k) The extremities of $(B{⊆⊆}D)∩\calU'$ are $B'$ and $D'$, so:
k') $(B{⊆⊆}D)∩\calU' = (B'{⊆⊆}D')∩\calU'$ (i.e., $\calV_{01} = \calV_{11}$),
k'') $B' = \coIntU{'}(B)$ and $D' = \IntU{'}(D)$,
l) the extremities of $(B'{⊆⊆}D')∩\calU''$ are $B''$ and $D''$, so:
l') $(B'{⊆⊆}D')∩\calU'' = (B''{⊆⊆}D'')∩\calU'$ (i.e., $\calV_{12} = \calV_{22}$),
l'') $B'' = \coIntU{''}(B')$ and $D'' = \IntU{''}(D')$,
m) $B'' = \coIntU{''}(\coIntU{'}(B))$ and $D'' = \IntU{''}(\IntU{'}(D))$,
n) $B'' = \coIntU{''}(B)$ and $D'' = \IntU{''}(D)$ (by (i) and (j)),
o) the extremities of $(B{⊆⊆}D)∩\calU''$ are $B''$ and $D''$, so:
o') $(B{⊆⊆}D)∩\calU'' = (B''{⊆⊆}D'')∩\calU'$ (i.e., $\calV_{02} = \calV_{22}$),
\msk
If we replace $B$ by $C∖Q$, $D$ by $C∪Q$, $B'$ by $\co J'(C)$, $D'$ by
$J'(C)$, $B''$ by $\co J(C)$, $D''$ by $J(C)$ in the items (k) and
(n'') above we get:
(...)
\msk
m) $B' = \coIntU{'}(C∖Q)$ and $D' = \IntU{'}(C∪Q)$,
n) $B'' = \coIntU{''}(\coIntU{'}(C∖Q))$ and $D' = \IntU{''}(\IntU{'}(C∪Q))$,
o) $B'' = \coIntU{''}(C∖Q)$ and $D' = \IntU{''}(C∪Q)$,
% (phap 56 "extremities")
% Then the extremities of $(B{⊆⊆}D)∩\calU''$ can be calculated in two
% steps
% f) $\ol{B}$ and $\ul{D}$ are two open sects
%
%
% $(B{⊆⊆}D)∩\calU$ is CUAINE with extremities
% $\coInt(B)$ and $\Int(D)$.
%
% {\sl Proof}. Let's write $\calU_B^C$ for $(B{⊆⊆}C)∩\calU$, $\calU^C$
% for $(∅{⊆⊆}C)∩\calU$, and $\calU_B$ for $(B{⊆⊆}P)∩\calU$.
%
% Then:
%
% 1) $\calU^C$ is the set of all open sets contained in $C$
%
% 2) $\calU^C$ is CUAINE and $\Int(C) = ⋃\calU^C = \sup(\calU^C)$
%
% 3) $\calU_B$ is the set of all open sets containing $B$
%
% 4) $\calU_B$ is CUAINE and $\coInt(B) = ⋂\calU_B = \inf(\calU_B)$
%
% 5) $\calU_B^C = \calU_B∩\calU^C$
%
% and for any $D∈\calU_B^C$ we have:
%
% 6) $D∈\calU^C$, so $D⊆\Int(C)$
%
% 7) $D∈\calU_B$, so $\coInt(B)⊆D$
%
% so:
%
% 8) $⋃\calU^C⊆\Int(C)$
%
% 9) $\coInt(B)⊆⋂\calU_B$
%
%
%
%
%
%
% \msk
% \msk
%
% The sets $\calU$, $\calU'$ and $\calU''$ above are closed by unions
% and intersections. {\sl We will only deal with finite objects}, so we
% will not need to distinguish between ``closed by {\sl finite} unions
% and intersections'' and ``closed by {\sl arbitrary} unions and
% intersections''.
%
% \msk
%
% In the rest of this section we will prove some things that hold in
% general motivated by the example above. Let $P$ be a finite set.
%
%
% \msk
%
% {\sl Lemma 1:} if $\calU$ is a topology on $P$, $B⊆C⊆P$, and there is
% an open set $D∈\calU$ with $B⊆D⊆C$, then
% %
% $$\begin{tabular}{rl}
% a) & $B⊆B^\coInt⊆D⊆C^\Int⊆C$, \\
% b) & the extremities of $(B{⊆⊆}C)∩\calU$ are $B^\coInt$ and $C^\Int$, \\
% c) & $(B{⊆⊆}C)∩\calU$ = $(B^\coInt{⊆⊆}C^\Int)∩\calU$. \\
% \end{tabular}
% $$
%
% {\sl Proof:} (a) $C^\Int$ is the union of all open sets contained in
% $C$, and one of those open sets is $D$, so $D⊆C^\Int⊆C$; doing the
% same for $B^\coInt$ we get $B⊆B^\coInt⊆D$. (b) We have $B^\coInt, D,
% C^\Int ∈ (B{⊆⊆}C)∩\calU$ and all elements of $(B{⊆⊆}C)∩\calU$ contain
% $B^\coInt$ and are contained in $C^\Int$, so $B^\coInt$ and $C^\Int$
% are the extremities of $(B{⊆⊆}C)∩\calU$. (c) is a consequence of (b).
%
% \msk
%
% {\sl Lemma 2:} suppose that $\calU''⊆\calU' ⊆ \Pts(P)$ are topologies
% on $P$, $B⊆D⊆C⊆P$, and $D∈\calU''$, and define:
% %
% $$\begin{tabular}{rl}
% a) & $B'$ and $C'$ are the extremities of $(B{⊆⊆}C)∩\calU'$, \\
% b) & $B''$ and $C''$ are the extremities of $(B{⊆⊆}C)∩\calU''$. \\
% \end{tabular}
% $$
% %
% Then:
% %
% $$\begin{tabular}{rl}
% c) & $B' =\coInt_{\calU'} (B)$ and $C' =\Int_{\calU'} (C)$, \\
% d) & $B'' =\coInt_{\calU''}(B)$ and $C''=\Int_{\calU''}(C)$, \\
% e) & $B⊆B'⊆B''⊆D⊆C''⊆C'⊆C$, \\
% f) & $(B{⊆⊆}C)∩\calU' = (B'{⊆⊆}C')∩\calU'$, \\
% g) & $(B{⊆⊆}C)∩\calU'' = (B''{⊆⊆}C'')∩\calU''$, \\
% h) & $(B{⊆⊆}C)∩\calU'' = (B'{⊆⊆}C')∩\calU'' = (B''{⊆⊆}C'')∩\calU''$, \\
% i) & $\Int_{\calU'}(C) = \Int_{\calU'}(C') = C'$, \\
% j) & $\Int_{\calU''}(C) = \Int_{\calU''}(C') = \Int_{\calU''}(C'') = C''$, \\
% k) & $\coInt_{\calU'}(B) = \coInt_{\calU'}(B') = B'$, \\
% l) & $\coInt_{\calU''}(B) = \coInt_{\calU''}(B') = \coInt_{\calU''}(B'') = B''$. \\
% \end{tabular}
% $$
%
% {\sl Proofs:} almost trivial: (c) is by 2a and lemma 1a; (d) by 2b and
% lemma 1a; (e) by lemma 1a and $\calU''⊆\calU$; (f) by lemma 1c; (g) by
% lemma 1c; (h) by 2g and $B⊆B'⊆B''$ and $C''⊆C'⊆C$; (i) by 2f and 1c;
% (j) by 1b and 2h; (k) by 2f and 1c; (l) by 1b and 2h.
%
% \msk
%
% {\sl Lemma 3:} let $((P,A),B,C)$ be a 2CGQ and let $A'$ be $A$ without
% its intercolumn arrows. Suppose that $B⊆D⊆C$ and $D∈\Opens_A(P)$. Let
% %
% $$\begin{array}{ll}
% \calU' = \Opens(A')(P), \\
% \calU'' = \Opens(A)(P), \\
% B' = \coInt_{\calU }(B), & C' = \Int_{\calU }(C), \\
% B'' = \coInt_{\calU'}(B), & C'' = \Int_{\calU'}(C). \\
% \end{array}
% $$
%
% Then
% %
% $$\begin{array}{ll}
% B'' = \coInt_{\calU'}(B'), & C'' = \Int_{\calU'}(C'), \\
% \end{array}
% $$
% %
% $$\begin{array}{rcl}
% \OPENS((P,A),B,C) &=& \OPENS((P,A),B',C') \\
% &=& \OPENS((P,A),B'',C''), \\
% \end{array}
% $$
% %
% and the extremities of $\OPENS((P,A),B,C)$ are $B''$ and $C''$.
% ____ _ _
% | _ \ ___ ___| |_ __ _ _ __ __ _ _ _| | __ _ _ __
% | |_) / _ \/ __| __/ _` | '_ \ / _` | | | | |/ _` | '__|
% | _ < __/ (__| || (_| | | | | (_| | |_| | | (_| | |
% |_| \_\___|\___|\__\__,_|_| |_|\__, |\__,_|_|\__,_|_|
% |___/
%
% «rectangular-ZHAs» (to ".rectangular-ZHAs")
\section{Rectangular ZHAs}
\label{rectangular-ZHAs}
% (phap 56 "rectangular-ZHAs")
The ZHA $H$ above is generated by the 2CG $(P,A)$ below; we will
sometimes need the 2CG $(P,A')$ that is obtained by $(P,A)$ by
deleting the intercolumn arrows,
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("foo"):lrs():hs() :output()
%L tcg_spec = "4, 6; , "
%L tcgmed("bar"):lrs():hs() :output()
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgbig("foo"):lrs():hs():vs():output()
%L tcg_spec = "4, 6; , "
%L tcgbig("bar"):lrs():hs():vs():output()
%
$$
\pu
(P,A) = \foo
\qquad
(P,A') = \bar
$$
%
and we will need the ``rectangular versions'' of $H$ and $J$, that we
will call $H'$ and $J'$:
%
%L mp = mpnew({def="Hprime"}, "12345RR4321"):addlrs() :output()
%L mp = mpnew({def="Jprime"}, "12345RR4321"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%
$$\pu
H' = \Hprime
\qquad
J' = \Jprime
$$
% ___ _ _ _ _
% |_ _|_ __ | |_ ___ __ _ _ __ __| | (_)_ __ | |_ ___
% | || '_ \| __/ __| / _` | '_ \ / _` | | | '_ \| __/ __|
% | || | | | |_\__ \ | (_| | | | | (_| | | | | | | |_\__ \
% |___|_| |_|\__|___/ \__,_|_| |_|\__,_| |_|_| |_|\__|___/
%
% «on-intervals-and-interiors» (to ".on-intervals-and-interiors")
\section{A theorem on intervals and interiors}
\label {on-intervals-and-interiors}
% (phap 53 "on-intervals-and-interiors")
Consider these three partial orders on $P=\LC(4)∪\RC(6)$ (see
sec.\ref{2CGs}),
%
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgbig("tcgFull"):lrs():hs():vs():output()
%L tcgbig("tcgVert"):lrs() :vs():output()
%L tcgbig("tcgDisc"):lrs() :output()
%
$$
\pu
(P,∅) = \tcgDisc
\quad
(P,A') = \tcgVert
\quad
(P,A) = \tcgFull
$$
%
where $A'$ is obtained from $A$ by deleting the intercolumn arrows.
Writing $\pile(ab)$ as just $ab$ everywhere to make the notation
lighter, we have three nested topologies:
%
%L mp = mpnew({def="ZRect"}, "12345RR4321"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="ZOrig"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="ZRect", scale="7pt", meta="s"}, "12345RR4321"):addlrs() :output()
%L mp = mpnew({def="ZOrig", scale="7pt", meta="s"}, "1R2R3212RL1"):addlrs() :output()
%
$$\pu
\calU=\Pts(P)
\qquad
\calU'=\Opens_{A'}(P)=\ZRect
\qquad
\calU''=\Opens_{A}(P)=\ZOrig
$$
%
where $\calU⊇\calU'⊇\calU''$. The ZHAs will be named $H=\Opens_{A}(P)$
and $H='\Opens_{A'}(P)$; $H'$ is the rectangular ZHA associated to
$H$. Except in the passage from $H$ to $H'$ and from $A$ to $A'$ our
convention on the notation will be that addings primes always means
going to a topology with fewer open sets, or to smaller intervals.
We will prove a theorem that involves an interval $[B',C']$ in $H'$
and its (non-empty) intersection with $H$, and we will refer to the
extremities of $[B',C']∩H$ as $B''$ and $C''$. Visually:
%
%L mp = mpnew({def="ZRect"}, "12345RR4321"):put(v"10", "B'") :put(v"43", "C'") :addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="ZOrig"}, "1R2R3212RL1"):put(v"11", "B''"):put(v"23", "C''"):addcuts("c 4321/0 0123|45|6"):output()
%
$$\pu
\ZRect
\qquad
\ZOrig
$$
%
but $B'$ and $C'$ will be obtained by a $B$ and a $C$ with $B⊆C⊆P$ by
the operation described in the previous section that replaces the `?'s
above `1's by `1's and the `?'s below `0's by `0's. To make our
example case complete,
%
%L tcg_spec = "4, 6; , "
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgBC") :strs("1 ? ? ?", "? ? ? 0 ? 0") :output()
%L tcgmed("tcgBCp") :strs("1 ? ? ?", "? ? ? 0 0 0") :output()
%L tcgmed("tcgBCpp"):strs("1 ? 0 0", "1 ? ? 0 0 0"):hs():output()
%
$$\pu
\begin{array}{rcccl}
\OPENS((P,∅),B,C) &=& \tcgBC &=& (10{⊆⊆}43) \\\\
\OPENS((P,A'),B',C') &=& \tcgBCp &=& [10,43] \\\\
\OPENS((P,A),B'',C'') &=& \tcgBCpp &=& [11,23]∩H \\
\end{array}
$$
\newpage
\def\forget {\operatorname{\mathsf{forget}}}
\def\coInt{{\operatorname{\mathsf{coint}}}}
Translating these adjunctions to basic terms, they mean that for any
choices of $W,U∈\Opens(S)$ and $V∈\Opens(P)$ we have:
What happens when we combine $\forget_Q$ and $\OPENS$? Fix a ZHA $H$
and a J-operator $J$ on it, and from that produce $(P,A)$,
$\calU=\Opens_A(P)$, $S$, and $Q$. For any $cd∈H$ we have
%
$$\pile^{-1}(\OPENS(\forget_Q(\pile(cd)))) = [cd]^J,$$
%
which yields the J-equivalence class of $cd$ --- and we can use the
tricks from the last sections to obtain the top element, $J(cd)$, from
that equivalence class:
%
$$\begin{array}{rcl}
J(cd) &=& \sup([cd]^J) \\
&=& \sup(\pile^{-1}(\OPENS(\forget_Q(\pile(cd))))) \\
&=& \pile^{-1}(\sup(\OPENS(\forget_Q(\pile(cd))))) \\
&=& \pile^{-1}(\sup(\OPENS((P,A), \pile(cd)∖Q, \pile(cd)∪Q)))) \\
&=& \pile^{-1}(\Int(\pile(cd)∪Q)) \\
\pile(J(cd)) &=& \Int(\pile(cd)∪Q) \\
\end{array}
$$
We have two different natural operations from $\Opens_{A|_S}(S)$ to
$\Opens_A(P)$. One takes a $V∈\Opens_{A|_S}(S)$ and returns
$\Int(V∪Q)$ --- this one returns the top element of each J-equivalence
class --- and the other a $V∈\Opens_{A|_S}(S)$ and returns
$\coInt(V∖Q)$; this one
%L tcg_spec = "4, 6; 11 22 34 45, 25"
%L tcgmed("tcgO"):strs(split("1 0 0 0"), split("1 1 0 0 0 0")):hs():output()
%L tcgmed("tcgQ"):strs(split("1 ? ? ?"), split("? ? ? 0 ? 0")):hs():output()
%
%$$\pu
% %\Ques(\pile(12))
% \Ques(\{1\_, \; \_1, \_2\})
% \;\;=\;\;
% \Ques\tcgO
% \;\;=\;\;
% \tcgQ
%$$
\newpage
{\sl Theorem:} $f^! ⊣ f^* ⊣ f_*$.
{\sl Proof:} it is sufficient to prove (a) and (b). By a well-known
fact on adjoints on preorders (a) is equivalent to (c) and (e) below,
and (b) is equivalent to (e) and (f):
c) $f^*(f_*(U))⊆U$
d) $V⊆f_*(f^*(V))$
e) $W⊆f^*(f^!(W))$
f) $f^!(f^*(V))⊆V$
%
and we can rewrite conditions (c), (d), (e), (f) as:
c') $\Int(U∪Q)∩S⊆U$
d') $V⊆\Int((V∩S)∪Q)$
e') $W⊆\coInt(W)∩S$
f') $\coInt(V∩S)⊆V$
We will prove (d'), (f'), and the following stronger versions of (c')
and (e'):
c'') $\Int(U∪Q)∩S=U$
e'') $W=\coInt(W)∩S$
Here are the proofs:
c'') Choose an $U'∈\Opens(P)$ such that $U=U'∩S$. Then $U'$, $U$ and
$U∪Q$ are all Q-equivalent, and $U'⊆U∪Q$;
d')
e'')
f')
\newpage
% ____ _ _ _ _
% / ___| |__ (_) | __| |_ __ ___ _ __
% | | | '_ \| | |/ _` | '__/ _ \ '_ \
% | |___| | | | | | (_| | | | __/ | | |
% \____|_| |_|_|_|\__,_|_| \___|_| |_|
%
% «children» (to ".children")
\section{Appendix: on ``children''}
\label{children}
% Bad (phap 57 "children")
% (find-LATEXfile "" "istanbul1.tex")
% (find-LATEXfile "istanbul1.org")
% (find-LATEXfile "istanbul1.org" "Why study CT")
% (find-xpdfpage "~/LATEX/istanbul1.pdf")
% (find-xpdfpage "~/LATEX/istanbul1.pdf" 3)
% https://mail.google.com/mail/ca/u/0/#search/arndt/153e28089870b2ba
...from the slides of my minicourse in the UniLog 2016 (Istanbul):
\begin{itemize}
\item Why study Category Theory {\sl now}?
Public education in Brazil is being dismantled --- maybe we should
be doing better things than studying very technical \& inaccessible
subjects with no research grants ---
{\sl (Here I showed a photo called ``The New Girl From Ipanema'' ---
a girl walking on the Ipanema beach at night with a gas mask, with
a huge cloud of tear gas behind her)}
\item Category theory should be more accessible
Most texts about CT are for specialists in research universities...
{\sl Category theory should be more accessible.}.
To whom?...
\begin{itemize}
\item Non-specialists (in research universities)
\item Grad students (in research universities)
\item Undergrads (in research universities)
\item Non-specialists (in conferences - where we have to be quick)
\item Undergrads (e.g., in CompSci - in teaching colleges) - (``Children'')
\end{itemize}
\item What do we mean by "accessible"?
\begin{itemize}
\item Done on very firm grounds: mathematical objects made from
numbers, sets and tuples; FINITE, SMALL mathematical objects
whenever possible. Avoid references to non-mathematical things like
windows, cars and pizzas (like the object-orientation people do);
avoid reference to Physics; avoid Quantum Mecanics at all costs;
time is difficult to draw, prefer {\sl static} rather than {\sl
changing}
\item People have very short attention spans nowadays
\item Self-contained, but not {\sl isolated} or {\sl isolating}; our
material should make the literature more accessible
\item We learn better by doing. Our material should have lots of space
for exercises.
\item Most people with whom I interact are not from Maths/CS/etc
\item {\sl Proving} general cases is relatively hard. {\sl Checking}
and {\sl calculating} is much easier. People can believe that
something can be generalized after seeing a convincing particular
case. (Sometimes leave them to look for the right generalization by
themselves)
\end{itemize}
\end{itemize}
% \msk
% Most books on advanced mathematics mention, in their introductions,
% how much ``mathematical maturity'' a reader needs to have in order
% to understand their contents... the term ``mathematical maturity''
% means, among other things, the ability to {\sl work on very abstract
% settings}, to {\sl generalize}, to {\sl particularize}, and to {\sl
% use infinite objects}, besides familiarity with the notation,
% methods, and main concepts in mathematics. A nice term for people
% with very little mathematical maturity is ``children''.
% I've tried to write this paper in a way as to makes it as accessible
% as possible to ``children'' like humanities students, philosophers
% with little mathematical background, and freshmen Computer Science
% students. Most of the sections were written after I presented the
% material corresponding to them in a {\sl very} basic introductory
% course on lambda-calculus and logic that I gave in the second half
% of 2016, whose audience was a group of six CompSci students; the
% exercises that they solved in class are not included here.
% I've had a handful of opportunities to present parts of this
% material to humanities students --- with them I had to start with
% exercises on expressions, quantifiers, evaluation, functions, sets,
% and lambda-notation, that are not included here.
I've been using ``for children'' in titles for a while. This is a bit
of a marketing strategy, of course, but the term ``children'' here has
a precise, though unusual, meaning: it means ``people with very little
mathematical maturity'', where I am taking these as the main aspects
of ``mathematical maturity'': the ability to {\sl work on very
abstract settings}, to {\sl generalize}, to {\sl particularize}, and
to {\sl use infinite objects}.
Writing things ``for children'' in this sense results in material that
[is accessible] [exercises, not included here] [visual, easy to check]
[who I've tested this with]
\msk
{\sl A note for ``adults''.} In [Ochs2013] I sketched a method for
working in a general case and in a particular case (an ``archetypal
case'') in parallel, and also a way to prove things in the archetypal
case and then ``lift'' the proofs to the general case. This paper is
an offspring of that one; I believe that planar Heyting Algebras
presented here (ZHAs, sec.\ref{ZHAs}) are archetypal Heyting Algebras,
and when we add ``closure operators'' to ZHAs (as in the seminar notes
\url{http://angg.twu.net/math-b.html\#zhas-for-children}, pp.13--30;
they are called ``J-operators'' there) we get something that is
archetypal for studying toposes and sheaves; that will be the subject
of a sequel of this paper.
[Topos theory books are too hard for me] [a bridge between
philosophers and toposophers]
% besides familiarity with the notation, methods, and main concepts in
% mathematics.
% ____ _ _
% / ___|___ _ __ ___ _ __ _ __ ___| |__ ___ _ __ ___(_) ___ _ __
% | | / _ \| '_ ` _ \| '_ \| '__/ _ \ '_ \ / _ \ '_ \/ __| |/ _ \| '_ \
% | |__| (_) | | | | | | |_) | | | __/ | | | __/ | | \__ \ | (_) | | | |
% \____\___/|_| |_| |_| .__/|_| \___|_| |_|\___|_| |_|___/_|\___/|_| |_|
% |_|
%
% «comprehension» (to ".comprehension")
\section{Appendix: notations for set comprehension}
% Bad (phap 58 "comprehension")
% (find-angg "LATEX/2016-2-LA-zhas.tex")
% (lazp 1)
\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\text{#2}}} \def\ug#1{\und{#1}{gen}}
\def\uf#1{\und{#1}{filt}} \def\ue#1{\und{#1}{expr}}
\def\uv#1{\und{#1}{var}}
\def\tbl#1#2{\fbox{$\begin{array}{#1}#2\end{array}$}}
\def\tbl#1#2{\fbox{$\sm{#2}$}}
\def\V{\mathbf{T}}
\def\F{\mathbf{F}}
% "Stop":
\def\S{\omit\vrule\phantom{$\scriptstyle($}\hss} % stop
% strut:
\def\s{\mathstrut}
\def\s{\phantom{$|$}}
\def\s{\phantom{|}}
\def\s{}
This is section is just to clarify the exact meaning of the
``$\setofst{\ldots}{\ldots}$-expressions'' in the previous sections.
% The definition of $\LR$ in the previous sections deserves more
% explanations.
We'll use three notations for set comprehensions: a ``low-level'' one,
with generators and filters separated by commas, then a semicolon and
then the result expression, and two higher-level notations using a
`$|$', that are closer to the standard ones.
Here are some examples of the low-level notation,
%
$$\begin{array}{lll}
\{\ug{a∈\{1,2,3,4\}}; \ue{10a}\} &=& \{10,20,30,40\} \\
\{\ug{a∈\{1,2,3,4\}}; \ue{a}\} &=& \{1,2,3,4\} \\
\{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}; \ue{a}\} &=& \{3,4\} \\
\{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}; \ue{10a}\} &=& \{30,40\} \\
\{\ug{a∈\{10,20\}}, \ug{b∈\{3,4\}}; \ue{a+b}\} &=& \{13,14,23,24\} \\
\{\ug{a∈\{1,2\}}, \ug{b∈\{3,4\}}; \ue{(a,b)}\} &=& \{(1,3),(1,4),(2,3),(2,4)\} \\
\end{array}
$$
Here is how to calculate the results of some low-level comprehensions
using tables; note that when a filter yields ``false'' we stop ---
this is indicated by a vertical bar --- and we don't calculate the
rest of the line. The result of the comprehension is the set of the
results in the lines where all filters yielded ``true''.
%
$$\begin{array}{l}
\{\ug{x∈\{1,2,3\}}, \ug{y∈\{3,4\}}, \uf{x+y<6}; \ue{(x,y)}\}
= \{(1,3),(1,4),(2,3)\}
\\
\tbl{ccc}{
\s x & y & x+y<6 & (x,y) \\\hline
\s 1 & 3 & \V & (1,3) \\
\s 1 & 4 & \V & (1,4) \\
\s 2 & 3 & \V & (2,3) \\
\s 2 & 4 & \F & \S \\
\s 3 & 3 & \F & \S \\
\s 3 & 4 & \F & \S \\
}
\end{array}
$$
$$\begin{array}{l}
\{\ug{(x,y)∈\{1,2,3\}^2}, \uf{x>y}; \ue{(x,y)}\}
= \{(2,1), (3,1), (3,2)\}
\\
\tbl{ccc}{
\s (x,y) & x & y & x>y & (x,y) \\\hline
\s (1,1) & 1 & 1 & \F & \S \\
\s (1,2) & 1 & 2 & \F & \S \\
\s (1,3) & 1 & 3 & \F & \S \\
\s (2,1) & 2 & 1 & \V & (2,1) \\
\s (2,2) & 2 & 2 & \F & \S \\
\s (2,3) & 2 & 3 & \F & \S \\
\s (3,1) & 3 & 1 & \V & (3,1) \\
\s (3,2) & 3 & 2 & \V & (3,2) \\
\s (3,3) & 3 & 3 & \F & \S \\
}
\end{array}
$$
\bsk
Here are some examples of the higher-level, standard-ish notations for
set comprehensions, and how they can be translated into the low-level notation:
%
$$\begin{array}{llll}
& \text{(standard)} & & \text{(low-level)} \\[5pt]
%
& \setofst{\ue{10a}}{\ug{a∈\{1,2,3,4\}}} &=&
\{\ug{a∈\{1,2,3,4\}}; \ue{10a}\} \\
& \setofst{\ue{a}}{\ug{a∈\{1,2,3,4\}}} &=&
\{\ug{a∈\{1,2,3,4\}}; \ue{a}\} \\
& \setofst{\ue{10a}}{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}} &=&
\{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}; \ue{10a}\} \\
& \setofst{\ue{a}}{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}} &=&
\{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}; \ue{a}\} \\
& \setofst{\ug{a∈\{1,2,3,4\}}}{\uf{a≥3}} &=&
\{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}; \ue{a}\} \\
% & \{\ug{a∈\{10,20\}}, \ug{b∈\{3,4\}}; \ue{a+b}\} \\
% & \{\ug{a∈\{1,2\}}, \ug{b∈\{3,4\}}; \ue{(a,b)}\} \\
\end{array}
$$
The first four are of the form
``$\setofst{\text{expr}}{\text{generators and filters}}$''
(``e$|$gf''), and the last one is of the form
``$\setofst{\text{generator}}{\text{filters}}$'' (``g$|$f''). In
``g$|$f'' comprehensions the final `expr' is the variable of the
generator:
%
% (find-angg "LATEX/2016-2-LA-zhas.tex" "comprehension-2")
% (lazp 2)
%
$$\begin{array}{llll}
% & \text{(standard)} & & \text{(explicit)} \\[5pt]
& \setofst{\ug{\uv{a}∈\{1,2,3,4\}}}{\uf{a≥3}} &=&
\{\ug{a∈\{1,2,3,4\}}, \uf{a≥3}; \ue{a}\} \\
% & \setofst {\ug{\uv{(x,y)}∈\{1,2,3\}^2}} {\uf{x>y}} &=&
% \{\ug{(x,y)∈\{1,2,3\}^2}, \uf{x>y}; \ue{(x,y)}\} \\
\end{array}
$$
\end{document}
\newpage
\section{Cubes: old code}
%D diagram cube-and*-0
%D 2Dx 100 +30 +30
%D 2D 100 A1
%D 2D +25 A2 A3 A4
%D 2D +25 A5 A6 A7
%D 2D +25 A8
%D 2D
%D ren A1 ==> (P^*∧Q^*)^*
%D ren A2 A3 A4 ==> (P∧Q^*)^* P^*∧Q^* (P^*∧Q)^*
%D ren A5 A6 A7 ==> P∧Q^* (P∧Q)^* P^*∧Q
%D ren A8 ==> P∧Q
%D
%D (( A1 A2 <- A1 A3 <- A1 A4 <-
%D A2 A5 <- A2 A6 <- A3 A5 <- A3 A7 <- A4 A6 <- A4 A7 <-
%D A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%
%D diagram cube-or*-0
%D 2Dx 100 +30 +30
%D 2D 100 A1
%D 2D +25 A2 A3 A4
%D 2D +25 A5 A6 A7
%D 2D +25 A8
%D 2D
%D ren A1 ==> (P^*∨Q^*)^*
%D ren A2 A3 A4 ==> (P∨Q^*)^* P^*∨Q^* (P^*∨Q)^*
%D ren A5 A6 A7 ==> P∨Q^* (P∨Q)^* P^*∨Q
%D ren A8 ==> P∨Q
%D
%D (( A1 A2 <- A1 A3 <- A1 A4 <-
%D A2 A5 <- A2 A6 <- A3 A5 <- A3 A7 <- A4 A6 <- A4 A7 <-
%D A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%
%D diagram cube-imp*-0
%D 2Dx 100 +30 +30
%D 2D 100 A1
%D 2D +25 A2 A3 A4
%D 2D +25 A5 A6 A7
%D 2D +25 A8
%D 2D
%D ren A1 ==> (P→Q^*)^*
%D ren A2 A3 A4 ==> (P^*→Q^*)^* P→Q^* (P→Q)^*
%D ren A5 A6 A7 ==> P^*→Q^* (P^*→Q)^* P→Q
%D ren A8 ==> P^*→Q
%D
%D (( A1 A2 <- A1 A3 <- A1 A4 <-
%D A2 A5 <- A2 A6 <- A3 A5 <- A3 A7 <- A4 A6 <- A4 A7 <-
%D A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%D diagram cube-and*-2
%D 2Dx 100 +30 +30
%D 2D 100 A1
%D 2D +25 A2 A3 A4
%D 2D +25 A5 A6 A7
%D 2D +25 A8
%D 2D
%D ren A1 ==> (P^*∧Q^*)^*
%D ren A2 A3 A4 ==> (P∧Q^*)^* P^*∧Q^* (P^*∧Q)^*
%D ren A5 A6 A7 ==> P∧Q^* (P∧Q)^* P^*∧Q
%D ren A8 ==> P∧Q
%D
%D (( A1 A2 = A1 A3 = A1 A4 =
%D A2 A5 <- A2 A6 = A3 A5 <- A3 A7 <- A4 A6 = A4 A7 <-
%D A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%
%D diagram cube-or*-1
%D 2Dx 100 +30 +30
%D 2D 100 A1
%D 2D +25 A2 A3 A4
%D 2D +25 A5 A6 A7
%D 2D +25 A8
%D 2D
%D ren A1 ==> (P^*∨Q^*)^*
%D ren A2 A3 A4 ==> (P∨Q^*)^* P^*∨Q^* (P^*∨Q)^*
%D ren A5 A6 A7 ==> P∨Q^* (P∨Q)^* P^*∨Q
%D ren A8 ==> P∨Q
%D
%D (( A1 A2 = A1 A3 <- A1 A4 =
%D A2 A5 <- A2 A6 = A3 A5 <- A3 A7 <- A4 A6 = A4 A7 <-
%D A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%
%D diagram cube-imp*-1
%D 2Dx 100 +30 +30
%D 2D 100 A1
%D 2D +25 A2 A3 A4
%D 2D +25 A5 A6 A7
%D 2D +25 A8
%D 2D
%D ren A1 ==> (P→Q^*)^*
%D ren A2 A3 A4 ==> (P^*→Q^*)^* P→Q^* (P→Q)^*
%D ren A5 A6 A7 ==> P^*→Q^* (P^*→Q)^* P→Q
%D ren A8 ==> P^*→Q
%D
%D (( A1 A2 = A1 A3 = A1 A4 <-
%D A2 A5 = A2 A6 <- A3 A5 = A3 A7 <- A4 A6 <- A4 A7 <-
%D A5 A8 <- A6 A8 <- A7 A8 <-
%D ))
%D enddiagram
%
%:
%:
%: [P→Q]^1 (P→Q)→P [Q]^2
%: ------------------ -----3
%: P [P→Q]^1 P→Q (P→Q)→P
%: -------------------- ----------------
%: Q P
%: ---------1 ----2
%: (P→Q)→Q Q→P
%: ------------------------
%: ((P→Q)→Q)∧(Q→P)
%:
%: ^foo
%:
$$\pu
\def→{{\to}}
\ded{foo}
$$
% (phap 39)
% (phap 46)
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-anchor-format: "«%s»"
% End: