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


\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 forths["<.>"]  = function () pusharrow("<.>") end
%L forths["<-->"] = function () pusharrow("<-->") end
%L forths["|-->"] = function () pusharrow("|-->") end
%L forths["<--|"] = function () pusharrow("<--|") end

% %L dofile "edrxtikz.lua"  -- (find-LATEX "edrxtikz.lua")
% %L dofile "edrxpict.lua"  -- (find-LATEX "edrxpict.lua")
% \pu





% «defs»  (to ".defs")
\def\bfP{\mathbf{P}}
\def\Ups{\mathsf{U}}
\def\Downs{\mathsf{D}}
\def\Filts{\mathsf{F}}
\def\Jcan{{J_\mathrm{can}}}
\def\hasmax{\mathsf{hasmax}}
\def\trans {\mathsf{trans}}
\def\stab  {\mathsf{stab}}

\def\plarray#1{\left(\begin{array}{l}#1\end{array}\right)}

\def\setofsc#1#2{\{\,#1\;:\;#2\,\}}

\def\Sieveson{\mathsf{Sieves\_on}}
\def\Coveringsieveson{\mathsf{Covering\_sieves\_on}}
\def\Coveringsieveson{\mathsf{Covsieves\_on}}
\def\Int{\mathsf{Int}}
\def\GrTops{\mathsf{GrTops}}
\def\Nucs{\mathsf{Nucs}}
\def\nuc{(·)^*}

\def\OX{\Opens(X)}
\def\OH{\Opens(H)}
\def\OB{\Opens(B)}
\def\OU{\Opens(U)}
\def\OV{\Opens(V)}
\def\catD{{\mathbf{D}}}
\def\catN{{\mathbf{N}}}
\def\calM{{\mathcal{M}}}
\def\calY{{\mathcal{Y}}}
\def\calT{{\mathcal{T}}}
\def\calH{{\mathcal{H}}}
\def\SetD{{\Set^\catD}}

\def\DP {\calD(\bfP)}
\def\Ddp{\calD({↓}p)}

\def\GP{\calG(\bfP)}
\def\Ddp{\calD({↓}p)}
\def\Nuc{\mathrm{Nuc}}
\def\Con{\mathrm{Con}}
\def\NucDP{\Nuc(\DP)}
\def\ConDP{\Con(\DP)}


