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

% «.sheaves»		(to "sheaves")
% «.unique-glueing»	(to "unique-glueing")
% «.finite-topologies»	(to "finite-topologies")
% «.OO-House»		(to "OO-House")

\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{indentfirst}
\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")
%
% (find-es "tex" "geometry")
\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")





\def\Cinfty{\mathcal{C}^\infty}
\def\sfSets{\mathsf{Sets}}
\def↓{{\downarrow}}
\def\phop{{}^{\phantom{\op}}}

%L vee   = "1.2|.3."
%L kite  = ".1.|2.3|.4.|.5."
%L house = ".1.|2.3|4.5"
%L mp = MixedPicture.new({def="dagKite",  meta="t", scale="4pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagKite",  meta="s", scale="6pt"}, z):zfunction(kite):output()
%L mp = MixedPicture.new({def="dagHouse", meta="s", scale="5pt"}, z):zfunction(house):output()
%L mp = MixedPicture.new({def="dagVee",   meta="s", scale="5pt"}, z):zfunction(vee):output()
\pu
\def\V{\dagVee}

\def\dagVee#1#2#3{\vcenter{\hbox{\unitlength=5pt%
\celllower=2pt%
\def\cellfont{\scriptsize}%
\begin{picture}(3,2)(-0.5,-0.5)
  \put(0,1){\cell{#1}}
  \put(2,1){\cell{#2}}
  \put(1,0){\cell{#3}}
\end{picture}}}}



\title{On a way to visualize (some) sheaves}

\author{Eduardo Ochs \\
  \url{http://angg.twu.net/math-b.html}
}

\maketitle

\begin{abstract}

  This is an attempt to connect the way in which sheaves are presented
  in \cite{MacLaneMoerdijk} with the approach ``for children'' from
  \cite{PH1}, \cite{PH2}, and \cite{FavC} --- but these notes are a
  work in progress that is still in a very preliminary form.

\end{abstract}



%  ____  _                               
% / ___|| |__   ___  __ ___   _____  ___ 
% \___ \| '_ \ / _ \/ _` \ \ / / _ \/ __|
%  ___) | | | |  __/ (_| |\ V /  __/\__ \
% |____/|_| |_|\___|\__,_| \_/ \___||___/
%                                        
% «sheaves»  (to ".sheaves")
% (shvp 1 "sheaves")
% (shv    "sheaves")

\section{Sheaves}

The archetypal example of a sheaf is the operation
%
$$\begin{array}{rrcl}
  \Cinfty: & \Opens(\R)^\op &→& \Set \\
           & U & \mapsto & \setofst{f:U→\R}{f \text{ is } \Cinfty} \\
  \end{array}
$$
%
that expects open sets of $\R$ and returns sets of functions; more
precisely, for each subset $U⊆\R$ it returns $\Cinfty(U)$, the set of
infinitely differentiable functions from $U$ to $\R$.

This $\Cinfty$ is a {\sl contravariant functor}. The topology
$\Opens(\R)$ is a preorder category whose morphisms are the
inclusions, and the image by $\Cinfty$ of each inclusion map $V \ito
U$ is a {\sl restriction map} $\Cinfty(U) → \Cinfty(V)$. In a diagram:
%
%D diagram ??
%D 2Dx     100 +15 +25 +15 +25 +15
%D 2D  100 A0      B0
%D 2D        <-      ->
%D 2D  +15     A1      B1      C1
%D 2D        ->      <-      <-
%D 2D  +15 A2      B2      C2
%D 2D        <-      ->
%D 2D  +15     A3      B3
%D 2D
%D 2D  +15 D0
%D 2D  +10 D1 ---> D2
%D 2D
%D ren A0 A1 A2 A3 ==> \R U V ∅
%D ren B0 B1 B2 B3 ==> \Cinfty(\R) \Cinfty(U) \Cinfty(V) \Cinfty(∅)
%D ren C1 C2       ==> f_U f_U|_V
%D ren D0 D1 D2    ==> \Opens(\R) \Opens(\R)^\op \Set
%D
%D (( A3 A2 `-> A2 A1 `-> A1 A0 `->
%D    B0 B1 -> B1 B2 -> B2 B3 ->
%D    C1 C2 |->
%D    
%D    D0 place
%D    D1 D2 -> .plabel= a \Cinfty
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

This diagram follows the conventions from \cite[section 2]{FavC}. In
brief:

\begin{itemize}

\item[(CAI)] the diagram $∅ \ito V \ito U \ito \R$ is drawn above
  $\Opens(\R)$ to indicate that it is inside the category
  $\Opens(\R)$,

\item[(CFSh)] the image of $∅ \ito V \ito U \ito \R$ by the functor
  $\Cinfty$ is drawn as a diagram with the same shape as the original;
  in particular, the unnamed arrow $\Cinfty(V)←\Cinfty(U)$ is the
  image by $\Cinfty$ of the (unnamed) inclusion map $V \ito U$,

\item[(C$↦$)] the arrow $f_U \mapsto f_U|_V$ is the internal view of
  the unnamed arrow $\Cinfty(U)→\Cinfty(V)$, and $f_U|_V := \Cinfty(U
  \iot V)(f_U)$.

\end{itemize}

The rationale for having an `$\Opens(\R)$' above the
`$\Opens(\R)^\op$' is explained in \cite[section 7.4]{FavC}, and our
reasons for drawing topological spaces with the ``everything'' on top
and the ``nothing'' at the bottom are explained in \cite{PH1}; in
short, that's because we will at some point treat $\Opens(\R)$ as a
logic, in which $\R$ is `true', `top', and `$⊤$'.

% (favp 38 "opposite-categories")
% (fav     "opposite-categories")

%  _   _  ____ ____  
% | | | |/ ___|  _ \ 
% | | | | |  _| |_) |
% | |_| | |_| |  __/ 
%  \___/ \____|_|    
%                    
% «unique-glueing»  (to ".unique-glueing")
% (shvp 2 "unique-glueing")
% (shv    "unique-glueing")

\subsection{The unique glueing property}

$\Cinfty$ has the ``unique glueing property''. The UGP can be
formalized in several different, and slightly incompatible, ways.

Take any two open sets $U_1, U_2 ∈ \Opens(\R)$ and choose functions
$f_{U_1}∈\Cinfty(U_1)$ and $f_{U_2}∈\Cinfty(U_2)$. We say that
$f_{U_1}$ and $f_{U_2}$ are {\sl compatible} when their restrictions
to $\Cinfty(U_1∩U_2)$ are the same --- i.e., when $f_{U_1}|_{U_1∩U_2}
= f_{U_2}|_{U_1∩U_2}$. In a diagram:
%
%D diagram ??
%D 2Dx     100 +20 +20 +25 +20 +20 +25 +20 +20
%D 2D  100     A0          B0          C0
%D 2D
%D 2D  100 A1      A2  B1      B2  C1      C2
%D 2D
%D 2D  +20     A3          B3          C3
%D 2D
%D ren A1 A2 A3 ==> U_1 U_2 U_1∩U_2
%D ren B1 B2 B3 ==> \Cinfty(U_1) \Cinfty(U_2) \Cinfty(U_1∩U_2)
%D ren C1 C2 C3 ==> f_{U_1} f_{U_2} f_{U_1}|_{U_1∩U_2}=f_{U_2}|_{U_1∩U_2}
%D
%D (( A3 A1 `-> sl_ A3 A2 `->
%D    B1 B3  -> B2 B3  ->
%D    C1 C3 |-> C2 C3 |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

Our first version of the unique glueing property is this. For all
$U_1, U_2 ∈ \Opens(\R)$, for every {\sl compatible} pair
$(f_{U_1},f_{U_2}) ∈ \Opens(U_1)×\Opens(U_2)$ has a {\sl unique
  glueing}: there is a unique $f∈\Cinfty(U_1∪U_2)$ such that this $f$
restricts to $f_{U_1}$ and $f_{U_2}$, i.e., $f|_{U_1}=f_{U_1}$ and
$f|_{U_2}=f_{U_2}$. In a diagram:
%
%D diagram ??
%D 2Dx     100 +20 +20 +25 +20 +20 +25 +20 +20
%D 2D  100                             C0
%D 2D   +8     A0          B0         
%D 2D  +12                         C1'     C2'
%D 2D  +8  A1      A2  B1      B2  C1      C2
%D 2D
%D 2D  +20     A3          B3          C3
%D 2D
%D ren A0 A1 A2 A3 ==> U_1∪U_2 U_1 U_2 U_1∩U_2
%D ren B0 B1 B2 B3 ==> \Cinfty(U_1∪U_2) \Cinfty(U_1) \Cinfty(U_2) \Cinfty(U_1∩U_2)
%D ren    C1 C2 C3 ==> ∀f_{U_1} ∀f_{U_2} f_{U_1}|_{U_1∩U_2}=f_{U_2}|_{U_1∩U_2}
%D ren C0 C1' C2'  ==> ∃!f f|_{U_1} f|_{U_2}
%D
%D (( A1 A0 `-> A2 A0 `-> A3 A1 `-> sl_ A3 A2 `->
%D    B0 B1  -> B0 B2  -> B1 B3  ->     B2 B3  ->
%D    C1 C3 |-> C2 C3 |->
%D    C0 C1' |-> C0 C2' |->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$


Our second version of the UGP deals with compatible {\sl families} of
functions. Take an index set $I$, a family of open sets $(U_i)_{i∈I}$
such that each $U_i∈\Opens(\R)$, and a family of functions
$(f_i)_{i∈I}$ such that each $f_i∈U_i$. We say that this family of
functions is {\sl pairwise compatible} if
%
$$∀i,j∈I. f_i|_{U_i∩U_j} = f_j|_{U_i∩U_j},$$
%
and we say that this family {\sl has a unique glueing} if there is a
unique $f∈\Cinfty(U)$, where $U:=\bigcup_{i∈I}U_i$, such that
%
$$∀i∈I. f_i = f|_{U_i}.$$

% (find-books "__cats/__cats.el" "maclane-moerdijk")
% (find-maclanemoerdijkpage (+   11  64) "II. Sheaves of Sets")
% (find-maclanemoerdijkpage (+   11  64)   "1. Sheaves")
% (find-books "__logic/__logic.el" "hott")
% (find-hottpage (+ 12 25) "1.4 Dependent function types (-types)")
% (find-hottpage (+ 12 26) "1.5 Product types")
% (find-hottpage (+ 12 30) "1.6 Dependent pair types (-types)")

A standard reference for this is \cite{MacLaneMoerdijk}, section II.1,
but it uses some notational tricks that took me years (really!!!) to
understand... they are easy to decypher when we know some notations
from dependent types, though.

Let $A=\{2,3\}$, $B=\{4,5\}$, $C_2=\{20,21\}$, $C_3=\{32,33\}$. The
notations for the set of all pairs $(a,b)$ with $a∈A$ and $b∈B$ and
for all function that take each $a∈A$ to a $b∈B$ are well-known: $A×B$
and $B^A$, but we will sometimes write $B^A$ as $A{→}B$.
%
% using a `$→$' with very little whitespace around it to distinguish
% this from the other uses of the arrow.
%
The standard notations for the set of all pairs $(a,c)$ with $a∈A$ and
$c∈C_a$ and for the set of all functions that take each $a∈A$ to a
$c∈C_a$ are less familiar (see \cite[sections 1.4 and 1.6]{HOTT}):
$Σ_{a∈A}.C_a$ and $Π_{a∈A}.C_a$. Some programming languages with
support for dependent types, such as Agda, implement a notation that
looks like an extension of `$×$' and `$→$':
%
$$\begin{array}{rcl}
    (a:A)×C_a &:=& Σ_{a∈A}.C_a \\
    (a:A)→C_a &:=& Π_{a∈A}.C_a \\
  \end{array}
$$
%
So we have:
%
$$\begin{array}{rcl}
    (a:A)×C_a &:=& \{(2,20), (2,21), (3,32), (3,33)\}, \\
    (a:A)→C_a &:=& \{ \{(2,20), (3,32)\}, \\
                && \;\, \{(2,20), (3,33)\}, \\
                && \;\, \{(2,21), (3,32)\}, \\
                && \;\, \{(2,21), (3,33)\} \}. \\
  \end{array}
$$

A family of pairwise functions on $\Cinfty$ is a triple
%
$$(I,\calU,\calF) \quad : \quad
  (I:\sfSets) × (\calU:I→\Opens(\R)) × (\calF : (i:I)→\Cinfty(\calU i))
$$
%
obeying:
%
$$∀i,j∈I. (\calF i)|_{(\calU i ∩ \calU j)} = (\calF j)|_{(\calU i ∩ \calU j)}.
$$

\msk

Our third version of the UGP needs ``downward-closedness''. For a
subset $\calV⊆\Opens(\R)$ we define
%
$$↓\calV := \setofst{W∈\Opens(\R)}{∃V∈\calV. W⊆V},$$
%
and we say that a $\calV⊆\Opens(\R)$ is {\sl sieve} when $\calV =
↓\calV$. A {\sl compatible family $\calG$ on a sieve $\calV$} is a
family $\calG : (V:\calV) → \Cinfty(V)$ obeying:
%
$$∀V,W∈\calV.\; W⊆V → \calG W = \calG V|_W.
$$

A compatible family $\calG$ on a sieve $\calV$ has a unique glueing
iff there is a unique $f∈\Cinfty(U)$, where $U = \bigcup \calV$, such
that
%
$$∀V∈\calV,\; f|_V=\calG V.$$

A good way to understand how these ideas can be generalized is to work
on cases where everything is finite and everything can be drawn
explicitly.


%  ____                     _                          
% |  _ \ _ __ ___  ___  ___| |__   __ ___   _____  ___ 
% | |_) | '__/ _ \/ __|/ _ \ '_ \ / _` \ \ / / _ \/ __|
% |  __/| | |  __/\__ \  __/ | | | (_| |\ V /  __/\__ \
% |_|   |_|  \___||___/\___|_| |_|\__,_| \_/ \___||___/
%                                                      
% «finite-topologies»  (to ".finite-topologies")
% (shvp 4 "finite-topologies")
% (shv     "finite-topologies")

\subsection{Presheaves (on some finite topologies)}

In the previous sections we worked with a fixed topology,
$\Opens(\R)$, and with a fixed contravariant functor,
$\Cinfty:\Opens(\R)^\op→\Set$. We saw that $\Cinfty$ obeys three
different ``unique glueing properties'' that were easy to understand;
we will now generalize this, in two steps.

Let $X$ be the open interval $(0,3)⊂\R$, and let
%
$$\Opens(X) := \{∅,\, (1,2),\, (0,2),\, (1,3),\, (0,3)\},$$
%
which is a subtopology of the usual topology on $(0,3)$. As
$\Opens(X)$ is finite we can draw it, and its image by $\Cinfty$,
explicitly:
%
%D diagram presh-1
%D 2Dx     100 +20 +20 +35 +20 +20 +20 +20
%D 2D  100     A1          B1
%D 2D  +20 A2      A3  B2      B3
%D 2D  +20     A4          B4
%D 2D  +20     A5          B5
%D 2D
%D 2D  +15     C0
%D 2D  +10     C1          C2
%D 2D
%D ren A1 A2 A3 A4 A5 ==> (0,3) (0,2) (1,3) (1,2) ∅
%D ren B1 B2 B3 B4 B5 ==> \Cinfty((0,3)) \Cinfty((0,2)) \Cinfty((1,3)) \Cinfty((1,2)) \Cinfty(∅)
%D ren C0 C1 C2 ==> \Opens(X) \Opens(X)^\op \Set
%D
%D (( A5 A4 `-> A4 A2 `-> A4 A3 `-> A2 A1 `-> A3 A1 `->
%D    B1 B2  -> B1 B3  -> B2 B4  -> B3 B4  -> B4 B5  ->
%D    C0 place  C1 C2  -> .plabel= a \Cinfty
%D ))
%D enddiagram
%D
$$\pu
  \diag{presh-1}
$$


In \cite[sections 1, 2, 12, and 13]{PH1}, we saw how to interpret
diagrams like $\dagVee•••$ as directed acyclical graphs (DAGs), how to
define an order topology on a DAG, and how to draw these topologies.
If we replace $X$ by $\dagVee•••$ and $\Cinfty$ by an arbitrary
contravariant functor $F:\Opens(\dagVee•••)^\op→\Set$ we get this,
%
%D diagram presh-2
%D 2Dx     100 +20 +20 +35 +20 +20 +20 +20
%D 2D  100     A1          B1
%D 2D  +20 A2      A3  B2      B3
%D 2D  +20     A4          B4
%D 2D  +20     A5          B5
%D 2D
%D 2D  +15     C0
%D 2D  +10     C1          C2
%D 2D
%D ren A1 A2 A3 A4 A5 ==>   \V111    \V101    \V011    \V001    \V000
%D ren B1 B2 B3 B4 B5 ==> F(\V111) F(\V101) F(\V011) F(\V001) F(\V000)
%D ren C0 C1 C2 ==> \Opens(\V•••) \Opens(\V•••)^\op \Set
%D
%D (( A5 A4 `-> A4 A2 `-> A4 A3 `-> A2 A1 `-> A3 A1 `->
%D    B1 B2  -> B1 B3  -> B2 B4  -> B3 B4  -> B4 B5  ->
%D    C0 place  C1 C2  -> .plabel= a F
%D ))
%D enddiagram
%D
$$\pu
  \diag{presh-2}
$$
%
that by (an intentional) coincidence has the same shape as the
previous diagram. The trick to ``pronounce'' things like $\V011$ is
explained in \cite[section 1]{PH1}: if we read aloud the digits of
$\V011$ in ``reading order'', i.e., for top to bottom and in each line
from left to right, then it becomes ``zero-one-one''.

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

Now that our topology has a definite shape we can use that shape, with
`0's and `1's at the right positions, to talk of subsets of it. For
example, $\{\V101, \V011\} = \dagKite01100$, and this is not a sieve,
because $↓\dagKite01100 = \dagKite01111$; also, $\bigcup\dagKite01100
= \bigcup\{\V101, \V011\} = \V111$, and $↓\{\bigcup\dagKite01100\} =
\dagKite11111$.

We can also choose other presheaves and test if they obey the unique
glueing properties. Let $E$ be this functor:
%
%D diagram presh-3
%D 2Dx     100 +20 +20 +35 +20 +20 +20 +20
%D 2D  100     A1          B1
%D 2D  +20 A2      A3  B2      B3
%D 2D  +20     A4          B4
%D 2D  +20     A5          B5
%D 2D
%D 2D  +15     C0
%D 2D  +10     C1          C2
%D 2D
%D ren A1 A2 A3 A4 A5 ==>   \V111    \V101    \V011    \V001    \V000
%D ren B1 B2 B3 B4 B5 ==> \{23,24\} \{1\} \{1,2\} \{1\} \{0,1\}
%D ren C0 C1 C2 ==> \Opens(\V•••) \Opens(\V•••)^\op \Set
%D
%D (( A5 A4 `-> A4 A2 `-> A4 A3 `-> A2 A1 `-> A3 A1 `->
%D    B1 B2  -> B1 B3  -> B2 B4  -> B3 B4  -> B4 B5  ->
%D    C0 place  C1 C2  -> .plabel= a E
%D ))
%D enddiagram
%D
$$\pu
  \diag{presh-3}
$$

For the first version of the UGP, let $U_1=\V101$, $U_2=\V011$,
$f_{U_1} = 1$, $f_{U_2} = 2$. This is a compatible pair, because
$U_1∩U_2=\V001$ and $f_{U_1}|_{U_1∩U_2} = f_{U_2}|_{U_1∩U_2} = 1$ ---
but there is no $f∈E(U_1∪U_2)$ that restricts to both $f_{U_1}$ and
$f_{U_2}$; to check this we just need to test the two candidates, 23
and 24.

The second version of the UGP needs an index set. Take $I=\{42,200\}$
--- 42 and 200 are two of my favorite numbers ---, and $\calU =
\{(42,\V101), (200,\V011)\}$, $\calF = \{(42,1), (200,2)\}$. This is a
pairwise compatible family of functions, but it has two possible
glueings. We have $U:=\bigcup_{i∈I} U_i = \V111$, and both $23$ and
$24$ are glueings, i.e., are possible values for the
$f∈E(\bigcup_{i∈I} U_i)$ that obeys $∀i∈I. f_i = f|_{U_i}$.

The third version of the UGP is the nicest to draw. A pair
$(\calV⊆\Opens(\V111), \calG : (V:\calV) → E(V))$ can be drawn using
the conventions for drawing partial functions from \cite[section
  1]{PH1}: we call $\calV$ the {\sl support} of the family $(\calV,
\calG)$, and for each $V∈\Opens(\V•••)$ we draw $\calG V$ on the
position of $V$ if $V∈\calV$; when $V\not∈\calV$ we draw a `$·$'. For
example, let
%
$$\begin{array}{c}
  \calV = \{\V101, \V011, \V000\} = \dagKite·••·• = \dagKite01101, \\
  \calG = \{(\V101, 1), (\V011, 2), (\V000,0)\} = \dagKite·12·0, \\
  (\calV,\calG) = \left( \dagKite·••·•, \dagKite·12·0 \right). \\
  \end{array}
$$

This $\calV = \dagKite·••·•$ isn't a sieve, and this $\calG =
\dagKite·12·0$ isn't compatible downwards. We want to restrict our
attention to sieves, and it turns out the set of all sieves on
$\Opens(\dagVee•••)$ is exactly $\Opens(\Opens(\dagVee•••))$, the
order topology on the partial order $\dagKite•••••$. A very good place
to learn about this is the section about down-sets and up-sets of
\cite[page 20 onwards]{DaveyPriestley}; for an ordered set $P$ they
define $\Opens(P)$ as the ``ordered set of down-sets of $P$'' in a way
that is very easy to iterate


% (find-books "__alg/__alg.el" "davey-priestley")
% (find-daveypriestleypage (+ 14  20)  "Down-sets and up-sets")

% (find-LATEXgrep "grep --color -nH --null def.ito *")


\newpage


%D diagram ??
%D 2Dx     100 +40 +40 +40
%D 2D  100 A0  A1  C0  C1
%D 2D
%D 2D  +30 A2  A3  C2  C3
%D 2D
%D 2D  +25 B0      D0
%D 2D  +15 B1  B2  D1  D2
%D 2D
%D ren A0 ==> \left(\dagKite11111\right)
%D ren A2 ==> \left(\dagKite01111\right)
%D ren C0 ==> \left(\dagKite00001\right)
%D ren C2 ==> \left(\dagKite00000\right)
%D ren A1 ==> \left\{\dagKite{23}1211,\dagKite{24}1211\right\}
%D ren A3 ==> \left\{\dagKite·1111,\dagKite·1211\right\}
%D ren C1 ==> \left\{\dagKite····0,\dagKite····1\right\}
%D ren C3 ==> \left\{\dagKite·····\right\}
%D ren B0 B1 B2 ==> \Sub(\dagKite11111) \phop\Sub(\dagKite11111)^\op \Set
%D ren D0 D1 D2 ==> \Sub(\dagKite11111) \phop\Sub(\dagKite11111)^\op \Set
%D
%D (( A0 A1 |->
%D    A2 A0 `->
%D    A1 A3  ->
%D    A2 A3 |->
%D    A0 A3 harrownodes nil 20 nil
%D    B0 place
%D    B1 B2 -> .plabel= a E
%D
%D    C0 C1 |->
%D    C2 C0 `->
%D    C1 C3  ->
%D    C2 C3 |->
%D    C0 C3 harrownodes nil 20 nil
%D    D0 place
%D    D1 D2 -> .plabel= a E
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$



%  _   _                      
% | | | | ___  _   _ ___  ___ 
% | |_| |/ _ \| | | / __|/ _ \
% |  _  | (_) | |_| \__ \  __/
% |_| |_|\___/ \__,_|___/\___|
%                             
% «OO-House»  (to ".OO-House")
% (find-LATEX "2020maclane-moerdijk.tex" "OO-House")
% (find-books "__alg/__alg.el" "davey-priestley")
% (find-daveypriestleypage (+ 10  24)    "1.28 The ordered set O(P ) of down-sets")
% (find-daveypriestleytext (+ 10  24)    "1.28 The ordered set O(P ) of down-sets")

%R local y22, mid, lc, dnlc, y21 =
%R 1/ 0   \, 1/ 0   \, 1/ 0   \, 1/ 0   \, 1/ 0   \
%R  |  1  |   |  0  |   |  0  |   |  0  |   |  0  |
%R  | 1 1 |   | 0 0 |   | 0 0 |   | 0 0 |   | 1 0 |
%R  |1 1 1|   |1 1 1|   |1 1 0|   |1 1 0|   |1 1 0|
%R  | 1 1 |   | 1 1 |   | 0 0 |   | 1 1 |   | 1 1 |
%R  \  1  /   \  1  /   \  0  /   \  1  /   \  1  /
%R -- y22 :tozmp({zdef="y22",  meta="s", size="6pt"}):addcells():output()
%R y22 :tozmp({zdef="y22",  scale="8pt"}):addcells():output()
%R mid :tozmp({zdef="mid",  scale="8pt"}):addcells():output()
%R lc  :tozmp({zdef="lc",   scale="8pt"}):addcells():output()
%R dnlc:tozmp({zdef="dnlc", scale="8pt"}):addcells():output()
%R y21 :tozmp({zdef="y21",  scale="8pt"}):addcells():output()
%R y21 :tozmp({zdef="bott", scale="5pt"}):addbullets():output()
\pu

% (find-LATEX "2017planar-has-defs.tex" "defzha-and-deftcg")
%
% Let H be the "house" DAG:
%
%          1        3_
%         / \       |  \
%  H  =  2   3  ==  2_   _2
%        |   |      |     |
%        4   5      1_   _1
%
% Then O(H) is this ZHA:
%
%                32
%                  22
%                21  12
% B := O(H) =  20  11  02
%                10  01
%                  00
%
% Let B be the bottle ZHA above.
% Label its nodes like this:
%
%    L
%     M
%    L R
%   L M R
%    L R
%     M
%
% I name the elements of O(B) by counting how many 1s
% they have on Ls, Ms, and Rs. The topology O(B) is:
%
%         433
%            \
%             333
%              |
%             323
%            /   \
%         322     223
%        /   \   /   \
%     321     222     123
%        \   / | \   /
%         221 212 122
%          | X   X |
%         211 121 112
%        /   \ | /   \
%     210     111     012
%        \   /   \   /
%         110     011
%            \   /
%             010
%              |
%             000
%
%
% (find-LATEX "2017planar-has-defs.tex" "defzha-and-deftcg")
\def\Def#1#2{\expandafter\def\csname myDef#1\endcsname{#2}}
\def\Get  #1{\csname                 myDef#1\endcsname}
\def\Run  #1{\csname                 myDef#1\endcsname}
\def\Defupperargs   #1#2{\Def{21}{#1}\Def{12}{#2}}
\def\Defmiddleargs#1#2#3{\Def{20}{#1}\Def{11}{#2}\Def{02}{#3}}
\def\Deflowerargs   #1#2{\Def{10}{#1}\Def{01}{#2}}
\def\Defallargs#1.#2.#3.#4.#5.#6{
  \Def{32}{#1}
    \Def{22}{#2}
    \Defupperargs#3
    \Defmiddleargs#4
    \Deflowerargs#5
    \Def{00}{#6}
}
\def\Setbottle#1#2{\Def{#1}{\Defallargs#2}}

\Setbottle{433}{1.1.11.111.11.1}
\Setbottle{333}{0.1.11.111.11.1}
\Setbottle{323}{0.0.11.111.11.1}

\Setbottle{322}{0.0.10.111.11.1}
\Setbottle{223}{0.0.01.111.11.1}

\Setbottle{321}{0.0.10.110.11.1}
\Setbottle{222}{0.0.00.111.11.1}
\Setbottle{123}{0.0.01.011.11.1}

\Setbottle{221}{0.0.00.110.11.1}
\Setbottle{212}{0.0.00.101.11.1}
\Setbottle{122}{0.0.00.011.11.1}

\Setbottle{211}{0.0.00.100.11.1}
\Setbottle{121}{0.0.00.010.11.1}
\Setbottle{112}{0.0.00.001.11.1}

\Setbottle{210}{0.0.00.100.10.1}
\Setbottle{111}{0.0.00.000.11.1}
\Setbottle{012}{0.0.00.001.01.1}

\Setbottle{110}{0.0.00.000.10.1}
\Setbottle{011}{0.0.00.000.01.1}

\Setbottle{010}{0.0.00.000.00.1}

\Setbottle{000}{0.0.00.000.00.0}

%% A simple test using matrices:
%
% \def\pbottle{\psm{
%         \Get{32} \;\;\;      \\
%            \Get{22}          \\
%         \Get{21} \Get{12}    \\
%   \Get{20} \Get{11} \Get{02} \\
%         \Get{10} \Get{01}    \\
%            \Get{00}          \\
%   }}
% 
% \def\B#1#2#3{\Run{#1#2#3}\pbottle}
% 
% $\def\S{\phantom{mmm}}
%  \mat{  \B433 \phantom{mm} \\
%            \B333 \\
%            \B323 \\
%         \B322 \S \B223 \\
%      \B321 \S \B222 \S \B123 \\
%      \B221 \B212 \B122 \\
%      \B211 \B121 \B112 \\
%      \B210 \S \B111 \S \B012 \\
%         \B110 \S \B011 \\
%             \B000 \\
%  }
% $


\def\G  #1#2{\Get{#1#2}}
\def\B#1#2#3{\Run{#1#2#3}\zha{bottlesieve}}

%R local bottlesieve =
%R 4/    !G32            \
%R  |        !G22        |
%R  |    !G21    !G12    |
%R  |!G20    !G11    !G02|
%R  |    !G10    !G01    |
%R  \        !G00        /
%R bottlesieve:tozmp({zdef="bottlesieve", meta="s", scale="4.5pt"}):addcells():output()
%R local bottlesieves =
%R 5/     !B433               \
%R  |          !B333          |
%R  |          !B323          |
%R  |     !B322     !B223     |
%R  |!B321     !B222     !B123|
%R  |     !B221!B212!B122     |
%R  |     !B211!B121!B112     |
%R  |!B210     !B111     !B012|
%R  |     !B110     !B011     |
%R  |          !B010          |
%R  \          !B000          |
%R
%R -- A bug fix:
%R -- (find-dn6 "zhas.lua" "MixedPicture")
%R -- (find-dn6 "zhas.lua" "MixedPicture" "addarrowsexcept =")
%R -- (find-dn6 "zhas.lua" "MixedPicture-cuts")
%R -- (find-dn6file "zhas.lua" "addxys =")
%R -- (find-dn6 "picture.lua" "V" " xy =")
%R
%R V.__index.xy = function (v) return pformat("(%s,%s)", v[1], v[2]) end
%R
%R MixedPicture.__index.
%R    arrows = function (mp, w) return (mp.ar or mp.zha):arrows(w) end
%R
%R bottlesieves:tozmp({zdef="bottlesieves", meta="s", scale="42pt"})
%R      :addcells()
%R      :addarrowsexcept("w", "(0,5)0")
%R      :output()

\pu

$$\Opens(\Opens(\dagHouse•••••))
 \;\;=\;\;
 \Opens(\zha{bott})
 \;\;=\;\;
 \zha{bottlesieves}
$$


\printbibliography


\end{document}

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

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

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