Warning: this is an htmlized version!
The original is across this link,
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: