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

\directlua{tf_push("2019J-ops-classifier.tex")}


% «.classifier»			(to "classifier")
% «.Omega-and-j»		(to "Omega-and-j")
% «.pullbacks-formally»		(to "pullbacks-formally")
%   «.NTs-B-1»			(to "NTs-B-1")
%   «.NTs-B-C»			(to "NTs-B-C")
%   «.NTs-1-Om»			(to "NTs-1-Om")
%   «.NTs-C-Om»			(to "NTs-C-Om")
%   «.NTs-Om-Om»		(to "NTs-Om-Om")
%   «.fig:five-sqconds»		(to "fig:five-sqconds")
% «.pullbacks-visually»		(to "pullbacks-visually")



%   ____ _               _  __ _           
%  / ___| | __ _ ___ ___(_)/ _(_) ___ _ __ 
% | |   | |/ _` / __/ __| | |_| |/ _ \ '__|
% | |___| | (_| \__ \__ \ |  _| |  __/ |   
%  \____|_|\__,_|___/___/_|_| |_|\___|_|   
%                                          
% «classifier»  (to ".classifier")
% (jonp 31 "classifier")
% (joo     "classifier")

\subsection{The classifier}

Take a map $t:1→C$ in a topos. Choose a map $g:B→C$ and form the
pullback with $t$, obtaining maps $f:A→B$ and $h:A→1$. We can prove
that any map from the terminal is monic, and this implies that $t$ is
monic, and so, by a property of pullbacks, $f$ is a monic too; and $h$
is the unique map from $A$ to the terminal. In a diagram:
%
%D diagram cla-0
%D 2Dx     100 +25  +40 +25  +40 +25
%D 2D  100     A1   B0  B1   C0  C1
%D 2D
%D 2D  +25 A2  A3   B2  B3   C2  C3
%D 2D
%D ren    A1 A2 A3 ==>   1 B C
%D ren B0 B1 B2 B3 ==> A 1 B C
%D ren C0 C1 C2 C3 ==> A 1 B C
%D
%D (( A1 A3 -> .plabel= r t
%D    A2 A3 -> .plabel= b g
%D
%D    # A1 B2 midpoint .TeX= ⇒ place
%D    A1 B2 harrownodes nil 20 nil =>
%D
%D    B0 B1 -> .plabel= a h
%D    B0 B2 -> .plabel= l f
%D    B1 B3 -> .plabel= r t
%D    B2 B3 -> .plabel= b g
%D    B0 relplace 7 7 \pbsymbol{7}
%D
%D    # B1 C2 midpoint .TeX= ⇒ place
%D    B1 C2 harrownodes nil 20 nil =>
%D
%D    C0 C1  -> .plabel= a !
%D    C0 C2 >-> .plabel= l f
%D    C1 C3 >-> .plabel= r t
%D    C2 C3  -> .plabel= b g
%D    C0 relplace 7 7 \pbsymbol{7}
%D ))
%D enddiagram
%D
$$\pu
  \diag{cla-0}
$$

We can consider that the operation ``form the pullback with
$t:1 \monicto C$'' receives a map $g: B→C$ and returns a monic $f:
A \monicto B$ ``completing the pullback''.

Every topos has a classifier object $Ω$ and a ``true'' map
$⊤:1 \monicto Ω$ with the property that for every monic $f: A \monicto
B$ there is a unique map $χ:B→Ω$ ``completing the pullback''. In a
diagram:
%
%D diagram cla-1
%D 2Dx     100 +25  +40 +25  +45 +25 +40 +25
%D 2D  100 A0  A1   B0  B1   C0  C1  D0  D1
%D 2D
%D 2D  +25 A2  A3   B2  B3   C2  C3  D2  D3
%D 2D
%D ren A0 A1 A2 A3 ==> A  1 B Ω
%D ren B0 B1 B2 B3 ==> A  1 B Ω
%D ren C0 C1 C2 C3 ==> A  1 B Ω
%D ren D0 D1 D2 D3 ==> A' 1 B Ω
%D
%D (( A0 A2 >-> .plabel= l f
%D    A1 A3 >-> .plabel= r ⊤
%D
%D    A1 B2 harrownodes nil 20 nil =>
%D
%D    B0 B1  -> .plabel= a !
%D    B0 B2 >-> .plabel= l f
%D    B1 B3 >-> .plabel= r ⊤
%D    B2 B3  -> .plabel= b χ
%D    B0 relplace 7 7 \pbsymbol{7}
%D
%D
%D    C1 C3 -> .plabel= r ⊤
%D    C2 C3 -> .plabel= b χ
%D
%D    C1 D2 harrownodes nil 20 nil =>
%D
%D    D0 D1  -> .plabel= a !
%D    D0 D2 >-> .plabel= l f'
%D    D1 D3 >-> .plabel= r ⊤
%D    D2 D3  -> .plabel= b χ
%D    D0 relplace 7 7 \pbsymbol{7}
%D ))
%D enddiagram
%D
$$\pu
  \diag{cla-1}
$$

These two operations, $f↦χ$ and $χ↦f'$, are not exactly inverse to one
another: if we apply them in the order $f↦χ↦f'$ we may obtain an $f'$
that is isomorphic to $f$ in the sense that there is an iso $A ↔ A'$
such that the triangle below commutes:
%
%D diagram cla-triangle
%D 2Dx     100 +15 +15
%D 2D  100 A       A'
%D 2D
%D 2D  +25     O
%D 2D
%D ren O ==> Ω
%D
%D (( A  O >-> .plabel= l f
%D    A' O >-> .plabel= r f'
%D    A A' <->
%D ))
%D enddiagram
%D
$$\pu
  \diag{cla-triangle}
$$

This is explained in \cite[p.139]{LambekScott}

% (find-lambekscottpage (+ 8 139)     "subobject clasifier")




%   ___                              _     _ 
%  / _ \ _ __ ___     __ _ _ __   __| |   (_)
% | | | | '_ ` _ \   / _` | '_ \ / _` |   | |
% | |_| | | | | | | | (_| | | | | (_| |   | |
%  \___/|_| |_| |_|  \__,_|_| |_|\__,_|  _/ |
%                                       |__/ 
%
% «Omega-and-j»  (to ".Omega-and-j")
% (jonp 31 "Omega-and-j")
% (joe     "Omega-and-j")

\subsection{The classifier and the local operator}

We know that every category $\Set^{(P,A)}$ is a topos, but how do we
calculate and visualize its classifier object $Ω$ and the map $⊤:1→Ω$?
And what is the local operator $j:Ω→Ω$ ``associated to'' our
J-operator $J:\Sub(1)→\Sub(1)$?

\msk

%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 \ovl{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

% TODO: Explain the prequisites for this section. Explain that I
% learned this from Bell but McLarty is more readable.
%
% (find-books "__cats/__cats.el" "mclarty")
% (find-books "__cats/__cats.el" "bell")

We need to start by understanding two pullbacks. Remember that:

\begin{itemize}

\item $⊤:1→Ω$ has a property can be expressed in two equivalent ways:
  1) for each object $C$ we have $\Sub(C) ≅ \Hom(C,Ω)$, and 2) for
  every monic $B \monicto C$ there is exactly one map $χ_B:C→Ω$ making
  the square below --- ``the Q-shaped diagram'' --- a pullback:
  %
  $$\diag{Omega-and-j}
  $$

\item a local operator (also called a
  ``modality'', a ``Lawvere-Tierney topology'', or a ``topology'') is
  a map $j:Ω→Ω$ obeying $j∘⊤=⊤$, $j∘j=j$ and $j∘∧=∧∘(j×j)$,

  % (find-books "__cats/__cats.el" "mclarty")
  % (find-mclartypage (+ 4 196) "21. Topologies")

\item a local operator $j$ induces a $j$-closure operator --- see
  chapter 21 of \cite{McLarty} or chapter 5 of \cite{BellLST} ---, and
  this $j$-closure operator can be seen as a map from each $\Sub(C)$
  to itself. The closure of a subobject $i: B \monicto C$ is the
  subobject $\ovl 1 : \ovl B \monicto C$ obtained by pullback in the
  diagram below (``the rectangle''):
  %
  $$\diag{Omega-and-j-2}
  $$

\end{itemize}

We will write the restriction of a local operator $j$ to $\Sub(1)$ as
$\sfJ(j)$ and we will say that a $j$ is ``associated to'' a $J$ when
$\sfJ(j) = J$.

\msk

There are two ways to ``understand'' the pullbacks above: the first
one is by doing the calculations formally and checking that everything
works, the second one is by checking some particular cases and
developing visual intuition from that.

% In the next sections I will refer to the two diagrams above as ``the
% Q-shaped diagram'' and ``the rectangle''.


\newpage

%  ____  ____         __                            _ _       
% |  _ \| __ ) ___   / _| ___  _ __ _ __ ___   __ _| | |_   _ 
% | |_) |  _ \/ __| | |_ / _ \| '__| '_ ` _ \ / _` | | | | | |
% |  __/| |_) \__ \ |  _| (_) | |  | | | | | | (_| | | | |_| |
% |_|   |____/|___/ |_|  \___/|_|  |_| |_| |_|\__,_|_|_|\__, |
%                                                       |___/ 
%
% «pullbacks-formally»  (to ".pullbacks-formally")
% (jonp 32 "pullbacks-formally")
% (joo     "pullbacks-formally")
\subsection{Understanding the pullbacks formally}
\label{pullbacks-formally}

The calculations are routine if we know the right language, and if we
suppose --- without loss of generality --- that the monix $i:B\monicto
C$ is a ``canonical subobject'' in the sense that each $B(p)⊆C(p)$ and
each function $B(p\ton!q):B(p)→B(q)$ is a restriction of the
corresponding function $C(p\ton!q):C(p)→C(q)$.

We need some definitions:
%
$$\begin{array}{rcl}
  1(p)          &=& \{*\} \\
  1(p\ton!q)(*) &=& * \\
  Ω(p)          &=& \Sub(↓p) \\
  Ω(p\ton!q)(R) &=& R∧↓q   \\%
  %
  [5pt]
  %
  ⊤(p)(*)       &=& ↓p     \\
  j(p)(R)       &=& R^*∧↓p \\
  χ_B(p)(R)     &=& \setofst{r∈↓p}{C(p\ton!r)(c)∈B(r)} \\
  \end{array}
$$

The first step is to check the five naturality conditions in the next
page --- we leave the rest to the reader. The main exercise is to
check that if the monic $i:B\monicto C$ is $i:P\monicto 1$ for a
truth-value $P$ then its closure is $i:\ovl P\monicto 1$ with $\ovl P$
being exactly $J(P)$, i.e., $P^*$.

\newpage

% «NTs-B-1»  (to ".NTs-B-1")
%
%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(p) B(q) \{*\} \{*\}
%D ren b rb *p1 *p2 *p3 ==> b B(p\ton!q)(b) * * *
%D
%D (( p q -> .plabel= l !
%D    Bp 1p -> .plabel= a !
%D    Bp Bq -> .plabel= l B(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
%
% «NTs-B-C»  (to ".NTs-B-C")
%
%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(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
%
% «NTs-1-Om»  (to ".NTs-1-Om")
%
%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
%
% «NTs-C-Om»  (to ".NTs-C-Om")
%
%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
%
% «NTs-Om-Om»  (to ".NTs-Om-Om")
%
%D diagram Om->Om
%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
%
% «fig:five-sqconds»  (to ".fig:five-sqconds")
% (jonp 34 "fig:five-sqconds")
% (joo     "fig:five-sqconds")
%
\pu
\begin{figure}[h!]
  \centering
  $\pu
   \scalebox{0.9}{$
   \begin{array}{l}
   \diag{B->1}   \\ \\
   \diag{B->C}   \\ \\
   \diag{1->Om}  \\ \\
   \diag{C->Om}  \\ \\
   \diag{Om->Om} \\
   \end{array}
   $}
  $
  \caption{The five square conditions in the Q-shaped diagram}
  \label{fig:five-sqconds}
\end{figure}


\newpage

%  ____  ____              _                 _ _       
% |  _ \| __ ) ___  __   _(_)___ _   _  __ _| | |_   _ 
% | |_) |  _ \/ __| \ \ / / / __| | | |/ _` | | | | | |
% |  __/| |_) \__ \  \ V /| \__ \ |_| | (_| | | | |_| |
% |_|   |____/|___/   \_/ |_|___/\__,_|\__,_|_|_|\__, |
%                                                |___/ 
%
% «pullbacks-visually»  (to ".pullbacks-visually")
% (jonp 35 "pullbacks-visually")
% (joo     "pullbacks-visually")
\subsection{Understanding the pullbacks visually}
\label{pullbacks-visually}

The best way to develop visual intuition about the $Ω$ and the $j$
associated to a $((P,A),Q)$ is to try to work out the details in some
particular cases --- I've chosen two, presented as execises below.
They both use the $((P,A),Q)$, the $Ω$ and the $j$ from
Figure \ref{fig:classifier-big}.

\msk

{\bf Exercise 1.} In the case
%
%D diagram Omega-and-j-exercise-1-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 B C ==> 11 33
%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-exercise-1-rect
%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 B C ==> \ovl{11} 33
%D ren Om1 Om2 ==> Ω Ω
%D
%D (( B 1  -> .plabel= a !
%D    B C >-> .plabel= l \ovl{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-exercise-1-Q}
\qquad
\diag{Omega-and-j-exercise-1-rect}
$$
%
what is $χ_B$? And what is $\ovl{11}$?

\msk

{\bf Exercise 2.} In the case
%
%D diagram Omega-and-j-exercise-2-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 B C ==> 11 23
%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-exercise-2-rect
%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 B C ==> \ovl{11} 23
%D ren Om1 Om2 ==> Ω Ω
%D
%D (( B 1  -> .plabel= a !
%D    B C >-> .plabel= l \ovl{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-exercise-2-Q}
\qquad
\diag{Omega-and-j-exercise-2-rect}
$$

%
what is $χ_B$? And what is $\ovl{11}$?




% (elep 6 "elephant-A2.1.3")
% (ele    "elephant-A2.1.3")

% (elep 7 "elephant-A4.1.4")
% (ele    "elephant-A4.1.4")
% (elep 8 "elephant-A4.1.5")
% (ele    "elephant-A4.1.5")

% (ph1p 25 "topologies-as-partial-orders")
% (ph1     "topologies-as-partial-orders")


\directlua{tf_pop()}



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