|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% This file: (find-LATEX "2019J-ops-algebra.tex")
% See: (find-LATEX "2020J-ops-new.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019J-ops-algebra.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019J-ops-algebra.pdf"))
% (defun e () (interactive) (find-LATEX "2019J-ops-algebra.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019J-ops-algebra"))
% (find-pdf-page "~/LATEX/2019J-ops-algebra.pdf")
% (find-sh0 "cp -v ~/LATEX/2019J-ops-algebra.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2019J-ops-algebra.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2019J-ops-algebra.pdf
% file:///tmp/2019J-ops-algebra.pdf
% file:///tmp/pen/2019J-ops-algebra.pdf
% http://angg.twu.net/LATEX/2019J-ops-algebra.pdf
% (find-LATEX "2019.mk")
% «.polynomial-J-ops» (to "polynomial-J-ops")
% «.algebra-of-piccs» (to "algebra-of-piccs")
% «.algebra-of-J-ops» (to "algebra-of-J-ops")
% «.slashings-are-poly» (to "slashings-are-poly")
% (find-LATEX "2017planar-has-2.tex" "polynomial-J-ops")
\directlua{tf_push("2019J-ops-algebra.tex")}
% ____ _ _
% | _ \ ___ | |_ _ | | ___ _ __ ___
% | |_) / _ \| | | | | _ | |_____ / _ \| '_ \/ __|
% | __/ (_) | | |_| | | |_| |_____| (_) | |_) \__ \
% |_| \___/|_|\__, | \___/ \___/| .__/|___/
% |___/ |_|
%
% «polynomial-J-ops» (to ".polynomial-J-ops")
% (jonp 19 "polynomial-J-ops")
% (joa "polynomial-J-ops")
\section{Polynomial J-operators}
\label {polynomial-J-ops}
% (ph2p 29 "polynomial-J-ops")
% (ph2 "polynomial-J-ops")
% (phop 22)
% (pho "J-examples")
% (find-books "__cats/__cats.el" "fourman")
% (find-slnm0753page (+ 14 331) "polynomial")
\def\Jnotnot{{(¬¬)}}
\def\JiiR {{({→→}R)}}
\def\JoQ {{(∨Q)}}
\def\JiR {{({→}R)}}
\def\JfoQR {{(∨Q∧{→}R)}}
\def\JmiQ {({→→}Q∧{→}Q)}
{
It is not hard to check that for any Heyting Algebra $H$ and any
$Q,R∈H$ the operations $\Jnotnot$, $\ldots$, $\JfoQR$ below are
J-operators:
%
%$$\begin{array}{rclcrcl}
% (¬¬) &:=& λP{:}H.¬¬P && (¬¬)(P) &=& ¬¬P \\
% \JiiR &:=& λP{:}H.((P{→}R){→}R) && \JiiR(P) &=& (P{→}R){→}R \\
% \JoQ &:=& λP{:}H.(P{∨}Q) && \JoQ(P) &=& P∨Q \\
% \JiR &:=& λP{:}H.(P{→}R) && \JiR(P) &=& P{→}R\\
% \JfoQR &:=& λP{:}H.((P{∨}Q) ∧ (P{→}R)) && \JfoQR(P) &=& (P{∨}Q)∧(P{→}R) \\
% \end{array}
%$$
%
$$\begin{array}{rclcrcl}
(¬¬)(P) &=& ¬¬P \\
\JiiR(P) &=& (P{→}R){→}R \\
\JoQ(P) &=& P∨Q \\
\JiR(P) &=& P{→}R\\
\JfoQR(P) &=& (P{∨}Q)∧(P{→}R) \\
\end{array}
$$
Checking that they are J-operators means checking that each of them
obeys $\J1$, $\J2$, $\J3$. Let's define formally what are $\J1$, $\J2$
and $\J3$ ``for a given $F:H→H$'':
%
$$\begin{array}{rcc}
\J1_F &:=& (P ≤ F(P)) \\
\J2_F &:=& (F(P) = F(F(P)) \\
\J3_F &:=& (F(P∧P') = F(P)∧F(P')) \\
\end{array}
$$
%
and:
%
$$\J123_F \quad := \quad \J1_F ∧ \J2_F ∧ \J3_F.$$
% (ph1p 18 "logic-in-HAs")
% (ph1 "logic-in-HAs")
Checking that $\Jnotnot$ obeys $\J1$, $\J2$, $\J3$ means proving
$\J123_\Jnotnot$ using only the rules from intuitionist logic from
section 10 of \cite{OchsPH1}; we will leave the proof of this, of and
$\J123_\JiiR$, $\J123_\JoQ$, and so on, to the reader.
\msk
The J-operator $\JfoQR$ is a particular case of building more complex
J-operators from simpler ones. If $J,K: H→H$, we define:
%
$$(J∧K) := λP{:}H.(J(P){∧}K(P))$$
%
it not hard to prove $\J123_{(J∧K)}$ from $\J123_J$ and $\J123_K$
using only the rules from intuitionistic logic.
\msk
The J-operators above are the first examples of J-operators in Fourman
and Scott's ``Sheaves and Logic'' (\cite{Fourman}); they appear in
pages 329--331, but with these names (our notation for them is at the
right):
(i) {\sl The closed quotient,}
$$J_a p = a ∨ p \qquad J_Q = \JoQ.$$
(ii) {\sl The open quotient,}
$$J^a p = a→p \qquad J^R = \JiR.$$
(iii) {\sl The Boolean quotient}.
$$B_a p = (p→a)→a \qquad B_R = \JiiR.$$
(iv) {\sl The forcing quotient}.
$$(J_a∧J^b)p = (a∨p)∧(b→p) \qquad (J_Q∧J^R) = \JfoQR.$$
(vi) {\sl A mixed quotient.}
$$(B_a∧J^a)p = (p→a)→p \qquad (B_Q∧J^Q) = \JmiQ.$$
\msk
The last one is tricky. From the definition of $B_a$ and $J^a$ what we
have is
%
$$(B_a∧J^a)p = ((p→a)→a)∧(a→p),$$
%
but it is possible to prove
%
$$((p→a)→a)∧(a→p) \;\;↔\;\; ((p→a)→p)$$
%
intuitionistically.
The operators above are ``polynomials on $P,Q,R,→,∧,∨,⊥$'' in the
terminology of Fourman/Scott: ``If we take a polynomial in $→,∧,∨,⊥$,
say, $f(p,a,b,\ldots)$, it is a decidable question whether for all
$a,b,\ldots$ it defines a J-operator'' (p.331).
\msk
When I started studying sheaves I spent several years without any
visual intuition about the J-operators above. I was saved by ZHAs and
brute force --- and the brute force method also helps in testing if a
polynomial (in the sense above) is a J-operator in a particular case.
For example, take the operators $λP{:}H.(P∧22)$ and $({∨}22)$ on
$H=[00,44]$:
%
% (phop 23)
% (pho "J-ops-diagrams")
% (pho "J-ops-diagrams" "jout")
% (find-dn6 "zhas.lua" "shortoperators-tests")
% (find-dn6file "zhas.lua" "mpnewJ =")
%
%L shortoperators()
%L mpnewF = function (opts, spec, J)
%L return mpnew(opts, spec, J):setz():zhaJ()
%L end
%L
%L mpnewF({def="fooa"}, "123454321", function (P) return And(v"22", P) end):output()
%L mpnewF({def="fooo"}, "123454321", Cloq(v"22")):output()
%L mpnewJ({def="fooO"}, "123454321", Cloq(v"22")):zhaPs("22"):output()
%
$$\pu
\begin{array}{rcccl}
λP{:}H.(P∧22) &=& \fooa \\ \\
({∨}22) &=& \fooo &=& \fooO \\
\end{array}
$$
The first one, $λP{:}H.(P∧22)$, is not a J-operator; one easy way to
see that is to look at the region in which the result is 22 --- its
top element is 44, and this violates the conditions on slash-operators
in sec.\ref{slash-ops}. The second operator, $({∨}22)$, is a slash
operator and a J-operator; at the right we introduce a convenient
notation for visualizing the action of a polynomial slash-operator, in
which we draw only the contours of the equivalence classes and the
constants that appear in the polynomial.
Using this new notation, we have:
%
%L mpnewJ({def="fooboo", scale="7pt", meta="s"}, "123R2L1", Booq(v"00")):zhaPs("00"):output()
%L mpnewJ({def="foobii", scale="7pt", meta="s"}, "123R2L1", Booq(v"11")):zhaPs("11"):output()
%L
%L mpnewJ({def="fooboo", scale="7pt", meta="s"}, "123454321", Booq(v"00")):zhaPs("00"):output()
%L mpnewJ({def="foobii", scale="7pt", meta="s"}, "123454321", Booq(v"22")):zhaPs("22"):output()
%L mpnewJ({def="foobor", scale="7pt", meta="s"}, "1234567654321", Cloq(v"42")):zhaPs("42"):output()
%L mpnewJ({def="foobim", scale="7pt", meta="s"}, "1234567654321", Opnq(v"24")):zhaPs("24"):output()
%L mpnewJ({def="foofor", scale="7pt", meta="s"}, "1234567654321", Forq(v"42", v"24")):zhaPs("42 24"):output()
%L mpnewJ({def="foomix", scale="7pt", meta="s"}, "12345654321", Mixq(v"22")):zhaPs("22"):output()
%
\pu
$$
\begin{array}{c}
(¬¬) \;\;=\;\;
({→→}00) \;\;=\;\; \fooboo \qquad \qquad
({→→}22) \;\;=\;\; \foobii \\
\\
({∨}42) \;\;=\;\; \foobor \qquad
({→}24) \;\;=\;\; \foobim \\[-20pt]
\\
({∨}42∧{→}24) \;\;=\;\; \foofor \\
\qquad \qquad
\qquad \qquad
\qquad \qquad
({→→}22∧{→}22) \;\;=\;\; \foomix \\
\end{array}
$$
Note that the slashing for $({∨}42∧{→}24)$ has all the cuts for
$({∨}42)$ plus all the cuts for $({→}24)$, and $({∨}42∧{→}24)$
``forces $42≤24$'' in the following sense: if $P^* = ({∨}42∧{→}24)(P)$
then $42^*≤24^*$.
}
% _ _ _
% _ __ (_) ___ ___ ___ __ _| | __ _ ___| |__ _ __ __ _
% | '_ \| |/ __/ __/ __| / _` | |/ _` |/ _ \ '_ \| '__/ _` |
% | |_) | | (_| (__\__ \ | (_| | | (_| | __/ |_) | | | (_| |
% | .__/|_|\___\___|___/ \__,_|_|\__, |\___|_.__/|_| \__,_|
% |_| |___/
%
% «algebra-of-piccs» (to ".algebra-of-piccs")
% (jonp 21 "algebra-of-piccs")
% (joa "algebra-of-piccs")
\subsection{An algebra of piccs}
\label {algebra-of-piccs}
We saw in the last section a case in which $(J∧K)$ has all the cuts
from $J$ plus all the cuts from $K$; this suggests that we {\sl may}
have an operation dual to that, that behaves as this: $(J∨K)$ has
exactly the cuts that are both in $J$ and in $K$:
%
$$\begin{array}{rcl}
\Cuts(J∧K) &=& \Cuts(J)∪\Cuts(K) \\
\Cuts(J∨K) &=& \Cuts(J)∩\Cuts(K) \\
\end{array}
$$
And it $J_1, \ldots, J_n$ are all the slash-operators on a given ZHA,
then
%
$$\begin{array}{rclcl}
\Cuts(J_1∧\ldots∧J_n) &=& \Cuts(J_1)∪\ldots∪\Cuts(J_k) &=& \text{(all cuts)} \\
\Cuts(J_1∨\ldots∨J_n) &=& \Cuts(J_1)∩\ldots∩\Cuts(J_k) &=& \text{(no cuts)} \\
\end{array}
$$
%
yield the minimal element and the maximal element, respectively, of an
algebra of slash-operators; note that the slash-operator with ``all
cuts'' is the identity map $λP{:H}.P$, and the slash-operator with
``no cuts'' is the one that takes all elements to $⊤$: $λP{:H}.⊤$.
This yields a lattice of slash-operators, in which the partial order
is $J≤K$ iff $\Cuts(J) ⊇ \Cuts(K)$. This is somewhat counterintuitive
if we think in terms of cuts --- the order seems to be reversed ---
but it makes a lot of sense if we think in terms of piccs
(sec.\ref{piccs-and-slashings}) instead.
\msk
Each picc $P$ on $\{0,\ldots,n\}$ has an associated function $·^P$
that takes each element to the top element of its equivalence class.
If we define $P≤P'$ to mean $∀a∈\{0,\ldots,n\}.\,a^P≤a^{P'}$, then we
have this:
%
% (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
%
$$\pu
\begin{array}{ccccccc}
\grapha &≤& \graphb &≤& \graphc &≤& \graphd \\ \\
0|1|2|3|4|5 &≤& 01|23|45 &≤& 01|2345 &≤& 012345 \\
P &≤& P' &≤& P'' &≤& P''' \\
\end{array}
$$
This yields a partial order on piccs, whose bottom element is the
identity function $0|1|2|\ldots|n$, and the top element is $012\ldots
n$, that takes all elements to $n$.
The piccs on $\{0,\ldots,n\}$ form a Heyting Algebra, where
$⊤=01\ldots n$, $⊥=0|1|\ldots|n$, and `$∧$' and `$∨$' are the
operations that we have discussed above; it is possible to define a
`$→$' there, but this `$→$' is not going to be useful for us and we
are mentioning it just as a curiosity. We have, for example:
%
%D diagram algebra-of-piccs
%D 2Dx 100 +20 +20 +30 +20 +20
%D 2D 100 01234 T
%D 2D ^ ^
%D 2D | |
%D 2D +20 01|234 PvQ
%D 2D ^ ^ ^ ^
%D 2D / \ / \
%D 2D +20 0|1|234 01|2|34 P Q
%D 2D ^ ^ ^ ^
%D 2D \ / \ /
%D 2D +20 0|1|2|34 P&Q
%D 2D ^ ^
%D 2D | |
%D 2D +20 0|1|2|3|4 bot
%D 2D
%D (( T .tex= ⊤ PvQ .tex= P∨Q P&Q .tex= P∧Q bot .tex= ⊥
%D 01234 01|234 <- T PvQ <-
%D 01|234 0|1|234 <- 01|234 01|2|34 <- PvQ P <- PvQ Q <-
%D 0|1|234 0|1|2|34 <- 01|2|34 0|1|2|34 <- P P&Q <- Q P&Q <-
%D 0|1|2|34 0|1|2|3|4 <- P&Q bot <-
%D
%D ))
%D enddiagram
%D
$$\pu \diag{algebra-of-piccs}$$
% _ _ _
% | | ___ _ __ ___ __ _| | __ _ ___| |__ _ __ __ _
% _ | |_____ / _ \| '_ \/ __| / _` | |/ _` |/ _ \ '_ \| '__/ _` |
% | |_| |_____| (_) | |_) \__ \ | (_| | | (_| | __/ |_) | | | (_| |
% \___/ \___/| .__/|___/ \__,_|_|\__, |\___|_.__/|_| \__,_|
% |_| |___/
%
% «algebra-of-J-ops» (to ".algebra-of-J-ops")
% (jonp 22 "algebra-of-J-ops")
% (joa "algebra-of-J-ops")
\subsection{An algebra of J-operators}
\label {algebra-of-J-ops}
% Bad (ph2p 50 "algebra-of-J-ops")
% (find-books "__cats/__cats.el" "fourman")
Fourman and Scott define the operations $∧$ and $∨$ on J-operators in
pages 325 and 329 (\cite{Fourman}), and in page 331 they list ten
properties of the algebra of J-operators:
%
$$
\def\li#1 #2 #3 #4 #5 #6 #7 #8 {\text{#1}& &\text{#5}& \\}
\def\li#1 #2 #3 #4 {\text{#1}& }
\begin{array}{rlclcrlclc}
\li (i) J_a∨J_b = J_{a∨b} && (∨21)∨(∨12)=(∨22) \\
\li (ii) J^a∨J^b = J^{a∧b} && ({→}32)∨({→}23)=({→}22) \\
\li (iii) J_a∧J_b = J_{a∧b} && (∨21)∧(∨12)=(∨11) \\
\li (iv) J^a∧J^b = J^{a∨b} && ({→}32)∧({→}23)=({→}33) \\
\li (v) J_a∧J^a = ⊥ && (∨22)∧({→}22)=(⊥) \\
\li (vi) J_a∨J^a = ⊤ && (∨22)∨({→}22)=(⊤) \\
\li (vii) J_a∨K = K∘J_a \\
\li (viii) J^a∨K = J^a∘K \\
\li (ix) J_a∨B_a = B_a \\
\li (x) J^a∨B_b = B_{a→b} \\
\end{array}
$$
% (pho "J-ops-algebra-2")
% (phop 28 "J-ops-algebra-2")
The first six are easy to visualize; we won't treat the four last
ones. In the right column of the table above we've put a particular
case of (i), $\ldots$, (vi) in our notation, and the figures below put
all together.
In Fourman and Scott's notation,
%D diagram J-alg-1
%D 2Dx 100 +20 +20 +10 +10 +20 +20
%D 2D 100 T
%D 2D +30 A E
%D 2D +20 B C F G
%D 2D +20 D H
%D 2D +30 bot
%D 2D
%D ren T ==> J_⊤=⊤=J^⊥
%D ren A E ==> J_{22} J^{22}
%D ren B C F G ==> J_{21} J_{12} J^{32} J^{23}
%D ren D H ==> J_{11} J^{11}
%D ren bot ==> J_⊥=⊥=J^⊤
%D
%D (( A T -> E T ->
%D B A -> C A -> F E -> G E ->
%D D B -> D C -> H F -> H G ->
%D bot D -> bot H ->
%D ))
%D enddiagram
%D
$$\pu
\diag{J-alg-1}
$$
%
in our notation,
%
%D diagram J-alg-2
%D 2Dx 100 +20 +20 +10 +10 +20 +20
%D 2D 100 T
%D 2D +30 A E
%D 2D +20 B C F G
%D 2D +20 D H
%D 2D +30 bot
%D 2D
%D 2Dx 100 +20 +20 +15 +15 +20 +20
%D 2D 100 T
%D 2D +35 A E
%D 2D +20 B C F G
%D 2D +20 D H
%D 2D +35 bot
%D 2D
%D ren T ==> (⊤∨)=(λP.⊤)=(⊥{→})
%D ren A E ==> (22∨) (22{→})
%D ren B C F G ==> (21∨) (12∨) (32{→}) (23{→})
%D ren D H ==> (11∨) (33{→})
%D ren bot ==> (⊥∨)=(λP.P)=(⊤{→})
%D
%D (( A T -> E T ->
%D B A -> C A -> F E -> G E ->
%D D B -> D C -> H F -> H G ->
%D bot D -> bot H ->
%D ))
%D enddiagram
%D
$$\pu
\diag{J-alg-2}
$$
%
and drawing the polynomial J-operators as in
sec.\ref{polynomial-J-ops}:
%
%L deforp = function (P, draw, name)
%L PP(P, name)
%L mpnewJ({def=name, scale="4.5pt", meta="t"}, "123454321", Cloq(v(P))):zhaPs(draw):print():output()
%L end
%L defimp = function (P, draw, name)
%L PP(P, name)
%L mpnewJ({def=name, scale="4.5pt", meta="t"}, "123454321", Opnq(v(P))):zhaPs(draw):print():output()
%L end
%L deforp("21", "21", "ora")
%L deforp("22", "22", "orb")
%L deforp("11", "11", "orc")
%L deforp("12", "12", "ord")
%L deforp("00", "", "orB")
%L defimp("32", "32", "ima")
%L defimp("22", "22", "imb")
%L defimp("33", "33", "imc")
%L defimp("34", "34", "imd")
%L defimp("00", "", "imB")
%
%R local algebra =
%R 4/ !imB \
%R | |
%R | !orb !imb |
%R |!ora !ord !ima !imd|
%R | !orc !imc |
%R | |
%R \ !orB /
%R
%R algebra:tomp({def="foo", scale="30pt"}):addcells():output()
$$\pu
% \bhbox{$
\begin{array}{c}
\\
\foo \\
\\
\end{array}
% $}
$$
% $$
% \def\li#1 #2 #3 #4 #5 #6 #7 #8 {\text{#1}& &\text{#5}& \\}
% \begin{array}{rlclcrlclc}
% \li (i) J_a∨J_b = J_{a∨b} (ii) J^a∨J^b = J^{a∧b}
% \li (iii) J_a∧J_b = J_{a∧b} (iv) J^a∧J^b = J^{a∨b}
% \li (v) J_a∧J^a = ⊥ (vi) J_a∨J^a = ⊤
% \li (vii) J_a∨K = K∘J_a (viii) J^a∨K = J^a∘K
% \li (ix) J_a∨B_a = B_a (x) J^a∨B_b = B_{a→b}
% \end{array}
% $$
%
% $$\begin{array}{rclcrcl}
% (¬¬) &:=& λP:H.¬¬P && (¬¬)(P) &=& ¬¬P \\
% (→→R) &:=& λP:H.((P{→}R){→}R) && (→→R)(P) &=& (P{→}R){→}R \\
% (∨Q) &:=& λP:H.(P{∨}Q) && (∨Q)(P) &=& P∨Q \\
% (→R) &:=& λP:H.(P{→}R) && (→R)(P) &=& P{→}R\\
% (∨Q∧→R) &:=& λP:H.((P{∨}Q) ∧ (P{→}R)) && (∨Q∧→R)(P) &=& (P{∨}Q)∧(P{→}R) \\
% \end{array}
% $$
% ____ _ _ _
% / ___|| | __ _ ___| |__ _ __ ___ | |_ _
% \___ \| |/ _` / __| '_ \ | '_ \ / _ \| | | | |
% ___) | | (_| \__ \ | | | | |_) | (_) | | |_| |
% |____/|_|\__,_|___/_| |_| | .__/ \___/|_|\__, |
% |_| |___/
% «slashings-are-poly» (to ".slashings-are-poly")
% (jonp 24 "slashings-are-poly")
% (joa "slashings-are-poly")
\subsection{All slash-operators are polynomial}
\label {slashings-are-poly}
% (ph2p 51 "slashings-are-poly")
% (find-xpdfpage "~/LATEX/2015planar-has.pdf" 30)
% (find-LATEX "2015planar-has.tex" "zquotients-poly")
{
%L local ba, bb, bc = Booq(v"04"), Booq(v"23"), Booq(v"45")
%L local babc = Jand(ba, Jand(bb, bc))
%L mpnewJ({def="slaT", scale="7pt", meta="s"}, "1R2R3212RL1", babc ):addlrs() :output():print()
%L mpnewJ({def="slaA", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"04")):addlrs() :output():print()
%L mpnewJ({def="slaB", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"23")):addlrs() :output():print()
%L mpnewJ({def="slaC", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"45")):addlrs() :output():print()
%L mpnewJ({def="fooa", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"04")):zhaPs("04") :output():print()
%L mpnewJ({def="foob", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"23")):zhaPs("23") :output():print()
%L mpnewJ({def="fooc", scale="7pt", meta="s"}, "1R2R3212RL1", Booq(v"45")):zhaPs("45") :output():print()
%L mpnewJ({def="food", scale="7pt", meta="s"}, "1R2R3212RL1", babc ):zhaPs("04 23 45"):output():print()
%L mpnew ({def="fooe", scale="7pt", meta="s"}, "1R2R3212RL1" ):addlrs():output()
%L mpnewJ({def="foof", scale="7pt", meta="s"}, "1R2R3212RL1", babc):zhaJ() :output()
\pu
Here is an easy way to see that all slashings --- i.e., J-operators on
ZHAs --- are polynomial. Every slashing $J$ has only a finite number of
cuts; call them $J_1, \ldots, J_n$. For example:
%
$$J=\slaT \qquad J_1=\slaA \quad J_2=\slaB \quad J_3=\slaC$$
Each cut $J_i$ divides the ZHA into an upper region and a lower
region, and $J_i(00)$ yields the top element of the lower region.
Also, $({→→}J_i(00))$ is a polynomial way of expressing that cut:
%
$$\def\foo#1#2{
\begin{array}{rr}
J_#1= \\
% ({→→}J_#1(00))= \\
(→→#2)= \\
\end{array}}
\foo1{04} \fooa \quad
\foo2{23} \foob \quad
\foo3{45} \fooc
$$
The conjunction of these `$({→→}J_i(00))$'s yields the original
slashing:
%
% $$
% \begin{array}{c}
% \fooa ∧ \foob ∧ \fooc = \food
% \end{array}
% $$
%
$$(→→04)∧(→→23)∧(→→45) = \food = J$$
}
\directlua{tf_pop()}
% Local Variables:
% coding: utf-8-unix
% ee-tla: "joa"
% End: