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

% «.defs»			(to "defs")
%   «.House»			(to "House")
%   «.Bottle»			(to "Bottle")
%   «.WideBottle»		(to "WideBottle")
%   «.SlantedHouse»		(to "SlantedHouse")
%   «.ArtDecoN»			(to "ArtDecoN")
% «.title»			(to "title")
%   «.abstract»			(to "abstract")
%   «.toc»			(to "toc")
% «.introduction»		(to "introduction")
% «.the-hierarchy»		(to "the-hierarchy")
% «.davey-priestley»		(to "davey-priestley")
% «.order-topologies»		(to "order-topologies")
% «.down-sets»			(to "down-sets")
% «.an-example»			(to "an-example")
% «.defining-groth-tops»	(to "defining-groth-tops")
% «.the-properties»		(to "the-properties")
% «.drawing-the-properties»	(to "drawing-the-properties")
% «.other-groth-tops»		(to "other-groth-tops")
% «.ex-lion-tamer»		(to "ex-lion-tamer")
%   «.ex-topologies»		(to "ex-topologies")
%   «.X=H-and-D=N»		(to "X=H-and-D=N")
% «.sieves-as-tvs»		(to "sieves-as-tvs")
% «.union-modality»		(to "union-modality")
% «.nuclei-congs-and-Hs»	(to "nuclei-congs-and-Hs")
%   «.double-negation»		(to "double-negation")
%   «.forcing»			(to "forcing")
% «.meaning-from-pictures»	(to "meaning-from-pictures")
% «.LT-topologies»		(to "LT-topologies")

\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{indentfirst}               % (find-es "tex" "indentfirst")
\usepackage{tocloft}                   % (find-es "tex" "tocloft")
\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 dofile "edrxtikz.lua"  -- (find-LATEX "edrxtikz.lua")
%L dofile "edrxpict.lua"  -- (find-LATEX "edrxpict.lua")
\pu


% (find-dn6 "heads6.lua" "lua-head")
% (find-dn6 "block.lua" "Block")




% «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\pmt         #1{\pmat{\text{#1}}}
\def\pmtt      #1#2{\pmat{\text{#1} \\ \text{#2}}}
\def\pmttt   #1#2#3{\pmat{\text{#1} \\ \text{#2} \\ \text{#3}}}
\def\pmtttt#1#2#3#4{\pmat{\text{#1} \\ \text{#2} \\ \text{#3} \\ \text{#4}}}

\def\Sieveson{\mathsf{Sieves\_on}}
\def\Coveringsieveson{\mathsf{Covering\_sieves\_on}}
\def\Coveringsieveson{\mathsf{Covsieves\_on}}

\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\SetOXop{{\Set^{\OX^\op}}}
\def\SetCop {{\Set^{\catC^\op}}}

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

\def\DP{\calD(\bfP)}
\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")
% (grcp  1 "ArtDecoN")
% (grcp 30 "ArtDecoN")
% (grca    "ArtDecoN")

%L ArtDecoN_ts   = TCGSpec.new("33; 32,"):LRcolstrs("!ga{L1} !ga{L2} !ga{L3}",
%L                                                  "!ga{R1} !ga{R2} !ga{R3}")
%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_td_4 = TCGDims {h=85, v=80,  q=15, crh=35,  crv=35, qrh=5}
%L ArtDecoN_tq   = TCGQ.newdsoa(ArtDecoN_td_0, ArtDecoN_ts,
%L                              {tdef="ArtDecoNSmall", meta="1pt s"},
%L                              "h ap LR o")
%L ArtDecoN_tq   = TCGQ.newdsoa(ArtDecoN_td_1, ArtDecoN_ts,
%L                              {tdef="ArtDecoNMed", meta="1pt s"},
%L                              "h v ap LR o")
%L ArtDecoN_tq   = TCGQ.newdsoa(ArtDecoN_td_2, ArtDecoN_ts,
%L                              {tdef="ArtDecoNBig", meta="1pt"},
%L                              "h v ap LR o")
%L ArtDecoN_tq   = TCGQ.newdsoa(ArtDecoN_td_3, ArtDecoN_ts,
%L                              {tdef="ArtDecoNBigg", meta="1pt"},
%L                              "h v ap LR o")
%L ArtDecoN_tq   = TCGQ.newdsoa(ArtDecoN_td_4, ArtDecoN_ts,
%L                              {tdef="ArtDecoNBigg", meta="1pt"},
%L                              "h v ap LR o")

%
\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\ArtDecoNBiggg#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)}
\def\padnbiggg#1#2#3#4#5#6{\left( \ArtDecoNBiggg{#1}{#2}{#3}{#4}{#5}{#6} \right)}









% «title»  (to ".title")
% (find-LATEX "2020clops-and-tops.tex" "title")
% (ph1p 1 "abstract")
% (ph1    "abstract")

\title{Grothendieck Topologies for Children}

\author{Eduardo Ochs}



\maketitle

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

\begin{abstract}

  The paper ``Planar Heyting Algebras for Children'' (\cite{PH1})
  showed how to use Planar Heyting Algebras to visualize the
  truth-values and the operations of Propositional Calculus in certain
  toposes; the ``...for children'' of its title means: ``we will start
  from some motivating examples (`for children') that are easy to
  visualize, and then go the general case (`for adults') --- {\sl but
    there are precise techniques for working on the case `for
    children' and on the case `for adults' in parallel}''. These
  techniques are described in detail in \cite{FavC}; see also
  sec.\ref{meaning-from-pictures}.

  In these notes we will use these techniques to visualize
  Grothendieck topologies --- first in the ``archetypal'' case of the
  canonical Grothendieck topology on a certain finite topological
  space, and then we will generalize that to arbitrary Grothendieck
  topologies on certain finite posets, that we will treat as
  ``ex-topologies'' (sec.\ref{ex-lion-tamer}).

  {\sl This is a working draft! It is still messy and incomplete at
    many points! I want/need to rewrite several sections of it and
    reorder everything!}

  \msk

  The latest version is at:

  % http://angg.twu.net/math-b.html\#favco
  % http://angg.twu.net/math-b.html#2021-groth-tops
  \url{http://angg.twu.net/math-b.html\#2021-groth-tops}

  % The notes in \cite{FavC} describe several techniques that I
  % developed to 

  % \cite[section 3.1]{Johnstone}, \cite[chapter 21]{McLarty},
  % \cite[section V.1]{MacLaneMoerdijk}, \cite[chapter 5]{BellLST}
  % \cite{FavC} \cite[section 16]{IDARCT} \cite[section
  %   2.15]{LambekScott} \cite[section 1.4]{FreydAspects}
  % \cite[definition 2.11]{Fourman} and \cite{PH2}

\end{abstract}

% «toc»  (to ".toc")
% (favp 2 "toc")
% (fav    "toc")
% (find-es "tex" "tocloft")
\renewcommand{\cfttoctitlefont}{\bfseries}
%\renewcommand{\cfttoctitlefont}{\mdseries}
\setlength{\cftbeforesecskip}{2.5pt}
\tableofcontents




% «introduction»  (to ".introduction")
% (grcp 1 "introduction")
% (grca   "introduction")

\section{Introduction}

One of the key ideas for understanding sheaves is {\sl Grothendieck
  topologies}. They are defined by a long zig-zag of steps in which
the `zig's are like ``take this familiar construction'', the `zag's
are like ``here is the {\sl right} generalization of the previous
step'', and the reasons for these choices of generalizations only
become clear many steps afterwards --- when we define sheaves in
several different ways. We will use some of the conventions in
\cite{FavC} to compare these different definitions of sheaves ---
mainly these three conventions, from \cite[sec.2]{FavC}:

% (favp 8 "the-conventions")
% (fav    "the-conventions")

\begin{quote}
\begin{itemize}

\item[(CPSh)] A particular case of a diagram $D$ is drawn with the
  same shape as $D$.

\item[(CNSh)] A translation of a diagram $D$ to another notation is
  drawn with the same shape as $D$.

\item[(CFSh)] The image by a functor of a diagram $D$ is drawn with
  the same shape as $D$.

\end{itemize}
\end{quote}

Here is one example of a shape that we will use often. Start with a
topology $\OX$. The topos $\SetOXop$ has objects $Ω$ and $\Jcan$, with
an inclusion $\Jcan \ito Ω$. For each open set $U∈\OX$ the set $Ω(U)$
is the set of ``sieves on $U$'', and the subset $\Jcan(U)⊂Ω(U)$ is the
set of ``covering sieves on $U$''. The elements of the set $\Jcan(U)$
are called ``covering sieves (on $U$)'', and denoted by letters like
$\calU$; each covering sieve is a set of open sets, i.e., of elements
of $\OX$, and they are denoted by letters like $V$. We will draw all
--- or, more honestly, most of --- this information as:
%
$$\begin{array}{cccccccc}
  \OX \\
  \rotatebox{90}{$\in$}   \\
  V &∈& \calU &∈& \Jcan(U) &⊂& Ω(U) \\ 
  \\
  \pmtt{our}{topology}    \\
  \rotatebox{90}{$\in$}   \\[-7.5pt]
  \pmttt{an}{open}{set}
    &∈& \pmttt   {a}{covering}{sieve}
    &∈& \pmtttt{all}{covering}{sieves}{on $U$}
    &∈& \pmttt           {all}{sieves}{on $U$} \\  
  \end{array}
$$

In Section \ref{ex-lion-tamer} we will generalize this to:
%
$$\begin{array}{cccccccc}
  D \\
  \rotatebox{90}{$\in$}         \\
  v &∈& \calU &∈& J(u) &⊂& Ω(u) \\ 
  \\
  \pmtt{our ex-}{topology}      \\
  \rotatebox{90}{$\in$}         \\[-7.5pt]
  \pmttt{an ex-}{open}{set}
    &∈& \pmttt   {a}{$J$-covering}{sieve}
    &∈& \pmtttt{all}{$J$-covering}{sieves}{on $u$}
    &∈& \pmttt               {all}{sieves}{on $u$} \\  
  \end{array}
$$

We will also use this shape to compare our notational conventions with
the ones in \cite{MacLaneMoerdijk} and \cite{Lindenhovius}, and to
show our conventions for drawing particular cases.

\msk

Grothendieck Topologies are not only hard to {\sl define}. They are
also very hard to {\sl visualize}, even when we start with finite
topologies like the Planar Heyting Algebras of \cite{PH1}, that {\sl
  ought to} yield nice archetypal cases --- in the sense of
\cite[section 16]{IDARCT}; see also \cite{ChengMorally}. Let me sketch
why.

Take a topological space $(X,\Opens(X))$. If we follow the ideas in
\cite{PH1} this $\Opens(X)$ will be a planar poset (I'll refrain from
mentioning lattices at this point!), with the empty set $∅$ as its
bottom element, and the $X$ at its top. Choose an open set
$U∈\Opens(X)$; $\Opens(U)$ will be a sub-poset of $\Opens(X)$. A
subset $\calS⊆\Opens(U)$ is a {\sl sieve on $U$} when it is closed
downwards; if we write $\Downs(\Opens(U))$ for
%
$$\Downs(\Opens(U)) \;\; = \;\; \setofst{\calS⊆\Opens(U)}{S \text{ is
    closed downwards}}$$
%
then the set of sieves on $U$ is exactly $\Downs(\Opens(U))$.

We say that a sieve $\calS∈\Downs(\Opens(U))$ {\sl covers} $U$ when
$\bigcup \calS = U$. The set of covering sieves on $U$ contains the
top element of $\Downs(\Opens(U))$, and is closed upwards and by
finite intersections --- so the set of covering sieves on $U$ is a
filter on $\Downs(\Opens(U))$, and if we write $\Filts(\bfP)$ for the
set of filters on a poset $\bfP$ then the set of covering sieves on
$U$ is a element of $\Filts(\Downs(\Opens(U))$. The {\sl canonical
  Grothendieck topology} on a topological space $(X,\Opens(X))$ is an
operation $\Jcan$ that chooses for each $U∈\Opens(X)$ a filter
$\Jcan(U)∈\Filts(\Downs(\Opens(U)))$, and to define Grothendieck
topologies in general we need to understand some properties of this
operation $\Jcan$, and the generalize them {\sl in the right way}.

We will discuss ways to draw posets, topologies, down-sets, and
filters in sections \ref{order-topologies} and \ref{down-sets}. In
section \ref{an-example} we will see how to draw our first
Grothendieck topology, and in sections \ref{defining-groth-tops} and
\ref{other-groth-tops} we will show how to define Grothendieck
topologies.

\newpage

%  _____ _            _     _                         _           
% |_   _| |__   ___  | |__ (_) ___ _ __ __ _ _ __ ___| |__  _   _ 
%   | | | '_ \ / _ \ | '_ \| |/ _ \ '__/ _` | '__/ __| '_ \| | | |
%   | | | | | |  __/ | | | | |  __/ | | (_| | | | (__| | | | |_| |
%   |_| |_| |_|\___| |_| |_|_|\___|_|  \__,_|_|  \___|_| |_|\__, |
%                                                           |___/ 
% «the-hierarchy»  (to ".the-hierarchy")
% (grcp 5 "the-hierarchy")
% (grca   "the-hierarchy")
\section{The hierarchy}
\label{the-hierarchy}

The definition of a Grothendieck topology on a topological space
$(X,\OX)$ uses elements and subsets a lot. It also uses lots of
linguistic constructs like ``a $J$-covering sieve on $U$ is...'', and
lots of notational conventions on the default meanings and the default
types of some letters and fonts. We need to extend the conventions in
\cite{FavC} a bit to handle that; here is a first attempt. Let's take
this (incomplete) version on the definition:

\begin{itemize}

\item Fix a topological space $(X,\OX)$.

\item Take any element $U∈\OX$. This $U$ is an open set. 

\item The set $Ω(U)$ is the set of {\sl sieves} on $U$, defined as
  $Ω(U)=\Downs(\OU)$; i.e., a sieve $\calS$ on $U$ is a down-set
  $\calS∈\Downs(\OU)=Ω(U)$.

\item The set $J(U)⊂Ω(U)$ is the set of $J$-covering sieves on $U$. We
  say that a sieve $\calU$ on $U$ is {\sl $J$-covering} when
  $\calU∈J(U)$.

\item Every element $V$ of a sieve $\calS$ is an open set of $X$;
  every element $V$ of a covering sieve $\calU$ is an open set of $X$.

\end{itemize}

We can organize this in two parallel diagrams, as:
%
$$\begin{array}{c}
    \begin{array}{ccccccccc}
    U &∈& \OX \\
       && \rotl{⊂} \\
    V &∈& \calS &∈& Ω(U) &=& \Downs(\OU) &⊂& \Pts(\OU) \\
       &&        && \rotl{⊂} \\
    V &∈& \calU &∈& J(U)  \\
    \end{array}
    \\
    \\
    \scalebox{0.85}{$
      \begin{array}{ccccccccc}
      \pmttt{an}{open}{set} &∈& \pmtt{our}{topology} \\[10pt]
         && \rotl{⊂} \\
      \pmttt{an}{open}{set}
        &∈& \pmtt{a}{sieve}
        &∈& \pmttt{all}{sieves}{on $U$}
        &=& \pmttt{all down-}{sets of}{$\OU$}
        &⊂& \pmttt{all}{subsets}{of $\OU$} \\
         &&        && \rotl{⊂} \\
      \pmttt{an}{open}{set}
        &∈& \pmttt {a}{covering}{sieve}
        &∈& \pmtttt{all $J$-}{covering}{sieves}{on $U$} \\
      \end{array}
    $}
  \end{array}
$$

I {\sl guess} that some experimental extensions to some proof
assistants like Agda --- that supports unicode characters in symbol
names --- may have ways to attribute default types for some names, but
at this moment I don't even know where to look for. {\sl All hints and
  pointers are welcome!}

\msk

The diagrams above shows a certain hierarchy between our symbols:
going right or going upwards in practically all cases means moving to
something bigger. We won't use diagrams with that shape much ---
instead we will use the smaller version below:
%
$$\begin{array}{cccccccc}
  \OX \\
  \rotl{∈}   \\
  V &∈& \calU &∈& J(U) &⊂& Ω(U) \\ 
  \\
  \pmtt{our}{topology}    \\
  \rotatebox{90}{$\in$}   \\[-7.5pt]
  \pmttt{an}{open}{set}
    &∈& \pmttt        {a}{covering}{sieve}
    &∈& \pmtttt{all $J$-}{covering}{sieves}{on $U$}
    &∈& \pmttt                {all}{sieves}{on $U$} \\  
  \end{array}
$$

We will call that shape ``the hierarchy'', and will often use it to
show examples of particular cases, by also drawing a copy in which the
$\OX$ is replaced by a particular topology, $U$ is replaced by a
particular open set in $\OX$, and so on.


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


\newpage

%  ____                              ____       _           _   _            
% |  _ \  __ ___   _____ _   _      |  _ \ _ __(_) ___  ___| |_| | ___ _   _ 
% | | | |/ _` \ \ / / _ \ | | |_____| |_) | '__| |/ _ \/ __| __| |/ _ \ | | |
% | |_| | (_| |\ V /  __/ |_| |_____|  __/| |  | |  __/\__ \ |_| |  __/ |_| |
% |____/ \__,_| \_/ \___|\__, |     |_|   |_|  |_|\___||___/\__|_|\___|\__, |
%                        |___/                                         |___/ 
%
% «davey-priestley»  (to ".davey-priestley")
% (grcp 2 "davey-priestley")
% (grca   "davey-priestley")

\section{Davey and Priestley}
\label{davey-priestley}

The book \cite{DaveyPriestley} is a standard reference on lattices; I
guess that its way of drawing lattices should be considered standard,
too. On pages 20--21 it defines and draws {\sl the ordered set $\Opens(P)$
  of down-sets of a poset $P$} like this:



% (find-books "__alg/__alg.el" "davey-priestley")
% (find-daveypriestleypage (+ 14  20)    "1.28 The ordered set O(P ) of down-sets")
% (find-daveypriestleytext (+ 14  20)    "1.28 The ordered set O(P ) of down-sets")

% (find-LATEX "material-para-GA.tex" "cells")

\celllower=4pt

$$\begin{array}{rc}
 N \;\;=\;\;
 %\left(
 \vcenter{\hbox{%
 \unitlength=20pt
\beginpicture(-2,0)(5,1)
%
\put(-1,0){\cell{a=}}
\put(-1,1){\cell{b=}}
\put(2,1){\cell{=c}}
\put(2,0){\cell{=d}}
%
\Line(1,0)(0,1)
\Line(0,0)(0,1)
\Line(1,0)(1,1)
\put(0,0){\opendot}
\put(1,0){\opendot}
\put(0,1){\opendot}
\put(1,1){\opendot}
 \end{picture}%
 }}
 %\right)
 \\
 \\
 \\
 \Opens(N) \;\;=\;\;
 %\left(
 \vcenter{\hbox{%
 \unitlength=20pt
\beginpicture(-5,0)(6,4)
%
\put(-1.3,4){\cell{\{a,b,c,d\}=}}
\put(-2.4,3){\cell{{↓}b=\{a,b,d\}=}}
\put(-0.8,2){\cell{\{a,d\}=}}
\put(-1.9,1){\cell{{↓}a=\{a\}=}}
\put(0,0){\cell{∅=}}
%
\put(3.9,3){\cell{=\{a,c,d\}}}
\put(5.2,2){\cell{=\{c,d\}={↓}c}}
\put(4.0,1){\cell{=\{d\}={↓}d}}
%
\Line(1,0)(0,1)
\Line(1,0)(2,1)
\Line(2,1)(1,2)
\Line(0,1)(1,2)
\Line(2,1)(3,2)
\Line(1,2)(0,3)
\Line(3,2)(2,3)
\Line(1,2)(2,3)
\Line(2,3)(1,4)
\Line(0,3)(1,4)
\put(1,0){\opendot}
\put(0,1){\closeddot}
\put(2,1){\closeddot}
\put(1,2){\opendot}
\put(3,2){\closeddot}
\put(0,3){\closeddot}
\put(2,3){\opendot}
\put(1,4){\opendot}
 \end{picture}%
 }}
 %\right)
 \\
 \\
  \end{array}
$$

The book usually draws the ``join-irreducible'' elements of lattices
using ``shaded dots''; see its page 54. Here is an example from the
book:

% (find-daveypriestleypage (+ 14 54) "The join-irreducible elements are shaded")
% (find-daveypriestleytext (+ 14 54) "The join-irreducible elements are shaded")

$$
 %\left(
 \vcenter{\hbox{%
 \unitlength=20pt
 \beginpicture(0,0)(4,7)
\Line(2,0)(1,1)
\Line(2,0)(3,1)
\Line(1,1)(0,2)
\Line(3,1)(2,2)
\Line(1,1)(2,2)
\Line(3,1)(4,2)
\Line(2,2)(1,3)
\Line(4,2)(3,3)
\Line(2,2)(2,3)
\Line(0,2)(1,3)
\Line(2,2)(3,3)
\Line(2,3)(1,4)
\Line(3,3)(2,4)
\Line(1,3)(1,4)
\Line(3,3)(3,4)
\Line(1,3)(2,4)
\Line(2,3)(3,4)
\Line(1,4)(0,5)
\Line(3,4)(2,5)
\Line(2,4)(2,5)
\Line(1,4)(2,5)
\Line(3,4)(4,5)
\Line(2,5)(1,6)
\Line(4,5)(3,6)
\Line(0,5)(1,6)
\Line(2,5)(3,6)
\Line(3,6)(2,7)
\Line(1,6)(2,7)
\put(2,0){\opendot}
\put(1,1){\closeddot}
\put(3,1){\closeddot}
\put(0,2){\closeddot}
\put(2,2){\opendot}
\put(4,2){\closeddot}
\put(1,3){\opendot}
\put(2,3){\closeddot}
\put(3,3){\opendot}
\put(1,4){\opendot}
\put(2,4){\opendot}
\put(3,4){\opendot}
\put(0,5){\closeddot}
\put(2,5){\opendot}
\put(4,5){\closeddot}
\put(1,6){\opendot}
\put(3,6){\opendot}
\put(2,7){\opendot}
   %\pictgrid%
   %\pictaxes%
 \end{picture}%
 }}
 %\right)
$$

And here is a bigger example:
%
$$
  \Opens
\left(
 \vcenter{\hbox{%
 \unitlength=20pt
\beginpicture(0,0)(4,5)
\Line(2,0)(1,1)
\Line(2,0)(3,1)
\Line(1,1)(0,2)
\Line(3,1)(2,2)
\Line(1,1)(2,2)
\Line(3,1)(4,2)
\Line(2,2)(1,3)
\Line(4,2)(3,3)
\Line(0,2)(1,3)
\Line(2,2)(3,3)
\Line(3,3)(2,4)
\Line(1,3)(2,4)
\Line(2,4)(1,5)
\put(2,0){\opendot}
\put(1,1){\closeddot}
\put(3,1){\closeddot}
\put(0,2){\closeddot}
\put(2,2){\opendot}
\put(4,2){\closeddot}
\put(1,3){\opendot}
\put(3,3){\opendot}
\put(2,4){\opendot}
\put(1,5){\closeddot}
 \end{picture}%
 }}
 \right)
 %
 \quad
 =
 \quad
 %
 % obottle:
 \left(
 \vcenter{\hbox{%
 \unitlength=20pt
\beginpicture(0,0)(4,10)
\Line(2,0)(2,1)
\Line(2,1)(1,2)
\Line(2,1)(3,2)
\Line(1,2)(0,3)
\Line(3,2)(2,3)
\Line(1,2)(2,3)
\Line(3,2)(4,3)
\Line(2,3)(1,4)
\Line(4,3)(3,4)
\Line(2,3)(2,4)
\Line(0,3)(1,4)
\Line(2,3)(3,4)
\Line(2,4)(1,5)
\Line(3,4)(2,5)
\Line(1,4)(1,5)
\Line(3,4)(3,5)
\Line(1,4)(2,5)
\Line(2,4)(3,5)
\Line(1,5)(0,6)
\Line(3,5)(2,6)
\Line(2,5)(2,6)
\Line(1,5)(2,6)
\Line(3,5)(4,6)
\Line(2,6)(1,7)
\Line(4,6)(3,7)
\Line(0,6)(1,7)
\Line(2,6)(3,7)
\Line(3,7)(2,8)
\Line(1,7)(2,8)
\Line(2,8)(2,9)
\Line(2,9)(1,10)
\put(2,0){\opendot}
\put(2,1){\closeddot}
\put(1,2){\closeddot}
\put(3,2){\closeddot}
\put(0,3){\closeddot}
\put(2,3){\opendot}
\put(4,3){\closeddot}
\put(1,4){\opendot}
\put(2,4){\closeddot}
\put(3,4){\opendot}
\put(1,5){\opendot}
\put(2,5){\opendot}
\put(3,5){\opendot}
\put(0,6){\closeddot}
\put(2,6){\opendot}
\put(4,6){\closeddot}
\put(1,7){\opendot}
\put(3,7){\opendot}
\put(2,8){\opendot}
\put(2,9){\closeddot}
\put(1,10){\closeddot}
 \end{picture}%
 }}
 \right)
$$

We will pronounce ``$\Opens(P)$'' as ``the order topology on the poset
$P$''.

%\end{document}



%   ___          _             _                    _             _           
%  / _ \ _ __ __| | ___ _ __  | |_ ___  _ __   ___ | | ___   __ _(_) ___  ___ 
% | | | | '__/ _` |/ _ \ '__| | __/ _ \| '_ \ / _ \| |/ _ \ / _` | |/ _ \/ __|
% | |_| | | | (_| |  __/ |    | || (_) | |_) | (_) | | (_) | (_| | |  __/\__ \
%  \___/|_|  \__,_|\___|_|     \__\___/| .__/ \___/|_|\___/ \__, |_|\___||___/
%                                      |_|                  |___/             
%
% «order-topologies»  (to ".order-topologies")
% (grcp 8 "order-topologies")
% (grca   "order-topologies")

\section{Order topologies}
\label{order-topologies}

Most of the material in \cite{PH1} was tested on ``real children'', as
explained in this part of its introduction:

\begin{quote}

  This paper can be seen as part of bigger projects in at least the
  two ways described above, but it was also written to be as readable
  and as self-contained as possible. In 2016 and 2017 I had the
  opportunity to test some of the ideas here on ``real children'', in
  the sense of ``people with little mathematical {\sl knowledge} and
  little mathetical {\sl maturity}''. I gave a seminar course about
  Logic and $λ$-calculus that had no prerequisites, and that was
  mostly based on exercises that the students would try to solve
  together by discussing on the whiteboard; it was mostly attended by
  Computer Science students who had just finished a course on Discrete
  Mathematics (...)

\end{quote}

They found the notation for order topologies below much easier to
start with.

% One recurrent theme in \cite{FavC} is that certain people (``...who
% think very visually'')

% (ph1p 25 "topologies-on-ZSets")
% (ph1     "topologies-on-ZSets")
% (ph1p 26 "topologies-as-partial-orders")
% (ph1     "topologies-as-partial-orders")
% (ph1p 5 "positional")
% (ph1    "positional")
% (ph1p  6 "ZDAGs")
% (ph1     "ZDAGs")


In section 13 of \cite{PH1} we defined $H$ as the ``house'' poset at
the left here (see also section 1 for the ``reading order'' and
section 2 for the ``black pawns moves''):
%
\pu
$$
  \begin{array}{ccl}
  % (H,\BPM(H))
  H = \zha{House}
    & \qquad
    & (\Opens(H), ⊂_1) = \def\h{\zfHouse}\zha{OHouse} \\
  \end{array}
$$

Here we will prefer this slanted version of the house DAG, that is a
2-column graph (\cite[section 14]{PH1}):
%
%L tcg_big    = {scale="14pt", meta="p",   dv=2, dh=2.75, ev=0.32, eh=0.275}
%L tcg_Big    = {scale="14pt", meta="p",   dv=2, dh=3.5,  ev=0.32, eh=0.200}
%L tcg_medium = {scale= "9pt", meta="p s", dv=1, dh=2.2,  ev=0.32, eh=0.275}
%L tcgnew = function (opts, def, str)
%L     return TCG.new(opts, def, unpack(split(str, "[ %d]+")))
%L   end
%L tcgbig = function (def, spec) return tcgnew(tcg_big,    def, spec or tcg_spec) end
%L -- tcgBig = function (def, spec) return tcgnew(tcg_Big,    def, spec or tcg_spec) end
%L -- tcgmed = function (def, spec) return tcgnew(tcg_medium, def, spec or tcg_spec) end
%L
%L tcg_spec = "3, 2; 32, "
%L tcgbig("tcghouse")   :lrs():vs():hs():output()
%L -- tcg_spec = "3, 4; 14, 32"
%L -- tcgbig("tcgbigwithbowtie"):lrs():vs():hs():output()
%L
%L -- (find-dn6 "tcgs.lua" "TCGSpec-test")
%L ts = TCGSpec.new("32; 32,")
%L ts:mp({scale="22pt", zdef="bottledag"}):addlrs():addarrows("w"):output()
%
\pu
$$H = \tcghouse
  \qquad
  (\Opens(H), ⊂_1) = \zha{bottledag}
$$
%
but we will sometimes use the unslanted for drawing subsets of $H$: we will draw
%
%L tspec_mini  = TCGSpec.new("32; 32,")
%L tdims_micro = TCGDims {h=15,  v=8,  q=15, crh=3.5,  crv=7, qrh=5}
%L tcgq = TCGQ.newdsoa(tdims_micro, tspec_mini, {tdef="Tbu", meta="1pt s"}, "h ap")
%L tcgq:digits("110", "10"):output()
%
$$\pu
  \zfHouse01011 \qquad \text{instead of:} \qquad \tcg{Tbu} \;\; .
$$

The ZHA with 10 elements at the right is the ``bottle'' poset, and we
will call it $B$. So:
%
$$\Opens(H) \;\;=\;\; B.$$



%  ____                                     _       
% |  _ \  _____      ___ __        ___  ___| |_ ___ 
% | | | |/ _ \ \ /\ / / '_ \ _____/ __|/ _ \ __/ __|
% | |_| | (_) \ V  V /| | | |_____\__ \  __/ |_\__ \
% |____/ \___/ \_/\_/ |_| |_|     |___/\___|\__|___/
%                                                   
% «down-sets»  (to ".down-sets")
% (grcp 10 "down-sets")
% (grca    "down-sets")

\section{Down-sets, up-sets, and filters}
\label{down-sets}

We will define ``down-sets'', ``up-sets'', and ``filters'' on posets
{\sl almost} in the standard way, i.e., as in \cite{DaveyPriestley};
but we need to take into account that it $H$ the arrows go down, and
in $B$ they go up. So: if $\bfP$ is a poset with underlying set
$\bfP_0$,

\begin{itemize}

\item A subset $D⊆\bfP_0$ is a {\sl down-set} of $\bfP$ iff
%
$$∀p,q∈\bfP_0.\; (p \text{ above } q) → \pmat{p∈D \\↓\\ q∈D},$$

\item A subset $U⊆\bfP_0$ is an {\sl up-set} of $\bfP$ iff
%
$$∀p,q∈\bfP_0.\; (p \text{ above } q) → \pmat{p∈U \\↑\\ q∈U},$$

\item If $\bfP$ has a top element $⊤$ and a binary meet operation
  `$∧$', then a subset $F⊆\bfP_0$ is a {\sl filter} iff: 1) $F$ is an
  up-set of $\bfP$, 2) $⊤∈F$, 3)
%
$$∀p,q∈\bfP_0.\; \pmat{p∈F \text{ and } q∈F \\↓\\ p∧q∈F}.$$

\end{itemize}

We will define $\Downs(\bfP)$, $\Ups(\bfP)$, and $\Filts(\bfP)$ as:
%
$$\begin{array}{rcl}
  \Downs(\bfP) &=& \setofst{D⊆\bfP_0}{D \text{ is a down-set of } \bfP}, \\
  \Ups  (\bfP) &=& \setofst{U⊆\bfP_0}{U \text{ is an up-set of  } \bfP}, \\
  \Filts(\bfP) &=& \setofst{F⊆\bfP_0}{U \text{ is a filter in   } \bfP}, \\
  \end{array}
$$
%
and if $S∈\bfP_0$ we will denote the down-set of $\bfP$ generated by
$S$ as ${↓}S$ or ${↓}_\bfP S$, and the up-set of $\bfP$ generated by
$S$ as ${↑}S$ or ${↑}_\bfP S$. When $p∈\bfP_0$ we will sometimes write
${↓}\{p\}$ as just ${↓}p$, and ${↑}\{p\}$ as just ${↑}p$.

Here are some examples:
%
%R local Ba, Bb, Bc, Bd, Be, Bf = 1/ 1   \, 1/ 1   \, 1/ 0   \, 1/ 0   \, 1/ 0   \, 1/ 0   \
%R                                 |  1  |   |  1  |   |  0  |   |  0  |   |  0  |   |  1  |
%R                                 | 1 1 |   | 1 1 |   | 0 0 |   | 0 0 |   | 0 0 |   | 1 1 |
%R                                 |1 0 0|   |1 1 0|   |1 0 0|   |1 1 1|   |1 1 1|   |1 1 1|
%R                                 | 0 0 |   | 1 0 |   | 1 0 |   | 0 0 |   | 1 1 |   | 1 1 |
%R                                 \  0  /   \  0  /   \  1  /   \  0  /   \  1  /   \  1  /
%R
%R Ba:tomp({zdef="Ba", scale="5pt", meta="s"}):addcells():output()
%R Bb:tomp({zdef="Bb", scale="5pt", meta="s"}):addcells():output()
%R Bc:tomp({zdef="Bc", scale="5pt", meta="s"}):addcells():output()
%R Bd:tomp({zdef="Bd", scale="5pt", meta="s"}):addcells():output()
%R Be:tomp({zdef="Be", scale="5pt", meta="s"}):addcells():output()
%R Bf:tomp({zdef="Bf", scale="5pt", meta="s"}):addcells():output()
%
$$\pu
  \begin{array}{c}
  \begin{array}{ccc}
  \zfHouse00011     ∈ \Downs(H)    &\text{but}& \zfHouse00011 \not∈ \Ups(H), \\[15pt]
  \zfHouse10100 \not∈ \Downs(H)    &\text{but}& \zfHouse10100     ∈ \Ups(H), \\[15pt]
  ↓\zfHouse01100 \; = \zfHouse01111,   && ↑\zfHouse01100 \; = \zfHouse11100, \\[15pt]
  \zha{Ba} ∈ \Ups(B)         &\text{but}& \zha{Ba} \not∈ \Filts(B), \\[15pt]
                             &          & \zha{Bb}     ∈ \Filts(B). \\[15pt]
  \end{array}
  \\
  \\
  \begin{array}{c}
  {↓}_H \; 2▁ = \zfHouse01010 = 20, \\[12pt]
  {↓}_B \; {↓}_H \; 2▁ = {↓}_B \; 20 = \{20,10,00\} = \zha{Bc}, \\[15pt]
  20∩11 = \zfHouse01010 ∩ \zfHouse00011 = \zfHouse00010 = 10, \\[15pt]
  20∪11 = \zfHouse01010 ∩ \zfHouse00011 = \zfHouse01011 = 21, \\[15pt]
  % \bigcup \Bottle 0 100 010 001 % \zha{Bd}
    \bigcup \bo{0 100 010 001} % \zha{Bd}
    = \zfHouse01010 ∪ \zfHouse00011 ∪ \zfHouse00101 = \zfHouse01111 = 22, \\[15pt]
  ↓ \; \bigcup \bo{0 100 010 001} = \; ↓ 22 = \bo{0 111 111 111}, \\[15pt]
  ↓ \bo{0 100 010 001} = \bo{0 100 110 111}. \\[15pt]
  \end{array}
  \end{array}
$$

\newpage

And here are some notations for sets of down-sets:

$$\begin{array}{rcl} 
  \left[ \bo{0 000 1?? 111} \right]
    &=& \setofst{U ∈ \Opens(B)}{\text{$U$ is of the form $\bo{0 000 1?? 111}$}} \\
    &=& \setofst{U ∈ \Opens(B)}{\bo{0 000 100 111} ⊆ U ⊆ \bo{0 000 111 111}} \\
    &=& \left\{ \bo{0 000 100 111}, \;
                \bo{0 000 110 111}, \;
                \bo{0 000 111 111}  
        \right\} \\
  \\
  \left[ \bo{· ··· 1?? 111} \right]
    &=& \setofst{U ∈ \Opens(12)}{\text{$U$ is of the form $\bo{· ··· 1?? 111}$}} \\
    &=& \setofst{U ∈ \Opens(12)}{\bo{· ··· 100 111} ⊆ U ⊆ \bo{· ··· 111 111}} \\
    &=& \left\{ \bo{· ··· 100 111}, \;
                \bo{· ··· 110 111}, \;
                \bo{· ··· 111 111}  
        \right\} \\[18pt]
    &=& \{\; 
        {↓}\{10,02\}, \; 
        {↓}\{11,02\}, \;
        {↓}12
        \;\} \\ 
  \end{array}
$$

\msk

Note that $\{\; {↓}\{10,02\}, \; {↓}\{11,02\}, \; {↓}12 \;\}$ is an
up-set, a filter, and a principal filter. More precisely,

$$\def\FOO{
    \{\; {↓}\{10,02\}, \; {↓}\{11,02\}, \; {↓}12 \;\}
  }
  \begin{array}{rcl} 
  \FOO &⊆& \Downs(\Opens(12)), \\
  \FOO &∈& \Ups(\Downs(\Opens(12))), \\
  \FOO &∈& \Filts(\Downs(\Opens(12))), \\
  \FOO &=& {↑}_{\Downs(\Opens(12))}({↓}\{10,02\}). \\
  \end{array}
$$

\msk

The `$·$'s in this notation mean ``this point is out of the domain''.
They help to indicate that we are in $\Downs(\Opens(12))$, not in
$\Downs(\Opens(22))$ or $\Downs(\Opens(32))$.


%     _                                           _      
%    / \   _ __     _____  ____ _ _ __ ___  _ __ | | ___ 
%   / _ \ | '_ \   / _ \ \/ / _` | '_ ` _ \| '_ \| |/ _ \
%  / ___ \| | | | |  __/>  < (_| | | | | | | |_) | |  __/
% /_/   \_\_| |_|  \___/_/\_\__,_|_| |_| |_| .__/|_|\___|
%                                          |_|           
%
% «an-example»  (to ".an-example")
% (grcp 8 "an-example")
% (grca   "an-example")
\section{An example}
\label{an-example}

If you know more than the basics of Topos Theory then the following
figures should make a lot of sense... if you don't then it's better to
start from the definitions in the next section.

Remember that $\Opens(H) = B$. The classifier object of the topos
$\Set^{\Opens(H)^\op}$ is a functor $Ω: \Opens(H)^\op → \Set$ whose
action on objects takes each $U∈\Opens(H)$ to $\Opens(U)$. Using the
notations from the previous section and the trick for ``drawing
functors as objects'' from \cite[section 7.12]{FavC}, we have:

% (favp 50 "functors-as-objects")
% (fav     "functors-as-objects")

$$Ω =
  \left(
  \BottleSetArgs{
                                              {\bbo{? ??? ??? ???}}
  {\bbo{· ?·· ?·· ?··}} {\bbo{· ??· ??· ??·}} {\bbo{· ??? ??? ???}}
  {\bbo{· ··· ?·· ?··}} {\bbo{· ··· ??· ??·}} {\bbo{· ··· ??? ???}}
  {\bbo{· ··· ··· ?··}} {\bbo{· ··· ··· ??·}} {\bbo{· ··· ··· ???}}}
  \zha{Bottle^2}
  \right)
$$

(Hint: compare the drawing for $Ω$ above with the one in section
  \ref{sieves-as-tvs})

And the canonical Grothendieck topology in $\Set^{\Opens(H)^\op}$ is:
%
$$\Jcan =
  \left(
  \BottleSetArgs{
                                              {\bbo{1 111 111 111}}
  {\bbo{· 1·· 1·· 1··}} {\bbo{· 1?· 1?· 11·}} {\bbo{· 1?? 1?? 111}}
  {\bbo{· ··· 1·· 1··}} {\bbo{· ··· 1?· 11·}} {\bbo{· ··· 1?? 111}}
  {\bbo{· ··· ··· 1··}} {\bbo{· ··· ··· 11·}} {\bbo{· ··· ··· 111}}}
  \zha{Bottle^2}
  \right)
$$

\newpage

The morphism $⊤:1 \ito Ω$ in this topos is the inclusion map that goes
from this terminal object to the $Ω$ that we have just defined:
%
$$1 =
  \left(
  \BottleSetArgs{
                                              {\bbo{1 111 111 111}}
  {\bbo{· 1·· 1·· 1··}} {\bbo{· 11· 11· 11·}} {\bbo{· 111 111 111}}
  {\bbo{· ··· 1·· 1··}} {\bbo{· ··· 11· 11·}} {\bbo{· ··· 111 111}}
  {\bbo{· ··· ··· 1··}} {\bbo{· ··· ··· 11·}} {\bbo{· ··· ··· 111}}}
  \zha{Bottle^2}
  \right)
$$

\msk

The meaning of ``inclusion map'' here should be obvious, but there is
a formal definition of it in these notes: \cite{ClopsAndTops}. Note
that we have these inclusions in $\Set^{\Opens(H)^\op}$:
%
$$1 \ito \Jcan \ito Ω\;.$$

\newpage

% «defining-groth-tops»  (to ".defining-groth-tops")
% (grcp 12 "defining-groth-tops")
% (grca    "defining-groth-tops")

\section{Defining Grothendieck topologies}
\label{defining-groth-tops}

Here's how to define Grothendieck topologies on a category
$\Opens(X)$.

\begin{enumerate}

\item We start with a topological space $(X,\Opens(X))$, and with the
  category $\Opens(X)$ --- the poset of open sets of $X$, in which an
  arrow $V→U$ exists iff $V⊆U$. We will define Grothendieck topologies
  ``on $\Opens(X)$'' now, and generalize this later.

\item For every $U∈\Opens(X)$ the {\sl maximal sieve on $U$} is the
  set $t(U) = \Opens(U)$.

\item A {\sl sieve on $U$} is a subset $\calS ⊆ t(U)$ that is closed
  downwards.

\item We write $Ω(U)$ for the set of sieves on $U$.

\item This $\Om$ is a functor $Ω:\Opens(X)^\op \to \Set$. Its
  definition by a diagram (in the sense of \cite[section 5.2]{FavC})
  is:
%
%D diagram ??
%D 2Dx     100  +35 +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 ==> U Ω(U) V Ω(V)
%D ren C0 C1 ==> \calS \calS∩\Opens(V)
%D ren B0 B1 ==> \phantom{{}^\op}\Opens(X)^\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= \Opens(X) place
%D    B0 B1 ->
%D    C0 C1 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

\item We say that a sieve $\calS$ on $U$ {\sl covers} $U$ iff this
  holds: $\bigcup \calS = U$.

\item We write $\Jcan(U)$ for the set of sieves on $U$ that cover $U$.
  Note that $\Jcan(U)⊆Ω(U)$.

\item This $\Jcan$ is a functor $\Jcan:\Opens(X)^\op$. Its definition
  by a diagram is
%
%D diagram ??
%D 2Dx     100  +35 +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 ==> U Ω(U) V Ω(V)
%D ren C0 C1 ==> \calS \calS∩\Opens(V)
%D ren B0 B1 ==> \phantom{{}^\op}\Opens(X)^\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= \Opens(X) place
%D    B0 B1 ->
%D    C0 C1 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

\item This $\Jcan$ is a {\sl subfunctor} of $Ω$: we have a natural
  transformation $i:\Jcan \ito Ω$ in which each map $i(U): \Jcan(U)
  \ito Ω(U)$ is an inclusion in $\Set$.

\item We call this functor $\Jcan: \Opens(X)^\op → \Set$ the {\sl
  canonical Grothendieck topology on $\Opens(X)$}, or ``on (the
  topological space) $X$''.

% \item In some small cases this $\Jcan$ can be drawn explicitly (see
%   section sss).

\item For each $U∈\Opens(X)$ the corresponding $\Jcan(U)$ is a filter.
  More precisely: each sieve $\calS$ on $U$ is a down-set of
  $\Opens(U)$; in the notation of section sss,
  $\calS∈\Downs(\Opens(U))$; so $\Jcan(U) ⊆ \Downs(\Opens(U))$. And:

  \begin{enumerate}

  \item The top element of $\Downs(\Opens(U))$, $t(U)$, is a
    covering sieve on $U$, so $t(U) ∈ \Jcan(U)$.
    
  \item If $\calA$ and $\calB$ are sieves on $U$ and $\calA$ covers
    $U$, then $\calB$ also covers $U$. This means that $\Jcan(U)$ is
    closed upwards, and so $\Jcan(U)$ is an up-set: $\Jcan(U) ∈
    \Ups(\Downs(\Opens(U)))$.

  \item If $\calA$ and $\calB$ are covering sieves on $U$ then
    $\calA∩\calB$ is also a covering sieve on $U$. This means that
    $\Jcan(U)$ is closed by binary meets, and so $\Jcan(U)$ obeys all
    the conditions for being a filter: $\Jcan(U) ∈
    \Filts(\Downs(\Opens(U)))$.

  \item The intersection $\bigcap \Jcan(U)$ is a sieve on $U$ that is
    ``below'' all covering sieves $\calU ∈ \Jcan(U)$; more precisely,
    for every $\calU ∈ \Jcan(U)$ we have $\bigcap \Jcan(U) ⊆ \calU$.
    This means that the filter $\Jcan(U)$ is contained in the
    principal filter $↑_{\Downs(\Opens(U))}\;\bigcap \Jcan(U)$.

  \item When $\Opens(X)$ is a finite set all the `$\Opens(U)$'s and
    `$\Downs(\Opens(U))$'s are finite sets. In this case each
    $\Jcan(U)$ is closed by arbitrary meets, and $\bigcap\Jcan(U) ∈
    \Jcan(U)$. Each $\Jcan(U)$ is a principal filter, and
    $\Jcan(U) = {↑}_{\Downs(\Opens(U))}\;\bigcap \Jcan(U)$.

  \end{enumerate}

\item This $\Jcan$ obeys the properties $\hasmax_\Jcan$,
  $\stab_\Jcan$, and $\trans_\Jcan$, described in section
  \ref{the-properties}.

\item We define the {\sl Grothendieck topologies on $\Opens(X)$} as
  the subfunctors $J \ito Ω$ that obey the properties $\hasmax_J$,
  $\stab_J$, and $\trans_J$.

\item The properties $\hasmax_J$, $\stab_J$, and $\trans_J$ imply that
  each $J(U)$ contains the top element $t(U)$ and is closed upwards
  and by binary meets; so each $J(U)$ is a filter on
  $\Downs(\Opens(U))$, i.e., $J(U) ∈ \Filts(\Downs(\Opens(U)))$.

\end{enumerate}



% «the-properties»  (to ".the-properties")
% (grcp 14 "the-properties")
% (grca   "the-properties")

\section{The properties $\hasmax_\J$, $\stab_\J$, and $\trans_\J$}
\label{the-properties}

This is the definition of a Grothendieck topology on an arbitrary
category, taken from \cite[page 110]{MacLaneMoerdijk}:
%
% (find-maclanemoerdijkpage (+ 11 110) "Definition 1. A Grothendieck Topology")
%
\begin{quote}

  {\bf Definition 1.} A {\sl Grothendieck Topology} on a category
  $\catC$ is a function $J$ which assigns to each object $C$ of
  $\catC$ a collection $J(C)$ of sieves on $C$, in such a way that:
  
  \begin{enumerate}

  \item The maximal sieve $t_C = \setofst{f}{\cod(f)=C}$ is in $J(C)$;

  \item (stability axiom) is $S∈J(C)$, then $h^*(S)∈J(D)$ for any
    arrow $h:D→C$;

  \item (transitivity axiom) if $S∈J(C)$ and $R$ is any sieve on $C$
    such that $h^*(S)∈J(D)$ for all $h:D→C$ in $S$, then $R∈J(C)$.

  \end{enumerate}

\end{quote}

It follows these notational conventions:
%
$$\begin{array}{cccccccc}
  \catC                     \\
  \SetCop                   \\
  (\SetCop)_1               \\
  \rotatebox{90}{$\in$}     \\
  h &∈& S &∈& J(C) &⊂& Ω(C) \\ 
  \\
  \pmtt{a small}{category}  \\
  \pmtt{our}{topos}         \\
  \pmtt{its}{morphisms}     \\
  \rotatebox{90}{$\in$}         \\[-15pt]
  \pmtt{a}{morphism}
    &∈& \pmttt   {a}{$J$-covering}{sieve}
    &∈& \pmtttt{all}{$J$-covering}{sieves}{on $C$}
    &∈& \pmttt               {all}{sieves}{on $C$} \\  
  \end{array}
$$

We will translate that definition to our definition of a Grothendick
Topology on a topological space in two steps.

\newpage

This is the first step of the translation --- note that here the
sieves are still collections of arrows, not collections of open sets:
%
\begin{quote}

  {\bf Definition \Onep.} A {\sl Grothendieck Topology} on a category
  $\Opens(X)$ is a function $J$ which assigns to each object $U$ of
  $\Opens(U)$ a collection $J(U)$ of sieves on $U$, in such a way
  that:
  
  \begin{enumerate}

  \item The maximal sieve $t(U) = \setofst{f}{\cod(f)=U}$ is in
    $J(U)$;

  \item (stability axiom) is $\calU∈J(U)$, then $h^*(\calU)∈J(V)$ for
    any arrow $h:V→U$;

  \item (transitivity axiom) if $\calU∈J(U)$ and $\calS$ is any sieve
    on $U$ such that $h^*(\calS)∈J(V)$ for all $h:V→U$ in $\calU$,
    then $\calS∈J(U)$.

  \end{enumerate}

\end{quote}

The definition above follows these notational conventions:
%
$$\begin{array}{cccccccc}
  \OX                       \\
  \SetOXop                  \\
  (\SetOXop)_1              \\
  \rotatebox{90}{$\in$}     \\
  h &∈& \calU &∈& J(U) &⊂& Ω(U) \\ 
  \\
  \pmtt{a}{topology}  \\
  \pmtt{our}{topos}         \\
  \pmtt{its}{morphisms}     \\
  \rotatebox{90}{$\in$}         \\[-15pt]
  \pmtt{a}{morphism}
    &∈& \pmttt   {a}{$J$-covering}{sieve}
    &∈& \pmtttt{all}{$J$-covering}{sieves}{on $C$}
    &∈& \pmttt               {all}{sieves}{on $C$} \\  
  \end{array}
$$

\newpage

This is the second step of the translation. Here the sieves becomes
collections of open subsets, instead of collections of morphisms:
%
\begin{quote}

  {\bf Definition \Onepp.} A {\sl Grothendieck Topology} on a category
  $\Opens(X)$ is a function $J$ which assigns to each object $U$ of
  $\Opens(U)$ a collection $J(U)$ of sieves on $U$, in such a way
  that:
  
  \begin{enumerate}

  \item The maximal sieve $t(U) = \setofst{V∈\Opens(X)}{V⊆U}$ is in
    $J(U)$;

  \item (stability axiom) is $\calU∈J(U)$, then $(V⊆U)^*(\calU)∈J(V)$
    for any open set $V∈\Opens(U)$;

  \item (transitivity axiom) if $\calU∈J(U)$ and $\calS$ is any sieve
    on $U$ such that $(U⊆V)^*(\calS)∈J(V)$ for all $V∈\Opens(U)$ in
    $\calU$, then $\calS∈J(U)$.

  \end{enumerate}

\end{quote}

Here are its notational conventions, in the same shape as before:
%
$$\begin{array}{cccccccc}
  \OX \\
  \rotatebox{90}{$\in$}   \\
  V &∈& \calU &∈& J(U) &⊂& Ω(U) \\ 
  \\
  \pmtt{our}{topology}    \\
  \rotatebox{90}{$\in$}   \\[-7.5pt]
  \pmttt{an}{open}{set}
    &∈& \pmttt   {a}{covering}{sieve}
    &∈& \pmtttt{all}{covering}{sieves}{on $U$}
    &∈& \pmttt           {all}{sieves}{on $U$} \\  
  \end{array}
$$

Many very important details from Definitions 1, \Onep, and \Onepp{}
were left out of these L-shaped diagrams, so let's create something
more detailed --- in two steps. In the first one we will translate the
three conditions to something closer to first-order logic, but with
some of the implications being drawn vertically to stress what is
``above'' and what is ``below'', following that the convention that
bigger open sets are above and small ones are below. We get this.


This is Definition 1,
%
\def\DefinitionOneHalfway{
  \begin{array}{rcl}
  \hasmax_J &:=& (∀C∈\catC.\;t(C)∈J(C))
                     \\[5pt]
  \stab_J   &:=& \plarray{∀h:D→C. \\
                          ∀S∈\Sieveson(C). \\
                           \pmat{
                             S∈J(C) \\
                             ↓ \\
                             h^*(S)∈J(D) \\
                          } }
                      \\[40pt]
  \trans_J  &:=& \plarray{
                      ∀C∈\catC. \\
                      ∀S∈J(U). \\
                      ∀R∈\Sieveson(U). \\
                      \pmat{
                        (R∈J(C)) \\
                        ↑ \\
                        ∀(h:D→C)∈S.\;(h^*(R)∈J(D)) \\
                      } \\
                     } \\
  \end{array}
}
%
$$\DefinitionOneHalfway
$$

\msk

And this is Definition \Onepp:
%
$$\begin{array}{rcl}
  \hasmax_J &:=& (∀U∈\Opens(X).t(U)∈J(U))
                     \\[5pt]
  \stab_J   &:=& \plarray{∀V⊆U. \\ ∀\calU∈\Sieveson(U). \\
                           \pmat{
                             \calU∈J(V) \\
                             ↓ \\
                             (V⊆U)^*(\calU)∈J(V) \\
                          } }
                      \\[40pt]
  \trans_J  &:=& \plarray{
                      ∀U∈\Opens(X). \\
                      ∀\calU∈J(U). \\
                      ∀\calS∈\Sieveson(U). \\
                      \pmat{
                        (\calS∈J(U)) \\
                        ↑ \\
                        ∀V∈\calU.((V⊆U)^*(\calS)∈J(V)) \\
                      } \\
                     } \\
  \end{array}
$$

\newpage

% «drawing-the-properties»  (to ".drawing-the-properties")
% (grcp 16 "drawing-the-properties")
% (grca    "drawing-the-properties")

\section{Drawing the properties}
\label{drawing-the-properties}

Here is my (current) favorite way to draw the properties $\hasmax_\J$,
$\stab_\J$, and $\trans_\J$ for a Grothendieck topology $J$ on the
topological space $(X,\Opens(X))$:
%
%D diagram groth-top-usual
%D 2Dx     100 +35 +60
%D 2D  100 A1      A3  
%D 2D          
%D 2D  +12 B1      B3
%D 2D       |       | 
%D 2D  +17 C1      C3
%D 2D          
%D 2D  +12 D1  D2  D3
%D 2D       |   |   |
%D 2D  +17 E1  E2  E3
%D 2D
%D ren A1    A3 ==>  U                     (\Opens(U)∈J(U))
%D ren B1    B3 ==>  U                     (\calU∈J(U))
%D ren C1    C3 ==>  V                     (\calU∩\Opens(V)∈J(V))
%D ren D1 D2 D3 ==>  U \calS                    (\calS∈J(U))
%D ren E1 E2 E3 ==> ∀V \calS∩\Opens(V) (∀V{∈}\,\calU.\;\calS∩\Opens(V)∈J(V))
%D
%D (( A1 place A3 place
%D    C1 B1 ->
%D    B3 C3 ->
%D
%D    newnode: D1' at: @D1+v(12,0) .TeX= \calU place
%D    newnode: E1' at: @D1+v(7,9)  .TeX= \rotatebox{60}{$\in$} place
%D    E1 D1 ->
%D    D2 E2 |->
%D    D3 E3 <-
%D
%D ))
%D enddiagram
%D
\pu
$$\diag{groth-top-usual}
$$

[Rewrite this paragraph:]

Some details of the formal translation are omitted in that diagram,
but most of them can be reconstructed from the fonts and the
placements. Actually the main intent of that diagram is to list
notational conventions; in the case above, 1) the objects of the
category $\Opens(X)$ have names like $U$ and $V$; 2) the arrows in
$\Opens(X)$ go upwards, so our topos is $\Set^{\OX^\op}$; not
$\Set^{\OX}$; 3) the top element in each $\J(U)$ can be denoted by
$\OU$; 4) we denote sieves by names like $\calS$; 5) our typical name
for a covering sieve on $U$ is $\calU$; 6) the operation that
``restricts sieves'' and moves them downward in diagrams like the ones
in section \ref{an-example} is `$∩\;\Opens(V)$'.

\msk

If I draw the Definition 1 in that shape I get this:
%
%D diagram groth-top-on-C
%D 2Dx     100 +35 +70
%D 2D  100 A1      A3  
%D 2D          
%D 2D  +12 B1      B3
%D 2D       |       | 
%D 2D  +17 C1      C3
%D 2D          
%D 2D  +12 D1  D2  D3
%D 2D       |   |   |
%D 2D  +17 E1  E2  E3
%D 2D
%D ren A1    A3 ==>  C                     (t_C∈J(C))
%D ren B1    B3 ==>  C                     (S∈J(C))
%D ren C1    C3 ==>  D                     (h^*(S)∈J(D))
%D ren D1 D2 D3 ==>  C R                   (R∈J(C))
%D ren E1 E2 E3 ==> ∀D h^*(R) (∀(h:D→C)∈S.\,h^*(R)∈J(D))
%D
%D (( A1 place A3 place
%D    C1 B1 -> .plabel= l h
%D    B3 C3 ->
%D
%D    newnode: D1' at: @D1+v(12,0) .TeX= S place
%D    newnode: E1' at: @D1+v(6,5)  .TeX= \rotatebox{38}{$\in$} place
%D    E1 D1  -> .plabel= l ∀h
%D    D2 E2 |->
%D    D3 E3  <-
%D
%D ))
%D enddiagram
%D
\pu
$$\diag{groth-top-on-C}
$$

Note that in the first drawing the `$∈$' points to the `$V$', and in
the second one to the `$h$'.

\newpage

Here is Definition 1 again, followed by its two translations to the
more visual ways to represent the properties, that stress that
$\stab_J$ propagates $J$-coveringness down and $\trans_J$ propagates
$J$-coveringness up:

\begin{quote}
\begin{enumerate}

\item The maximal sieve $t_C = \setofst{f}{\cod(f)=C}$ is in $J(C)$;

\item (stability axiom) is $S∈J(C)$, then $h^*(S)∈J(D)$ for any
  arrow $h:D→C$;

\item (transitivity axiom) if $S∈J(C)$ and $R$ is any sieve on $C$
  such that $h^*(S)∈J(D)$ for all $h:D→C$ in $S$, then $R∈J(C)$.

\end{enumerate}
\end{quote}
%
$$\DefinitionOneHalfway$$

\msk

$$\diag{groth-top-on-C}
$$



\newpage

I learned most of what I know about Grothendieck topologies on posets
from \cite{Lindenhovius}. He uses the notational conventions below to
define Grothendieck topologies on a poset $\bfP$ (in pages 8--9 of the
paper):
%
% (find-books "__cats/__cats.el" "lindenhovius-gtop")
% (find-grtopsonposetspage  8 "2 Grothendieck topologies on posets")
%
%D diagram groth-top-lindenhovius
%D 2Dx     100 +35 +60
%D 2D  100 A1      A3  
%D 2D          
%D 2D  +12 B1      B3
%D 2D       |       | 
%D 2D  +17 C1      C3
%D 2D          
%D 2D  +12 D1  D2  D3
%D 2D       |   |   |
%D 2D  +17 E1  E2  E3
%D 2D
%D ren A1    A3 ==>  p                     ({↓}p∈J(p))
%D ren B1    B3 ==>  p                     (S∈J(p))
%D ren C1    C3 ==>  q                     (S∩{↓}q∈J(q))
%D ren D1 D2 D3 ==>  p R                    (R∈J(p))
%D ren E1 E2 E3 ==> ∀q R∩{↓}q (∀q{∈}\,S.\;R∩{↓}q∈J(q))
%D
%D (( A1 place A3 place
%D    C1 B1 -> .plabel= l q≤p\;
%D    B3 C3 ->
%D
%D    newnode: D1' at: @D1+v(12,0) .TeX= S place
%D    newnode: E1' at: @D1+v(7,9)  .TeX= \rotatebox{60}{$\in$} place
%D    E1 D1 -> .plabel= l q≤p\;
%D    D2 E2 |->
%D    D3 E3 <-
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{groth-top-lindenhovius}
$$

I will use notational conventions for grtops on posets that are very
close to the first diagram in this section, that showed the properties
of a grtop on a topological space $(X,\OX)$.

In the diagrams of section \ref{an-example} I showed how to visualize
the canonical Grothendieck topology $\Jcan$ on the topological space
$(H,\Opens(H))$; this $\Jcan$ was an object of the topos
$\Set^{\OH^\op}$, but we had this:
%
$$\OH \;\;=\;\; B \;\;=\;\; \zha{bottledag}$$
%
so that $\Jcan$ was also an object of $\Set^{B^\op}$. Let's see how to
define grtops on arbitrary posets $D$ (mnemonic: ``DAG''), i.e., in
categories $\Set^{D^\op}$ or $\Set^{D}$.

\newpage

Suppose that $D$ is a poset with its arrows pointing up. Our
notational conventions for grtops on $D$ will be exactly the same as
the ones that we used for grtops on $\Opens(X)$, with only these
changes: 1) elements of $D$ will be denoted by $u$ and $v$ (instead of
$U,V∈\Opens(X)$, where the $U$ and $V$ were in uppercase); 2) we will
write ${↓}u$ and ${↓}v$ instead of $\OU$ and $\OV$; 3) we will write
$D$ instead of $\OX$. We will still use $\calS$ for a sieve and
$\calU$ for a covering sieve (but now $\calU$ covers $u$, not on $U$);
so $\calS$ and $\calU$ are down-sets of $D$, and $\calS, \calU ⊆ D$
(instead of $\calS, \calU ⊆ \Opens(X)$).

This was our diagram for a grtop on a topological space $(X,\OX)$:
%
$$\diag{groth-top-usual}
$$

This is our diagram for a grtop on a poset $D$ with its arrows
pointing up:
%
%D diagram groth-top-D-up-arrows
%D 2Dx     100 +35 +60
%D 2D  100 A1      A3  
%D 2D          
%D 2D  +12 B1      B3
%D 2D       |       | 
%D 2D  +17 C1      C3
%D 2D          
%D 2D  +12 D1  D2  D3
%D 2D       |   |   |
%D 2D  +17 E1  E2  E3
%D 2D
%D ren A1    A3 ==>  u                     ({↓}u∈J(u))
%D ren B1    B3 ==>  u                     (\calU∈J(u))
%D ren C1    C3 ==>  v                     (\calU∩{↓}v∈J(v))
%D ren D1 D2 D3 ==>  u \calS                    (\calS∈J(u))
%D ren E1 E2 E3 ==> ∀v \calS∩{↓}v  (∀v{∈}\,\calU.\;\calS∩{↓}v∈J(v))
%D
%D (( A1 place A3 place
%D    C1 B1 ->
%D    B3 C3 ->
%D
%D    newnode: D1' at: @D1+v(12,0) .TeX= \calU place
%D    newnode: E1' at: @D1+v(7,9)  .TeX= \rotatebox{60}{$\in$} place
%D    E1 D1 ->
%D    D2 E2 |->
%D    D3 E3 <-
%D
%D ))
%D enddiagram
%D
\pu
$$\diag{groth-top-D-up-arrows}
$$

This characterizes the subobjects $J⊆Ω$ of a category $\Set^{D^\op}$
that are Grothendieck topologies. To define grtops when the arrows in
$D$ point down --- the 2-column graphs of \cite[section 14]{PH1} use
arrows pointing down --- we just need to switch the direction of the
arrows in the left column.

\newpage

% «other-groth-tops»  (to ".other-groth-tops")
% (grcp 19 "other-groth-tops")
% (grca    "other-groth-tops")

\section{Other Grothendieck topologies}
\label{other-groth-tops}

In the section \ref{an-example} we drew a specific Grothendieck
topology on $(H,\Opens(H))$: the ``canonical'' one, that was a
subobject $\Jcan \ito Ω$ in $\Set^{\OH^\op}$. Let's start by a way to
obtain other grtops on $(H,\Opens(H))$.

Remember that we use $\calU$ and $\calS$ to denote subsets of a
topology $\Opens(X)$: $\calS$ denotes a sieve, and $\calU$ denotes a
covering sieve. Let's use the letter $\calY$ to denote an {\sl
  arbitrary} subset of $\Opens(X)$. We define the Grothendieck
topology $J_\calY$ on $\Opens(X)$ by:
%
$$\begin{array}{rcl}
  J_\calY(U) &:=& \setofst{ \calS∈Ω(U) }{ \calY∩\Opens(U) ⊆ \calS } \\
              &=& \setofst{ \calS∈Ω(U) }{ {↓}(\calY∩\Opens(U)) ⊆ \calS } \\
              &=& {↑}_{\Downs(Ω(U))} \; {↓}(\calY∩\Opens(U)) \\
  \end{array}
$$

Let's start with an example. We will work in $(H,\Opens(H))$, as in
section \ref{an-example}, and let $\calY := \{01,02,11,12\}$. So:
%
$$\calY = \bo{0 000 011 011}$$

Then:
%
$$\begin{array}{rcl}
  J_\calY(21) &:=& \setofst{ \calS∈Ω(21) }{ {↓}(\calY∩\Opens(21)) ⊆ \calS } \\[5pt]
              &:=& \setofst{ \calS∈\bbo{· ??· ??· ??·} }
                           { {↓}\left( \bo{0 000 011 011} \;∩\; \bo{0 110 110 110}
                                \right)
                             ⊆ \calS
                           } \\[15pt]
              &:=& \setofst{ \calS∈\bbo{· ??· ??· ??·} }
                           { {↓}\left( \bo{0 000 010 010}
                                \right)
                             ⊆ \calS
                           } \\[15pt]
              &:=& \setofst{ \calS∈\bbo{· ??· ??· ??·} }
                           { \left( \bo{0 000 110 110}
                             \right)
                             ⊆ \calS
                           } \\[15pt]
              &:=& \bbo{· ??· 11· 11·} \\
  \end{array}
$$

\newpage

So for this $\calY$
%
$$\calY \;\;=\;\; \{01,02,11,12\} \;\;=\;\; \bo{0 000 011 011} \;\;⊂\;\; \Opens(H)$$
% 
we have:
%
$$J_\calY =
  \left(
  \BottleSetArgs{
                                              {\bbo{? ??? 111 111}}
  {\bbo{· ?·· ?·· ?··}} {\bbo{· ??· 11· 11·}} {\bbo{· ??? 111 111}}
  {\bbo{· ··· ?·· ?··}} {\bbo{· ··· 11· 11·}} {\bbo{· ··· 111 111}}
  {\bbo{· ··· ··· ?··}} {\bbo{· ··· ··· 11·}} {\bbo{· ··· ··· 111}}}
  \zha{Bottle^2}
  \right)
$$

All grtops on a finite poset $D$ are of the form $J_\calY$ for some
$\calY⊆D$ (see \cite[page 43]{Lindenhovius}); in particular, our
$\Jcan$ is a $J_\calY$ for this $\calY$:
%
% (find-grtopsonposetspage 43   "Conclusion")
% (find-grtopsonposetstext 43   "Conclusion")
%
$$\calY \;\;=\;\; \{{↓}▁1, {↓}▁2, {↓}1▁, {↓}2▁, {↓}3▁\}
        \;\;=\;\; \{01,02,10,20,32\}
        \;\;=\;\; \bo{1 100 100 011} \; .
$$

\newpage

The definition for $J_\calY$ given above also works on arbitrary
posets, and there is also a way to start with any Grothendieck
topology $J$ on an arbitrary poset and obtain the $\calY$ such that
$J=J_\calY$. Here are the two constructions in the notation of
\cite[pages 11--12]{Lindenhovius}, each one followed by its
translations into our two notations:
%
% (find-grtopsonposetspage 11   "Proposition 2.8")
% (find-grtopsonposetstext 11   "Proposition 2.8")
%
$$\begin{array}{rcl}
      J_X(p) &:=& \setofst{S∈\calD({↓}p)}{X∩{↓}p⊆S} \\
  J_\calY(U) &:=& \setofst{ \calS∈Ω(U) }{ \calY∩\Opens(U) ⊆ \calS } \\
  J_\calY(u) &:=& \setofst{ \calS∈Ω(u) }{ \calY∩{↓}u ⊆ \calS } \\
  \\
      X_J &:=& \setofst{p∈\bfP}{J(p) = \{{↓}p\}} \\
  \calY_J &:=& \setofst{U∈\Opens(X)}{J(U) = \{{↓}U\}} \\
  \calY_J &:=& \setofst{u∈D}{J(u) = \{{↓}u\}} \\
  \end{array}
$$



Let's see an example of this. Let $D:=H$, the (slanted) house DAG with
arrows going downwards, and let:
%
$$\calY \;\;=\;\; \{ 1▁, \; ▁2\} \;\;=\;\; \SlantedHouse 00110$$

This $\calY$ generates this Grothendieck topology, $J_\calY⊆Ω$, in the
topos $\Set^H$:

\msk

$$J_\calY \;\; = \;\;
  \SlantedHouseBig
  {\bsh??111}
  {\bsh·?·1·}  {\bsh··1·1}
  {\bsh···1·}  {\bsh····?}
$$

\newpage

%  _____           _     _               _____                         
% | ____|_  __    | |   (_) ___  _ __   |_   _|_ _ _ __ ___   ___ _ __ 
% |  _| \ \/ /____| |   | |/ _ \| '_ \    | |/ _` | '_ ` _ \ / _ \ '__|
% | |___ >  <_____| |___| | (_) | | | |   | | (_| | | | | | |  __/ |   
% |_____/_/\_\    |_____|_|\___/|_| |_|   |_|\__,_|_| |_| |_|\___|_|   
%                                                                      
% «ex-lion-tamer»  (to ".ex-lion-tamer")
% (grcp 22 "ex-lion-tamer")
% (grca    "ex-lion-tamer")

\section{Ex-Lion Tamer}
\label{ex-lion-tamer}

% (find-books "__etc/__etc.el" "pinkflag")

\begin{quote}

  The title words are absent from the song itself, which has travelled
  far from its origins. Newman initially wrote a lyric featuring a
  lion tamer. ``Graham took one look, said, `This is rubbish' and
  rewrote it. There was a lion tamer involved somewhere.'' According
  to Lewis, ``That was the thing I thought was most memorable, but
  totally irrelevant in the end. I rewrote it and, by the end, it was
  called `Ex-Lion Tamer' because even the lion tamer had
  disappeared.'' (\cite{PinkFlag})

\end{quote}

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

%L ts = TCGSpec.new("32; 32,")
%L ts:mp({scale="10pt", zdef="thisbottle"}):addlrs():output()
%L ts:mp({scale="7pt",  zdef="thisbottle", meta="s"}):addlrs():output()
\pu


Let's review our archetypal case, its terminology and its notational
conventions, and then make some changes to that.

We started with a topological space $\OX$, that was usually regarded
as a poset; that poset was also denoted by $\OX$. In most examples
$\Opens(X)$ was the order topology on the (slanted) house DAG $H$,
that had 5 elements, and $\Opens(X)$-as-a-poset was the bottle DAG
$B$, with 10 elements (see sec.\ref{order-topologies}). We referred to
the elements of $\OX$ as ``open sets'', and denoted them by letters
like $U$ and $V$. A {\sl sieve} is a subset of $\Opens(X)$ obeying
certain properties; we denoted sieves by calligraphic letters like
$\calR$, $\calS$, and $\calU$, where $\calU$ was a {\sl covering
  sieve} (on $U$). Also, we used the calligraphic letter $\calY$ to
denote a subset of $\OX$ that did not need to be a sieve. The set of
all sieves on an open set $U∈\OX$ was denoted by $Ω(U)$, and the set
of all covering sieves on a $U∈\OX$ by $J(U)$. We had this:
%
$$\begin{array}{ccccccccc}
  \Opens(X) \\
  \rotl{∈} \\
  V &∈& \calU &∈& J(U)  &⊂& Ω(U) \\ 
  V &∈& \calU &∈& J(21) &⊂& Ω(21) \\ 
  \\
  \zha{thisbottle} \\[17pt]
  \rotl{∈} \\[-3pt]
  10 &∈& \bo{0 000 100 110} &∈& \bbo{· ??· ??· 11·} &⊂& \bbo{· ??· ??· ??·} \\[15pt]
      &&    \rotl{=} \\
      &&    \csm{ \! 10,\;\;\;\;01, \!\! \\ 00 } \\
  \end{array}
$$

Note that this diagram includes particular cases --- in:
%
$$\begin{array}{ccccccc}
  V &∈& \calU &∈& J(U)  &⊂& Ω(U) \\ 
  V &∈& \calU &∈& J(21) &⊂& Ω(21) \\ 
  \end{array}
$$
%
the bottom line specializes the top line to the case $U=21$. It also
includes examples, like ``in this context 10 is a possible value
for $V$''.

% (favp 11 "to-deserve-a-name")
% (fav     "to-deserve-a-name")

\msk

So: we first learned how to define Grothendieck topologies on a
topological space $\OX$, with this $\OX$ being regarded as a poset,
and then we saw how to define Grothendieck topologies on posets that
do not need to come from topologies. We will use Wire's trick, and
refer to these ``posets that no longer need to be topologies'' as
``ex-topologies'', and to their elements as ``ex-open sets''. Our
notational conventions for them will change: the topology $\OX$ will
become the ex-topology $D$ (a poset), and the open sets $U,V∈\OX$ will
become ex-open sets $u,v∈D$. The rest will be kept unchanged: for
example, sieves will still be called sieves, and will be denoted by
the same calligraphic letters as before.

%L tspec_HHH  = TCGSpec.new("33; 32,")
%L tdims_big   = TCGDims {h=50, v=50,  q=15, crh=19,  crv=15, qrh=5}
%L tdims_mini  = TCGDims {h=15,  v=8,  q=15, crh=3.5,  crv=7, qrh=5}
%L tdims_micro = TCGDims {h=25, v=22,  q=15, crh=7.5,  crv=7, qrh=5}
%L tcg_HHH = TCGQ.newdsoa(tdims_big,   tspec_HHH, {tdef="HHH0", meta="1pt s"}, "h v ap")
%L tcg_Hhh = TCGQ.newdsoa(tdims_micro, tspec_HHH, {tdef="Hhh0", meta="1pt s"}, "h v ap")
%L tcg_hhh = TCGQ.newdsoa(tdims_mini,  tspec_HHH, {tdef="hhh0", meta="1pt s"}, "h   ap")
%L tcg_HHH:LRputs("!ga{L1} !ga{L2} !ga{L3}", "!ga{R1} !ga{R2} !ga{R3}"):output()
%L tcg_Hhh:LRputs("!ga{L1} !ga{L2} !ga{L3}", "!ga{R1} !ga{R2} !ga{R3}"):output()
%L tcg_hhh:LRputs("!ga{L1} !ga{L2} !ga{L3}", "!ga{R1} !ga{R2} !ga{R3}"):output()
%
\pu

\def\HHH#1#2#3#4#5#6{{
  \sa{L3}{#1}\sa{R3}{#2}%
  \sa{L2}{#3}\sa{R2}{#4}%
  \sa{L1}{#5}\sa{R1}{#6}%
  \tcg{HHH0}
  }}
\def\Hhh#1#2#3#4#5#6{{
  \sa{L3}{#1}\sa{R3}{#2}%
  \sa{L2}{#3}\sa{R2}{#4}%
  \sa{L1}{#5}\sa{R1}{#6}%
  \tcg{Hhh0}
  }}
%\def\hhh#1#2#3#4#5#6{{
%  \sa{L3}{#1}\sa{R3}{#2}%
%  \sa{L2}{#3}\sa{R2}{#4}%
%  \sa{L1}{#5}\sa{R1}{#6}%
%  \tcg{hhh0}
%  }}

\def\pHHH#1{{\left( \HHH#1 \right)}}
\def\pHhh#1{{\left( \Hhh#1 \right)}}
\def\bHHH#1{{\left[ \HHH#1 \right]}}
%\def\phhh#1{{\left( \hhh#1 \right)}}
%\def\bhhh#1{{\left[ \hhh#1 \right]}}

\def\phhh#1{\padn#1}
\def\bhhh#1{\badn#1}

% $\pHHH{{3▁}{▁3}{2▁}{▁2}{1▁}{▁1}}$



%  _____           _                    _             _           
% | ____|_  __    | |_ ___  _ __   ___ | | ___   __ _(_) ___  ___ 
% |  _| \ \/ /____| __/ _ \| '_ \ / _ \| |/ _ \ / _` | |/ _ \/ __|
% | |___ >  <_____| || (_) | |_) | (_) | | (_) | (_| | |  __/\__ \
% |_____/_/\_\     \__\___/| .__/ \___/|_|\___/ \__, |_|\___||___/
%                          |_|                  |___/             
%
% «ex-topologies»  (to ".ex-topologies")
% (grcp 30 "ex-topologies")
% (grca    "ex-topologies")

\subsection{Ex-topologies: sieves as two-digit numbers}
\label{ex-topologies}

% «X=H-and-D=N»  (to ".X=H-and-D=N")
% (find-LATEX "2021groth-tops-defs.tex" "X=H-and-D=N")
%
%L H_ts = TCGSpec.new("32; 32,")
%L D_ts = TCGSpec.new("33; 32,")
%L H_td = TCGDims {h=35,  v=28,  q=15, crh=7.5,  crv=9, qrh=5}
%L D_td = TCGDims {h=35,  v=28,  q=15, crh=7.5,  crv=9, qrh=5}
%L H_tq = TCGQ.newdsoa(H_td, H_ts, {tdef="H", meta="1pt p"}, "h v ap")
%L D_tq = TCGQ.newdsoa(D_td, D_ts, {tdef="D", meta="1pt p"}, "h v ap")
%L H_tq:lrs():output()
%L D_tq:lrs():output()
%L H_mp = H_ts:mp({zdef="H_zha", scale="11pt", meta=nil})
%L D_mp = D_ts:mp({zdef="D_zha", scale="11pt", meta=nil})
%L H_mp:addlrs():output()
%L D_mp:addlrs():output()
\pu

We will also change something else. In the case of Grothendieck
topologies on topological spaces we used this:
%
$$X = H = \tcg{H}
  \qquad
  \Opens(X) = \Opens(H) = \zha{H_zha}
$$
%
There the two-digit numbers, like 10, denoted open sets.

In the new setting, i.e., in the case of Grothendieck topologies on
ex-topological spaces, we will switch to this other convention:
%
$$D = N = \tcg{D}
  \qquad
  \Downs(D) = \Downs(N) = \zha{D_zha}
$$
%
Here it is our ex-topological space, $D$, that is a 2-column graph.
This will let us draw the set $\Downs(D)$ of all down-sets on $D$,
i.e., the set of all {\sl sieves} in this context, as the ZHA
associated to the 2-column graph $D$, as above; see
sec.\ref{order-topologies}, and \cite[sec.15]{PH1} for the details.
This will give us an alternative way to represent sieves and sets of
sieves: sieves are now two-digit numbers, and sets of sieves are sets
of two-digit numbers.

Here is a translation of the previous diagram to this new case:
%
$$\begin{array}{ccccccccc}
  D        \\
  \rotl{∈} \\
  v &∈& \calU &∈& J(u)  &⊂& Ω(u) \\ 
  v &∈& \calU &∈& J(3▁) &⊂& Ω(3▁) \\ 
  \\
  \padnmed{3▁}{▁3}{2▁}{▁2}{1▁}{▁1} \\[17pt]
  \rotl{∈} \\[-3pt]
  2▁ &∈& \phhh{00 10 11} &∈& \bhhh{?· 1? 11} &⊂& \bhhh{?· ?? ??} \\[15pt]
      &&    \rotl{=}     &&    \rotl{=}      &&    \rotl{=} \\
      &&    21           &∈& \pwibo{{32}· ·{21}{22}· ···· ····}
                         &⊂& \pwibo{{32}· {20}{21}{22}· {10}{11}{12}· {00}{01}{02}·} \\
      &&    \rotl{=} \\
      &&    \csm{ 2▁, \;\;\;\;\; \\
                  1▁, \, ▁1 } \\
  \end{array}
$$
%
Note that here we have $v=2▁$ and $u=3▁$ (two ex-open sets), $\calU =
21$ (a sieve), $Ω(u) = Ω(3▁) = {↓}{↓}3▁ = {↓}32$, and $J(3▁) =
{↑}_{Ω(3▁)}\,21$. The 6-node poset that plays the role of $D$ in this
example will sometimes be called by its proper name: ``Art Déco N'',
or just ``$N$'', because in some Art Déco fonts the uppercase N is
drawn like this:
%
$$\vcenter{\hbox{%
  \unitlength=15pt
  \beginpicture(0,0)(1,2)
  \Line(0,0)(0,2)(1,1)
  \Line(1,0)(1,2)
  \end{picture}%
  }}
$$


% «sieves-as-tvs»  (to ".sieves-as-tvs")
% (grcp 32 "sieves-as-tvs")
% (grca    "sieves-as-tvs")

\section{Sieves as truth-values}
\label{sieves-as-tvs}

From this point onwards all our examples will use the Art Déco N of
the end of the last section as our ex-topology; in other words, our
examples will use $D:=N$. Also, from here onwards $N$ will always
stand for the Art Déco N, not for the traditional N with four nodes of
section \ref{davey-priestley}. We will write $D$ and $N$ as $\catD$
and $\catN$ when we regard them as categories; their arrows will point
downwards.

This is the subobject classifier of the topos $\Set^\catN$ (compare it
with the $Ω$ in section \ref{an-example}):

$$Ω = \padnbig
    {\bhhh{?·????}} {\bhhh{·?·?·?}}
    {\bhhh{··?·?·}} {\bhhh{···?·?}}
    {\bhhh{····?·}} {\bhhh{·····?}}
    = \padnbigg
    {\wibo{{32}·    {20}{21}{22}·    {10}{11}{12}·    {00}{01}{02}·   }}
    {\wibo{·   ·    ·   ·   ·   ·    ·   ·   ·   ·    {00}{01}{02}{03}}}
    {\wibo{·   ·    {20}·   ·   ·    {10}·   ·   ·    {00}·   ·   ·   }}
    {\wibo{·   ·    ·   ·   ·   ·    ·   ·   ·   ·    {00}{01}{02}·   }}
    {\wibo{·   ·    ·   ·   ·   ·    {10}·   ·   ·    {00}·   ·   ·   }}
    {\wibo{·   ·    ·   ·   ·   ·    ·   ·   ·   ·    {00}{01}·   ·   }}
$$

\msk

Note that the maximal sieves on $3▁$ and $▁3$ are:

$$\begin{array}{rcl}
             && t_{3▁} = {↓}3▁ = 32 = \phhh{1·1111} \\[15pt]
  \text{and} && t_{▁3} = {↓}▁3 = 03 = \phhh{·1·1·1} \;,
  \end{array}
$$
%
so here we have sieves that are not in any of the `$Ω(u)$'s. The set
of all sieves on the ex-topology $N$ is:
%
$$\Downs(N) = \pwibo{{32}{33} {20}{21}{22}{23} {10}{11}{12}{13} {00}{01}{02}{03}}\;,$$
%
that is exactly the set of subobjects of the terminal object
$1∈\Set^\catN$. So:
%
$$\Sub(1_{\Set^\catN}) = \bhhh{??????}$$

This holds for any poset $D$. More precisely: our way of speaking of
Grothendieck topologies on a poset $D$ requires treating $D$ as an
ex-topology and working on the topos $\Set^\catD$; in the terminology
that we are using the set of truth-values of that topos,
$\Sub(1_{\Set^\catD})$, is essentially the same thing as the set of
sieves on $D$, $\Downs(D)$.

\msk

To be coherent with our notational conventions we will use for
truth-values the same letters that we use for sieves: $\calR, \calS,
\calU, \calV$. When $D$ is a (finite, acyclic) 2-column graph the set
of truth-values of $\Set^\catD$ will be a Planar Heyting Algebra --- a
ZHA. The paper \cite{PH1} is about how to visualize the operations of
Propositional Calculus on ZHAs, and we will reuse all its ideas and
notations, except that here we will use letters like $\calR, \calS,
\calU, \calV$ to denote truth-values, instead of $P, Q, R, S$. Also,
very important:

\begin{quote}
From this point onwards the letter $H$ will denote the Heyting Algebra
$H = \Sub(1_{\Set^\catD}) = \Downs(D)$, instead of the house DAG. This
Heyting Algebra $H = \Downs(D)$ will be a ZHA when $D$ is a (finite,
acyclic) 2-column graph.
\end{quote}




%  _   _       _                                   _       _ _ _         
% | | | |_ __ (_) ___  _ __    _ __ ___   ___   __| | __ _| (_) |_ _   _ 
% | | | | '_ \| |/ _ \| '_ \  | '_ ` _ \ / _ \ / _` |/ _` | | | __| | | |
% | |_| | | | | | (_) | | | | | | | | | | (_) | (_| | (_| | | | |_| |_| |
%  \___/|_| |_|_|\___/|_| |_| |_| |_| |_|\___/ \__,_|\__,_|_|_|\__|\__, |
%                                                                  |___/ 
% «union-modality»  (to ".union-modality")
% (grcp 24 "union-modality")
% (grca    "union-modality")

\section{The union as a modality}

Let's go back to the case of Grothendieck topologies on a topological
space $\Opens(X)$ for a moment. We defined the canonical topology
there by saying that a sieve $\calS$ in $\Opens(U)$ ``covers'' $U$ iff
$\bigcup \calS = U$. This is equivalent to saying that a sieve $\calS$
in $\Opens(U)$ covers $U$ iff ${↓}\bigcup\calS = {↓}U$, and if we
define an operation $(·)^*$ on sieves by:
%
$$\calS^* := {↓}\bigcup\calS$$
%
then we can redefine the notion of canonical Grothendieck topology in
terms of it (details soon!). This operation $(·)^*:H→H$, where $H$ is
the Heyting Algebra of sieves-a.k.a.-truth-values obeys, for all
sieves $\calR$ and $\calS$,
%
$$\calS ⊆ \calS^* = \calS^{**}
  \qquad \text{and} \qquad
  (\calR∩\calS)^* = \calR^*∩\calS^* \;\;,
$$
%
which are exactly the conditions on J-operators in \cite{PH2}, except
that J-operators act on ZHAs, not in Heyting Algebras in general.

An operation $(·)^*:H→H$ on a Heyting Algebra $H$ that obeys $\calS ⊆
\calS^* = \calS^{**}$ and $(\calR∩\calS)^* = \calR^*∩\calS^*$ is
called a {\sl nucleus} on $H$. In \cite{PH2} there are lots of
examples of nuclei and ways to visualize them, but the operation
$\calS^* := {↓}\bigcup\calS$ doesn't appear there. In the next section
we will see how to convert nuclei to Grothendick topologies, and
vice-versa.

Note that in the page of examples in sec.\ref{down-sets} the operation
$\calS^* := {↓}\bigcup\calS$ appears at the end {\color{red}(...not
  yet! fix this!)}




%  _   _                    /\/|       _   _ _     
% | \ | |_   _  ___ ___    |/\/___    | | | ( )___ 
% |  \| | | | |/ __/ __|      / __|   | |_| |// __|
% | |\  | |_| | (__\__ \_     \__ \_  |  _  | \__ \
% |_| \_|\__,_|\___|___( )    |___( ) |_| |_| |___/
%                      |/         |/               
%
% «nuclei-congs-and-Hs»  (to ".nuclei-congs-and-Hs")
% (grcp 27 "nuclei-congs-and-Hs")
% (grca    "nuclei-congs-and-Hs")

\section{Nuclei, congruences, and sub-HAs}
\label{nuclei-congs-and-Hs}

In section \ref{other-groth-tops} we saw a way to take a set $\calY$
of sieves and generate a Grothendieck topology $J_\calY$ from it, and
how to take a Grothendieck topology $J$ and generate a set of sieves
$\calY_J$ from it. Now we will do something much more powerful. We
will use a shorter notation: we will use $J$ to denote a Grothendieck
topology, $\calY$ to denote a set of sieves, $∼$ to denote a
congruence, $(·)^*$ to denote a nucleus, and $H'$ to denote a sub-ZHA
(of our planar Heyting Algebra $H$); note that we are using indefinite
articles everywhere --- they imply that there is a ``space of all
`$J$'s'', a ``space of all `$∼$'s'', and so on. From these space of
`$J$'s, of `$∼$'s, etc, we can build the spaces of all functions
between them, and when we say ``a function $(J \mapsto ∼)$'' it will
be implicit that it will be a function that receives `$J$'s and
returns `$∼$'s --- an element of that space of functions.

Fix a two-column graph $D$; let $H$ be the planar Heyting Algebra of
the down-sets of $D$. This $H=\Downs(D)$ is also the algebra of
truth-values of the topos $\SetD$: $H = \Sub(1_\SetD)$. Let $Ω$ be the
(canonical) subobject classifier of the topos $\SetD$. We will need
the 10 definitions below, that suppose that $D$, $H$, and $Ω$ are
fixed:

\begin{enumerate}

\item a {\sl proto-Grothendieck topology} $J$ is an operation that
  takes each $u∈D$ to a subset $J(u)⊂Ω(u)$, and a {\sl Grothendieck
    topology} $J$ is a proto-Grothendieck topology $J$ plus the
  assurance (in the sense of \cite[sections 6.4 and 7.5]{FavC}) that
  this $J$ obeys $\hasmax_J$, $\trans_J$, and $\stab_J$,
  %
  % (favp 33 "basic-example-full")
  % (fav     "basic-example-full")
  % (favp 39 "ness")
  % (fav     "ness")

\item a {\sl proto-congruence} $∼$ is a relation $∼\;⊂H×H$, and a {\sl
  congruence} $∼$ is a proto-congruence $∼$ plus the assurance that
  this $∼$ is an equivalence relation on $H$,

\item a {\sl proto-nucleus} $(·)^*$ is a function $(·)^*: H→H$, and a
  {\sl nucleus} $(·)^*$ is a proto-nucleus $(·)^*$ plus the assurance
  that for all $\calR,\calS∈H$ the conditions $\calR ≤ \calR^* =
  \calR^{**}$ and $(\calR∧\calS)^* = \calR^*∧\calS^*$ hold,

\item a {\sl proto-sub-HA} is a subset $H'⊂H$, and a {\sl sub-HA} is a
  $H'$ that is a Heyting Algebra (obs: with operations $∨_{H'}$ and
  $→_{H'}$ defined in a funny way; see \cite[Definition
  B.10]{Lindenhovius}. TODO: explain that!),
  %
  % (find-lindpage)
  % (find-lindtext)
  % (find-lindpage 54 "Definition B.10")
  % (find-lindtext 54 "Definition B.10")

\item a {\sl proto-set of sieves} $\calY$ is a subset $\calY⊆D$, and a
  {\sl set of sieves} is the same thing as a proto-set of sieves.

\end{enumerate}

In some contexts ``an operation $(J \mto ∼)$'' will be a function that
receives proto-Grothendieck topologies and returns proto-congruences,
and in other contexts it will be a function that receives
(non-proto-)Grothendieck topologies and returns
(non-proto-)congruences --- the notation won't change. We will always
say very clearly if the current context is ``everything is proto'' or
``nothing is proto''.

We will always draw our $(·)^*$s, $H'$s, $∼$s, $J$s and $\calY$s in
this position:
%
$$\mat{ (·)^* &       & H' \\
              & \calY &    \\
          ∼   &       & J  \\
      }
  \qquad
  \qquad
  \setlength{\arraycolsep}{-10pt}
  \mat{ \text{(nucleus)}    &                        & \text{(sub-HA)}    \\
                            & \text{(set of sieves)} &                    \\
        \text{(congruence)} &                        & \text{(Groth.top)} \\
      }
$$

Our first twelve conversion functions will be these ones:
%
$$
  \begin{array}{crll}
    (\calY↦J)     & J(u)    &= \setofst{ \calS∈Ω(u) }{ \calY∩{↓}u⊆\calS } \\
    (J↦\calY)     & \calY   &= \setofst{ u∈D }{ J(u)=\{{↓}u\} } \\
    \\
    ((·)^*↦H') & H'      & =  \setofst{ \calS∈H }{ \calS^*=\calS }=H^* \\
    (H'↦(·)^*) & \calS^* & =  \bigcap\setofst{ \calT∈H' }{ \calS⊆\calT } \\
    \\
    ((·)^*↦∼) & ∼       & =  \setofst{ (\calR,\calS)∈H^2 }{ \calR^*=\calS^* }\\
    (∼↦(·)^*) & \calS^* & =  \bigcup\setofst{ \calR∈H }{ \calR∼\calS }\\
    \\
    ((·)^*↦J) & J(u)    & = \setofst{ \calS∈Ω(u) }{ u∈\calS^* }               \\
    (J↦(·)^*) & \calS^* & = \setofst{ u∈D }{ \calS∩{↓}u∈J(u) }          \\
    \\
    (H'↦J)    & J(u)    & = \setofst{ \calS∈Ω(u) }{ ∀\calT∈H'.\;(\calS⊆\calT ⇒ u∈\calT) }  \\
    (J↦H')    & H'      & = \setofst{ \calS∈H }{ ∀ u∈D.\; (\calS∩{↓}u∈J(u) ⇒ u∈\calS) } \\
    \\
    (∼↦J)     & J(u) & = \setofst{ \calS∈Ω(u) }{ \calS∼{↓}u } \\
    (J↦∼)     & ∼    & = \setofst{ (\calR,\calS)∈H^2 }{ ∀ u∈D.\;(\calR∩{↓}u∈J(u) ↔ \calS∩{↓}u∈ J(u)) } \\
  \end{array}
$$

They correspond to the arrows in these diagrams,
%
%D diagram twelve-conversions
%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 enddiagram
%D
\pu
$$\diag{twelve-conversions}
$$

The right half of that diagram corresponds to this diagram 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
%D 2D  100 A0 - A1
%D 2D      |     |
%D 2D  +25 A2 - A3
%D 2D
%D ren A0 A1 A2 A3 ==> \NucDP \Sub(\DP)^\op \ConDP \GP
%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 enddiagram
%D
$$\pu
  \diag{??}
$$
%
but Lindenhovius uses `$j$'s for nuclei, `$\calM$'s for subframes (we
use sub-HAs instead of subframes), and `$θ$'s for congruences.


Lindenhovius presents the conversions in the way that is standard in
mathematical texts: he starts by defining each of the four corners of
the diagram in its non-proto version, first as a set, and then as a
poset --- see the references in the diagram below,
%
%D diagram references
%D 2Dx     100  +80 +30  +25 +20  +25
%D 2D  100 A0 - A1  B0 - B1  C0 - C1 
%D 2D      |     |  |     |  |     | 
%D 2D  +50 A2 - A3  B2 - B3  C2 - C3 
%D 2D
%D ren A0 ==> \Nuclei
%D ren A1 ==> \Sublocales
%D ren A2 ==> \Congruences
%D ren A3 ==> \Grotops
%D
%D (( A0 A1 -> .plabel= a \Upper
%D    A0 A2 -> .plabel= l \Left
%D    A0 A3 -> .plabel= m \Diag
%D    A1 A3 -> .plabel= r \Right
%D    A2 A3 -> .plabel= b \Lower
%D
%D    # B0 B1 |->
%D    # B0 B2 |->
%D    # B0 B3 |->
%D    # B1 B3 |->
%D    # B2 B3 |->
%D ))
%D enddiagram
%D
$$\pu
  \def\Nuclei     {\mat{\NucDP        \\ \scriptsize \text{(def.~B.6)}}}
  \def\Congruences{\mat{\ConDP        \\ \scriptsize \text{(def.~B.15)}}}
  \def\Sublocales {\mat{\Sub(\DP)^\op \\ \scriptsize \text{(def.~B.10)}}}
  \def\Grotops    {\mat{\GP           \\ \scriptsize \text{(def.~2.1)}}}
  \def\Upper      {\text{(prop.~B.12)}}
  \def\Left       {\text{(prop.~B.23)}}
  \def\Right      {\text{(thm.~B.25)}}
  \def\Lower      {\text{(thm.~B.25)}}
  \def\Diag       {\text{(prop.~B.8)}}
  \diag{references}
$$
%
and then he defines each of the five arrows above as a ``non-proto''
order isomorphism, and this takes at least a half page of his paper in
each case. Let me explain what I mean by ``proto'' and ``non-proto''
here, and explain how we can change the order of the definitions and
leave everything that is not ``proto'' to a second stage (``for
adults''). This idea comes from sections 12 and 19 of \cite{IDARCT}.

\msk

Look at this diagram:
%
%D diagram ??
%D 2Dx     100 +25 +35
%D 2D  100 A   A'  A''
%D 2D
%D 2D  +30 B   B'  B''
%D 2D
%D ren A'' ==> =\setofst{a∈A}{P(a)}
%D ren B'' ==> =\setofst{b∈A}{Q(a)}
%D
%D (( A B -> sl_ .plabel= l f
%D    A B <- sl^ .plabel= r g
%D    A' B' --> sl_ .plabel= l f'
%D    A' B' <-- sl^ .plabel= r g'
%D    A'' place B'' place
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$
%
Suppose that
$A$ is our set of proto-`$a$'s,
$A'$ is our set of `$a$'s,
$B$ is our set of proto-`$b$'s, and
$B'$ is our set of `$b$'s.
Also,
$P$ is a proposition on $A$, and
$Q$ is a proposition on $B$.

When we define a bijection between sets $A$ and $B$ in a proof
assistant or in a type theory we define it as a 4-uple, made of an
arrow $f:A→B$, an arrow $g:B→A$, and assurances that $g∘f=\id$ and
$f∘g=\id$. A {\sl proto-bijection} is just the pair of arrows $(f,g)$,
without the assurances (i.e., without the ``proof-terms''). In order
to show that this bijection restricts to a bijection between $A'$ and
$B'$ we need two other proof terms: one for $∀a∈A.(P(a)→Q(f(a)))$ and
another for $∀b∈B.(Q(b)→P(g(b)))$. Lindenhovius uses this order of
definition,
%
$$\begin{array}{l}
  A, P, B, Q, \\
  f, (∀a∈A.(P(a)→Q(f(a)))), \\
  g, (∀b∈B.(Q(b)→P(g(b)))), \\
  (∀a∈A.(P(a)→a=g(f(a)))), \\
  (∀b∈B.(Q(b)→b=f(g(b)))), \\
  \end{array}
$$
%
and on top of that he also defines ordering on its sets $A'$ and $B'$,
and proves that his `$f$'s and `$g$'s preserve these orderings.

Our intent here is to show that to understand Grothendieck topologies
on (finite) posets we {\sl can}, and we {\sl should}, start by just
the ``proto'' part,
%
$$\begin{array}{l}
  A, B, f, g
  \end{array}
$$
%
that in this case will be the definitions of proto-Grothendieck
topology, proto-congruence, proto-nucleus, proto-sub-HA and proto-set
of sieves from the beginning of this section, plus the 12 conversion
functions in this diagram:
%
$$\diag{twelve-conversions}
$$

Let's fix a two-column graph $D$; we will use the Art Déco N of
section \ref{ex-topologies} as our $D$. Remember that its algebra of
truth-values is this ZHA:
%
$$H = \Downs(N) = \pwibo{{32}{33} {20}{21}{22}{23} {10}{11}{12}{13} {00}{01}{02}{03}}$$

In sections 1 and 2 of \cite{PH2} we defined ``slashings'' on a ZHA.
They looked like this:
%
%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
$$\zha{WB_notnot}$$
%
but they could be interpreted in many ways. We will add subscripts to
them to disambiguate:
%
$$(·)^* = \left(\zha{WB_notnot}\right)_{(·)^*}
  \qquad
  ∼ \; = \left(\zha{WB_notnot}\right)_{(∼)}
$$
%
Here the subscript $(·)^*$ in the first slashing indicates that we are
interpreting it as the operation that takes all elements in each
region to the top element of that region, and the subscript $(∼)$ 
in
the second one indicate that we are interpreting it as the equivalence
relation that says that $\calR∼\calS$ is true iff $\calS$ and $\calS$
are both in the same region. The ``$(·)^*$='' and the ``$∼\;=$'' mean
``let $(·)^*$ be this function from $H$ to $H$'' and ``let $∼$ be this
equivalence relation on $H$''.

\msk

The {\sl X-shaped diagram} associated to a given set of sieves $\calY$
is built as this: 1) take this $\calY$, and use the twelve conversions
in any order you like to build the $(·)^*$, the $H'$, the $∼$, and the
$J$ associated to it; the theorems in \cite{Lindenhovius} indicate
that the results will be will-defined and don't depend on the order
used to define them; 2) draw them in this position,
%
$$\mat{ (·)^* &       & H' \\
              & \calY &    \\
          ∼   &       & J  \\
      }
$$
%
replacing each symbol by its corresponding value.

\newpage


Here are two examples of X-shaped diagrams.

\msk

% «double-negation»  (to ".double-negation")
% (grcp 33 "double-negation")
% (grca    "double-negation")

\def\mysetofsieves{\{1▁,▁1\}}

1. For $\calY = \mysetofsieves$ we get this --- compare it

with the double negation modality of \cite[sec.6]{PH2}:

%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\mysubzha    {\wiBo{·{33} {20}··· ···· {00}··{03}}}
\def\mynucleus   {\left( \zha{ArtDecoNQ} \right)_{(·)^*}}
\def\mycongruence{\left( \zha{ArtDecoNQ} \right)_{(∼)}}
%
$$\scalebox{0.95}{$
  \setlength{\arraycolsep}{0pt}
  \begin{array}{ccc}
  \mynucleus && \mysubzha \\
     &\mysetofsieves& \\
  \mycongruence && \scalebox{0.8}{$\mygrotop$} \\
  \end{array}
  $}
$$


% «forcing»  (to ".forcing")
% (grcp 33 "forcing")
% (grca    "forcing")

\def\mysetofsieves{\csm{
  3▁,▁3,\\
  \;\;\;\;\;\;▁2,\\
  1▁,▁1}}

2. For $\calY = \mysetofsieves$ we get this --- the

``forcing modality'' $({∧}21∧{→}12)$ of \cite[sec.6]{PH2}):

% (jonp 19 "polynomial-J-ops")
% (joa     "polynomial-J-ops")

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


\newpage

%  __  __                  _                __                     
% |  \/  | ___  __ _ _ __ (_)_ __   __ _   / _|_ __ ___  _ __ ___  
% | |\/| |/ _ \/ _` | '_ \| | '_ \ / _` | | |_| '__/ _ \| '_ ` _ \ 
% | |  | |  __/ (_| | | | | | | | | (_| | |  _| | | (_) | | | | | |
% |_|  |_|\___|\__,_|_| |_|_|_| |_|\__, | |_| |_|  \___/|_| |_| |_|
%                                  |___/                           
%
% «meaning-from-pictures»  (to ".meaning-from-pictures")
% (grcp 41 "meaning-from-pictures")
% (grca    "meaning-from-pictures")
\section{Extracting meaning from pictures}
\label{meaning-from-pictures}

(This section is a mess)

\msk

After calculating a few X-shaped diagrams by brute force we get ---
or, let me be more honest: {\sl I got} --- some visual intuition on
what the twelve conversions from section \ref{nuclei-congs-and-Hs}
``mean''... in particular, I became able to reconstruct the
definitions of the twelve conversions from vague memories of what they
should do. My memory is especially bad, and I have to reconstruct
definitions and proofs all the time; I wrote a bit about that in
\cite[section 10]{IDARCT} and \cite[section 6]{FavC}.

This is an excerpt from a long blog post by Kevin Buzzard
(\cite{Buzzard2021}):
%
% https://xenaproject.wordpress.com/2021/01/21/formalising-mathematics-an-introduction/
%
\begin{quote}

  {\bf Mathematicians think in pictures}

  I have a picture of the real numbers in my head. It's a straight
  line. This picture provides a great intuition as to how the real
  numbers work. I also have a picture of what the graph of a
  differentiable function looks like. It's a wobbly line with no kinks
  in. This is by no means a perfect picture, but it will do in many
  cases. For example: If someone asked me to prove or disprove the
  existence of a strictly increasing infinitely differentiable
  function $f:\R→\R$ such that $f'(37)=0$ and $f''(37)<0$ then I would
  start by considering a picture of a graph of a strictly increasing
  function (monotonically increasing as we move from left to right),
  and a second picture of a function whose derivative at $x=37$ is
  zero and whose second derivative is negative (a function with a
  local maximum). I then note that there are features in these
  pictures which make them incompatible with each other. Working with
  these pictures in mind, I can now follow my intuition and write down
  on paper a picture-free proof that such a function cannot exist, and
  this proof would be acceptable as a model solution to an exam
  question. My perception is that other working mathematicians have
  the same pictures in their head when presented with the same
  problem, and would go through roughly the same process if they were
  asked to write down a sketch proof of this theorem.

\end{quote}

A good part of \cite{Lindenhovius} is about nice properties that we
have when our posets are finite, or Artinian, and that do not need to
hold in more complex cases --- and I don't have a way to discuss them
with diagrams yet.

(To do: mention Badiou, and how the non-mathematicians that study
Badiou that I know try to understand his uses of toposes)



%  _   _____     _                    _             _           
% | | |_   _|   | |_ ___  _ __   ___ | | ___   __ _(_) ___  ___ 
% | |   | |_____| __/ _ \| '_ \ / _ \| |/ _ \ / _` | |/ _ \/ __|
% | |___| |_____| || (_) | |_) | (_) | | (_) | (_| | |  __/\__ \
% |_____|_|      \__\___/| .__/ \___/|_|\___/ \__, |_|\___||___/
%                        |_|                  |___/             
%
% «LT-topologies»  (to ".LT-topologies")
% (grcp 36 "LT-topologies")
% (grca    "LT-topologies")
\section{Lawvere-Tierney topologies}
\label{LT-topologies}

It is easy to connect what we saw in the previous sections with
Lawvere-Tierney topologies. Let me state some facts without proof.

1. Start with a nucleus $(·)^*$ on a ZHA, and calculate both its
associated set of sieves $\calY$ and its 2-column graph with question
marks (as in \cite[section 1.1]{PH2}). The elements of $\calY$ are
exactly the points of the 2CG that do not have question marks. For
example, here $\calY = \{3▁,1▁,▁1,▁2,▁3\}$:

%L ArtDecoNQ_ts   = TCGSpec.new("33; 32, ", ".??", ".??")
%L ArtDecoNQ_ts   = TCGSpec.new("33; 32, ", "?.?", ".?.")
%L ArtDecoNQ_td_1 = TCGDims {h=35,  v=25,  q=15, crh=12,  crv=8, qrh=0}
%L ArtDecoNQ_ts:mp({zdef="ArtDecoNQ", scale="12pt", meta=""}):addlrs():output()
%L ArtDecoNQ_tq   = TCGQ.newdsoa(ArtDecoNQ_td_1, ArtDecoNQ_ts,
%L                              {tdef="ArtDecoNQ", meta="1pt p"},
%L                              "h v q ap"):lrs():output()
\pu

$$\zha{ArtDecoNQ} \quad \squigbij \quad \tcg{ArtDecoNQ}$$

2. Start with a nucleus $(·)^*$ on a ZHA, and calculate its associated
Grothendieck topology $J$ and its Lawvere-Tierney topology $j$. This
$j$ is the characteristic map of the inclusion $J \ito Ω$ in the
pullback diagram below:
%
%D diagram j-and-J
%D 2Dx     100  +25
%D 2D  100 A0 - A1
%D 2D      |     |
%D 2D  +25 A2 - A3
%D 2D
%D ren A0 A1 A2 A3 ==> J 1 Ω Ω
%D
%D (( A0 A1  -> .plabel= a !
%D    A0 A2 `-> .plabel= l i
%D    A1 A3 `-> .plabel= r ⊤
%D    A2 A3  -> .plabel= b j:=χ_i
%D
%D ))
%D enddiagram
%D
$$\pu
  \diag{j-and-J}
$$

Our big diagram in section \ref{ex-topologies} hinted at an
alternative way to draw each $J(u)$ and each $Ω(u)$, in this part:
%
$$\begin{array}{ccc}
  \bhhh{?· 1? ?1} &⊂& \bhhh{?· ?? ??} \\[15pt]
    \rotl{=}      &&    \rotl{=} \\
  \pwibo{{32}· ·{21}{22}· ···· ····}
  &⊂&
  \pwibo{{32}· {20}{21}{22}· {10}{11}{12}· {00}{01}{02}·} \\
  \end{array}
$$

Let's take this alternative way further. For each ex-open set $u∈D$
the map $j(u):Ω(u)→Ω(u)$ can be drawn in a very nice way as a slashing
on just $Ω(u)$; we draw the points of $H$ that are not in $Ω(u)$ as
dots to indicate that they are outside of the domain, as we did in
section \ref{down-sets}.

We can calculate the $J$ and the $j$ for the nucleus $(·)^*$ above by
brute force, and draw them. We get this:
%
% (cltp 3 "inclusions")
% (clt    "inclusions")
%
%L ts = TCGSpec.new("33; 32, ")
%L mp = ts:mpunder("32", {zdef="A:J:3_", scale="8pt", meta="s"}, "21"):output()
%L mp = ts:mpunder("20", {zdef="A:J:2_", scale="8pt", meta="s"}, "20"):output()
%L mp = ts:mpunder("10", {zdef="A:J:1_", scale="8pt", meta="s"}, "00"):output()
%L mp = ts:mpunder("03", {zdef="A:J:_3", scale="8pt", meta="s"}, "03"):output()
%L mp = ts:mpunder("02", {zdef="A:J:_2", scale="8pt", meta="s"}, "01"):output()
%L mp = ts:mpunder("01", {zdef="A:J:_1", scale="8pt", meta="s"}, "01"):output()
%L
%L ts = TCGSpec.new("33; 32, ", ".??",".??")
%L ts = TCGSpec.new("33; 32, ", "?.?",".?.")
%L mp = ts:mpunder("32", {zdef="A:j:3_", scale="8pt", meta="s"}):output()
%L mp = ts:mpunder("20", {zdef="A:j:2_", scale="8pt", meta="s"}):output()
%L mp = ts:mpunder("10", {zdef="A:j:1_", scale="8pt", meta="s"}):output()
%L mp = ts:mpunder("03", {zdef="A:j:_3", scale="8pt", meta="s"}):output()
%L mp = ts:mpunder("02", {zdef="A:j:_2", scale="8pt", meta="s"}):output()
%L mp = ts:mpunder("01", {zdef="A:j:_1", scale="8pt", meta="s"}):output()
\pu
%
$$J =
  \scalebox{0.95}{$
  \padnbiggg
  {\zha{A:J:3_}} {\zha{A:J:_3}}
  {\zha{A:J:2_}} {\zha{A:J:_2}}
  {\zha{A:J:1_}} {\zha{A:J:_1}}
  $}
  %
  \quad
  %
  j =
  \scalebox{0.95}{$
  \padnbiggg
  {\zha{A:j:3_}} {\zha{A:j:_3}}
  {\zha{A:j:2_}} {\zha{A:j:_2}}
  {\zha{A:j:1_}} {\zha{A:j:_1}}
  $}
$$


We have: a) $j(u)(\calS) = \calS^*∧{↓}u$, and b)
$J(u)=\setofst{\calS∈Ω(u)}{\calS^*={↓}u}$, i.e., $J(u)$ is made of the
points of $Ω(u)$ in the topmost region of $j(u)$. It is possible to
prove that these properties hold in general, and they mean that if we
start from a nucleus $(·)^*$ it is very easy to draw the $j$ and the
$J$ associated to it: each $j(u)$ is made by ``restricting $(·)^*$ to
${↓}u$'', and each $J(u)$ in this notation is made of the elements of
the topmost region of the corresponing $j(u)$; to draw each $J(u)$ in
the other notation we have to erase everything above ${↓}u$ and write
the ex-open sets with question marks as `$?$'s and the other ones as
`$1$'. For example:
%
$$\tcg{ArtDecoNQ}
  \qquad
  \squigto
  \qquad
  \bhhh{?· 1? ?1} = J(3▁)
$$




% \cite[sections 1 and 1.1]{ClopsAndTops}
% (cltp 3 "inclusions")
% (clt    "inclusions")
% (cltp 33 "Jop-to-top")
% (clt     "Jop-to-top")
% (cltp 38 "def-j-example")
% (clt     "def-j-example")
% (cltp 28 "SetT-classifier-defs")
% (clt     "SetT-classifier-defs")


\section{Etc}

TODO: closure operators, sheaves, the sheafification functor. Clean up
\cite{ClopsAndTops} and \cite{PH2}. The functor `$+$' of
\cite[p.129]{MacLaneMoerdijk}.

THANKS: to Ana Luiza Tenório for all the encouragement, comments, and
questions!

\bsk




% \section*{Garbage}
%
% (Everything below this point is garbage)




% (find-books "__cats/__cats.el" "picado-pultr")
% (find-books "__cats/__cats.el" "joyal-tierney")





\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=2021groth-tops-children veryclean
make -f 2019.mk STEM=2021groth-tops-children pdf

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