|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2019planar-has-2-slashings.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019planar-has-2-slashings.tex"))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019planar-has-2-slashings.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2019planar-has-2-slashings.pdf"))
% (defun b () (interactive) (find-zsh "bibtex 2019planar-has-2-slashings; makeindex 2019planar-has-2-slashings"))
% (defun e () (interactive) (find-LATEX "2019planar-has-2-slashings.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019planar-has-2-slashings"))
% (find-xpdfpage "~/LATEX/2019planar-has-2-slashings.pdf")
% (find-sh0 "cp -v ~/LATEX/2019planar-has-2-slashings.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2019planar-has-2-slashings.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2019planar-has-2-slashings.pdf
% file:///tmp/2019planar-has-2-slashings.pdf
% file:///tmp/pen/2019planar-has-2-slashings.pdf
% http://angg.twu.net/LATEX/2019planar-has-2-slashings.pdf
% «.picturedots» (to "picturedots")
% «.title» (to "title")
% «.abstract» (to "abstract")
%
% «.introduction» (to "introduction")
% «.piccs-and-slashings» (to "piccs-and-slashings")
% «.slash-regions» (to "slash-regions")
% «.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")
\documentclass[oneside]{article}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
\usepackage{color} % (find-LATEX "edrx15.sty" "colors")
\usepackage{colorweb} % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof} % For derivation trees ("%:" lines)
\input diagxy % For 2D diagrams ("%D" lines)
%\xyoption{curve} % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx15} % (find-LATEX "edrx15.sty")
\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
%
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
%L dofile "edrxtikz.lua" -- (find-LATEX "edrxtikz.lua")
%L dofile "edrxpict.lua" -- (find-LATEX "edrxpict.lua")
\pu
\input 2017planar-has-defs.tex % (find-angg "LATEX/2017planar-has-defs.tex")
\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}
\def\eqQp{\sim_{Q'}}
\def\ECube{\mathsf{ECube}} \def\ecube{\mathsf{ecube}}
\def\OCube{\mathsf{OCube}} \def\ocube{\mathsf{ocube}}
\def\FCube{\mathsf{FCube}} \def\fcube{\mathsf{fcube}}
\def\VCube{\mathsf{VCube}} \def\vcube{\mathsf{vcube}}
\def\Exprs{\mathsf{Exprs}}
\def\Thms{\mathsf{Thms}}
\def\thms{\mathsf{thms}}
\def\vthms{\mathsf{vthms}}
\def\NClasses{\mathsf{NClasses}}
\def\nclasses{\mathsf{nclasses}}
\def\ZHAstar{ZHA${}^*$}
\def\sfE{\mathsf{E}}
\def\sfV{\mathsf{V}}
\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\obeys{\mathsf{obeys}}
\def\isoftheform{\operatorname{\mathsf{is\ of\ the\ form}}}
% ____ _
% | _ \(_) ___ ___ ___
% | |_) | |/ __/ __/ __|
% | __/| | (_| (__\__ \
% |_| |_|\___\___|___/
%
% «piccs-and-slashings» (to ".piccs-and-slashings")
\section{Piccs and slashings}
\label {piccs-and-slashings}
% Good (ph2p 2 "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}
A picc (``partition into contiguous classes'') of an interval
$I=\{0,\ldots,n\}$ is a partition $P$ of $I$ that obeys this
condition (``picc-ness''):
%
$$∀a,b,c∈\{0,\ldots,n\}.\; (a<b<c \;\;\&\;\; a \eqP c) → (a \eqP b \eqP c).$$
%
So $P = \{\{0\},\{1,2,3\},\{4,5\}\}$ is a picc of $\{0,\ldots,5\}$,
and $P' = \{\{0\},\{1,2,4,5\},\{3\}\}$ is a partition of
$\{0,\ldots,5\}$ that is not a picc.
A short notation for piccs is this:
%
$$0|123|45 \equiv \{\{0\},\{1,2,3\},\{4,5\}\}$$
%
we list all digits in the ``interval'' $\{0,\ldots,n\}$ in order, and
we put bars to indicate where we change from one equivalence class to
another.
We write $[b]_P$ for the equivalence class of $b$ in a picc $P$,
$×_\LR$ for the product in $\LR$, and $[ab,ef]$ for an ``interval'' in
$\LR$:
%
$$\begin{array}{rcl}
\{2,3,4\} × \{5,6,7\} &=& \setofst{(x,y)}{x∈\{2,3,4\}, y∈\{5,6,7\}} \\
\{2,3,4\}×_\LR\{5,6,7\} &:=& \setofst{〈a,b〉}{a∈\{2,3,4\}, b∈\{5,6,7\}} \\{}
[ab,ef] \;:=\; [\ang{a,b},\ang{e,f}]
&:=& \{a,\ldots,e\} ×_\LR \{b,\ldots,f\} \\
&=& \setofst {\ang{c,d}∈\LR} {a≤c≤e \;∧\; b≤d≤f}.
\end{array}
$$
A {\sl slashing} $S$ on a ZHA $H$ with top element $ab$ is a pair of
piccs, $S=(L,R)$, where $L$ is a picc on $\{0,\ldots,a\}$ and $R$ is a
picc on $\{0,\ldots,b\}$; for example, $S=(4321/0,\, 0123∖45∖6)$
is a slashing on $[00,46]$. We write the bars in $L$ as `$/$'s and the
bars in $R$ as `$∖$' as a reminder that they are to be interpreted
as northeast and northwest ``cuts'' respectively; $S=(4321/0,\,
0123∖45∖6)$ is interpreted as the diagram at the left below, and
it ``slashes'' $[00,46]$ and the ZHA at the right below as:
%
%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
$$
A slashing $S=(L,R)$ on a ZHA $H$ with top element $ab$ induces an
equivalence relation `$\eqS$' on $H$ that works like this: $\ang{c,d}
\eqS \ang{e,f}$ iff $c \eqL e$ and $d \eqR f$. The equivalence classes
of a slashing are called {\sl slash-regions}. Note that:
%
$$\begin{array}{rcl}
% [c]_L &:=& \setofst {e∈\{0,\ldots,a\}} {c \eqL e} \\ \relax
% [d]_R &:=& \setofst {f∈\{0,\ldots,b\}} {d \eqL f} \\ \relax
[cd]_S &:=& \setofst {ef∈H} {cd \eqS ef} \\
&=& \setofst {ef∈H} {e∈[c]_L ∧ f∈[d]_R} \\
&=& \setofst {ef∈H} {ef∈[c]_L ×_\LR [d]_R} \\
&=& H∩([c]_L ×_\LR [d]_R) \\
\end{array}
$$
For example, in the ZHA at the right at the example above we have:
%
$$\begin{array}{rcl}
[1]_L &=& \{1,2,3,4\}, \\ \relax
[2]_R &=& \{0,1,2,3\}, \\ \relax
[12]_S &=& [10,43]∩H \; = \; \{11,12,13,22,23\}. \\
\end{array}
$$
%
for the equivalence classes, and note that
%
% (find-planarhas "zquotients")
% (find-planarhaspage 26 "ZQuotients")
% (find-planarhastext 26 "ZQuotients")
%
$$\begin{array}{lrcl}
\text{if} & [c]_L &=& \{c',\ldots,c''\} \\
\text{and} & [d]_L &=& \{d',\ldots,d''\} \\
\text{then} & [cd]_S &=& [c'd',c''d'']∩H; \\
\end{array}
$$
%
We say that a slashing $S$ on a ZHA $H$ partitions $H$ into {\sl
slash-regions}; later (sec.\ref{J-ops-and-regions}) we will see that
a J-operator $J$ also partitions $H$, and we will refer to its
equivalence classes as {\sl J-regions}.
Slash-regions are intervals, but note that neither 10 or 43 belong to
the slash-region $[12]_S = [10,43]∩H$ above.
\msk
When we
write $[b]_P = \{a,\ldots,c\}$ it is implicit that $a$ and $c$ are the
minimal and the maximal elements of $[b]_P$; note that
$\{a,\ldots,c\}$ is an ``interval'' in $\N$.
We write $×_\LR$ for the
product in $\LR$, and $[ab,ef]$ for
\msk
Let's define a notation for ``intervals'' in $\LR$,
%
%
Note that it can be adapted to define ``intervals'' in a ZHAs $H$:
%
$$\begin{array}{rcl}
[ab,ef]∩H & := & \setofst {\ang{c,d}∈\LR} {a≤c≤e \;\;\&\;\; b≤d≤f}∩H \\
& = & \setofst {\ang{c,d}∈H} {a≤c≤e \;\;\&\;\; b≤d≤f}. \\
\end{array}
$$
\msk
A {\sl slash-partition} is a partition on a ZHA induced by a slashing,
and a {\sl slash-equivalence} is an equivalence relation on a ZHA
induced by a slashing. Formally, a slash-partition on $H$ is a set of
subsets of $H$, and a slash-equivalence is subset of $H×H$, but it is
so easy to convert between partitions and equivalence relations that
we will often use both terms interchangeably. Our visual
representation for slash-partitions and slash-equivalences on a ZHA
$H$ will be the same: $H$ slashed by diagonal cuts.
% ____ _ _ _
% / ___|| | __ _ ___| |__ _ __ ___ __ _(_) ___ _ __ ___
% \___ \| |/ _` / __| '_ \ _____| '__/ _ \/ _` | |/ _ \| '_ \/ __|
% ___) | | (_| \__ \ | | |_____| | | __/ (_| | | (_) | | | \__ \
% |____/|_|\__,_|___/_| |_| |_| \___|\__, |_|\___/|_| |_|___/
% |___/
% «slash-regions» (to ".slash-regions")
\section{Slash-regions}
\label {slash-regions}
% (p2sp 99 "slash-regions")
% (p2s "slash-regions")
The equivalence classes of a slashing will be called {\sl
slash-regions}. Let $ab∈H$ and let
% ____ _ _ _
% / ___|| | __ _ ___| |__ _ __ __ _ _ __| |_
% \___ \| |/ _` / __| '_ \ _____| '_ \ / _` | '__| __|
% ___) | | (_| \__ \ | | |_____| |_) | (_| | | | |_
% |____/|_|\__,_|___/_| |_| | .__/ \__,_|_| \__|
% |_|
% «slash-partitions» (to ".slash-partitions")
\section{From slash-partitions back to slashings}
\label {slash-partitions}
% Good (ph2p 4 "slash-partitions")
We saw how to go from a slashing $S=(L,R)$ on $H$ to an equivalence
relation $\eqS$ on $H$; let's see now how to recover $L$ and $R$ from
$\eqS$.
% Let's see a way to recover the piccs $L$ and $R$ from an equivalence
% relation $\eqS$ on a ZHA $H$.
Let $LW_H$ be the left wall of $H$, and $RW_H$ the right wall of $H$.
For example,
%
%L -- mp = mpnew({def="foo"}, "1R2R3212RL1"):addlrs():output()
%L mp = mpnew({def="foo"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
$$\pu
H = \;\;\foo
\quad
\begin{array}[t]{r}
LW_H = \{00,01,11,12,22,23,24,34,35,45,46\} \\
RW_H = \{00,01,02,03,04,14,24,25,26,36,46\} \\
\end{array}
$$
To recover the picc $L$ --- which is a picc on $\{0,1,2,3,4\}$ --- we
need to find where we change from an $L$-equivalence class to another
when we go from one digit to the next; and to recover the picc $R$ ---
which is a picc on $\{0,1,2,3,4,5,6\}$ --- we need to find where we
change from an $R$-equivalence class to another when we go from one
digit to the next.
We can recover $L$ and $R$ by walking $LW_H$ (or $RW_H$) from bottom
to top in a series of white pawns moves, and checking when we change
from one $S$-equivalence class to another. Northwest moves give
information about $L$, and northeast moves give information about $R$.
Look at the example below, in which we walk on $RW_H$:
%
\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∖#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 }
%
%L mp = mpnew({def="foo"}, "1R2R3212RL1"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="LWH"}, "1RLRLRRLRLR"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
%L mp = mpnew({def="RWH"}, "1RRRRLLRRLL"):addlrs():addcuts("c 4321/0 0123|45|6"):output()
$$\pu
\begin{array}{c}
H = \;\;\foo
\qquad
LW_H = \;\;\LWH
\quad
RW_H = \!\!\!\!\!\!\!\!\RWH
%
\\ \\
%
\begin{array}{ll}
& \neno 25 26 \\
& \neyes 24 25 \\
\nwyes 36 46 & \neno 03 04 \\
\nwyes 26 36 & \neyes 02 03 \\
\nwyes 14 24 & \neyes 01 02 \\
\nwno 04 14 & \neyes 00 01 \\
\end{array}
%
\\ \\
%
% ⇒ \quad
(L,R) \;=\; (4321/0, 0123∖45∖6)
\end{array}
$$
% ____ _ _
% / ___|| | __ _ ___| |__ _ __ ___ __ ___ __
% \___ \| |/ _` / __| '_ \ _____| '_ ` _ \ / _` \ \/ /
% ___) | | (_| \__ \ | | |_____| | | | | | (_| |> <
% |____/|_|\__,_|___/_| |_| |_| |_| |_|\__,_/_/\_\
%
% «slash-max» (to ".slash-max")
\section{Slash-regions have maximal elements}
\label {slash-max}
% Good (ph2p 5 "slash-max")
...here is how our argument will work, in a particular case:
%
$$\begin{array}{rcl}
[1]_L &=& \{1,2,3,4\}, \\ \relax
[2]_R &=& \{0,1,2,3\}, \\ \relax
I &=& [10,43], \\ \relax
[12]_S &=& I∩H \; = \; \{11,12,13,22,23\}. \\
\end{array}
$$
$$\def\uoo#1#2{ \und{#1}{oo:#2} }
\def\uo #1#2{(\und{#1}{oo:#2})}
%
\def\uoo#1#2{ \und{#1}{\sm{=#2 ∈I}} }
\def\uo #1#2{(\uoo{#1}{#2})}
\uoo{\uo{\uo{\uo{11∨12}{12}∨13}{13}∨22}{23}∨23}{23}
\qquad
\def\uoo#1#2{ \und{#1}{\sm{=#2 ∈H}} }
\def\uo #1#2{(\uoo{#1}{#2})}
\uoo{\uo{\uo{\uo{11∨12}{12}∨13}{13}∨22}{23}∨23}{23}
$$
$$\bigvee [12]_S
= \bigvee \{11,12,13,22,23\}
= 11∨12∨13∨22∨23
∈ I∩H
$$
$$11 ≤ \bigvee [12]_S, \;
12 ≤ \bigvee [12]_S, \;
\ldots, \;
23 ≤ \bigvee [12]_S
$$
We have $[12]_S = I∩H$, and $\bigvee [12]_S$ belongs to $I∩H$ and is
greter-or-equal than all elements of $I∩H$, so $\bigvee [12]_S$ is the
maximal element of $[12]_S$.
\bsk
Here is how we can do that in the general case. Let $S=(L,R)$ be a
slashing on a ZHA $H$. Let $P$ be a point of $H$. The equivalence
class $[P]_S$ is a finite set $\{P_1, \ldots, P_n\}$, and we know that
$[P]_S=H∩I$ for some interval $I$. Look at the elements $P_1$,
$P_1∨P_2$, $(P_1∨P_2)∨P_3$, $\ldots$, $((P_1∨P_2)∨\ldots)∨P_n$ We can
see that all of them belong to both $H$ and $I$, so we conclude that
$\bigvee [P]_S = ((P_1∨P_2)∨\ldots)∨P_n$ belongs to $H∩I$, and it is
easy to see that it is greater-or-equal that all elements in $H∩I$, so
it is the maximal element of $H∩I$.
A similar argument shows that $\bigwedge [P]_S =
((P_1∧P_2)∧\ldots)∧P_n$ is the smallest element of $[P]_S$.
\msk
The same argument shows that if $C$ is any non-empty set of the form
$I∩H$, where $I$ is an interval, then $\bigvee C ∈ C$, $\bigwedge C ∈
C$, $[\bigwedge C, \bigvee C]∩H = C$.
Remember that an {\sl interval} in a ZHA $H$ is any set of the form
$[P,Q]∩H$. Let's introduce a new definition: a {\sl closed interval}
in a ZHA $H$ is a non-empty set $C⊂H$, with $⋁C∈C$, $⋀C∈C$, $[⋀C,
⋁C]∩H = C$; informally, a closed interval in a ZHA has a lowest and
highest element, and it ``is'' everything between them.
% ____ _ _ _
% / ___| _| |_ ___ ___| |_ ___ _ __ _ __ (_)_ __ __ _
% | | | | | | __/ __| / __| __/ _ \| '_ \| '_ \| | '_ \ / _` |
% | |__| |_| | |_\__ \ \__ \ || (_) | |_) | |_) | | | | | (_| |
% \____\__,_|\__|___/ |___/\__\___/| .__/| .__/|_|_| |_|\__, |
% |_| |_| |___/
%
% «cuts-stopping-midway» (to ".cuts-stopping-midway")
\section{Cuts stopping midway}
\label {cuts-stopping-midway}
% Good (ph2p 6 "cuts-stopping-midway")
We saw in the last section that every slash-region is a closed
interval. A {\sl partition into closed intervals} of a ZHA $H$ is, as
its name says, a partition of $H$ whose equivalence classes are all
closed intervals in $H$.
Some partitions into closed intervals of a ZHA are not slashings ---
for example, take the partition $P$ with these equivalence classes:
%
%L mp = mpnew({def="foo", meta="10pt"}, "1234LL321")
%L -- mp:addlrs():addcuts("c 01|23 10w-11n 32w-33n"):output()
%L mp:addlrs():addcuts("c 01|23 20w-21n 32w-33n"):output()
$$\pu
\foo
$$
Here is an easy way to prove formally that the partition above does
not come from a slashing $S=(L,R)$. We will adapt the idea from
sec.\ref{slash-partitions}, where we recovered $L$ and $R$ from
northwest and northeast steps.
%
\def\undtrue #1{\und{#1}{\text{true}}}
\def\undfalse#1{\und{#1}{\text{false}}}
\def\undfrown#1{\und{#1}{=(}}
\def\iff{\;\;↔\;\;}
\def\notiff{\;\not↔\;}
%
$$\begin{array}{rcl}
\undfalse{21 \eqP 31} \;\;↔\;\; \undfrown{2 \eqL 3} \;\;↔\;\; \undtrue {22 \eqP 32} \\
\undtrue {31 \eqP 41} \;\;↔\;\; \undfrown{3 \eqL 4} \;\;↔\;\; \undfalse{32 \eqP 42} \\
\end{array}
$$
The problem is that the figure above has ``cuts stopping midway''...
if its cuts all crossed the ZHA all the way through, we would have
this for $L$ and northeast cuts,
%
$$\begin{array}{c}
0\eqL1 \iff 00\eqP10 \iff 01\eqP11 \iff 02\eqP12 \iff 03\eqP13 \\
1\eqL2 \iff 10\eqP20 \iff 11\eqP21 \iff 12\eqP22 \iff 13\eqP23 \\
2\eqL3 \iff 20\eqP30 \iff 21\eqP31 \iff 22\eqP32 \iff 23\eqP33 \\
3\eqL4 \iff 30\eqP40 \iff 31\eqP41 \iff 32\eqP42 \iff 33\eqP43 \\
4\eqL5 \iff 40\eqP50 \iff 41\eqP51 \iff 42\eqP52 \iff 43\eqP53 \\
5\eqL6 \iff 50\eqP60 \iff 51\eqP61 \iff 52\eqP62 \iff 53\eqP63 \\
\end{array}
$$
%
and something similar for $R$ and northwest cuts.
\msk
Formally, a partition $P$ on $H$ has an ``L-cut between $c$ and $c^+$
stopping midway'' if $cd \eqP c^+d \notiff cd \eqP c^+d$ for some $d$,
and it has an ``R-cut between $d$ and $d^+$ stopping midway'' if $cd
\eqP cd^+ \notiff c^+d \eqP c^+d^+$ for some $c$; here we are writing
$x^+$ for $x+1$.
\msk
{\sl Theorem: a partition of $H$ into closed intervals is a
slash-partition if and only if it doesn't have any cuts stopping
midway.} Proof: use the ideas above to recover $L$ and $R$ from
$\eqP$, and then check that $S=(L,R)$ induces an equivalence relation
$\eqS$ that coincides with $\eqP$.
% ____ _ _
% / ___|| | __ _ ___| |__ ___ _ __ ___
% \___ \| |/ _` / __| '_ \ _____ / _ \| '_ \/ __|
% ___) | | (_| \__ \ | | |_____| (_) | |_) \__ \
% |____/|_|\__,_|___/_| |_| \___/| .__/|___/
% |_|
% «slash-ops» (to ".slash-ops")
\section{Slash-operators}
\label {slash-ops}
% Good (ph2p 7 "slash-ops")
We can define operations that take each each $P∈H$ to the maximal and
to the minimal element of its $S$-equivalent class, now that we know
that these maximal and minimal elements exist:
%
$$\begin{array}{rclll}
P^S &:=& \bigvee [P]_S && \text{(maximal element),} \\
P^{\co S} &:=& \bigwedge [P]_S && \text{(minimal element).}
\end{array}
$$
Note that $[P]_S = [P^{\co S}, P^S]∩H$.
We will use the operation $·^S$ a lot and $·^{\co S}$ very little. The
`$\co$' in `$\co S$' means that $·^{\co S}$ is dual to $·^S$, in a
sense that will be made precise later.
\msk
A {\sl slash-operator} on a ZHA $H$ is a function $·^S:H→H$ induced by
a slashing $S=(L,R)$ on $H$. It is easy to see that $P ≤ P^S$
(``\,$·^S$ is non-decreasing'') and that $P^S = (P^S)^S$ (``\,$·^S$ is
idempotent'').
\msk
Any idempotent function $·^F:H→H$ induces an equivalence relation on
$H$: $P \eqF Q$ iff $P^F = Q^F$. We can use that to test if a given
$·^F:H→H$ is a slash-operator: $·^F$ is a slash-operator iff it obeys
all this:
1) $·^F$ is idempotent,
2) $·^F$ is non-decreasing,
3) $\eqF$ partitions $H$ into closed intervals,
4) $\eqF$ doesn't have cuts stopping midway.
% ____ _ _ _
% / ___|| | __ _ ___| |__ _ __ _ __ ___ _ __ ___ _ __| |_ _ _
% \___ \| |/ _` / __| '_ \ | '_ \| '__/ _ \| '_ \ / _ \ '__| __| | | |
% ___) | | (_| \__ \ | | | | |_) | | | (_) | |_) | __/ | | |_| |_| |
% |____/|_|\__,_|___/_| |_| | .__/|_| \___/| .__/ \___|_| \__|\__, |
% |_| |_| |___/
%
% «slash-ops-property» (to ".slash-ops-property")
\section{Slash-operators: a property}
\label {slash-ops-property}
% Good (ph2p 8 "slash-ops-property")
Slash-operators obey a certain property that will be very important
later. Let's state that property in five equivalent ways:
1) If $cd \eqS c'd'$ and $ef \eqS e'f'$ then $cd∧ef \eqS c'd'∧e'f'$.
2) If $P \eqS P'$ and $Q \eqS Q'$ then $P∧Q \eqS P'∧Q'$.
3) If $P \eqS P'$ and $Q \eqS Q'$ then $(P∧Q)^S = (P'∧Q')^S$.
4) If $P \eqS P'$ and $Q \eqS Q'$ then
%
$$\begin{array}{rclll}
(P∧Q)^S &=& (P^S∧Q^S)^S && \text{(a)} \\
&=& ((P')^S∧(Q')^S)^S && \text{(b)} \\
&=& (P'∧Q')^S && \text{(c)} \\
\end{array}
$$
5) $(P∧Q)^S = (P^S∧Q^S)^S$.
\msk
\noindent Here's a proof of $1↔2↔3↔4↔5$.
$1↔2$: we just changed notation,
$2↔3$: because $A \eqS B$ iff $A^S = B^S$,
$3→5$: make the substitution $\subst{P':=P^S \\ Q':=Q^S}$ in 3,
$5→4$: 4a is just a copy of 5, and 4c is a copy of 5 with
$\subst{P:=P' \\ Q:=Q'}$. For 4b, note that $P \eqP P'$ implies $P^S =
(P')^S$ and $Q \eqP Q'$ implies $Q^S = (Q')^S$,
$4→3$: 4 is an equality between more expressions than 3,
\msk
\noindent ...and here is a way to visualize what is going on:
%
% (find-planarhas "J-figure")
% (find-planarhaspage 19 "How J-operators interact with the connectives: figure")
% (find-planarhastext 19 "How J-operators interact with the connectives: figure")
%
%L -- The (&*) cube
%L mp = mpnew({def="andcube", scale="12.5pt"}, "1234321"):addcuts("c 3/210 012|3"):addlrs():output()
%L mp = mpnew({def="andCube", scale="12.5pt"}, "1234321"):addcuts("c 3/210 012|3")
%L mp:put(v"30", "P"):put(v"31", "P'", "P'"):put(v"32", "P*", "P^S")
%L mp:put(v"03", "Q"):put(v"13", "Q'", "Q'"):put(v"23", "Q*", "Q^S")
%L mp:output()
%
$$\pu
\begin{array}{c}
\andcube
\qquad
\andCube
\\ \\
\und{( \und{ \und{P}{30} ∧ \und{Q}{03} }{00} )^S}{22} =
\und{( \und{ \und{\und{P }{30}{}^S}{32} ∧ \und{\und{Q }{03}{}^S}{23} }{22} )^S}{22} =
\und{( \und{ \und{\und{P'}{31}{}^S}{32} ∧ \und{\und{Q'}{13}{}^S}{23} }{22} )^S}{22} =
\und{( \und{ \und{P'}{31} ∧ \und{Q'}{13} }{11} )^S}{22}
\\
\end{array}
$$
%
Note that all subexpressions belong to three $S$-regions: a region
with $P$, $P'$, $P^S=P'{}^S$, another with $Q$, $Q'$, $Q^S=Q'{}^S$,
and one with all the `$∧$'s. If we had cuts stopping midway then some
of the `$∧$'s could be in different regions.
I think that the clearest way to show (1) is by putting its proof in
tree form:
%
%L addabbrevs("(~S)", "\\eqS ", "(~L)", "\\eqL ", "(~R)", "\\eqR ")
%:
%: cd(~S)c'd' ef(~S)e'f' cd(~S)c'd' ef(~S)e'f'
%: ---------- ---------- ---------- ----------
%: c(~L)c' e(~L)e' d(~R)d' f(~R)f'
%: ------------------------ ------------------------
%: \min(c,e)(~L)\min(c',e') \min(d,f)(~L)\min(d',f')
%: ----------------------------------------------------
%: \min(c,e)\min(d,f)(~S)\min(c',e')\min(d',f')
%: --------------------------------------------
%: cd∧ef(~S)c'd'∧e'f'
%:
%: ^foo
%:
$$\pu
\ded{foo}
$$
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-tla: "p2s"
% End: