% 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}&#2&#3&#4& &\text{#5}&#6&#7&#8& \\}
\def\li#1 #2 #3 #4                {\text{#1}&#2&#3&#4& }
\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}&#2&#3&#4& &\text{#5}&#6&#7&#8& \\}
% \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:
