% (find-LATEX "2019classifier.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2019classifier.tex" :end))
% (defun d () (interactive) (find-pdf-page "~/LATEX/2019classifier.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2019classifier.pdf"))
% (defun e () (interactive) (find-LATEX "2019classifier.tex"))
% (defun u () (interactive) (find-latex-upload-links "2019classifier"))
% (find-pdf-page   "~/LATEX/2019classifier.pdf")
% (find-sh0 "cp -v  ~/LATEX/2019classifier.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2019classifier.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2019classifier.pdf
%               file:///tmp/2019classifier.pdf
%           file:///tmp/pen/2019classifier.pdf
% http://angg.twu.net/LATEX/2019classifier.pdf
% (find-LATEX "2019.mk")
%
% (find-TH "math-b" "2020-classifier")

% «.title»		(to "title")
% «.introduction»	(to "introduction")
% «.make»		(to "make")

\documentclass[oneside]{article}
\usepackage[colorlinks,urlcolor=DarkRed,citecolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\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")
\input 2017planar-has-defs.tex    % (find-LATEX "2017planar-has-defs.tex")
%
\usepackage[backend=biber,
   style=alphabetic]{biblatex} % (find-es "tex" "biber")
\addbibresource{catsem-u.bib}  % (find-LATEX "catsem-u.bib")
%
% (find-es "tex" "geometry")
\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

\def\dnto{{\downarrow}}
\def\ovl{\overline}




%  _____ _ _   _      
% |_   _(_) |_| | ___ 
%   | | | | __| |/ _ \
%   | | | | |_| |  __/
%   |_| |_|\__|_|\___|
%                     
% «title»  (to ".title")

\title{Notes about classifiers and local operators in a
  $\Set^{(P,A)}$}

\author{Eduardo Ochs}

\maketitle

%     _    _         _                  _   
%    / \  | |__  ___| |_ _ __ __ _  ___| |_ 
%   / _ \ | '_ \/ __| __| '__/ _` |/ __| __|
%  / ___ \| |_) \__ \ |_| | | (_| | (__| |_ 
% /_/   \_\_.__/|___/\__|_|  \__,_|\___|\__|
%                                           
% «abstract» (to ".abstract")
% (cl9p 1 "abstract")
% (cl9    "abstract")

\begin{abstract}

The last section of the paper \cite{OchsPH2} shows, quite briefly, how
to translate slashings on Planar Heyting Algebras to local operators
on toposes, but it omits some details and calculations and says that
they are ``routine''. These notes are an attempt to fill those gaps.

\end{abstract}




%  ___       _                 _            _   _             
% |_ _|_ __ | |_ _ __ ___   __| |_   _  ___| |_(_) ___  _ __  
%  | || '_ \| __| '__/ _ \ / _` | | | |/ __| __| |/ _ \| '_ \ 
%  | || | | | |_| | | (_) | (_| | |_| | (__| |_| | (_) | | | |
% |___|_| |_|\__|_|  \___/ \__,_|\__,_|\___|\__|_|\___/|_| |_|
%                                                             
% «introduction»  (to ".introduction")
% (cl9p 1  "introduction")
% (cl9     "introduction")
% (jopp 25 "the-right-classifier")
% (joe     "the-right-classifier")

\bsk
\bsk

{\bf Warning:} this is currently 1) a mess 2) a work in progress!

\bsk

If $F$ and $G$ are functors from $\catA$ to $\Set$ and $T:F→G$ then we
can draw the two internal views of the square condition of $T$ as:
%
%D diagram sqcond-1
%D 2Dx     100 +30   +30  +30    +45
%D 2D  100 B   FB -> GB   x |--> rx
%D 2D      |   |     |    -      -
%D 2D      |   |     |    |      v
%D 2D  +22 v   v     v    v      drx
%D 2D  +8  C   FC -> GC   dx |-> rdx
%D 2D
%D 2D  +20     F --> G
%D 2D
%D ren rx drx ==> (TB)(x) (Gv∘TB)(x)
%D ren dx rdx ==> (Fv)(x) (TC∘Fv)(x)
%D
%D (( B C -> .plabel= l v
%D    F G -> .plabel= a T
%D
%D    FB GB -> .plabel= a TB
%D    FB FC -> .plabel= l Fv
%D    GB GC -> .plabel= r Gv
%D    FC GC -> .plabel= a TC
%D
%D    x rx |-> rx drx |->
%D    x dx |-> dx rdx |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{sqcond-1}
$$

Formally, this is: $∀(v:B→C). \, ∀x∈FB. \, (Gv∘TB)(x) = (TC∘Fv)(x)$.

\bsk

In Section 7 of \cite{OchsPH2} I used these two diagrams to discuss
$Ω$ and $j$,
%
%D diagram Omega-and-j
%D 2Dx     100   +30     +30
%D 2D  100 B --> 1
%D 2D      |     |
%D 2D      v     v
%D 2D  +30 C --> Om1 --> Om2
%D 2D
%D ren Om1 Om2 ==> Ω Ω
%D
%D (( B 1  -> .plabel= a !
%D    B C >-> .plabel= l i
%D    1 Om1 >-> .plabel= r ⊤
%D    C Om1 -> .plabel= a χ_B
%D    Om1 Om2 -> .plabel= a j
%D    B relplace 7 7 \pbsymbol{7}
%D ))
%D enddiagram
%D
%D diagram Omega-and-j-2
%D 2Dx     100   +30     +30
%D 2D  100 B ----------> 1
%D 2D      |             |
%D 2D      v             v
%D 2D  +30 C --> Om1 --> Om2
%D 2D
%D ren Om1 Om2 B ==> Ω Ω \ovl{B}
%D
%D (( B 1  -> .plabel= a !
%D    B C >-> .plabel= l i
%D    1 Om2 >-> .plabel= r ⊤
%D    C Om1 -> .plabel= a χ_B
%D    Om1 Om2 -> .plabel= a j
%D    B relplace 7 7 \pbsymbol{7}
%D ))
%D enddiagram
%D
\pu
$$\diag{Omega-and-j}
  \qquad
  \diag{Omega-and-j-2}
$$
%
and I defined the objects $1$ and $Ω$ by:
%
$$\begin{array}{rcl}
        1(p) &=& \{*\}    \\
  1(p\ton!q) &=& λ*.*     \\
        Ω(p) &=& \Sub(↓p) \\
  Ω(p\ton!q) &=& λR{:}\Sub(↓p).R∧↓q  \\
  \end{array}
$$
%
Let's suppose that $B \monicto C$ is a canonical subobject, i.e., we
have $∀p∈P.B(p)⊆C(p)$ and every map $B(p\ton!q)$ is a restriction of
the corresponding map $C(p\ton!q)$. This means that:
%
%D diagram B->C-inj
%D 2Dx     100 +30     +40  +35     +55
%D 2D  100 p   Bp ---> Cp   b |---> cb 
%D 2D      |   |       |    -        -  
%D 2D      |   |       |    |        |  
%D 2D      |   |       |    |        v  
%D 2D  +25 v   v       v    v       rcb
%D 2D   +8 q   Bq ---> Cq   rb |--> crb
%D 2D
%D 2D  +20     B ----> C
%D 2D
%D ren Bp Bq Cp Cq ==> B(p) B(q) C(p) C(q)
%D ren b cb rcb rb crb ==> b b C(p\ton!q)(b) B(p\ton!q)(b) B(p\ton!q)(b)
%D
%D (( p q -> .plabel= l !
%D    Bp Cp `-> .plabel= a ip
%D    Bp Bq  -> .plabel= l B(p\ton!q)
%D    Cp Cq  -> .plabel= r C(p\ton!q)
%D    Bq Cq `-> .plabel= a iq
%D    B C   `-> .plabel= a i
%D
%D    b  cb |->  cb rcb |->
%D    b  rb |->  rb crb |->
%D ))
%D enddiagram
%
$$\pu
  \diag{B->C-inj}
$$





$$\begin{array}{rcl}
  \end{array}
$$



% (jopp 25 "the-right-classifier")
% (joe     "the-right-classifier")






\newpage

% (nyop 12 "first-yoneda-bijection-4")
% (nyo     "first-yoneda-bijection-4")
% (nyo     "yoneda-bij")

%D diagram B->1
%D 2Dx     100 +30     +40  +35     +45 
%D 2D  100 p   Bp ---> 1p   b |---> *p1 
%D 2D      |   |       |    -        -  
%D 2D      |   |       |    |        |  
%D 2D      |   |       |    |        v  
%D 2D  +25 v   v       v    v       *p2
%D 2D   +8 q   Bq --> 1q    rb |--> *p3
%D 2D
%D 2D  +20     B ----> 1
%D 2D
%D ren Bp Bq 1p 1q ==> B_0(p) B_0(q) \{*\} \{*\}
%D ren b rb *p1 *p2 *p3 ==> b B_1(p\ton!q)(b) * * *
%D
%D (( p q -> .plabel= l !
%D    Bp 1p -> .plabel= a !
%D    Bp Bq -> .plabel= l B_1(p\ton!q)
%D    1p 1q -> .plabel= r !
%D    Bq 1q -> .plabel= a !
%D    B 1 ->
%D
%D    b *p1 |-> *p1 *p2 |->
%D    b  rb |->  rb *p3 |->
%D ))
%D enddiagram

$\pu
 \diag{B->1}
$

\bsk
\bsk 

%D diagram B->C
%D 2Dx     100 +30     +40  +35     +55
%D 2D  100 p   Bp ---> Cp   b |---> cb 
%D 2D      |   |       |    -        -  
%D 2D      |   |       |    |        |  
%D 2D      |   |       |    |        v  
%D 2D  +25 v   v       v    v       rcb
%D 2D   +8 q   Bq ---> Cq   rb |--> crb
%D 2D
%D 2D  +20     B ----> C
%D 2D
%D ren Bp Bq Cp Cq ==> B_0(p) B_0(q) C_0(p) C_0(q)
%D ren b cb rcb rb crb ==> b b C_1(p\ton!q)(b) B_1(p\ton!q)(b) B_1(p\ton!q)(b)
%D
%D (( p q -> .plabel= l !
%D    Bp Cp `-> .plabel= a ip
%D    Bp Bq  -> .plabel= l B_1(p\ton!q)
%D    Cp Cq  -> .plabel= r C_1(p\ton!q)
%D    Bq Cq `-> .plabel= a iq
%D    B C   `-> .plabel= a i
%D
%D    b  cb |->  cb rcb |->
%D    b  rb |->  rb crb |->
%D ))
%D enddiagram

$\pu
 \diag{B->C}
$

\bsk
\bsk 

%D diagram 1->Om
%D 2Dx     100 +30     +40  +35     +45 
%D 2D  100 p   1p ---> Omp  * |---> t* 
%D 2D      |   |       |    -       -  
%D 2D      |   |       |    |       |  
%D 2D      |   |       |    |       v  
%D 2D  +25 v   v       v    v       rt*
%D 2D   +8 q   1q --> Omq   r* |--> tr*
%D 2D
%D 2D  +20     1 ----> Om
%D 2D
%D ren 1p 1q Omp Omq ==> \{*\} \{*\} \Sub(↓p) \Sub(↓q)
%D ren * t* rt* r* tr* ==> * ↓p ↓p∧↓q * ↓q
%D ren Om ==> Ω
%D
%D (( p   q   -> .plabel= l !
%D    1p  Omp -> .plabel= a ⊤p
%D    1p  1q  -> .plabel= l !
%D    Omp Omq -> .plabel= r !
%D    1q  Omq -> .plabel= a ⊤q
%D    1   Om  -> .plabel= a ⊤
%D
%D    * t* |-> t* rt* |->
%D    * r* |-> r* tr* |->
%D ))
%D enddiagram

$\pu
 \diag{1->Om}
$

\bsk
\bsk 

%D diagram C->Om
%D 2Dx     100 +30     +40   +45     +95 
%D 2D  100 p   Cp ---> Omp   c |---> chic
%D 2D      |   |         |   -        -  
%D 2D      |   |         |   |        |  
%D 2D      |   |         |   |        v  
%D 2D  +25 v   v         v   v       rchic
%D 2D   +8 q   Cq ---> Omq   rc |--> chirc
%D 2D
%D 2D  +20     C ----> Om
%D 2D
%D ren Cp Omp ==> C(p) \Sub(↓p)
%D ren Cq Omq ==> C(q) \Sub(↓q)
%D ren C  Om  ==> C Ω
%D
%D ren c   chic ==> c              \setofst{r∈↓p}{C(p\ton!r)(c)∈B(r)}
%D ren    rchic ==>                \setofst{r∈↓p}{C(p\ton!r)(c)∈B(r)}∧↓q
%D ren rc chirc ==> C(p\ton!q)(c)  \setofst{s∈↓q}{C(q\ton!s)(C(p\ton!q)(c))∈B(s)}
%D
%D (( p q -> .plabel= l !
%D    Cp Omp  -> .plabel= a χ_B(p)
%D    Cp Cq   -> .plabel= l C(p\ton!q)
%D    Omp Omq -> .plabel= r Ω(p\ton!q)
%D    Cq  Omq -> .plabel= a χ_B(q)
%D    C   Om  -> .plabel= a χ_B
%D
%D    c chic |-> chic rchic |->
%D    c rc   |->   rc chirc |->
%D ))
%D enddiagram

$\pu
 \diag{C->Om}
$

\bsk
\bsk 

%D diagram classifier-j
%D 2Dx     100 +30     +40   +35     +45 
%D 2D  100 p   Sp1 --> Sp2   R |---> jR 
%D 2D      |   |         |   -        -  
%D 2D      |   |         |   |        |  
%D 2D      |   |         |   |        v  
%D 2D  +25 v   v         v   v       rjR
%D 2D   +8 q   Sq1 --> Sq2   rR |--> jrR
%D 2D
%D 2D  +20     Om1 --> Om2
%D 2D
%D ren Sp1 Sp2 ==> \Sub(↓p) \Sub(↓p)
%D ren Sq1 Sq2 ==> \Sub(↓q) \Sub(↓q)
%D ren Om1 Om2 ==> Ω Ω
%D ren R jR rjR ==> R R^*∧↓p (R^*∧↓p)∧↓q
%D ren   rR jrR ==>     R∧↓q (R∧↓q)^*∧↓q
%D
%D (( p q -> .plabel= l !
%D    Sp1 Sp2 -> .plabel= a j(p)
%D    Sp1 Sq1 -> .plabel= l Ω(p\ton!q)
%D    Sp2 Sq2 -> .plabel= r Ω(p\ton!q)
%D    Sq1 Sq2 -> .plabel= a j(q)
%D    Om1 Om2 -> .plabel= a j
%D
%D    R jR |-> jR rjR |->
%D    R rR |-> rR jrR |->
%D ))
%D enddiagram

$\pu
 \diag{classifier-j}
$


\newpage

\section{Garbage?}

$Ω(p) = \Sub(↓p)$

$Ω(p\ton!q) = λR{:}\Sub(↓p).(R∧↓q)$

\bsk

We need to understand these five morphisms in $\Set^{(P,A)}$.

Each one of them is a natural transformation.

The object $1∈\Set^{(P,A)}$ is $1_0(p) = \{*\}$, $1_1(p\ton!q) = λ{*}.{*}$.

The object $Ω∈\Set^{(P,A)}$ is $Ω_0(p) = ↓p$, $Ω_1(p\ton!q) = λr{:}↓p.r∧↓q$.

\msk

$B\ton!1$ is trivial: $(B\ton!1)(p) = λb{:}B_0(p).*$.

\msk

$B \diagxyto/^{ (}->/^{i} C$ is an inclusion:

for every $p∈P$ we have $B_0(p)⊆C_0(p)$, and

for every $p\ton!q$ the map $(B \diagxyto/^{ (}->/^{i} C)(p\ton!q)$ is
a restriction of $C_1(p\ton!q)$.

\msk

$1 \diagxyto/{ >}->/^{⊤} Ω$ is $λp{:}P.λ{*}{:}1(p).↓p$.

\msk

$C \diagxyto/->/^{χ_B} Ω$ is $λp{:}P.λc{:}C(p).???$.


% (find-sh "locate calvin")




%D diagram Q
%D 2Dx     100   +30     +30
%D 2D  100 B --> 1
%D 2D      |     |
%D 2D      v     v
%D 2D  +30 C --> Om1 --> Om2
%D 2D
%D ren Om1 Om2 ==> Ω Ω
%D
%D (( B 1  -> .plabel= a !
%D    B C `-> .plabel= l i
%D    1 Om1 >-> .plabel= r ⊤
%D    C Om1 -> .plabel= a χ_B
%D    Om1 Om2 -> .plabel= a j
%D ))
%D enddiagram
%D
$$\pu
  \diag{Q}
$$




\printbibliography




\end{document}

%  __  __       _        
% |  \/  | __ _| | _____ 
% | |\/| |/ _` | |/ / _ \
% | |  | | (_| |   <  __/
% |_|  |_|\__,_|_|\_\___|
%                        
% «make»  (to ".make")

 (eepitch-shell)
 (eepitch-kill)
 (eepitch-shell)
# (find-LATEXfile "2017planar-has-1.mk")
make -f 2017planar-has-1.mk STEM=2019classifier veryclean
make -f 2017planar-has-1.mk STEM=2019classifier pdf
# (cl9p)
# (jopp 25)



% Local Variables:
% coding: utf-8-unix
% ee-tla: "cla"
% End:

