% (find-LATEX "2020clops-and-tops-garbage.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020clops-and-tops-garbage.tex" :end))
% (defun C () (interactive) (find-LATEXSH "lualatex 2020clops-and-tops-garbage.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page      "~/LATEX/2020clops-and-tops-garbage.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020clops-and-tops-garbage.pdf"))
% (defun e () (interactive) (find-LATEX "2020clops-and-tops-garbage.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020clops-and-tops-garbage"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun d0 () (interactive) (find-ebuffer "2020clops-and-tops-garbage.pdf"))
%          (code-eec-LATEX "2020clops-and-tops-garbage")
% (find-pdf-page   "~/LATEX/2020clops-and-tops-garbage.pdf")
% (find-sh0 "cp -v  ~/LATEX/2020clops-and-tops-garbage.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2020clops-and-tops-garbage.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2020clops-and-tops-garbage.pdf
%               file:///tmp/2020clops-and-tops-garbage.pdf
%           file:///tmp/pen/2020clops-and-tops-garbage.pdf
% http://angg.twu.net/LATEX/2020clops-and-tops-garbage.pdf
% (find-LATEX "2019.mk")

% «.defs»	(to "defs")
%
% «.SetCs-and-SetDs»		(to "SetCs-and-SetDs")
%   «.SetD-yoneda»		(to "SetD-yoneda")
%
% «.J-ops»			(to "J-ops")
%   «.clop-to-Jop»		(to "clop-to-Jop")
%   «.Jop-to-top»		(to "Jop-to-top")
%     «.Jop-to-top-defs»	  (to "Jop-to-top-defs")
%     «.def-j»			  (to "def-j")
%     «.def-j-NT»		  (to "def-j-NT")
%     «.def-j-obeys-J1-J2-J3»	  (to "def-j-obeys-J1-J2-J3")
%%     «.def-j-example»		  (to "def-j-example")
%%   «.clop-Jop-bij»		(to "clop-Jop-bij")
%   «.SetD-dense-closed»	(to "SetD-dense-closed")
%   «.SetD-sheaves»		(to "SetD-sheaves")
%   «.SetD-closure»		(to "SetD-closure")
%   «.topological-lemmas»	(to "topological-lemmas")

\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=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-slides.bib}        % (find-LATEX "catsem-slides.bib")
%
% (find-es "tex" "geometry")
\begin{document}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

% %L -- (find-dn6 "output.lua" "Deletecomments-class")
% %L deletecomments = function (bigstr) return DeleteComments.from(bigstr) end
% %L dofile "edrxtikz.lua"  -- (find-LATEX "edrxtikz.lua")
% %L dofile "edrxpict.lua"  -- (find-LATEX "edrxpict.lua")
% \pu



%L forths["<-'"] = function () pusharrow("<-^{) }") end

%L kite  = ".1.|2.3|.4.|.5."
%L mp = MixedPicture.new({def="dagKite", meta="s", scale="6pt"}, z):zfunction(kite):output()
%L -- mp = MixedPicture.new({def="dagKite", meta="s", scale="10pt"}, z):zfunction(kite):output()
%L -- mp = MixedPicture.new({def="dagKote", meta="s", scale="10pt"}, z):zfunction(kite):output()
\pu

% «defs»  (to ".defs")

\def\Incs     {\mathsf{Incs}}
\def\inc      {\mathsf{inc}}
\def\CanSub   {\mathsf{CanSub}}
\def\SubPoints{\mathsf{SubPoints}}
\def\Subsets  {\mathsf{Subsets}}
\def\Can      {\mathsf{Can}}
\def\can      {\mathsf{can}}
\def\Eq       {\mathsf{Eq}}
\def\eq       {\mathsf{eq}}
\def\Futs     {\mathsf{Futures}}
\def\Innerpts {\mathsf{Innerpoints}}
\def\Logic    {\mathsf{Logic}}
\def\Po       {\mathsf{Po}}
\def\Ob       {\mathsf{Ob}}
\def\catH     {\mathbf{H}}
\def\catK     {\mathbf{K}}
\def\catT     {\mathbf{T}}
\def\catW     {\mathbf{W}}
\def\Clo      {\textsc{Cl}}
\def\univ     {\text{univ}}
\def\pcdot    {(·)}
\def\opcdot   {\ovl{(·)}}
\def\clop     {\ovl{(·)}}
\def\SetC     {\Set^\catC}
\def\SetD     {\Set^\catD}
\def\SetH     {\Set^\catH}
\def\SetK     {\Set^\catK}
\def\SetT     {\Set^\catT}
\def\calW     {\mathcal{W}}
\def\chizi    {χ_{01}}
\def\chizim   {χ_{01m}}
\def\toM      {\ton{\text{M}}}
\def\ph       {\phantom}

\def\Jcan  {{J_\mathrm{can}}}
\def\hasmax{\mathsf{hasmax}}
\def\trans {\mathsf{trans}}
\def\stab  {\mathsf{stab}}

\def\Above   {\mathop{\textsf{above}}}
\def\Covers  {\mathop{\textsf{covers}}}
\def\JCovers {\mathop{\textsf{$J$-covers}}}
\def\RCovers {\mathop{\textsf{r-covers}}}
\def\RJCovers{\mathop{\textsf{r-$J$-covers}}}

\def\Downs    {\mathsf{D}}
\def\Cst      {\mathsf{CST}}

\def\sa#1#2{\expandafter\def\csname myarg#1\endcsname{#2}}
\def\ga#1{\csname myarg#1\endcsname}

\def\rotl#1{\rotatebox{90}{$#1$}}

\def\eqP{\sim_P}
\def\eqJ{\sim_J}
\def\eqL{\sim_L}
\def\eqR{\sim_R}
\def\eqS{\sim_S}

\def\TODO{(TODO)}

% «theorem»  (to ".theorem")
% (find-es "tex" "newtheorem")
% (find-es "tex" "newcounter")
%
\newtheorem{thmsection}      {My Theorem}[section]
\newtheorem{thmsubsection}   {My Theorem}[subsection]
\newtheorem{thmsubsubsection}{My Theorem}[subsubsection]
\def\stepThm#1{\refstepcounter{#1}\csname the#1\endcsname}
\def\Theoremsection         {{\bf Theorem \stepThm{thmsection}. }}
\def\Theoremsubsection      {{\bf Theorem \stepThm{thmsubsection}. }}
\def\Theoremsubsubsection   {{\bf Theorem \stepThm{thmsubsubsection}. }}
\def\Lemmasection           {{\bf Lemma   \stepThm{thmsection}. }}
\def\Lemmasubsection        {{\bf Lemma   \stepThm{thmsubsection}. }}
\def\Lemmasubsubsection     {{\bf Lemma   \stepThm{thmsubsubsection}. }}
\def\Conjecturesection      {{\bf Conjecture   \stepThm{thmsection}. }}
\def\Conjecturesubsection   {{\bf Conjecture   \stepThm{thmsubsection}. }}
\def\Conjecturesubsubsection{{\bf Conjecture   \stepThm{thmsubsubsection}. }}
\def\Examplesection         {{\bf Example \stepThm{thmsection}. }}
\def\Examplesubsection      {{\bf Example \stepThm{thmsubsection}. }}
\def\Examplesubsubsection   {{\bf Example \stepThm{thmsubsubsection}. }}

% \newcounter{Counts}[section]
% \newcounter{Countss}[subsection]
% \newcounter{Countsss}[subsubsection]
% \def\stepCount#1{\refstepcounter{#1}\csname the#1\endcsname}
% \def\Theoremsection      {{\bf Theorem \stepThm{Counts}.}}
% \def\Theoremsubsection   {{\bf Theorem \stepThm{Countss}.}}
% \def\Theoremsubsubsection{{\bf Theorem \stepThm{Countsss}.}}









\newpage

% ----------------------------------------
% ----------------------------------------
% ----------------------------------------
% ----------------------------------------
% ----------------------------------------
%   ____            _                        
%  / ___| __ _ _ __| |__   __ _  __ _  ___ _ 
% | |  _ / _` | '__| '_ \ / _` |/ _` |/ _ (_)
% | |_| | (_| | |  | |_) | (_| | (_| |  __/_ 
%  \____|\__,_|_|  |_.__/ \__,_|\__, |\___(_)
%                               |___/        



%  ____       _    ____                       _   ____       _   ____      
% / ___|  ___| |_ / ___|___    __ _ _ __   __| | / ___|  ___| |_|  _ \ ___ 
% \___ \ / _ \ __| |   / __|  / _` | '_ \ / _` | \___ \ / _ \ __| | | / __|
%  ___) |  __/ |_| |___\__ \ | (_| | | | | (_| |  ___) |  __/ |_| |_| \__ \
% |____/ \___|\__|\____|___/  \__,_|_| |_|\__,_| |____/ \___|\__|____/|___/
%                                                                          
% «SetCs-and-SetDs»  (to ".SetCs-and-SetDs")
% (clgp 30 "SetCs-and-SetDs")
% (clga    "SetCs-and-SetDs")
\section{Toposes of the form $\SetC$ and $\SetD$}
\label{SetCs-and-SetDs}

From here onwards we will reserve the symbol $\catC$ for small
categories and $\catD$ for ``DAG categories'', that we define as
follows: a category $\catD$ is a {\sl DAG category} iff there is a
{\sl finite} DAG $(P,A)$ such that $\catD$ is the transitive-reflexive
closure $(P,A^*)$ of $(P,A)$, regarded as a category.

We are especially interested in two kinds of DAG categories:

% (ph1p 5 "positional" "1.")
% (ph1    "positional")
%
%R local K, W, H = 1/ 1 \, 1/1 2 3\, 1/ 1 \
%R                  |2 3|   \ 4 5 /   |2 3|
%R                  | 4 |             \4 5/  
%R                  \ 5 /               
%R H:tomp({zdef="H",  scale="20pt", meta=nil}):addcells():addarrows():output()
%R K:tomp({zdef="K",  scale="20pt", meta=nil}):addcells():addarrows():output()
%R W:tomp({zdef="W",  scale="20pt", meta=nil}):addcells():addarrows():output()

% (jonp 27 "classifier-big-figure")
% (joe     "classifier-big-figure")
%
%L myspec = "1232RL1"
%L tdims_mini  = TCGDims {h=32,  v=25,  q=15, crh=8,  crv=7, qrh=5}
%L tdims_big   = TCGDims {h=110, v=110,       crh=30, crv=45}
%L tspec_mini = TCGSpec.new("33; 32, 13", "?.?", "??.")
%L tspec_mini = TCGSpec.new("33; 32, 13")
%L tspec_big  = TCGSpec.new("33; 32, 13")
%L tcg_T   = TCGQ.newdsoa(tdims_mini,  tspec_mini, {tdef="T",   meta="1pt"}, "h v lr")
%L tcg_T  :output()
%L
%L tspec_mini = TCGSpec.new("33; 32, 13")
%L tdims_micro = TCGDims {h=15,  v=8,  q=15, crh=3.5,  crv=7, qrh=5}
%L tcg_Tbu = TCGQ.newdsoa(tdims_micro, tspec_mini, {tdef="Tbu", meta="1pt"}, "h b")
%L tcg_Tbu:output()
%L
%L mpnew({zdef="T"}, myspec):addlrs():print():output()
\pu

\begin{enumerate}

\item The ones coming from the ZDAGs of \cite{PH1}, sections 1--2,
  with their objects labeled in the ``reading order'', as the
  categories $\catH$ (``house''), $\catK$ (``kite''), and $\catW$
  below:
%
$$\pu
  \catH = \!\!\!\zha{H}
  \qquad
  \catK = \!\!\!\zha{K}
  \qquad
  \catW = \!\!\!\zha{W}
$$

\item ``2-column graphs'', like the one below:
%
$$\catT = \;\; \tcg{T}
$$
%
They will be discussed in the next section.

\end{enumerate}

%L tspec_mini  = TCGSpec.new("33; 32, 13")
%L tdims_micro = TCGDims {h=15,  v=8,  q=15, crh=3.5,  crv=7, qrh=5}
%L tcg_Tbu = TCGQ.newdsoa(tdims_micro, tspec_mini, {tdef="Tbu", meta="1pt"}, "h b")
%L tcg_Tbu:output()
\pu

The paper \cite{PH1} defines a language in which certain diagrams have
precise meanings as mathematical objects, but these meanings depends
on the context, and new meanings can be added. This bullet diagram
%
$$\dagKite•••••$$
%
can be interpreted as a subset of $\Z^2$ (section 1) and as a DAG with
arrows going downward (section 2); a diagram with `0's and `1's like
%
$$\dagKite00111$$
%
can be interpreted as:

\begin{enumerate}

\item a function, a characteristic function, or a subset (section 1),

\item a set or an open set in an arbitrary topology (section 11),

\item a stable subset (section 12),

\item an open set in the default topology (section 12),

\item an open set of an order topology (section 12),

\item a point in a certain partial order (section 13),

\item a point in a certain planar Heyting Algebra (in a ``ZHA'';
  sections 4, 13, 16)

\end{enumerate}

Here we will add some new meanings to these lists. When we say 
%
$$\catK = \dagKite••••• \qquad \text{or} \qquad \catT = \tcg{Tbu}
$$
%
these will be shorter versions of the definitions of the DAG
categories $\catK$ and $\catT$ in the beginning of the section, and
this
%
$$\dagKite00111 \ito \dagKite11111
$$
%
will be an inclusion in the category $\SetK$, that we can expand as:
%
%D diagram sub-K-left
%D 2Dx     100 +20 +20
%D 2D  100     A0
%D 2D        /    \
%D 2D  +20 A1      A2
%D 2D        \    /
%D 2D  +20     A3
%D 2D          |
%D 2D  +20     A4
%D 2D
%D ren A0 A1 A2 A3 A4 ==> ∅ ∅ \{*\} \{*\} \{*\}
%D
%D (( A0 A1 ->
%D    A0 A2 ->
%D    A1 A3 ->
%D    A2 A3 ->
%D    A3 A4 ->
%D ))
%D enddiagram
%D
%D diagram sub-K-right
%D 2Dx     100 +20 +20
%D 2D  100     A0
%D 2D        /    \
%D 2D  +20 A1      A2
%D 2D        \    /
%D 2D  +20     A3
%D 2D          |
%D 2D  +20     A4
%D 2D
%D ren A0 A1 A2 A3 A4 ==> \{*\} \{*\} \{*\} \{*\} \{*\}
%D
%D (( A0 A1 ->
%D    A0 A2 ->
%D    A1 A3 ->
%D    A2 A3 ->
%D    A3 A4 ->
%D ))
%D enddiagram
%D
%D diagram sub-K-inclusion
%D 2Dx     100  +85
%D 2D  100 A0 - A1
%D 2D  
%D 2D  +50 B0 - B1
%D 2D
%D ren B0 B1 ==> D E
%D
%D (( A0 .tex= \left(\diag{sub-K-left}\right) BOX
%D    A1 .tex= \left(\diag{sub-K-right}\right) BOX
%D    A0 A1 `->
%D  # B0 B1 `-> .plabel= a T
%D ))
%D enddiagram
%D
$$\pu
  \diag{sub-K-inclusion}
$$

% (ph1p 25 "topologies-on-ZSets" "12.")
% (ph1     "topologies-on-ZSets")
% (ph1p 29 "topologies-on-2CGs" "15.")
% (ph1     "topologies-on-2CGs")

Suppose that $A = \dagKite01000$ is an object of $\SetK$. This $A$ has
an arrow from a 1 to 0: the image of the morphism $2→4$ in $K$ by $A$
is a morphism from $\{*\}$ to $∅$ in $\Set$, but $\Hom(\{*\},∅)$ is
empty, so this is absurd. A diagram like $\dagKite01000$, ``with an
arrow $1→0$'', denotes a non-stable subset of a ZSet in \cite[section
  12]{PH1}, and a non-open subset in \cite[section 15]{PH1}; here
it will denote something that is not an object of the DAG category
that we are dealing with.


\newpage



% __   __                   _       
% \ \ / /__  _ __   ___  __| | __ _ 
%  \ V / _ \| '_ \ / _ \/ _` |/ _` |
%   | | (_) | | | |  __/ (_| | (_| |
%   |_|\___/|_| |_|\___|\__,_|\__,_|
%                                   
% «SetD-yoneda»  (to ".SetD-yoneda")
% (clgp 32 "SetD-yoneda")
% (clga    "SetD-yoneda")
\subsection{The classifier in a $\Set^\catD$ (via Yoneda)}
\label{SetD-yoneda}

% (find-maclanemoerdijkpage (+ 11 36) "For an arbitrary small category C,")

Most texts about basic topos theory define the classifier of a $\SetC$
directly, as we did in sections \ref{SetD-classifier}--\ref{SetD-chi}:
they define an object $Ω$ whose action on objects takes each $B∈\catC$
to the set of subfunctors of $\Hom(B,-)$ and whose action on morphisms
is the ``obvious'' one, and then they show that this $Ω$ obeys the
properties that we expect from the classifier.

The book \cite{MacLaneMoerdijk} does that but it also shows, in its
pages 36--39, that we can use Yoneda to prove that
$ΩB≅\Sub(\Hom(B,-))$. I struggled a lot to understand their proof, but
I found that when I specialize it to `$\SetD$'s it becomes easy to
visualize. Let me show how.

\msk

Let $(P,A)$ be a 2-column graph, let $\catD$ be $(P,A)$ regarded as a
category, and let $\catE$ be the topos $\SetD$. Let $Ω$ be any
classifier object in $\catE$. This $Ω$ is a functor from $\catD$ to
$\Set$, and:

\ssk

\Theoremsubsection The action on objects of $Ω$ takes each $B∈\catD$
to a set isomorphic to ${↓}{↓}B$.

\msk

% (favp 35 "yoneda-lemma")
% (fav     "yoneda-lemma")
% (favp 40 "representable-functors")
% (fav     "representable-functors")

The proof needs the two diagrams below. The one on the left is the
``standard Yoneda Lemma'': it is the diagram $\mathsf{Y}1$ of
\cite[section 7.2]{FavC} with its functor $R:\catB→\Set$ replaced by
$Ω:\catD→\Set$. The diagram on the right is the ``Yoneda Lemma for
representable functors'' --- the second diagram from \cite[section
  7.6]{FavC} with its representable functor $R:\catB→\Set$ replaced by
$\Incs: (\Set^\catD)^\op → \Set$; its universal arrow is $\nameof{⊤}$,
that selects the element $(⊤:1 \monicto Ω) ∈ \Incs(Ω)$.
%
% (mmop 3 "Omega-in-presheaf")
% (mmo    "Omega-in-presheaf")
%
%D diagram Omega-in-a-SetD
%D 2Dx     100  +50  +50  +55
%D 2D  100      A1        D1
%D 2D            |         |
%D 2D  +20 A2 - A3   D2 - D3
%D 2D      |     |   |     |
%D 2D  +20 A4 - A5   D4 - D5
%D 2D                    
%D 2D  +20 B0 - B1   E0 - E1
%D 2D                    
%D 2D  +15 C0 - C1   F0 - F1
%D 2D         \  |      \  |
%D 2D  +20      C2        F2
%D 2D
%D ren A1 A2 A3 A4 A5 ==> 1 B Ω(B) C Ω(C)
%D ren B0 B1 C0 C1 C2 ==> \catD \Set \catD(B,-) \Set(1,Ω(-)) Ω(-)=Ω
%D ren D1 D2 D3 D4 D5 ==> 1 Ω \Incs(Ω) E \Incs(E)
%D ren E0 E1          ==> (\Set^\catD)^\op \Set
%D ren       F0 F1 F2 ==> \Set^\catD(-,Ω) \Set(1,\Incs(-)) \Incs(-)=\Incs
%D
%D (( A1 A3  ->
%D    A2 A3 |->
%D    A2 A4  ->
%D    A3 A5  ->
%D    A2 A5 harrownodes nil 20 nil |->
%D    A4 A5 |->
%D    B0 B1  -> .plabel= a Ω
%D    C0 C1  ->
%D    C1 C2 <->
%D    C0 C2  ->
%D    # B0 relplace 0 -8 \catD
%D    C0 relplace -22 0 {↓}B≅
%D ))
%D (( D1 D3  -> .plabel= r \sm{\nameof{⊤}\\(\univ)}
%D    D2 D3 |->
%D    D2 D4 <-
%D    D3 D5  ->
%D    D2 D5 harrownodes nil 20 nil |->
%D    D4 D5 |->
%D    E0 E1  -> .plabel= a \Incs
%D    F0 F1 <->
%D    F1 F2 <->
%D    F0 F2 <->
%D    E0 relplace 0 -7 \Set^\catD\phantom{...}
%D ))
%D enddiagram
%D
$$\pu
  \diag{Omega-in-a-SetD}
$$

Now we have this sequence of isomorphisms:

$$\begin{array}{rcl}
  Ω(B) & ≅ & \Set(1,Ω(B)) \\
       & ≅ & \Set^\catD({↓}B,Ω) \\
       & ≅ & \Incs({↓}B) \\
     % & = & \Incs(\catD(B,-)) \\
     % & = & \Incs(↓B) \\
  \end{array}
$$
%

where the movement is:
%
% (find-latexinkscape-links "2020closures-and-J-ops/cla-1")
$$\includegraphics[height=3cm]{2020closures-and-J-ops/cla-1.pdf}$$

Let's look at an example. If $\catD$ is the category $\catT$ and $B =
▁3$ then:
%
$$\Logic(\SetT) = \zha{T}
  \qquad
  \begin{array}{rcl}
  Ω(▁3) & ≅ & \Set(1,Ω(▁3)) \\
        & ≅ & \Set^\catD({↓}(▁3),Ω) \\
        & ≅ & \Incs({↓}(▁3)) \\
        & ≅ & \Incs(13) \\
        & ≅ & \Subsets(13) \\
        & ≅ & \{00, 01, 02, 10, 11, 12, 13\} \\
     % & = & \Incs(\catD(B,-)) \\
     % & = & \Incs(↓B) \\
  \end{array}
$$


% (jonp 2 "parts")
% (jon    "parts")
% (jonp 34 "fig:five-sqconds")
% (joo     "fig:five-sqconds")




\newpage

%      _                                  _                 
%     | |       ___  _ __   ___ _ __ __ _| |_ ___  _ __ ___ 
%  _  | |_____ / _ \| '_ \ / _ \ '__/ _` | __/ _ \| '__/ __|
% | |_| |_____| (_) | |_) |  __/ | | (_| | || (_) | |  \__ \
%  \___/       \___/| .__/ \___|_|  \__,_|\__\___/|_|  |___/
%                   |_|                                     

% «J-ops»  (to ".J-ops")
% (clgp 6 "J-ops")
% (clga   "J-ops")
\section{J-operators, slashings, and question marks}

%   ____ _                   __        _ 
%  / ___| | ___  _ __        \ \      | |
% | |   | |/ _ \| '_ \   _____\ \  _  | |
% | |___| | (_) | |_) | |_____/ / | |_| |
%  \____|_|\___/| .__/       /_/   \___/ 
%               |_|                      
%
% «clop-to-Jop»  (to ".clop-to-Jop")
% (clgp 6 "clop-to-Jop")
% (clga   "clop-to-Jop")
\subsection{Closure operators induce J-operators \TODO}
\label{clop-to-Jop}

Let $(P,A)$ be a 2-column graph. Let $\catE = \SetD$ be the DAG topos
generated by $(P,A)$, and let $H := \Logic(\catE)$. Let $\clop$ be a
closure operator on $\catE$. Define an operation $(·)^*: H→H$ by
defining $R^*$ as $\dom(\ovl{\inc(R,1)})$. More formally,
%
$$\begin{array}{rrcl}
  (·)^*: & \Logic(\catE) &→& \Logic(\catE) \\
         &             R &↦& \dom(\ovl{\inc(R,1)}) \\
  \end{array}
$$

And as a diagram:
%
%D diagram clop-to-Jop
%D 2Dx     100  +20  +20       +40  +20
%D 2D  100 A0 ------ A1
%D 2D      |  \      |  
%D 2D  +20 |    A2 --|------------- A4
%D 2D      |  /      |            /
%D 2D  +20 A5 ------ A6 ------ A7
%D 2D
%D ren A0 A1    ==> R T
%D ren A2    A4 ==> R^*  T
%D ren A5 A6 A7 ==> 1 Ω Ω
%D
%D (( # Horizontal arrows:
%D    A0 A1 >->
%D    A2 A4 >->
%D    A5 A6 >-> .plabel= b χ_{\inc(R,1)}
%D    A6 A7  -> .plabel= b j
%D  # A5 A7  -> .slide= -12.5pt .plabel= b χ_{\ovl{q}}
%D
%D    A0 A5 `-> .PLABEL= _(0.40) \inc(R,1)
%D    A0 A2 `->
%D    A2 A5 `-> .PLABEL= ^(0.40) \ovl{\inc(R,1)}
%D
%D    A1 A6 `-> # .PLABEL= _(0.30) ⊤
%D    A4 A7 `-> # .PLABEL= ^(0.30) ⊤
%D ))
%D enddiagram
%D
$$\pu
  \diag{clop-to-Jop}
$$

Note that we also have $R^* = \dom(σ(j∘χ_{\inc(R,1)}))$.

\msk

\Theoremsubsection
The operation $(·)^*$ defined above is a J-operator.

{\bf Proof.} The proofs of J1 and J2, i.e., of $R≤R^*$ and
$R^*=R^{**}$, are just the parts C1 and C2 of Theorem
\ref{thm:top-to-clop} with a slightly different notation: just rewrite
the $E$ as $1$, $D$ as $R$, $\ovl{D}$ as $R^*$, and $\ovl{\ovl{D}}$ as
$R^{**}$.

The proof of J3 is better done in two steps. First we establish the
notation, i.e., how the truth-values and their arrows to 1 will be
named, using the notation for intersection pullbacks that we defined
in Theorem \ref{thm:restr-clop-1}:
%
% (clgp 10 "top-to-clop")
% (clga    "top-to-clop")
% (clga    "top-to-clop" "thm:top-to-clop")
%
%D diagram C4-to-J3-notation-1
%D 2Dx     100  +35  +30  +35
%D 2D  100 A0 - A1   B0 - B1
%D 2D      |     |   |     |
%D 2D  +30 A2 - A3   B2 - B3
%D 2D
%D ren A0 A1 A2 A3 ==> C{∧}D D C 1
%D ren B0 B1 B2 B3 ==> C^*{∧}D^* D^* C^* 1
%D
%D (( A0 A1 `-> .plabel= a (c∩d)''
%D    A0 A2 `-> .plabel= l (c∩d)'
%D    A0 A3 `-> .plabel= m (c∩d)
%D    A1 A3 `-> .plabel= r d
%D    A2 A3 `-> .plabel= b c
%D ))
%D (( B0 B1 `-> .plabel= a (c∩d)''
%D    B0 B2 `-> .plabel= l (c∩d)'
%D    B0 B3 `-> .plabel= m (c∩d)
%D    B1 B3 `-> .plabel= r d
%D    B2 B3 `-> .plabel= b c
%D ))
%D enddiagram
%D
%D diagram C4-to-J3-notation-2
%D 2Dx     100 +20
%D 2D  100 A0
%D 2D
%D 2D  +20     A1
%D 2D
%D 2D  +20 A2
%D 2D
%D ren A0 A1 A2 ==> C{∧}D (C∧D)^* 1
%D
%D (( A0 A1 `->
%D    A0 A2 `-> .plabel= l c∩d
%D    A1 A2 `-> .plabel= r \ovl{c∩d}
%D ))
%D enddiagram
%D
$$\pu
  \diag{C4-to-J3-notation-1}
  \qquad
  \diag{C4-to-J3-notation-2}
$$

And here is the second step:
%
$$\def\c{c}
  \def\d{d}
  \begin{array}{rcl}
  (C∧D)^* &=& \dom(\ovl{\c∩\d}) \\
          &=& \dom(\ovl{\c}∩\ovl{\d}) \\
          &=& \dom(\ovl{\c})∩\dom(\ovl{\d}) \\
          &=& C^*∩D^* \\
  \end{array}
  %
  \quad
  %
  \def\c{\inc(C,1)}
  \def\d{\inc(D,1)}
  \begin{array}{rcl}
  (C∧D)^* &=& \dom(\ovl{\c∩\d}) \\
          &=& \dom(\ovl{\c}∩\ovl{\d}) \\
          &=& \dom(\ovl{\c})∩\dom(\ovl{\d}) \\
          &=& C^*∩D^* \\
  \end{array}
$$



\newpage

%      _       __    _              
%     | |      \ \  | |_ ___  _ __  
%  _  | |  _____\ \ | __/ _ \| '_ \ 
% | |_| | |_____/ / | || (_) | |_) |
%  \___/       /_/   \__\___/| .__/ 
%                            |_|    
%
% «Jop-to-top»  (to ".Jop-to-top")
% (clgp 7 "Jop-to-top")
% (clga   "Jop-to-top")
\subsection{J-operators induce topologies \TODO}

Let's state this in its general form first, and then see an example
that clarifies what it means and how it works.

\msk

\Theoremsubsection
\label{thm:Jop-to-top-generic}

\begin{tabular}{rl}
Suppose that: & $\catD$ is a DAG category, \\
              & $\catE$ is $\SetD$, \\
              & $j$ is a topology in $\catE$, \\
              & $\clop$ is the closure operator associated to $j$, \\
              & $B$ is an object of $D$, \\
              & $R$ is ${↓}B$ (so $R∈\Logic(E)$), \\
              & $(q:Q \ito R)∈\Incs(R)$ (so $Q≤R$), \\
              & $(\ovl{q}:\ovl{Q} \ito R)$ is the closure of $q$ (so $Q≤\ovl{Q}≤R$). \\
        Then: & $RB=\{*\}$, \\
              & $ΩB={↓}{↓}B={↓}R$, \\
              & $(χ_qB)(*)=Q$, \\
              & $(χ_{\ovl{q}}B)(*)=\ovl{Q}$, \\
      and so: & $\begin{array}[t]{rcl}
                 jB(Q) &=& jB(χ_qB(*)) \\
                       &=& (jB∘χ_qB)(*) \\
                       &=& (j∘χ_q)(B)(*) \\
                       &=& χ_{\ovl{q}}(B)(*) \\
                       &=& \ovl{Q}. \\
                 \end{array}
                $ \\
\end{tabular}

\msk

%D diagram Jop-to-top-generic
%D 2Dx     100  +20  +20       +40  +20
%D 2D  100 A0 ------ A1
%D 2D      |  \      |  
%D 2D  +20 |    A2 --|------------- A4
%D 2D      |  /      |            /
%D 2D  +20 A5 ------ A6 ------ A7
%D 2D
%D 2D  +25 B0 ------ B1 ------ B2
%D 2D
%D 2D  +25 C0 ------ C1
%D 2D  +8  C2 ---------------- C3
%D 2D  +8            C4 ------ C5
%D 2D
%D ren A0 A1    ==> Q T
%D ren A2    A4 ==> \ovl{Q}  T'
%D ren A5 A6 A7 ==> R Ω Ω'
%D
%D ren B0 B1 B2 ==> RB ΩB ΩB
%D
%D ren C0 C1    ==> * Q
%D ren C2    C3 ==> *   \ovl{Q}
%D ren    C4 C5 ==>   Q \ovl{Q}
%D
%D (( # Horizontal arrows:
%D    A0 A1 >->
%D    A2 A4 >->
%D    A5 A6 >-> .plabel= b χ_q
%D    A6 A7  -> .plabel= b j
%D    A5 A7  -> .slide= -12.5pt .plabel= b χ_{\ovl{q}}
%D
%D    A5 relplace -15 0 {↓}B=
%D
%D    A0 A5 `-> .PLABEL= _(0.40) q
%D    A0 A2 `->
%D    A2 A5 `-> .PLABEL= ^(0.40) \ovl{q}
%D
%D    A1 A6 `-> # .PLABEL= _(0.30) ⊤
%D    A4 A7 `-> # .PLABEL= ^(0.30) ⊤
%D
%D    B0 B1 -> .plabel= b χ_qB
%D    B1 B2 -> .plabel= b jB
%D    B0 B2 -> .slide= -12.5pt .plabel= b χ_{\ovl{q}}B
%D
%D    C0 C1 |->
%D    C2 C3 |->
%D    C4 C5 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{Jop-to-top-generic}
$$





\newpage


\Examplesubsection
\label{thm:Jop-to-top-1}
%
If we make $\catD=\catT$, $B=3▁$, $Q=11$, and $\ovl{Q}=21$ in the
previous diagram it becomes this:

%D diagram Jop-to-top-1
%D 2Dx     100  +20  +20       +40  +20
%D 2D  100 A0 ------ A1
%D 2D      |  \      |  
%D 2D  +20 |    A2 --|------------- A4
%D 2D      |  /      |            /
%D 2D  +20 A5 ------ A6 ------ A7
%D 2D
%D 2D  +25 B0 ------ B1
%D 2D  +8  B2 ---------------- B3
%D 2D  +8            B4 ------ B5
%D 2D
%D ren A0 A1    ==> 11 T
%D ren A2    A4 ==> 21  T'
%D ren A5 A6 A7 ==> 32 Ω Ω'
%D
%D ren B0 B1    ==> (3▁,*) (3▁,11)
%D ren B2    B3 ==> (3▁,*)         (3▁,21)
%D ren    B4 B5 ==>        (3▁,11) (3▁,21)
%D
%D (( # Horizontal arrows:
%D    A0 A1 >->
%D    A2 A4 >->
%D    A5 A6 >-> .plabel= b χ_q
%D    A6 A7  -> .plabel= b j
%D    A5 A7  -> .slide= -12.5pt .plabel= b χ_{\ovl{q}}
%D
%D    A5 relplace -15 0 {↓}3▁=
%D
%D    A0 A5 `-> .PLABEL= _(0.40) q
%D    A0 A2 `->
%D    A2 A5 `-> .PLABEL= ^(0.40) \ovl{q}
%D
%D    A1 A6 `-> # .PLABEL= _(0.30) ⊤
%D    A4 A7 `-> # .PLABEL= ^(0.30) ⊤
%D
%D    B0 B1 |->
%D    B2 B3 |->
%D    B4 B5 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{Jop-to-top-1}
$$



% «Jop-to-top-defs»  (to ".Jop-to-top-defs")
%
%L tdims_med  = TCGDims {h=30,  v=10,    crh=11, crv=8}
%L tspec_med  = TCGSpec.new("33; 32, 13")
%L tcg_med    = TCGQ.newdsoa(tdims_med, tspec_med,
%L                           {tdef="Tmed", meta="1pt s"},
%L                           "h p")
%L tcg_med:Lput(3, "\\Ta");    tcg_med:Rput(3, "\\Tb")
%L tcg_med:Lput(2, "\\Tc");    tcg_med:Rput(2, "\\Td")
%L tcg_med:Lput(1, "\\Te");    tcg_med:Rput(1, "\\Tf")
%L tcg_med:output()
\pu
\def\Tmed#1#2#3#4#5#6{{
  \def\Ta{#1} \def\Tb{#2}
  \def\Tc{#3} \def\Td{#4}
  \def\Te{#5} \def\Tf{#6}
  \left(\!\!\!
  \tcg{Tmed}
  \!\right)
  }}
\def\C#1{\{#1\}}
\def\UN{{\C{*}}}
\def\TT{{\Tmed
  {\C{32}} {\C{13}}
  {\C{20}} {\C{02}}
  {\C{10}} {\C{01}}
  }}
\def\TA{{\Tmed ∅∅   ∅∅     \UN\UN}}
\def\TB{{\Tmed ∅∅   \UN∅   \UN\UN}}
\def\TC{{\Tmed \UN∅ \UN\UN \UN\UN}}


Here is its internal view:
%
%D diagram Jop-to-top-big-ex
%D 2Dx     100  +30  +30       +50  +30
%D 2D  100 A0 ------ A1
%D 2D      |  \      |  
%D 2D  +30 |    A2 --|------------- A4
%D 2D      |  /      |            /
%D 2D  +30 A5 ------ A6 ------ A7
%D 2D
%D 2D  +25 B0 ------ B1
%D 2D  +8  B2 ---------------- B3
%D 2D  +8            B4 ------ B5
%D 2D
%D ren A0 A1    ==> \TA \TT
%D ren A2    A4 ==> \TB  \TT
%D ren A5 A6 A7 ==> \TC Ω Ω'
%D
%D ren B0 B1    ==> (3▁,*) (3▁,11)
%D ren B2    B3 ==> (3▁,*)         (3▁,21)
%D ren    B4 B5 ==>        (3▁,11) (3▁,21)
%D
%D (( # Horizontal arrows:
%D    A0 A1 >->
%D    A2 A4 >->
%D    A5 A6 >-> .plabel= b χ_q
%D    A6 A7  -> .plabel= b j
%D    A5 A7  -> .slide= -12.5pt .plabel= b χ_{\ovl{q}}
%D
%D    A5 relplace -15 0 {↓}3▁=
%D
%D    A0 A5 `-> .PLABEL= _(0.40) q
%D    A0 A2 `->
%D    A2 A5 `-> .PLABEL= ^(0.40) \ovl{q}
%D
%D    A1 A6 `-> # .PLABEL= _(0.30) ⊤
%D    A4 A7 `-> # .PLABEL= ^(0.30) ⊤
%D
%D    B0 B1 |->
%D    B2 B3 |->
%D    B4 B5 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{Jop-to-top-big-ex}
$$

I did not expand the `$Ω$'s because their internal views would be too
big -- see the last diagram in section \ref{SetD-classifier}. Note
that the images of $R$ by the monics $χ_q$ and $χ_{\ovl{q}}$ (that are
not inclusions!) are, respectively:
%
$$\Tmed {\C{11}} {∅}
        {\C{10}} {\C{01}}
        {\C{10}} {\C{01}}
  \qquad
  \text{and}
  \qquad
  \Tmed {\C{21}} {∅}
        {\C{20}} {\C{01}}
        {\C{10}} {\C{01}}
  \;.
$$




\newpage

% «def-j»  (to ".def-j")
% (clgp 9 "def-j")
% (clga   "def-j")

\Theoremsubsection 
\label{thm:Jop-to-top-formula}

\begin{tabular}{rl}
      Suppose that: & $(P,A)$ is a 2-column graph, \\
                    & $\catD$ is $(P,A)$ as a DAG category, \\
                    & $\catE$ is $\SetD$, \\
                    & $H$ is $\Logic(\catE)$, \\
                    & $(·)^*$ is a J-operator on $H$. \\
 Then the operation & $j = λB⠆P.λQ⠆{↓}Q.Q^*∧{↓}B$ \\
      is a morphism & $j:Ω→Ω$ \\
         that obeys & $j∘j=j$, \\
                    & $j∘⊤_Ω=⊤_Ω$, \\
                    & $∧∘j=(j×j)∘∧$, \\
              i.e., & $j$ is a topology on $\catE$. \\ 
\end{tabular}

%D diagram Jop-to-top-def-j
%D 2Dx     100  +20  +20       +40  +20
%D 2D  100 A0 ------ A1
%D 2D      |  \      |  
%D 2D  +20 |    A2 --|------------- A4
%D 2D      |  /      |            /
%D 2D  +20 A5 ------ A6 ------ A7
%D 2D
%D 2D  +25 B0 ------ B1 ------ B2
%D 2D
%D 2D  +25 C0 ------ C1
%D 2D  +8  C2 ---------------- C3
%D 2D  +8            C4 ------ C5
%D 2D
%D ren A0 A1    ==> Q T
%D ren A2    A4 ==> Q^*{∧}{↓}B  T'
%D ren A5 A6 A7 ==> R Ω Ω'
%D
%D ren B0 B1 B2 ==> RB ΩB ΩB
%D
%D ren C0 C1    ==> * Q
%D ren C2    C3 ==> *   Q^*{∧}{↓}B
%D ren    C4 C5 ==>   Q Q^*{∧}{↓}B
%D
%D (( # Horizontal arrows:
%D    A0 A1 >->
%D    A2 A4 >->
%D    A5 A6 >-> .plabel= b χ_q
%D    A6 A7  -> .plabel= b j
%D    A5 A7  -> .slide= -12.5pt .plabel= b χ_{\ovl{q}}
%D
%D    A5 relplace -15 0 {↓}B=
%D
%D    A0 A5 `-> .PLABEL= _(0.40) q
%D    A0 A2 `->
%D    A2 A5 `-> .PLABEL= ^(0.40) \ovl{q}
%D
%D    A1 A6 `-> # .PLABEL= _(0.30) ⊤
%D    A4 A7 `-> # .PLABEL= ^(0.30) ⊤
%D
%D    B0 B1 -> .plabel= b χ_qB
%D    B1 B2 -> .plabel= b jB
%D    B0 B2 -> .slide= -12.5pt .plabel= b χ_{\ovl{q}}B
%D
%D    C0 C1 |->
%D    C2 C3 |->
%D    C4 C5 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{Jop-to-top-def-j}
$$


\msk

\def\adb{{∧}{↓}B}

% «def-j-NT»  (to ".def-j-NT")
% (clgp 35 "def-j-NT")
% (clga    "def-j-NT")

To prove that this $j:Ω→Ω$ is a natural transformation in $\SetD$ we
need to check that the square at the right here commutes:
%
%D diagram def-j-NT
%D 2Dx     100 +20  +25  +40  +50
%D 2D  100 A0  B0 - B1   E0 - E1 
%D 2D      |   |     |   |     | 
%D 2D  +17 |   |     |   |    E3' 
%D 2D   +8 A1  B2 - B3   E2 - E3 
%D 2D                           
%D 2D  +15     C0 - C1   
%D 2D
%D ren A0 A1       ==> B C
%D ren B0 B1 B2 B3 ==> ΩB ΩB ΩC ΩC
%D ren C0 C1       ==> Ω Ω
%D ren E0 E1 E3'   ==> Q Q^*\adb (Q{∧}{↓}B)^*{∧}{↓}C
%D ren E2 E3       ==> Q{∧}{↓}C (Q{∧}{↓}C)^*{∧}{↓}C
%D
%D (( A0 A1 -> .plabel= l f
%D    B0 B1 -> .plabel= a jB
%D    B0 B2 -> .plabel= l Ωf
%D    B1 B3 -> .plabel= r Ωf
%D    B2 B3 -> .plabel= a jC
%D    C0 C1 -> .plabel= a j
%D ))
%D
%D (( E0 E1  |->
%D    E0 E2  |->
%D    E1 E3' |->
%D    E2 E3  |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{def-j-NT}
$$


\newpage

% «def-j-obeys-J1-J2-J3»  (to ".def-j-obeys-J1-J2-J3")
% (clgp 38 "def-j-obeys-J1-J2-J3")
% (clga    "def-j-obeys-J1-J2-J3")

To prove that $j$ obeys J1, J2, J3 we need to check that the lower
three diagrams here commute:
%
%D diagram def-j-1
%D 2Dx     100 +20 +20 +20 +30 +25
%D 2D  100 A0  A1  B0  B1  C0  C1
%D 2D
%D 2D  +20     A2      B2  C2  C3
%D 2D
%D ren A0 A1 A2 ==> Ω Ω Ω
%D ren B0 B1 B2 ==> Ω Ω Ω
%D ren C0 C1 C2 C3 ==> Ω×Ω Ω Ω×Ω Ω
%D
%D (( A0 A1 -> .plabel= a ⊤
%D    A0 A2 -> .plabel= l ⊤
%D    A1 A2 -> .plabel= r j
%D
%D    B0 B1 -> .plabel= a j
%D    B0 B2 -> .plabel= l j
%D    B1 B2 -> .plabel= r j
%D
%D    C0 C1 -> .plabel= a ∧
%D    C0 C2 -> .plabel= l j×j
%D    C1 C3 -> .plabel= r j
%D    C2 C3 -> .plabel= a ∧
%D ))
%D enddiagram
%D
$$\pu
  \diag{def-j-1}
$$

%D diagram def-j-2
%D 2Dx     100 +20 +20 +25 +30 +45
%D 2D  100 A0  A1  B0  B1  C0  C1
%D 2D
%D 2D  +20     A2      B2  C2  C3
%D 2D
%D ren A0 A1 A2 ==> ΩB ΩB ΩB
%D ren B0 B1 B2 ==> ΩB ΩB ΩB
%D ren C0 C1 C2 C3 ==> ΩB{×}ΩB ΩB ΩB{×}ΩB ΩB
%D
%D (( A0 A1 -> .plabel= a jB
%D    A0 A2 -> .plabel= l jB
%D    A1 A2 -> .plabel= r jB
%D
%D    B0 B1 -> .plabel= a ⊤_ΩB
%D    B0 B2 -> .plabel= l ⊤_ΩB
%D    B1 B2 -> .plabel= r jB
%D
%D    C0 C1 -> .plabel= a λQ,R.Q{∧}R
%D    C0 C2 -> .plabel= l jB×jB
%D    C1 C3 -> .plabel= r jB
%D    C2 C3 -> .plabel= a λQ,R.Q{∧}R
%D ))
%D enddiagram
%D
$$\pu
  \diag{def-j-2}
$$


%D diagram def-j-3
%D 2Dx     100  +30 +30  +25 +45  +65
%D 2D  100 A0 - A1  B0 - B1  C0 - C1
%D 2D        \   |    \   |  |     |
%D 2D  +17    \ A2'    \ B2' |    C3'
%D 2D   +8      A2       B2  C2 - C3
%D 2D
%D ren A0 A1 A2' A2 ==> Q Q^*\adb (Q^*\adb)^*\adb Q^*\adb
%D ren B0 B1 B2' B2 ==> Q {↓}B ({↓}B)^*\adb {↓}B
%D ren C0 C1 C3' C2 C3 ==> (Q,R) Q{∧}R (Q{∧}R)^*\adb (Q^*\adb,R^*\adb) (Q^*\adb){∧}(R^*\adb)
%D
%D (( A0 A1  |->
%D    A1 A2' |->
%D    A0 A2  |-> .curve= _20pt
%D
%D    B0 B1  |->
%D    B1 B2' |->
%D    B0 B2  |-> .curve= _20pt
%D
%D    C0 C1  |->
%D    C1 C3' |->
%D    C0 C2  |->
%D    C2 C3  |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{def-j-3}
$$


% \newpage

% «def-j-example»  (to ".def-j-example")
% (clgp 42 "def-j-example")
% (clga    "def-j-example")
% (clgp 28 "SetT-classifier-defs")
% (clga    "SetT-classifier-defs")

% % «clop-Jop-bij»  (to ".clop-Jop-bij")
% % (clgp 28 "clop-Jop-bij")
% % (clga    "clop-Jop-bij")
% \subsection{A bijection \TODO}
% 


% «SetD-dense-closed»  (to ".SetD-dense-closed")
% (clgp 38 "SetD-dense-closed")
% (clga    "SetD-dense-closed")
\subsection{Dense and closed maps in a $\SetD$ \TODO}

Let $\catD$ be a DAG topos with a J-operator. If $R$ and $S$ are two
truth-values in it with $R≤S$ we can name the inclusions between $R$,
$S$, and $1$ like this:
%
%D diagram ??
%D 2Dx     100 +15 +15
%D 2D  100 A0      A1
%D 2D
%D 2D  +25     A2
%D 2D
%D ren A0 A1 A2 ==> R S 1
%D
%D (( A0 A1 `-> .plabel= a m
%D    A0 A2 `-> .plabel= l r
%D    A1 A2 `-> .plabel= r s
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$
%
and can use the Theorem \ref{thm:restr-clop-1} to calculate $\ovl{m}$
using just the J-operator. We have this:
%
%D diagram ??
%D 2Dx     100 +20
%D 2D  100 A0
%D 2D
%D 2D  +20     A1
%D 2D
%D 2D  +20 A2
%D 2D
%D ren A0 A1 A2 ==> R R^S{=}R^*{∧}S S
%D
%D (( A0 A1 `-> .plabel= r (dense)
%D    A0 A2 `-> .plabel= l m
%D    A1 A2 `-> .plabel= r \sm{\ovl{m}\\(closed)}
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$
%
where we call the mediating map $d$, and we know that $d$ is dense and
$\ovl{m}$ is closed by Theorem \ref{thm:dense-and-closed-2}.

This gives us lots of examples of dense and closed maps in a topos
with a J-operator. For example, if $R=11$ and $S=14$ in the figure
below, then $R^*=23$ and $R^S=R^*∧S=13$:
%
% (jonp 16 "valuations")
% (jov     "valuations")
%
%L mp = mpnew({zdef="11-13-14", scale="12pt", meta="s"}, "1R2R3212RL1")
%L mp:addcuts("c 4321/0 0123|45|6")
%L mp:put(v"11", "R"):put(v"23", "R*", "R^*")
%L mp:put(v"14", "S"):put(v"13", "RS", "R^S")
%L mp:output()
%
%D diagram ??
%D 2Dx     100 +25
%D 2D  100 A0
%D 2D
%D 2D  +25     A1
%D 2D
%D 2D  +25 A2
%D 2D
%D ren A0 A1 A2 ==> 11 13{=}23{∧}14 14
%D ren A0 A1 A2 ==> 11 13=23∧14 14
%D
%D (( A0 A1 `->   .plabel= r (dense)
%D    A0 A2 `-> # .plabel= l m
%D    A1 A2 `->   .plabel= r (closed)
%D ))
%D enddiagram
%D
\pu
$$%\zha{O_A(P),J}
  %\qquad
  \zha{11-13-14}
  \qquad
  \qquad
  \diag{??}
$$

By trying many examples of this factorization I got two conjectures:

\Conjecturesubsection an inclusion $R \ito R'$ in the logic is dense
iff both $R$ and $R'$ belong to the same region of the slashing,

\Conjecturesubsection an inclusion $S' \ito S$ in the logic is dense
iff $S'$ cannot be moved upwards toward $S$ without crossing a line of
the slashing.

They are both easy to prove. (...)



% «SetD-sheaves»  (to ".SetD-sheaves")
% (clgp 39 "SetD-sheaves")
% (clga    "SetD-sheaves")
\subsection{Sheaves in a $\SetD$ \TODO}

% (find-mclartypage (+ 4 196) "21. Topologies")
% (find-books "__cats/__cats.el" "bell-lst")
% (find-belltpage (+ 14 174)    "(mu-)sheaf")
% (find-books "__cats/__cats.el" "johnstone-topostheory")
% (find-topostheorypage (+ 24  81) "3.2. Sheaves")
% (find-toposthepubpage       113  "3.2. Sheaves")
% (find-toposthepubtext       113  "3.2. Sheaves")

The usual definition of a sheaf in a topos $\catE$ with a topology $j$
is that an object $S∈\catE$ is a ($j$-)sheaf iff for every dense monic
$d: D \monicto E$ in $\catE$ every map $f: D \to S$ factors uniquely
through $d: D \monicto E$. I prefer to write this backwards: $S$ is a
sheaf iff for every dense monic $d: D \monicto E$ the map of hom-sets
$(∘d): \Hom(E,S) → \Hom(D,S)$ is a bijection. In a diagram:
%
%D diagram ??
%D 2Dx     100  +25  +40  +30
%D 2D  100 A0        B0   C0
%D 2D      |  \      |
%D 2D  +25 A1 - A2   B1   C1
%D 2D
%D ren A0 A1 A2 ==> ∀D ∀E S
%D ren B0 B1    ==> \Hom(D,S) \Hom(E,S)
%D ren C0 C1    ==> g∘d g
%D
%D (( A0 A1 `-> .plabel= l \sm{∀d\\dense} sl_
%D    A0 A2  -> .plabel= r ∀f
%D    A1 A2  -> .plabel= b ∃!g
%D
%D    B1 B0 -> .plabel= l \sm{∘d\\iso}
%D
%D    C1 C0 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

In a $\SetD$ we can get lots of properties that sheaves must obey by
understanding what the condition above means on a very small family of
dense maps --- the ``basic dense maps''. Suppose that we have a DAG
with question marks $((P,A),Q)$ and that our topos $\catE$ with
topology $j$ is generated by that $((P,A),Q)$. For every point $B$ of
the set of question marks $Q$ let $bd(B): D \ito E$ be the inclusion
in which $E$ is ${↓}B$ and $D$ is $E$ minus the point $B$. We will
call these `$bd(B)$'s the {\sl basic dense maps} of our topos.



% % «SetD-closure»  (to ".SetD-closure")
% % (clgp 41 "SetD-closure")
% % (clga    "SetD-closure")
% \subsection{From question marks to a closure operator \TODO}
% 
% %L -- (find-dn6 "tcgs.lua" "TCGQ")
% %L -- (find-dn6 "tcgs.lua" "TCGQ" "Lput  =")
% %L TCGQ.__index.Lputs = function (tq, arr)
% %L     if type(arr) == "string" then arr = split(arr) end
% %L     for y,str in ipairs(arr) do tq:Lput(y, str) end
% %L     return tq
% %L   end
% %L TCGQ.__index.Rputs = function (tq, arr)
% %L     if type(arr) == "string" then arr = split(arr) end
% %L     for y,str in ipairs(arr) do tq:Rput(y, str) end
% %L     return tq
% %L   end
% %L
% %L tdims_clo  = TCGDims {qrh=5, q=15, crh=12, h=60, v=25, crv=7}   -- with v arrows
% %L tspec_clo1 = TCGSpec.new("46; 11 22 34 45, 25", ".???", "???.?.")
% %L tspec_clo2 = TCGSpec.new("46; 11 22 34 45, 25", "....", "???...")
% %L tcg_clo1   = TCGQ.newdsoa(tdims_clo, tspec_clo1, {tdef="clo-1", meta="1pt p"}, "q h")
% %L tcg_clo2   = TCGQ.newdsoa(tdims_clo, tspec_clo2, {tdef="clo-2", meta="1pt p"}, "q h")
% %L tcg_clo1:Lputs("1 · · ·")
% %L tcg_clo2:Lputs("1 · · ·")
% %L tcg_clo1:Rputs("1 0 0 0 · ·")
% %L tcg_clo2:Rputs("1 0 0 0 · ·")
% %L tcg_clo1:output()
% %L tcg_clo2:output()
% \pu
% $$\tcg{clo-1}
%   \qquad
%   \tcg{clo-2}
% $$









% «topological-lemmas»  (to ".topological-lemmas")
% (clgp 30 "topological-lemmas")
% (clga    "topological-lemmas")
\subsection{Some topological lemmas \TODO}

Let $(X,\Opens(X))$ be a topological space.

\msk

\Lemmasubsection If $A,B⊆X$ then $\Int(A∩B) = \Int(A)∩\Int(B)$.

{\bf Proof.} Suppose that $c∈\Int(A)∩\Int(B)$. Then we have open sets
$W,V∈\Opens(X)$ that make all the inferences in the tree at the left
below true, and so $c∈\Int(A∩B)$. Now suppose that $d∈\Int(A∩B)$. We
have an open set $U∈\Opens(X)$ that makes all the inferences in the
tree at the right below true, and so $d∈\Int(A)∩\Int(B)$. This means
that $\Int(A)∩\Int(B)⊆\Int(A∩B)$ and $\Int(A∩B)⊆\Int(A)∩\Int(B)$, and
so $\Int(A∩B) = \Int(A)∩\Int(B)$.
%:
%:  c∈\Int(A)∩\Int(B)    c∈\Int(A)∩\Int(B)
%:  -----------------    -----------------
%:     c∈\Int(A)            c∈\Int(B)     
%:    -----------          -----------    
%:    c∈V⊆\Int(A)          c∈V⊆\Int(B)    
%:    -----------          -----------    
%:       c∈V⊆A                c∈W⊆B       
%:      -------              -------      
%:      c∈V∩W⊆A              c∈V∩W⊆B      
%:      -----------------------------
%:              c∈V∩W⊆A∩B      
%:             -----------
%:             c∈\Int(A∩B)
%:
%:             ^top-lemma-1
%:
%:
%:   d∈\Int(A∩B)      d∈\Int(A∩B) 
%:  -------------    -------------
%:  d∈U⊆\Int(A∩B)    d∈U⊆\Int(A∩B)
%:  -------------    -------------
%:     d∈U⊆A∩B          d∈U⊆A∩B   
%:     -------          -------   
%:     d∈U⊆A            d∈U⊆B     
%:   ---------        ---------   
%:   d∈\Int(A)        d∈\Int(B)   
%:   --------------------------   
%:      d∈\Int(A)∩\Int(B)   
%:
%:      ^top-lemma-2
%:
\pu
$$\ded{top-lemma-1}$$
$$\ded{top-lemma-2}$$

\msk

\Lemmasubsection If $W,V∈\Opens(X)$, $W⊆V$, and $A⊆X$, then

$\Int(W∪A)∩V = \Int(W∪(A∩V))$.

{\bf Proof:}
%
$$\begin{array}{rcl}
  \Int(W∪A)∩V &=& \Int(W∪A)∩\Int(V) \\
              &=& \Int((W∪A)∩V) \\
              &=& \Int((W∩V)∪(A∩V)) \\
              &=& \Int(W∪(A∩V)). \\
  \end{array}
$$



















\printbibliography

\GenericWarning{Success:}{Success!!!}  % Used by `M-x cv'

\end{document}

%  __  __       _        
% |  \/  | __ _| | _____ 
% | |\/| |/ _` | |/ / _ \
% | |  | | (_| |   <  __/
% |_|  |_|\__,_|_|\_\___|
%                        
% <make>

 (eepitch-shell)
 (eepitch-kill)
 (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2020clops-and-tops-garbage veryclean
make -f 2019.mk STEM=2020clops-and-tops-garbage pdf

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