\def\Onep {1${}'$}
\def\Onepp{1${}''$}

% «House»  (to ".House")
%
%R local house, ohouse = 2/  #1  \, 7/       !h11111                     \
%R                        |#2  #3|   |              !h01111              |
%R                        \#4  #5/   |       !h01011       !h00111       |
%R                                   |!h01010       !h00011       !h00101|
%R                                   |       !h00010       !h00001       |
%R                                   \              !h00000              /
%R local houser = 1/ 1 \
%R                 |2 3|
%R                 \4 5/
%R
%R  house:tomp({def="zfHouse#1#2#3#4#5", scale="6pt", meta="s"}):addcells():output()
%R  house:tomp({zdef="House" , scale="20pt", meta=nil}):addbullets():addarrows():output()
%R houser:tomp({zdef="House" , scale="25pt", meta=nil}):addcells():addarrows():output()
%R ohouse:tomp({zdef="OHouse", scale="32pt", meta=nil}):addcells():addarrows("w"):output()
\pu


% «Bottle»  (to ".Bottle")
% (find-LATEX "2021groth-tops-defs.tex" "Bottle")

% (find-angg "LUA/defwithmanyargs.lua" "SetManyArgs-tests")
% (find-angg "LUA/defwithmanyargs.lua" "SetManyArgs-tests" "Bottle")
%
\def\sa#1#2{\expandafter\def\csname myarg#1\endcsname{#2}}
\def\ga#1{\csname myarg#1\endcsname}
%
\makeatletter
\def\BottleSetArgs#1{\BottleSetArgs@#1}
\def\BottleSetArgs@#1#2#3#4#5{%
  \sa{32}{#1}\sa{20}{#2}\sa{21}{#3}\sa{22}{#4}\sa{10}{#5}%
  \BottleSetArgs@@}
\def\BottleSetArgs@@#1#2#3#4#5{%
  \sa{11}{#1}\sa{12}{#2}\sa{00}{#3}\sa{01}{#4}\sa{02}{#5}%
  }
\makeatother
%
%R local Bottle = 7/       !ga{32}                     \
%R                 |              !ga{22}              |
%R                 |       !ga{21}       !ga{12}       |
%R                 |!ga{20}       !ga{11}       !ga{02}|
%R                 |       !ga{10}       !ga{01}       |
%R                 \              !ga{00}              /
%R Bottle:tomp({zdef="Bottle-5pt", scale="5pt", meta="s"}):addcells():output()
%R Bottle:tomp({zdef="Bottle-6pt", scale="6pt", meta="s"}):addcells():output()
%R Bottle:tomp({zdef="Bottle-8pt", scale="8pt", meta="s"}):addcells():output()
%R Bottle:tomp({zdef="Bottle^2",  scale="52pt", meta=nil}):addcells():addarrows():output()

\pu
\def\bo  #1{{       \BottleSetArgs{#1}\zha{Bottle-5pt}        }}
\def\bbo #1{{\left[ \BottleSetArgs{#1}\zha{Bottle-5pt} \right]}}
\def\pwbo#1{{\left( \BottleSetArgs{#1}\zha{Bottle-8pt} \right)}}

% % Tests:
% $\bo{0 123 456 789} \bbo{0 123 456 789} \pwbo{· {20}{21}· {10}{11}· {00}{01}·}$
% 
% $$Ω =
%   \left(
%   \BottleSetArgs{
%                                               {\bbo{? ??? ??? ???}}
%   {\bbo{· ?·· ?·· ?··}} {\bbo{· ??· ??· ??·}} {\bbo{· ??? ??? ???}}
%   {\bbo{· ··· ?·· ?··}} {\bbo{· ··· ??· ??·}} {\bbo{· ··· ??? ???}}
%   {\bbo{· ··· ··· ?··}} {\bbo{· ··· ··· ??·}} {\bbo{· ··· ··· ???}}}
%   \zha{Bottle^2}
%   \right)
% $$


% «WideBottle»  (to ".WideBottle")
% (find-LATEX "2021groth-tops-defs.tex" "WideBottle")

% (find-angg "LUA/defwithmanyargs.lua" "SetManyArgs-tests")
% (find-angg "LUA/defwithmanyargs.lua" "SetManyArgs-tests" "WideBottle")
\makeatletter
\def\WideBottleSetArgs#1{\WideBottleSetArgs@#1}
\def\WideBottleSetArgs@#1#2#3#4#5{%
  \sa{32}{#1}\sa{33}{#2}\sa{20}{#3}\sa{21}{#4}\sa{22}{#5}%
  \WideBottleSetArgs@@}
\def\WideBottleSetArgs@@#1#2#3#4#5{%
  \sa{23}{#1}\sa{10}{#2}\sa{11}{#3}\sa{12}{#4}\sa{13}{#5}%
  \WideBottleSetArgs@@@}
\def\WideBottleSetArgs@@@#1#2#3#4{%
  \sa{00}{#1}\sa{01}{#2}\sa{02}{#3}\sa{03}{#4}%
  }
\makeatother

%R local WideBottle = 7/              !ga{33}                     \
%R                     |       !ga{32}       !ga{23}              |
%R                     |              !ga{22}       !ga{13}       |
%R                     |       !ga{21}       !ga{12}       !ga{03}|
%R                     |!ga{20}       !ga{11}       !ga{02}       |
%R                     |       !ga{10}       !ga{01}              |
%R                     \              !ga{00}                     /
%R WideBottle:tomp({zdef="WideBottle",    scale="7pt", meta="s"}):addcells():output()
%R WideBottle:tomp({zdef="WideBottleMed", scale="10pt", meta=""}):addcells():output()
\pu

\def\wibo #1{{       \WideBottleSetArgs{#1} \zha{WideBottle}        }}
\def\pwibo#1{{\left( \WideBottleSetArgs{#1} \zha{WideBottle} \right)}}

\def\wiBo #1{{       \WideBottleSetArgs{#1} \zha{WideBottleMed}        }}
\def\pwiBo#1{{\left( \WideBottleSetArgs{#1} \zha{WideBottleMed} \right)}}


% «SlantedHouse»  (to ".SlantedHouse")
% (find-LATEX "2021groth-tops-defs.tex" "SlantedHouse")
%
%L SlantedHouse_ts   = TCGSpec.new("32; 32,")
%L SlantedHouse_td_0 = TCGDims {h=15,  v=8,  q=15, crh=3.5,  crv=7, qrh=5}
%L SlantedHouse_td_2 = TCGDims {h=65, v=50,  q=15, crh=20,  crv=15, qrh=5}
%L SlantedHouse_tq   = TCGQ.newdsoa(SlantedHouse_td_0, SlantedHouse_ts,
%L                                  {tdef="SlantedHouseSmall", meta="1pt s"},
%L                                  "h ap")
%L SlantedHouse_tq:LRputs("!ga{L1} !ga{L2} !ga{L3}", "!ga{R1} !ga{R2}"):output()
%L
%L SlantedHouse_tq   = TCGQ.newdsoa(SlantedHouse_td_2, SlantedHouse_ts,
%L                                  {tdef="SlantedHouseBig", meta="1pt p"},
%L                                  "h v ap")
%L SlantedHouse_tq:LRputs("!ga{L1} !ga{L2} !ga{L3}", "!ga{R1} !ga{R2}"):output()
%
\pu
%
\def\SlantedHouseSetargs#1#2#3#4#5{
  \sa{L3}{#1}%
  \sa{L2}{#2}\sa{R2}{#3}%
  \sa{L1}{#4}\sa{R1}{#5}}
%
\def\SlantedHouse#1#2#3#4#5{{%
  \SlantedHouseSetargs{#1}{#2}{#3}{#4}{#5}
  \tcg{SlantedHouseSmall}}}
%
\def\SlantedHouseBig#1#2#3#4#5{{%
  \SlantedHouseSetargs{#1}{#2}{#3}{#4}{#5}
  \tcg{SlantedHouseBig}}}
%
\def\bsh#1#2#3#4#5{\left[ \SlantedHouse#1#2#3#4#5 \right]}
\def\bsht{\bsh01234}


% «ArtDecoN»  (to ".ArtDecoN")
% (find-LATEX "2021groth-tops-defs.tex" "ArtDecoN")

%L ArtDecoN_ts   = TCGSpec.new("33; 32,")
%L ArtDecoN_td_0 = TCGDims {h=15,  v=8,  q=15, crh=3.5,  crv=7, qrh=5}
%L ArtDecoN_td_1 = TCGDims {h=25, v=22,  q=15, crh=7.5,  crv=7, qrh=5}
%L ArtDecoN_td_2 = TCGDims {h=65, v=50,  q=15, crh=20,  crv=15, qrh=5}
%L ArtDecoN_td_3 = TCGDims {h=85, v=70,  q=15, crh=30,  crv=30, qrh=5}
%L ArtDecoN_tq   = TCGQ.newdsoa(ArtDecoN_td_0, ArtDecoN_ts,
%L                                  {tdef="ArtDecoNSmall", meta="1pt s"},
%L                                  "h ap")
%L ArtDecoN_tq:LRputs("!ga{L1} !ga{L2} !ga{L3}", "!ga{R1} !ga{R2} !ga{R3}"):output()
%L
%L ArtDecoN_tq   = TCGQ.newdsoa(ArtDecoN_td_1, ArtDecoN_ts,
%L                                  {tdef="ArtDecoNMed", meta="1pt s"},
%L                                  "h v ap")
%L ArtDecoN_tq:LRputs("!ga{L1} !ga{L2} !ga{L3}", "!ga{R1} !ga{R2} !ga{R3}"):output()
%L
%L ArtDecoN_tq   = TCGQ.newdsoa(ArtDecoN_td_2, ArtDecoN_ts,
%L                                  {tdef="ArtDecoNBig", meta="1pt"},
%L                                  "h v ap")
%L ArtDecoN_tq:LRputs("!ga{L1} !ga{L2} !ga{L3}", "!ga{R1} !ga{R2} !ga{R3}"):output()
%L
%L ArtDecoN_tq   = TCGQ.newdsoa(ArtDecoN_td_3, ArtDecoN_ts,
%L                                  {tdef="ArtDecoNBigg", meta="1pt"},
%L                                  "h v ap")
%L ArtDecoN_tq:LRputs("!ga{L1} !ga{L2} !ga{L3}", "!ga{R1} !ga{R2} !ga{R3}"):output()

%
\pu
%
\def\ArtDecoNSetargs#1#2#3#4#5#6{
  \sa{L3}{#1}\sa{R3}{#2}%
  \sa{L2}{#3}\sa{R2}{#4}%
  \sa{L1}{#5}\sa{R1}{#6}}
%
\def\ArtDecoN#1#2#3#4#5#6{{%
  \ArtDecoNSetargs{#1}{#2}{#3}{#4}{#5}{#6}
  \tcg{ArtDecoNSmall}}}
%
\def\ArtDecoNMed#1#2#3#4#5#6{{%
  \ArtDecoNSetargs{#1}{#2}{#3}{#4}{#5}{#6}
  \tcg{ArtDecoNMed}}}
%
\def\ArtDecoNBig#1#2#3#4#5#6{{%
  \ArtDecoNSetargs{#1}{#2}{#3}{#4}{#5}{#6}
  \tcg{ArtDecoNBig}}}
%
\def\ArtDecoNBigg#1#2#3#4#5#6{{%
  \ArtDecoNSetargs{#1}{#2}{#3}{#4}{#5}{#6}
  \tcg{ArtDecoNBigg}}}
%
\def\adn #1#2#3#4#5#6{       \ArtDecoN{#1}{#2}{#3}{#4}{#5}{#6}        }
\def\padn#1#2#3#4#5#6{\left( \ArtDecoN{#1}{#2}{#3}{#4}{#5}{#6} \right)}
\def\badn#1#2#3#4#5#6{\left[ \ArtDecoN{#1}{#2}{#3}{#4}{#5}{#6} \right]}

\def\padnmed #1#2#3#4#5#6{\left( \ArtDecoNMed {#1}{#2}{#3}{#4}{#5}{#6} \right)}
\def\padnbig #1#2#3#4#5#6{\left( \ArtDecoNBig {#1}{#2}{#3}{#4}{#5}{#6} \right)}
\def\padnbigg#1#2#3#4#5#6{\left( \ArtDecoNBigg{#1}{#2}{#3}{#4}{#5}{#6} \right)}





% ----------------------------------------

{\setlength{\parindent}{0em}
\footnotesize

Notes on Bert Lindenhovius's

``Grothendieck topologies on posets''


\url{https://arxiv.org/abs/1405.4408v2}

\url{https://arxiv.org/abs/1405.4408v2.pdf}

\ssk

These notes are at:

\url{http://angg.twu.net/LATEX/2020lindenhovius.pdf}

}


% (find-books "__cats/__cats.el" "lindenhovius-gtop")




%D diagram ??
%D 2Dx     100 +35 +60 +80
%D 2D  100 A0  B0  C0  D0
%D 2D      |   |   |   |
%D 2D  +30 A1  B1  C1  D1
%D 2D      |   |   |   |
%D 2D  +30 A2  B2  C2  D2
%D 2D
%D ren A0 A1 A2 ==> 3 2 1
%D ren B0 B1 B2 ==> {↓}3=\{3,2,1\} {↓}2=\{2,1\} {↓}1=\{1\}
%D ren C0 ==> \calD({↓}3)=\csm{\{3,2,1\},\\\{2,1\},\\\{1\},\\∅}
%D ren C1 ==>             \calD({↓}2)=\csm{\{2,1\},\\\{1\},\\∅}
%D ren C2 ==>                       \calD({↓}1)=\csm{\{1\},\\∅}
%D ren D0 ==> \calF({↓}3)=\Ftop
%D ren D1 ==> \calF({↓}3)=\Fmid
%D ren D2 ==> \calF({↓}1)=\Fbot
%D
%D (( A2 A1 -> A1 A0 ->
%D    B0 place B1 place B2 place
%D    C0 place C1 place C2 place
%D    D0 place D1 place D2 place
%D ))
%D enddiagram
%D
$$\pu
  \def\Ftop{\csm{\{\{3,2,1\}\},\\
                 \{\{3,2,1\},\{2,1\}\},\\
                 \{\{3,2,1\},\{2,1\},\{1\}\},\\
                 \{\{3,2,1\},\{2,1\},\{1\},∅\}}}
  \def\Fmid{\csm{\{\{2,1\}\},\\
                 \{\{2,1\},\{1\}\},\\
                 \{\{2,1\},\{1\},∅\}}}
  \def\Fbot{\csm{\{\{1\}\},\\
                 \{\{1\},∅\}}}
  \diag{??}
$$

%D diagram ??-2
%D 2Dx     100 +35 +60 +80
%D 2D  100 A0  B0  C0  D0
%D 2D      |   |   |   |
%D 2D  +30 A1  B1  C1  D1
%D 2D      |   |   |   |
%D 2D  +30 A2  B2  C2  D2
%D 2D
%D ren A0 A1 A2 ==> 3 2 1
%D ren B0 B1 B2 ==> {↓}3=\{3,2,1\} {↓}2=\{2,1\} {↓}1=\{1\}
%D ren C0 ==> \calD({↓}3)=\csm{{↓}3,\\{↓}2,\\{↓}1,\\∅}
%D ren C1 ==>        \calD({↓}3)=\csm{{↓}2,\\{↓}1,\\∅}
%D ren C2 ==>               \calD({↓}3)=\csm{{↓}1,\\∅}
%D ren D0 ==> \calF(\calD({↓}3))=\Ftop
%D ren D1 ==> \calF(\calD({↓}3))=\Fmid
%D ren D2 ==> \calF(\calD({↓}1))=\Fbot
%D
%D (( A2 A1 -> A1 A0 ->
%D  # B0 place B1 place B2 place
%D    C0 place C1 place C2 place
%D    D0 place D1 place D2 place
%D ))
%D enddiagram
%D
$$\pu
  \def\Ftop{\csm{{↑}{↓}3,\\
                 {↑}{↓}2,\\
                 {↑}{↓}1,\\
                 {↑}∅}}
  \def\Fmid{\csm{{↑}{↓}2,\\
                 {↑}{↓}1,\\
                 {↑}∅}}
  \def\Fbot{\csm{{↑}{↓}1,\\
                 {↑}∅}}
  \diag{??-2}
$$


\newpage


% 3. For $\calY = \cmat{\;\;\;\;\;\;▁3,\\1▁,▁1}$ we get:
% 
% %L ArtDecoNQ_ts   = TCGSpec.new("33; 32, ", ".??",".?.")
% %L ArtDecoNQ_ts:mp({zdef="ArtDecoNQ", scale="12pt", meta=""}):addlrs():output()
% \pu
% %
% \def\mygrotop{{
%   \padnbig
%   {\badn?·??11}  {\badn·1·?·1}
%   {\badn··?·1·}  {\badn···?·1}
%   {\badn····1·}  {\badn·····1}
%   }}
% \def\mygrotopz{{
%   \padnbigg
%   {\wibo{{32}·    ·   {21}{22}·    ·   {11}{12}·    ·   ·   ·   ·   }}
%   {\wibo{·   ·    ·   ·   ·   ·    ·   ·   ·   ·    ·   {01}{02}{03}}}
%   {\wibo{·   ·    {20}·   ·   ·    {10}·   ·   ·    ·   ·   ·   ·   }}
%   {\wibo{·   ·    ·   ·   ·   ·    ·   ·   ·   ·    ·   {01}{02}·   }}
%   {\wibo{·   ·    ·   ·   ·   ·    {10}·   ·   ·    ·   ·   ·   ·   }}
%   {\wibo{·   ·    ·   ·   ·   ·    ·   ·   ·   ·    ·   {01}·   ·   }}
%   }}
% \def\mysubzha    {\wiBo{{32}{33} {20}··· ···· {00}··{03}}}
% \def\mynucleus   {\left( \zha{ArtDecoNQ} \right)_{(·)^*}}
% \def\mycongruence{\left( \zha{ArtDecoNQ} \right)_{(∼)}}
% \def\mysetofsieves{\cmat{\;\;\;\;\;\;▁3,\\1▁,▁1}}
% %
% $$\setlength{\arraycolsep}{0pt}
%   \begin{array}{ccc}
%   \mynucleus && \mysubzha \\
%      &\mysetofsieves& \\
%   \mycongruence && \scalebox{0.8}{$\mygrotop$} \\
%   \end{array}
% $$


% (lindp 64 "B.25")
% (lind     "B.25")
% (find-grtopsonposetspage 64 "Proposition B.25.")
% (find-grtopsonposetstext 64 "Proposition B.25.")



$$
  \begin{array}{crll}
    (\calY↦(·)^*) & \calS^* &= \calY\to \calS \\
    (\calY↦H')    & H'      &= \{\calS\in H:\calS=(\calY\to\calS)\}=\{(\calY\to\calS):\calS∈H\} \\
    (\calY↦∼)     & ∼       &= \{(\calR,\calS)∈H^2:\calR∩\calY=\calS∩\calY\} \\
    (\calY↦J)     & J(u)    &= \{\calS\inΩ(u):u\in (\calY\to \calS)\} \\
  \end{array}
$$




and we will define some operations, with names like $(J \mapsto
\calY)$ and $(\calY \mapsto)$, that ``convert'' a $J$ to a $\calY$ and
vice-versa. We will define all these conversions first, then get some
visual intuition about how they work, and only then discuss which
composites of them are identities.

This section is about how to understand the ``essence'' of some
sections of \cite{Lindenhovius} from some examples. The precise
meaning of this ``essence'' will be discussed at the end.

% (find-grtopsonposetspage 48 "B Grothendieck topologies and Locale Theory")





\newpage

% «double-negation-old»  (to ".double-negation-old")
% (grcp 28 "double-negation")
% (grc     "double-negation")

{\bf The double negation topology:}

%L ArtDecoNQ_ts   = TCGSpec.new("33; 32, ", ".??",".??")
%L ArtDecoNQ_ts   = TCGSpec.new("33; 32, ", ".??",".?.")
%L ArtDecoNQ_ts:mp({zdef="WB_notnot", scale="12pt", meta=""}):addlrs():output()
\pu

%L ArtDecoNQ_ts   = TCGSpec.new("33; 32, ", ".??",".??")
%L ArtDecoNQ_ts:mp({zdef="ArtDecoNQ", scale="12pt", meta=""}):addlrs():output()
\pu

\def\mygrotop{{
  \padnbig
  {\badn?·??11}  {\badn·?·?·1}
  {\badn··?·1·}  {\badn···?·1}
  {\badn····1·}  {\badn·····1}
  }}
\def\mygrotopz{{
  \padnbigg
  {\wibo{{32}·    ·   {21}{22}·    ·   {11}{12}·    ·   ·   ·   ·   }}
  {\wibo{·   ·    ·   ·   ·   ·    ·   ·   ·   ·    ·   {01}{02}{03}}}
  {\wibo{·   ·    {20}·   ·   ·    {10}·   ·   ·    ·   ·   ·   ·   }}
  {\wibo{·   ·    ·   ·   ·   ·    ·   ·   ·   ·    ·   {01}{02}·   }}
  {\wibo{·   ·    ·   ·   ·   ·    {10}·   ·   ·    ·   ·   ·   ·   }}
  {\wibo{·   ·    ·   ·   ·   ·    ·   ·   ·   ·    ·   {01}·   ·   }}
  }}
\def\mysubzha    {\wiBo{·{33} {20}··· ···· {00}··{03}}}
\def\mynucleus   {\left( \zha{ArtDecoNQ} \right)_{(·)^*}}
\def\mycongruence{\left( \zha{ArtDecoNQ} \right)_{(∼)}}

$$\begin{array}{ccc}
  \mynucleus && \mysubzha \\
  \\
     &\{1▁,▁1\}& \\
  \\
  \mycongruence && \mygrotop \\
  \end{array}
$$


$$\scalebox{0.8}{$\mygrotopz$}
  =\mygrotop
$$



From \cite{Lindenhovius}, proposition B.8, page 51:
%
% (find-grtopsonposetspage 51 "Proposition B.8.")
% (find-grtopsonposetstext 51 "Proposition B.8.")
% (lindp 51 "B.8")
% (lind     "B.8")
%
%D diagram B.8
%D 2Dx     100  +45  +35 +10
%D 2D  100 A0   B0   C0  C1  D0
%D 2D      ||   ||    |  |
%D 2D  +20 A1   B1   C2  C3  D1
%D 2D
%D 2D  +15      E0   F0  F1  G0
%D 2D           ||    |  |
%D 2D  +20      E1   F2  F3  G1
%D 2D
%D ren A0 A1       ==> \NucDP \GP
%D ren B0 B1       ==> j:\DP→\DP J∈\GP
%D ren C0 C1 C2 C3 ==> j j_J J_j J
%D ren E0 E1       ==> (·)^*:H→H J⊆Ω
%D ren F0 F1 F2 F3 ==> (·)^* (·)^* J J
%D
%D (( A0 A1 -> sl_
%D    A0 A1 <- sl^
%D    B0 B1 |-> sl_
%D    B0 B1 <-| sl^
%D    C0 C2 |->
%D    C1 C3 <-|
%D    E0 E1 |-> sl_
%D    E0 E1 <-| sl^
%D    F0 F2 |->
%D    F1 F3 <-|
%D    newnode: D0 at: @C1+v(60,0)
%D    newnode: D1 at: @C3+v(60,0)
%D    D0 .TeX= j_J(U):=\setofst{p∈\bfP}{U∩{↓}p∈J(p)} place
%D    D1 .TeX= J_j(p):=\setofst{S∈\Ddp}{p∈j(S)} place
%D    newnode: G0 at: @F1+v(60,0)
%D    newnode: G1 at: @F3+v(60,0)
%D    G0 .TeX= \calS^*:=\setofst{u∈H}{\calS∩{↓}u∈J(u)} place
%D    G1 .TeX= J(u):=\setofst{\calS∈Ω(u)}{u∈\calS^*} place
%D ))
%D enddiagram
%D
$$\pu
  \diag{B.8}
$$

From \cite{Lindenhovius}, proposition B.12, page 55:
%
% (find-grtopsonposetspage 55 "Proposition B.12")
% (find-grtopsonposetstext 55 "Proposition B.12")
%
%D diagram B.12
%D 2Dx     100  +45  +35 +10
%D 2D  100 A0   B0   C0  C1  D0
%D 2D      ||   ||    |  |
%D 2D  +20 A1   B1   C2  C3  D1
%D 2D
%D 2D  +15      E0   F0  F1  G0
%D 2D           ||    |  |
%D 2D  +20      E1   F2  F3  G1
%D 2D
%D ren A0 A1       ==> \NucDP \Sub(\DP)^\op
%D ren B0 B1       ==> j:\DP→\DP M⊆\DP
%D ren C0 C1 C2 C3 ==> j j_M M_j J
%D ren E0 E1       ==> (·)^*:H→H H'⊆H
%D ren F0 F1 F2 F3 ==> (·)^* (·)^* H' H'
%D
%D (( A0 A1 -> sl_
%D    A0 A1 <- sl^
%D    B0 B1 |-> sl_
%D    B0 B1 <-| sl^
%D    C0 C2 |->
%D    C1 C3 <-|
%D    E0 E1 |-> sl_
%D    E0 E1 <-| sl^
%D    F0 F2 |->
%D    F1 F3 <-|
%D    newnode: D0 at: @C1+v(60,0)
%D    newnode: D1 at: @C3+v(60,0)
%D    D0 .TeX= j_M(a):=\bigwedge\setofst{m∈M}{a≤m} place
%D    D1 .TeX= M_j:=\setofst{x∈L}{j(x)=x} place
%D    newnode: G0 at: @F1+v(60,0)
%D    newnode: G1 at: @F3+v(60,0)
%D    G0 .TeX= \calR^*:=\bigwedge\setofst{\calS∈H'}{\calR≤\calS} place
%D    G1 .TeX= H':=\setofst{\calR∈H}{\calR^*=\calR} place
%D ))
%D enddiagram
%D
$$\pu
  \diag{B.12}
$$



From \cite{Lindenhovius}, proposition B.23, page 63:
%
% (find-grtopsonposetspage 63 "Proposition B.23.")
% (find-grtopsonposetstext 63 "Proposition B.23.")
%
%D diagram B.23
%D 2Dx     100  +45  +35 +10
%D 2D  100 A0   B0   C0  C1  D0
%D 2D      ||   ||    |  |
%D 2D  +20 A1   B1   C2  C3  D1
%D 2D
%D 2D  +15      E0   F0  F1  G0
%D 2D           ||    |  |
%D 2D  +20      E1   F2  F3  G1
%D 2D
%D ren A0 A1       ==> \NucDP \ConDP
%D ren B0 B1       ==> j:\DP→\DP θ⊆\DP^2
%D ren C0 C1 C2 C3 ==> j j_θ θ_j θ
%D ren E0 E1       ==> (·)^*:H→H ∼\;⊆H×H
%D ren F0 F1 F2 F3 ==> (·)^* (·)^* ∼ ∼
%D
%D (( A0 A1 -> sl_
%D    A0 A1 <- sl^
%D    B0 B1 |-> sl_
%D    B0 B1 <-| sl^
%D    C0 C2 |->
%D    C1 C3 <-|
%D    E0 E1 |-> sl_
%D    E0 E1 <-| sl^
%D    F0 F2 |->
%D    F1 F3 <-|
%D    newnode: D0 at: @C1+v(60,0)
%D    newnode: D1 at: @C3+v(60,0)
%D    D0 .TeX= j_θ(a):=\bigvee\setofst{b∈\DP}{aθb} place
%D    D1 .TeX= θ_j:=\setofst{(a,b)∈\DP^2}{j(a)=j(b)} place
%D    newnode: G0 at: @F1+v(60,0)
%D    newnode: G1 at: @F3+v(60,0)
%D    G0 .TeX= \calS^*:=\bigvee\setofst{\calR∈H}{\calR∼\calS} place
%D    G1 .TeX= ∼\;:=\setofst{(\calR,\calS)∈H^2}{\calR^*=\calS^*} place
%D ))
%D enddiagram
%D
$$\pu
  \diag{B.23}
$$



\newpage

From \cite{Lindenhovius}, theorem B.25, page 64...
%
% (lindp 64 "B.25")
% (lind     "B.25")
% (find-grtopsonposetspage 64 "Proposition B.25.")
% (find-grtopsonposetstext 64 "Proposition B.25.")
%
%D diagram ??
%D 2Dx     100  +60 +30  +25 +20  +25
%D 2D  100 A0 - A1  B0 - B1  C0 - C1 
%D 2D      |     |  |     |  |     | 
%D 2D  +25 A2 - A3  B2 - B3  C2 - C3 
%D 2D
%D ren A0 A1 A2 A3 ==> \NucDP \Sub(\DP)^\op \ConDP \GP
%D ren B0 B1 B2 B3 ==> j M θ J
%D ren C0 C1 C2 C3 ==> (·)^* H' ∼ J
%D
%D (( A0 A1 -> .plabel= a j↦\calM_j
%D    A0 A2 -> .plabel= l j↦θ_j
%D    A0 A3 -> .plabel= m j↦J_j
%D    A1 A3 -> .plabel= r \calM↦J_\calM
%D    A2 A3 -> .plabel= b θ↦J_θ
%D
%D    B0 B1 |->
%D    B0 B2 |->
%D    B0 B3 |->
%D    B1 B3 |->
%D    B2 B3 |->
%D
%D    C0 C1 |-> sl^
%D    C0 C1 <-| sl_
%D    C0 C2 |-> sl^
%D    C0 C2 <-| sl_
%D    C0 C3 |-> sl^
%D    C0 C3 <-| sl_
%D    C1 C3 |-> sl^
%D    C1 C3 <-| sl_
%D    C2 C3 |-> sl^
%D    C2 C3 <-| sl_
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$


\def\M{\mathcal{M}}
\def\D{\mathcal{D}}
\def\G{\mathcal{G}}
\def\P{\mathbf{P}}
\def\down{{↓}}

$$
  \begin{array}{rll}
    J_\M(p) & = \{S\in\D(\down p):\forall M\in\M(S\subseteq M\implies p\in M)\}; & \M\in\Sub(\D(\P))  \\
    J_j(p) & = \{S\in\D(\down p):p\in j(S)\}; & j\in\Nuc(\D(\P))  \\
    J_\theta(p) & = \{S\in\D(\down p):S\theta\down p\}; & \theta\in\Con(\D(\P)) \\
    j_J(A) & =  \{p\in\P:A\cap\down p\in J(p)\}; &J\in\G(\P)\\
    j_\theta(A)  & =  \bigcup\{B\in\D(\P):B\theta A\}; & \theta\in\Con(\D(\P))\\
    j_\M(A) & =  \bigcap\{A\in\M:A\subseteq M\}; & \M\in\Sub(\D(\P)) \\
    \theta_j& =  \ker j=\{(A,B)\in\D(\P)^2:j(A)=j(B)\}; & j\in\Nuc(\D(\P))\\
    \theta_J & = \{(A,B)\in\D(\P)^2:\forall p\in\P(A\cap\down p\in J(p)\Longleftrightarrow B\cap\down p\in J(p))\}; &J\in\G(\P) \\
    \M_j & =  \{A\in\D(\P):j(A)=A\}=j[\D(\P)]; & j\in\Nuc(\D(\P))\\
    \M_J & =  \{A\in\D(\P):\forall p\in\P(A\cap\down p\in J(p)\implies p\in A)\}; &J\in\G(\P) \\
  \end{array}
$$



From \cite{Lindenhovius}, theorem C.4, page 74...
%
$$
  \begin{array}{crll}
        (X↦J) & J_X(p)   &=  \{S\in\D(\down p):p\in X\to S\} \\
    (\calY↦J) & J(u)     &=  \{\calS\inΩ(u):u\in (\calY\to \calS)\} \\
    \\
            (X↦j) & j_X(A)  &=  X\to A \\
    (\calY↦(·)^*) & \calS^* &=  \calY\to \calS \\
    \\
        (X↦θ) & \theta_X &= \ker i_X^{-1}= \{(A,B)\in\D(\P)^2:A\cap X=B\cap X\} \\
    (\calY↦∼) & ∼ &= \{(\calR,\calS)∈H^2:\calR∩\calY=\calS∩\calY\} \\
    \\
        (X↦\M) & \M_X     &=  \{A\in\D(\P):A=X\to A\}=\{X\to A:A\in\D(\P)\} \\
    (\calY↦H') & H'       &=  \{\calS\in H:\calS=(\calY\to\calS)\}=\{(\calY\to\calS):\calS∈H\} \\
  \end{array}
$$
%
% (lindp 74 "C.4")
% (lind     "C.4")
% (find-grtopsonposetspage 74 "Theorem C.4")
% (find-grtopsonposetstext 74 "Theorem C.4")
%
%D diagram ??
%D 2Dx     100 +30 +30 +30 +15 +15 +20 +15 +15
%D 2D  100 A0 ---- A1  B0 ---- B1  C0 ---- C1 
%D 2D      |  \  /  |  |  \  /  |  |  \  /  | 
%D 2D  +15 |   A4   |  |   B4   |  |   C4   | 
%D 2D      |  /  \  |  |  /  \  |  |  /   \ | 
%D 2D  +15 A2 ---- A3  B2 ---- B3  C2 ---- C3 
%D 2D
%D ren A0 A1 A2 A3 A4 ==> \NucDP \Sub(\DP)^\op \ConDP \GP \Pts(\bfP)^\op
%D ren B0 B1 B2 B3 B4 ==> j M θ J ?
%D ren C0 C1 C2 C3 C4 ==> (·)^* H' ∼ J \calY
%D
%D (( A0 A1 -> .plabel= a j↦\calM_j
%D    A0 A2 -> .plabel= l j↦θ_j
%D  # A0 A3 -> .plabel= m j↦J_j
%D    A1 A3 -> .plabel= r \calM↦J_\calM
%D    A2 A3 -> .plabel= b θ↦J_θ
%D    A4 A0 ->
%D    A4 A1 ->
%D    A4 A2 ->
%D    A4 A3 ->
%D
%D    B0 B1 |->
%D    B0 B2 |->
%D  # B0 B3 |->
%D    B1 B3 |->
%D    B2 B3 |->
%D    B4 B0 |->
%D    B4 B1 |->
%D    B4 B2 |->
%D    B4 B3 |->
%D
%D    C0 C1 |-> sl^
%D    C0 C1 <-| sl_
%D    C0 C2 |-> sl^
%D    C0 C2 <-| sl_
%D  # C0 C3 |-> sl^
%D  # C0 C3 <-| sl_
%D    C1 C3 |-> sl^
%D    C1 C3 <-| sl_
%D    C2 C3 |-> sl^
%D    C2 C3 <-| sl_
%D    C4 C0 |->
%D    C4 C1 |->
%D    C4 C2 |->
%D    C4 C3 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$


\newpage

% (fooi "\\cap" "∩" "\\down" "{↓}" "\\subseteq" "⊆" "\\in" "∈" "\\forall" "∀" "\\theta" "θ")

$$
  \begin{array}{crll}
    (\M↦J) & J_\M(p) & = \{S∈\D({↓} p):∀ M∈\M(S⊆ M\implies p∈ M)\}  \\
    (H'↦J) & J(u)    & = \{\calS∈Ω(u):∀\calT∈H'.\;(\calS⊆\calT\implies u∈\calT)\}  \\
    \\
    (j↦J)     & J_j(p) & = \{S∈\D({↓} p):p∈ j(S)\}               \\
    ((·)^*↦J) & J(u)   & = \{\calS∈Ω(u):u∈\calS^*\}               \\
    \\
    (θ↦J) & J_θ(p) & = \{S∈\D({↓} p):Sθ{↓} p\} \\
    (∼↦J) & J(u)   & = \{\calS∈Ω(u):\calS∼{↓}u\} \\
    \\
    (J↦j)     & j_J(A)  & =  \{p∈\P:A∩{↓} p∈ J(p)\}          \\
    (J↦(·)^*) & \calS^* & =  \{u∈D:\calS∩{↓}u∈J(u)\}          \\
    \\
    (θ↦j)     & j_θ(A)  & =  \bigcup\{B∈\D(\P):Bθ A\}\\
    (∼↦(·)^*) & \calS^* & =  \bigcup\{\calR∈H:\calR∼\calS\}\\
    \\
    (\M↦j)     & j_\M(A) & =  \bigcap\{A∈\M:A⊆ M\} \\
    (H'↦(·)^*) & \calS^* & =  \bigcap\{\calT∈H':\calS⊆\calT\} \\
    \\
    (j↦θ)     & θ_j & =  \ker j=\{(A,B)∈\D(\P)^2:j(A)=j(B)\}\\
    ((·)^*↦∼) & ∼ & =  \ker j=\{(\calR,\calS)∈H^2:\calR^*=\calS^*\}\\
    \\
    (J↦θ) & θ_J & = \{(A,B)∈\D(\P)^2:∀ p∈\P(A∩{↓} p∈ J(p) \Leftrightarrow B∩{↓} p∈ J(p))\} \\
    (J↦∼) & ∼   & = \{(\calR,\calS)∈H^2:∀ u∈D.\;(\calR∩{↓}u∈J(u) \Leftrightarrow \calS∩{↓}u∈ J(u))\} \\
    \\
    (j↦\M)     & \M_j & =  \{A∈\D(\P):j(A)=A\}=j[\D(\P)] \\
    ((·)^*↦H') & H'   & =  \{\calS∈H:\calS^*=\calS\}=H^* \\
    \\
    (J↦\M)     & \M_J & =  \{A∈\D(\P):∀ p∈\P(A∩{↓} p∈ J(p) ⇒ p∈ A)\} \\
    (J↦H')     & H'   & =  \{\calS∈H:∀ u∈D.\; (\calS∩{↓}u∈J(u) ⇒ u∈\calS)\} \\
  \end{array}
$$

\newpage


%D diagram ??
%D 2Dx     100 +15 +20 +15 +15 +20 +15 +15
%D 2D  100         B0 ---- B1  C0 ---- C1  
%D 2D              |  \     |  |  \  /  |
%D 2D  +15 A4      |        |  |   C4   |
%D 2D         \    |      \ |  |  /   \ |
%D 2D  +15     A3  B2 ---- B3  C2 ---- C3
%D 2D
%D ren          A3 A4 ==>            J \calY
%D ren B0 B1 B2 B3    ==> (·)^* H' ∼ J
%D ren C0 C1 C2 C3 C4 ==> (·)^* H' ∼ J \calY
%D
%D (( A4 A3 |-> sl^
%D    A4 A3 <-| sl_
%D    
%D    B0 B1 |-> sl^
%D    B0 B1 <-| sl_
%D    B0 B2 |-> sl^
%D    B0 B2 <-| sl_
%D    B0 B3 |-> sl^
%D    B0 B3 <-| sl_
%D    B1 B3 |-> sl^
%D    B1 B3 <-| sl_
%D    B2 B3 |-> sl^
%D    B2 B3 <-| sl_
%D
%D    C0 C1 |-> sl^
%D    C0 C1 <-| sl_
%D    C0 C2 |-> sl^
%D    C0 C2 <-| sl_
%D  # C0 C3 |-> sl^
%D  # C0 C3 <-| sl_
%D    C1 C3 |-> sl^
%D    C1 C3 <-| sl_
%D    C2 C3 |-> sl^
%D    C2 C3 <-| sl_
%D    C4 C0 |->
%D    C4 C1 |->
%D    C4 C2 |->
%D    C4 C3 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

$$
  \begin{array}{crll}
    (\calY↦J)     & J(u)    &= \{\calS∈Ω(u):\calY∩{↓}u⊆\calS\} \\
    (J↦\calY)     & \calY   &= \{u∈D:J(u)=\{{↓}u\}\} \\
    \\
    ((·)^*↦H') & H'      & =  \{\calS∈H:\calS^*=\calS\}=H^* \\
    (H'↦(·)^*) & \calS^* & =  \bigcap\{\calT∈H':\calS⊆\calT\} \\
    \\
    ((·)^*↦∼) & ∼       & =  \{(\calR,\calS)∈H^2:\calR^*=\calS^*\}\\
    (∼↦(·)^*) & \calS^* & =  \bigcup\{\calR∈H:\calR∼\calS\}\\
    \\
    ((·)^*↦J) & J(u)    & = \{\calS∈Ω(u):u∈\calS^*\}               \\
    (J↦(·)^*) & \calS^* & = \{u∈D:\calS∩{↓}u∈J(u)\}          \\
    \\
    (H'↦J)    & J(u)    & = \{\calS∈Ω(u):∀\calT∈H'.\;(\calS⊆\calT ⇒ u∈\calT)\}  \\
    (J↦H')    & H'      & = \{\calS∈H:∀ u∈D.\; (\calS∩{↓}u∈J(u) ⇒ u∈\calS)\} \\
    \\
    (∼↦J)     & J(u) & = \{\calS∈Ω(u):\calS∼{↓}u\} \\
    (J↦∼)     & ∼    & = \{(\calR,\calS)∈H^2:∀ u∈D.\;(\calR∩{↓}u∈J(u) ↔ \calS∩{↓}u∈ J(u))\} \\
    \\
    (\calY↦(·)^*) & \calS^* &= \calY\to \calS \\
    (\calY↦H')    & H'      &= \{\calS\in H:\calS=(\calY\to\calS)\}=\{(\calY\to\calS):\calS∈H\} \\
    (\calY↦∼)     & ∼       &= \{(\calR,\calS)∈H^2:\calR∩\calY=\calS∩\calY\} \\
    (\calY↦J)     & J(u)    &= \{\calS\inΩ(u):u\in (\calY\to \calS)\} \\
  \end{array}
$$




These are some other constructions that I am starting to translate...

$$\begin{array}{rcl}
        (·)^* &:& \Downs(\Opens(B)) → \Downs(\Opens(B)) \\
        (·)^* &:& \Downs(\Opens(X)) → \Downs(\Opens(X)) \\
         Ω(U) &=& \Downs(\Opens(U)) \\
     \Jcan(U) &=& \setofst{\calS∈Ω(U)}{\calS^*={↓}U} \\
  J(U)(\calS) &=& \calS^* \\
  \\
        (·)^* &:& \Downs(X) → \Downs(X) \\
         Ω(u) &=& \Downs({↓}u) \\
     \Jcan(u) &=& \setofst{\calS∈Ω(u)}{\calS^*={↓}u} \\
  J(u)(\calS) &=& \calS^* \\
  \\
   J_j(p) &:=& \setofst{S∈\calD({↓}p)}{p∈j(S)} \\
     J(U) &:=& \setofst{\calS∈\Downs({↓}U)}{U∈\calS^*} \\
  \\
   j_J(U) &:=& \setofst{p∈𝐛P}{p∈j(S)} \\
  \calS^* &:=& \setofst{V∈\Opens(B)}{\calS∩{↓}V∈J(V)} \\
  \\
                       𝐛P &≡& B \\
                \calD(𝐛P) &≡& \Opens(B) \\
  \mathrm{Nuc}(\calD(𝐛P)) &≡& \setofst{ (·)^*: \Opens(B)→\Opens(B) }{ (·)^* \text{ is a J-operator}} \\
                \calG(𝐛P) &≡& \setofst{ J⊆Ω_{\Set^{\Opens(B)^\op}} }{ J \text{ is a Gr.top.}} \\
  \end{array}
$$


% \section{Mac Lane/Moerdijk}
% 
% \cite[section V.1, page 38]{MacLaneMoerdijk}
% 
% % (find-books "__cats/__cats.el" "maclane-moerdijk")
% % (find-maclanemoerdijkpage (+ 11 38) "Sieve on C =")
% % (find-maclanemoerdijkpage (+ 11 38) "Omega(C) =")
% % (find-maclanemoerdijkpage (+ 11 38) "t(C)")
% % (find-maclanemoerdijkpage (+ 11 110) "Definition 1. A Grothendieck Topology")
% 
% $$\begin{array}{rcl}
%   \text{Sieve on $C$} &=& \text{Subfunctor of $\Hom_\catC(-,C)$} \\
%   Ω(C) &=& \setofst{S}{\text{$S$ is a sieve on $C$ in $\catC$}} \\
%   t(C) &=& \setofst{h}{\cod(h) = C} \\
%   \end{array}
% $$
% 
% And if $g:C'→C$ is an arrow in $\catC$ then:
% %
% $$\begin{array}{rrcl}
%   (-)·g: &Ω(C)& →& Ω(C')\\
%          & S  & ↦& S·g = \setofst{h}{g∘h∈S} \\
%   \end{array}
% $$
% 
% %D diagram ??
% %D 2Dx     100  +25 +30
% %D 2D  100 A0 - A1  C0
% %D 2D      |     |   |
% %D 2D  +20 A2 - A3  C1
% %D 2D
% %D 2D  +20 B0 - B1
% %D 2D
% %D ren A0 A1 A2 A3 ==> C Ω(C) C' Ω(C')
% %D ren C0 C1 ==> S S·g
% %D ren B0 B1 ==> \catC^\op \Set
% %D
% %D (( A0 A1 |->
% %D    A0 A2 <- .plabel= l g
% %D    A1 A3 -> .plabel= r (-)·g
% %D    A0 A3 harrownodes nil 20 nil |->
% %D    A2 A3 |->
% %D    newnode: B0' at: @B0+v(0,-8) .TeX= \catC place
% %D    B0 B1 ->
% %D    C0 C1 |->
% %D ))
% %D enddiagram
% %D
% $$\pu
%   \diag{??}
% $$
% 


\newpage

2021jun20:

%D diagram ??
%D 2Dx     100  +40
%D 2D  100 A0 - A1
%D 2D      |  /
%D 2D  +40 A2 - A3
%D 2D
%D ren A0 A1 A2 A3 ==> 𝓨 \nuc J j
%D
%D (( A0 A1 |-> sl^ .plabel= a C.4.2
%D    A0 A1 <--| sl_
%D    A0 A2 |-> sl_ .plabel= l \sm{2.8,\\C.4.1}
%D    A0 A2 <-| sl^ .plabel= r 2.9
%D    A2 A1 <-> .plabel= m \sm{B.8,\\B.25}
%D    A2 A3 <-->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$




Definition C.2:
%
% (lindp 64 "B.25")
% (linda    "B.25")
%
$$\begin{array}{rcl}
  X→Y &=& \bigcup \setofsc{A∈\DP}{A∩X⊆Y} \\
  𝓨→𝓩 &=& \bigcup \setofst{𝓢∈H}{𝓢∩𝓨⊆𝓩} \\
        &=& \bigcup \setofst{𝓢∈H}{𝓢 ⊆ 𝓨 →_M 𝓩} \\
        &=& \bigcup \setofst{𝓢∈H}{𝓢 ⊆ \Int(𝓨 →_M 𝓩)} \\
        &=&                             \Int(𝓨 →_M 𝓩) \\
  \end{array}
$$


2.8, C.4.1:
%
% (lindp 11 "2.8")
% (linda    "2.8")
% (lindp 74 "C.4")
% (linda    "C.4")
%
$$\begin{array}{lcr}
  J_X(p)      &=&                          \setofsc{S∈\Ddp}{X∩{↓}p⊆S} \\
  J_X         &=&                 λp∈𝐏. \; \setofsc{S∈\Ddp}{X∩{↓}p⊆S} \\
  (X↦J)(X)    &=&                 λp∈𝐏. \; \setofsc{S∈\Ddp}{X∩{↓}p⊆S} \\
  (X↦J)       &=& λX∈\Pts(𝐏). \; λp∈𝐏. \; \setofsc{S∈\Ddp}{X∩{↓}p⊆S} \\
         [5pt]
  J_X(p)      &=&                          \setofsc{S∈\Ddp}{p∈X→S} \\
  J_X         &=&                 λp∈𝐏. \; \setofsc{S∈\Ddp}{p∈X→S} \\
  (X↦J)(X)    &=&                 λp∈𝐏. \; \setofsc{S∈\Ddp}{p∈X→S} \\
  (X↦J)       &=& λX∈\Pts(𝐏). \; λp∈𝐏. \; \setofsc{S∈\Ddp}{p∈X→S} \\
         [5pt]
  (𝓨↦J)      &=& λ𝓨∈\Pts(𝐃_0). \; λu∈𝐃_0. \; \setofst{𝓢∈Ω(u)}{u∈𝓨→𝓢} \\
              &=& λ𝓨∈\Pts(𝐃_0). \; λu∈𝐃_0. \; \setofst{𝓢∈Ω(u)}{{↓}u⊆𝓨→𝓢} \\
              &=& λ𝓨∈\Pts(𝐃_0). \; λu∈𝐃_0. \; \setofst{𝓢∈Ω(u)}{{↓}u∩𝓨⊆𝓢} \\
              &=& λ𝓨∈\Pts(𝐃_0). \; λu∈𝐃_0. \; \setofst{𝓢∈Ω(u)}{𝓨∩{↓}u⊆𝓢} \\
  \end{array}
$$

% 2.8:
% %
% % (lindp 11 "2.8")
% % (linda    "2.8")
% %
% $$\begin{array}{lcr}
%   J_X(p)   &=&                                 \setofsc{S∈\Ddp}{X∩{↓}p⊆S} \\
%   J_X      &=&                        λp∈𝐏. \; \setofsc{S∈\Ddp}{X∩{↓}p⊆S} \\
%   (X↦J)(X) &=&                        λp∈𝐏. \; \setofsc{S∈\Ddp}{X∩{↓}p⊆S} \\
%   (X↦J)    &=&          λX∈\Pts(𝐏).\; λp∈𝐏. \; \setofsc{S∈\Ddp}{X∩{↓}p⊆S} \\
%   (𝓨↦J)   &=& λ𝓨∈\Pts(𝐃_0).\; λu∈𝐃_0. \; \setofst{𝓢∈Ω(u)}{𝓨∩{↓}u⊆𝓢} \\
%   \end{array}
% $$

2.9:
%
% (lindp 12 "2.9")
% (linda    "2.9")
%
$$\begin{array}{lcr}
  X_J       &=&                   \setofsc{p∈𝐏}{J(p)=\{{↓}p\}} \\
  (J↦X)(J)  &=&                   \setofsc{p∈𝐏}{J(p)=\{{↓}p\}} \\
  (J↦X)     &=& λJ∈\G(𝐏). \;      \setofsc{p∈𝐏}{J(p)=\{{↓}p\}} \\
  (J↦𝓨)    &=& λJ∈\GrTops(𝐃). \; \setofst{u∈𝐃_0}{J(u)=\{{↓}u\}} \\
  \end{array}
$$

B.8, B.25:
%
% (lindp 64 "B.25")
% (linda    "B.25")
%
$$\begin{array}{lcr}
  J_j(p)      &=&                                \setofsc{S∈\Ddp}{p∈j(S)} \\
  J_j         &=&                       λp∈𝐏. \; \setofsc{S∈\Ddp}{p∈j(S)} \\
  (j↦J)(j)    &=&                       λp∈𝐏. \; \setofsc{S∈\Ddp}{p∈j(S)} \\
  (j↦J)       &=&      λj∈\Nuc(\DP). \; λp∈𝐏. \; \setofsc{S∈\Ddp}{p∈j(S)} \\[5pt]
  (\nuc↦J)    &=& λ\nuc∈\Nucs(H). \; λu∈𝐃_0. \; \setofst{𝓢∈Ω(u)}{u∈𝓢^*} \\
  \\
  j_J(A)      &=&                                \setofsc{p∈𝐏}{A∩{↓}p∈J(p)} \\
  j_J         &=&                     λA∈\DP. \; \setofsc{p∈𝐏}{A∩{↓}p∈J(p)} \\
  (J↦j)(J)    &=&                     λA∈\DP. \; \setofsc{p∈𝐏}{A∩{↓}p∈J(p)} \\
  (J↦j)       &=&       λJ∈\G(𝐏). \; λA∈\DP. \; \setofsc{p∈𝐏}{A∩{↓}p∈J(p)} \\[5pt]
  (J↦\nuc)    &=& λJ∈\GrTops(𝐃). \; λ𝓢∈H. \; \setofst{u∈𝐃_0}{𝓢∩{↓}u∈J(u)} \\
  \end{array}
$$


C.4.2:
%
% (lindp 74 "C.4")
% (linda    "C.4")
%
$$\begin{array}{lcr}
  j_X(A)    &=&                           X→A \\
  j_X       &=&                λA∈\DP. \; X→A \\
  (X↦j)(X)  &=&                λA∈\DP. \; X→A \\
  (X↦j)     &=& λX∈\Pts(𝐏). \; λA∈\DP. \; X→A \\[5pt]
  (𝓨↦\nuc) &=& λ𝓨∈\Pts(𝐃_0). \; λ𝓢∈H. \; 𝓨→𝓢 \\
  \end{array}
$$


\newpage

% https://mail.google.com/mail/ca/u/0/#sent/QgrcJHrtvWmlxhvCBggGFXMszBggGkmQmdv

My hypothesis about C1:

$$\begin{array}{lcr}
  X_j       &=& \setofsc{p∈𝐏}{j({↓}p) ≠ j({↓}p∖\{p\})} \\
  (j↦X)(j)  &=& \setofsc{p∈𝐏}{j({↓}p) ≠ j({↓}p∖\{p\})} \\
  (j↦X)     &=& λj∈\Nuc(\DP). \; \setofsc{p∈𝐏}{j({↓}p) ≠ j({↓}p∖\{p\})} \\
  [5pt]
  (\nuc↦𝓨) &=& λ\nuc∈\Nucs(H). \; \setofst{u∈𝐃_0}{({↓}u)^* ≠ ({↓}u∖\{u\})^*} \\
  \end{array}
$$


\bsk

Trying to decypher the real C1:

C.1, p.70:

\def\iYm{{i_Y^{-1}}}
\def\iff{\text{iff}}

$$\begin{array}{rcr}
       X_f &   =  & \setofsc{p∈𝐏}{f({↓}p) ≠ f({↓}p∖\{p\})} \\
           [5pt]
  p∈X_\iYm & \iff & \iYm({↓}p) ≠ \iYm({↓}p∖\{p\}) \\
           & \iff &     Y∩{↓}p ≠ Y∩({↓}p∖\{p\}) \\
    X_\iYm &   =  & \setofsc{p∈𝐏}{Y∩{↓}p ≠ Y∩({↓}p∖\{p\})} \\
  \end{array}
$$



%D diagram C1a
%D 2Dx     100   +30    +30
%D 2D  100 A00 = A0 <-| A1
%D 2D
%D 2D  +15       B0 <-- B1
%D 2D
%D 2D  +15       C0 `-> C1
%D 2D
%D ren A00 A0 A1 ==> A∩Y \iYm(A) A
%D ren     B0 B1 ==> \D(Y) \DP
%D ren     C0 C1 ==> Y 𝐏
%D
%D (( A00 A0 = A0 A1 <-|
%D     B0 B1 <-  .plabel= a \iYm
%D     C0 C1 `-> .plabel= a i_Y
%D ))
%D enddiagram
%D
$$\pu
  \diag{C1a}
$$



%D diagram ??
%D 2Dx     100 +40
%D 2D  100 A0  A1
%D 2D
%D 2D  +20 A2  A3
%D 2D
%D 2D  +15 B0  B1
%D 2D
%D ren A0 A1 ==> X_f [f]_E
%D ren A2 A3 ==> Y [\iYm]_E
%D ren B0 B1 ==> \Pts(𝐏)^\op \calE(\DP)
%D
%D (( A0 A1 <-|
%D    A0 A2 -> A1 A3 ->
%D    A2 A3 |->
%D    B0 B1 <- sl^ .plabel= a F
%D    B0 B1 <- sl_ .plabel= b G
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

$$X_f = \setofsc{p∈𝐏}{f({↓}p) ≠ f({↓}p∖\{p\})}$$

\newpage

$$\begin{array}{rcl}
  𝓨→𝓩 &=& \bigcup \setofst{𝓢∈H}{𝓢∩𝓨⊆𝓩} \\
        &=& \bigcup \setofst{𝓢∈H}{𝓢 ⊆ 𝓨 →_M 𝓩} \\
        &=& \bigcup \setofst{𝓢∈H}{𝓢 ⊆ \Int(𝓨 →_M 𝓩)} \\
        &=&                             \Int(𝓨 →_M 𝓩) \\
  %
  [5pt]
  %
  (𝓨↦\nuc) &=& λ𝓨∈\Pts(𝐃_0). \; λ𝓢∈H. \; 𝓨→𝓢 \\
  (\nuc↦𝓨) &=& λ\nuc∈\Nucs(H). \; \setofst{u∈𝐃_0}{({↓}u)^* ≠ ({↓}u∖\{u\})^*} \\
  %
  [5pt]
  %
  (𝓨↦J)      &=& λ𝓨∈\Pts(𝐃_0). \; λu∈𝐃_0. \; \setofst{𝓢∈Ω(u)}{u∈𝓨→𝓢} \\
  (J↦𝓨)    &=& λJ∈\GrTops(𝐃). \; \setofst{u∈𝐃_0}{J(u)=\{{↓}u\}} \\
  %
  [5pt]
  %
  (\nuc↦J)    &=& λ\nuc∈\Nucs(H). \; λu∈𝐃_0. \; \setofst{𝓢∈Ω(u)}{u∈𝓢^*} \\
  (J↦\nuc)    &=& λJ∈\GrTops(𝐃). \; λ𝓢∈H. \; \setofst{u∈𝐃_0}{𝓢∩{↓}u∈J(u)} \\
  %
  %[5pt]
  \end{array}
$$


% (find-books "__cats/__cats.el" "lindenhovius-gtop")

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

%\printbibliography

\end{document}

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

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

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