% (find-angg "LATEX/2011ebl-slides.tex")
% (find-angg ".emacs" "eblslides")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && dednat5 -t 2011ebl-slides.tex && latex    2011ebl-slides.tex" 1 '(eek "M->")))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && dednat5 -t 2011ebl-slides.tex && pdflatex 2011ebl-slides.tex" 1 '(eek "M->")))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && dednat5 -t 2011ebl-slides.tex && pdflatex 2011ebl-slides.tex"))
% (find-LATEXfile "" "2011ebl-slides")
% (eev "cd ~/LATEX/ && Scp 2011ebl-slides.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (defun d () (interactive) (find-dvipage "~/LATEX/2011ebl-slides.dvi"))
% (find-dvipage "~/LATEX/2011ebl-slides.dvi")
% (find-pspage  "~/LATEX/2011ebl-slides.ps")
% (find-pspage  "~/LATEX/2011ebl-slides.pdf")
% (find-xpdfpage "~/LATEX/2011ebl-slides.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvipdf         2011ebl-slides.dvi 2011ebl-slides.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips       -o 2011ebl-slides.ps 2011ebl-slides.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips       -o 2011ebl-slides.ps 2011ebl-slides.dvi && ps2pdf 2011ebl-slides.ps 2011ebl-slides.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2011ebl-slides.ps 2011ebl-slides.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2011ebl-slides.ps 2011ebl-slides.dvi && ps2pdf 2011ebl-slides.ps 2011ebl-slides.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage  "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2011ebl-slides.dvi" (ee-twupfile "e.dvi") 'over)
% (ee-cp "~/LATEX/2011ebl-slides.pdf" (ee-twupfile "LATEX/2011ebl-slides.pdf") 'over)
% (ee-cp "~/LATEX/2011ebl-slides.pdf" (ee-twusfile "LATEX/2011ebl-slides.pdf") 'over)
% (find-twusfile     "LATEX/" "2011ebl-slides")
% http://angg.twu.net/LATEX/2011ebl-slides.pdf

% «.geometry»			(to "geometry")
% «.BOX»			(to "BOX")

% «.mention-modal»		(to "mention-modal")
% «.mention-sheaves»		(to "mention-sheaves")
% «.zsets»			(to "zsets")
% «.black-pawns-moves»		(to "black-pawns-moves")
% «.partial-orders»		(to "partial-orders")
% «.cycles-are-evil»		(to "cycles-are-evil")
% «.dags-are-good»		(to "dags-are-good")
% «.fav-top-space»		(to "fav-top-space")
% «.fav-sh-and-presh»		(to "fav-sh-and-presh")
% «.compatibility»		(to "compatibility")
% «.evil-presheaf»		(to "evil-presheaf")
% «.stack-ops»			(to "stack-ops")
% «.stack-ops-2»		(to "stack-ops-2")
% «.covers-and-families»	(to "covers-and-families")
% «.saturated-families»		(to "saturated-families")
% «.double-sat»			(to "double-sat")

% «.L5op»			(to "L5op")
% «.L5op-HA»			(to "L5op-HA")
% «.priming»			(to "priming")
% «.thinness»			(to "thinness")
% «.presheaves»			(to "presheaves")
% «.closure-ops»		(to "closure-ops")
% «.closure-partitions»		(to "closure-partitions")
% «.what-next»			(to "what-next")


% \documentclass[a4paper,10pt]{article}
\documentclass[10pt]{article}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}
% «geometry»  (to ".geometry")
% (find-angg ".emacs.papers" "latexgeom")
% (find-latexgeomtext "total={6.5in,8.75in},")
\usepackage[%total={6.5in,4in},
            textwidth=4in,  paperwidth=4.5in,
            textheight=5in, paperheight=4.5in,
            top=0.05in, left=0.2in%, includefoot
           ]{geometry}
% (find-LATEXfile "2009unilog-dnc.aux")
% (find-LATEXfile "2010unilog-current.aux")
\def\NOEDRXDNT{1}
\usepackage{edrx08}       % (find-dn4ex "edrx08.sty")
%%L process "edrx08.sty"  -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex   % (find-dn4ex "edrxheadfoot.tex")
\usepackage[x11names]{xcolor} % (find-es "tex" "xcolor")
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
\input 2011ebl-slides.dnt  % (find-fline "2011ebl-slides.dnt")
\begin{document}

\def\diagxyto{\ifnextchar/{\toop}{\toop/>/}}
\def\mon{\diagxyto/ >->/}
\def\epi{\diagxyto/->>/}
\def\toleft{\diagxyto/<-/}
\def\monleft{\diagxyto/<-< /}
\def\epileft{\diagxyto/<<-/}
\def\to{\rightarrow}

\def\BPM#1{\mathsf{BPM}_{#1}}
\def\ess{{\mathsf{ess}}}
\def\irr{{\mathsf{irr}}}
\def\refl{{\mathsf{refl}}}
\def\trans{{\mathsf{trans}}}

\def\bbC{{\mathbb{C}}}
\def\bbD{{\mathbb{D}}}
\def\bbE{{\mathbb{E}}}
\def\bbF{{\mathbb{F}}}
\def\bbG{{\mathbb{G}}}
\def\bbH{{\mathbb{H}}}
\def\bbK{{\mathbb{K}}}
\def\bbV{{\mathbb{V}}}
\def\bbW{{\mathbb{W}}}

\def\qcomment#1#2{\phantom{#1}\red{$\ot$ #2}}

% (find-dn5 "diagtex.lua" "arrows_to_defdiag")
% (find-dn4 "experimental.lua" "BOX")
% (find-dn5 "diagforth.lua" "enddiagram")
% (find-dn5 "diagtex.lua" "arrows_to_defdiag")

% «BOX»  (to ".BOX")
%L mybox_names = {
%L   "\\myboxa",
%L   "\\myboxb",
%L   "\\myboxc",
%L   "\\myboxd",
%L   "\\myboxe",
%L   "\\myboxf",
%L   "\\myboxg",
%L   "\\myboxh"
%L }
%L mybox_bodies = {}
%L forths["BOX"] = function ()
%L     tinsert(mybox_bodies, node_to_TeX(ds:pick(0)))
%L     ds:pick(0).tex = format("\\usebox{%s}", mybox_names[#mybox_bodies])
%L   end
%L arrows_to_defdiag = function (name, hyperlink)
%L     if #mybox_bodies > 0 then
%L       local prep = ""
%L       for i,body in ipairs(mybox_bodies) do
%L         prep = prep..format("  \\savebox{%s}{$%s$}\n", mybox_names[i], body)
%L       end
%L       return format("\\defdiagprep{%s}{%s\n%s  }{\n%s}",
%L                     name, (hyperlink or ""),
%L                     prep, arrows_to_TeX("  "))
%L     end
%L     return format("\\defdiag{%s}{%s\n%s}",
%L                   name, (hyperlink or ""),
%L                   arrows_to_TeX("  "))
%L   end
%L forths["enddiagram"] = function ()
%L     output(arrows_to_defdiag(diagramname, " % no hyperlink yet"))
%L     mybox_bodies = {}
%L   end

%L forths["sl^^"] = function () ds:pick(0).slide =    "5pt" end
%L forths["sl^"]  = function () ds:pick(0).slide =  "2.5pt" end
%L forths["sl_"]  = function () ds:pick(0).slide = "-2.5pt" end
%L forths["sl__"] = function () ds:pick(0).slide =   "-5pt" end

%L forths["<-"] = function () pusharrow("<-") end
%L forths["<--"] = function () pusharrow("<--") end

% (find-dn5 "diagforth.lua" "nodes")



% For "book":
\def\mychapter   #1#2{\chapter{#1}\label{#2}}
\def\mysection   #1#2{\section{#1}\label{#2}}
\def\mysubsection#1#2{\subsection{#1}\label{#2}}

% For "article":
\def\mychapter   #1#2{\section{#1}\label{#2}}
\def\mysection   #1#2{\subsection{#1}\label{#2}}
\def\mysubsection#1#2{\subsubsection{#1}\label{#2}}

\def\mysection   #1#2{\section{#1}\label{#2}}

\mylosopen{tmp.los}
\def\myslide   #1#2{\newpage{\bf #1}\par\label{#2}\addtolos{#1}}
% \mylosopen{tmp.los}
% \def\myslide   #1#2{\newpage{\bf #1}\par\label{#2}}

% Experimental, 2010jun19:
\def\anchortargettext#1#2#3{\hypertarget{#1}{\href{\##2}{#3}}}
\def\tocline#1#2{\par #1 \dotfill #2}
\def\tocline#1#2{\par \anchortargettext{.#2}{#2}{#1} \dotfill #2}
\def\myslide#1#2{\newpage{\bf #1}\par\label{#2}\addtolos{#1}}
\def\myslide#1#2{\newpage
  {\bf \anchortargettext{\the\count0}{.\the\count0}{\arabic{page}. #1}}
  \par\label{#2}\addtolos{#1}}

\def\lph#1{\leavevmode\phantom{#1}}
\setlength{\parindent}{0pt}
\pagestyle{empty}

Sheaves over finite DAGs may be archetypal

(Or: ``Sheaves for non-categorists''. \red{Work in progress})

\msk

Eduardo Ochs - PURO/UFF

eduardoochs@gmail.com

\url{http://angg.twu.net/}

\url{http://angg.twu.net/math-b.html#sheaves-on-zdags}

\msk

Presented at the XVI EBL

(\url{http://www.cle.unicamp.br/ebl2011/}),

held at Petrópolis, RJ, Brazil, on 2011may13.

\red{These slides will probably be updated soon}

\red{to make them more self-contained.}



\newpage



%
% (eedn4-51-bounded)

Index of the slides:
\msk
% To update the list of slides uncomment this line:
%\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")

\tocline {Let's mystify the audience with technical terms} {3}
\tocline {Let's mystify the audience a bit more} {4}
\tocline {Well-positioned subsets of $Z^2$ (and ZSets)} {5}
\tocline {Black pawn's moves (and ZDags)} {6}
\tocline {Partial orders} {7}
\tocline {Cycles are evil} {8}
\tocline {DAGs are good} {9}
\tocline {Our favorite topological space: ${\mathbb {V}}$} {10}
\tocline {Our favorite sheaves and presheaves} {11}
\tocline {Compatibility} {12}
\tocline {The evil presheaf} {13}
\tocline {Stack operations} {14}
\tocline {Stack operations (2)} {15}
\tocline {Covers and families} {16}
\tocline {Saturated families} {17}
\tocline {Adding unions} {18}
\tocline {Priming} {19}
\tocline {What next?} {20}

\newpage


% --------------------
% «mention-modal»  (to ".mention-modal")
% (s "Let's mystify the audience with technical terms" "mention-modal")
\myslide {Let's mystify the audience with technical terms} {mention-modal}


\msk

{\bf Modal logic:}
\par S4 has the finite model property.
\par We have Gödel's translation: intuitionistic logic $\to$ S4
\par So: as $¬¬P ¶ P$ is not a theorem of intutionistic logic
\par $\funto$ there is a finite model (with two worlds)
\par \lph{$\funto$} in which $¬¬P¶P$ is not true.
\par These finite counter-models are good for developing
\par intuition about intuitionistic logic.
\msk
\par {\bf Category Theory:}
\par Let $\bbW$ be a finite poset.
\par ($\bbW$ is a system of possible worlds for S4,
\par viewed as a category).
\par Then $\Set^\bbW$ is a topos of presheaves.
\par The logic of toposes is intuitionistic,
\par and in $\Set^\bbW = \Set^{\to}$ we can falsify $¬¬P¶P$.
\msk
\par Claim:
\par Toposes of the form $\Set^\bbW$ are good for developing
\par intuition about Topos Theory (and CT in general).




% --------------------
% «mention-sheaves»  (to ".mention-sheaves")
% (s "Let's mystify the audience a bit more" "mention-sheaves")
\myslide {Let's mystify the audience a bit more} {mention-sheaves}
\msk
\par Sheaves are very important in Topos Theory.
\par Category Theory is \red{hard} (too abstract).
\par Even \red{basic sheaf theory} is \red{too hard}.
\par Idea: Let's use toposes of the form $\Set^\bbW$
\par to learn about sheaves!
\msk
\par In ``Internal Diagrams in Category Theory'' (2010)
\par I ``defined'' (loosely) a way of thinking
\par diagrammatically, and a notion of how much
\par ``mental space'' each idea takes.
\msk
\par Specializations behave like projections,
\par Generalizations behave like liftings:
\msk

%L defarrows "<-- <- <-| <."

%D diagram spec-and-gen
%D 2Dx     100  +70
%D 2D  100 G    T
%D 2D
%D 2D  +50 P    S
%D 2D
%D (( G .tex= \arr{general\\theory}
%D    P .tex= \arr{particular\\case}
%D    T .tex= \arr{Toposes}
%D    S .tex= \arr{`$\Set^\bbW$'s}
%D    G P ->  sl_ .plabel= l \arr{specialization\\(projection)}
%D    G P <-- sl^ .plabel= r \arr{generalization\\(lifting)}
%D    T S ->  sl_
%D    T S <-- sl^
%D ))
%D enddiagram
%D
$\def\arr#1{\begin{array}{c}#1\end{array}}
  \def\arr#1{\begin{tabular}{c}#1\end{tabular}}
  \diag{spec-and-gen}
$
\msk

\par Can we learn/define/understand sheaves
\par in toposes of the form $\Set^\bbW$
\par and then lift the theory to the general case?



% --------------------
% «zsets»  (to ".zsets")
% (s "Well-positioned subsets of $Z^2$ (and ZSets)" "zsets")

\myslide {Well-positioned subsets of $Z^2$ (and ZSets)} {zsets}
\msk
\par Def: a subset $D = \{(x_1,y_1),...,(x_n,y_n)\} \subset \Z^2$
\par is {\bf well-positioned} when $\inf_i x_i = 0$ and $\inf_i y_i = 0$.
\msk
\par Def: {\bf ZSet} is a finite well-positioned subset of $\Z^2$.
\msk
\par Examples: 
\par $Y = \{(0,2),(2,2),(1,1),(1,0)\}$
\par $K = \{(1,3),\,(0,2),(2,2),\,(1,1),\,(1,0)\}$
\msk
\par They will usually be named according to their shapes
\par (`K' is for `Kite').



% --------------------
% «black-pawns-moves»  (to ".black-pawns-moves")
% (s "Black pawn's moves (and ZDags)" "black-pawns-moves")
\myslide {Black pawn's moves (and ZDags)} {black-pawns-moves}

\bsk

%D diagram Kite
%D 2Dx     100 +20 +20
%D 2D  100     K1
%D 2D         /  \
%D 2D  +20 K2      K3
%D 2D         \  /
%D 2D  +20     K4
%D 2D          |
%D 2D  +20     K5
%D 2D
%D (( K1 .tex= (1,3)
%D    K2 .tex= (0,2)
%D    K3 .tex= (2,2)
%D    K4 .tex= (1,1)
%D    K5 .tex= (1,0)
%D    K1 K2 -> K1 K3 ->
%D    K2 K4 -> K3 K4 ->
%D    K4 K5 ->
%D ))
%D enddiagram
%D
% (find-pspage "~/IMAGES/black_pawns_moves.eps")
$%
  \begin{array}{c}
  % \includegraphics[scale=0.35]{../IMAGES/black_pawns_moves.eps}
  \includegraphics[scale=0.35]{../IMAGES/black_pawns_moves}
  \end{array}
  \qquad
  \diag{Kite}
$

Example:

Let $K = \{(1,3),\,(0,2),(2,2),\,(1,1),\,(1,0)\}$.

Then the set of {\bf black pawn's moves} on $K$, $\BPM{K}$,

is the set of 5 arrows at the right.

Let $\bbK = (K, \BPM{K})$  \qcomment{mmm}{this a DAG.}

\bsk

Every ZSet $D$ induces a DAG

$\bbD = (D, \BPM{D})$   \qcomment{mmmmmi}{this a {\bf ZDag}.}




% --------------------
% «partial-orders»  (to ".partial-orders")
% (s "Partial orders" "partial-orders")
\myslide {Partial orders} {partial-orders}
\msk
\par We are interested in S4 and categories, so
\par we like relations that are reflexive and transitive.
\par It is clumsy to draw $(Y, \BPM{Y}^*)$ (at the right),
\par so we'd like to make $(Y, \BPM{Y})$ (at the left)
\par stand for $(Y, \BPM{Y}^*)$.

%D diagram Y
%D 2Dx     100 +20 +20
%D 2D  100 Y1      Y2 
%D 2D         \  /
%D 2D  +20     Y3     
%D 2D          |
%D 2D  +20     Y4     
%D 2D
%D (( Y1 .tex= (0,2)
%D    Y2 .tex= (2,2)
%D    Y3 .tex= (1,1)
%D    Y4 .tex= (1,0)
%D    Y1 Y3 -> Y2 Y3 -> Y3 Y4 ->
%D    # Y1 loop (ul,ur) 
%D    # Y2 loop (ul,ur) 
%D    # Y3 loop (ul,ur) 
%D    # Y4 loop (dl,dr) 
%D    # Y1 Y4 -> Y2 Y4 ->
%D ))
%D enddiagram
%D
%D diagram Y*
%D 2Dx     100 +25 +25
%D 2D  100 Y1      Y2 
%D 2D        \   /
%D 2D  +20     Y3     
%D 2D          |
%D 2D  +20     Y4     
%D 2D
%D (( Y1 .tex= (0,2)
%D    Y2 .tex= (2,2)
%D    Y3 .tex= (1,1)
%D    Y4 .tex= (1,0)
%D    Y1 Y3 -> Y2 Y3 -> Y3 Y4 ->
%D    Y1 loop (ul,ur) 
%D    Y2 loop (ul,ur) 
%D    Y3 loop (ul,ur) 
%D    Y4 loop (dl,dr) 
%D    Y1 Y4 -> Y2 Y4 ->
%D ))
%D enddiagram
%D
$\diag{Y}
  \two/->`<--/<400>^{\rm (saturate)}_{\rm (?)}
  \diag{Y*}
$

\par Let's say that two relations, $R$ and $S$,
\par are {\bf equivalent} if $R^* = S^*$.
\par The class $[R] = \sst{S}{S^* = R^*}$ has a top element,
\par $R^*$, obtained by a kind of saturation process
\par (transitive-reflexive closure).



% --------------------
% «cycles-are-evil»  (to ".cycles-are-evil")
% (s "Cycles are evil" "cycles-are-evil")
\myslide {Cycles are evil} {cycles-are-evil}
\msk
\par Let $T = (\{1,2,3\}, \{1,2,3\}^2)$ be the complete graph on $\{1,2,3\}$.
\par Then $[T]$ has two different minimal elements:
\msk

%D diagram 123
%D 2Dx     100 +15 +15
%D 2D  100 1       2
%D 2D
%D 2D  +20     3
%D 2D
%D (( 1 2 -> 2 3 -> 3 1 ->
%D ))
%D enddiagram
%D
%D diagram 321
%D 2Dx     100 +15 +15
%D 2D  100 1       2
%D 2D
%D 2D  +20     3
%D 2D
%D (( 1 2 <- 2 3 <- 3 1 <-
%D ))
%D enddiagram
%D
%D diagram 123*
%D 2Dx     100 +15 +15
%D 2D  100 1       2
%D 2D
%D 2D  +20     3
%D 2D
%D (( 1 2 -> sl^ 1 2 <- sl_ 1 loop (ur,ul)
%D    2 3 -> sl^ 2 3 <- sl_ 2 loop (ur,ul)
%D    3 1 -> sl^ 3 1 <- sl_ 3 loop (dr,dl)
%D ))
%D enddiagram
%D
%D diagram loops-are-evil
%D 2Dx     100   +70
%D 2D  100 123
%D 2D
%D 2D  +20       123*
%D 2D
%D 2D  +20 321
%D 2D
%D (( 123 .tex= \diag{123} BOX
%D    321 .tex= \diag{321} BOX
%D    123* .tex= \diag{123*} BOX
%D    123 123* -> sl^ 123 123* <-- sl_
%D    321 123* -> sl^ 321 123* <-- sl_
%D ))
%D enddiagram
%D
$\diag{loops-are-evil}$

\msk

\par If we want to represent partial orders by minimal graphs
\par we will need to avoid these...
\par ``Reflexive'' arrows, i.e., those of the form $\aa \to \aa$
\par are (sort of) irrelevant, so let's ignore them:
\par Def: $R^\refl$ is $R$ plus all reflexive arrows.
\par Def: $R^\irr$ is $R$ minus all reflexive arrows.
\par Def: $R$ is acyclic when \red{$R^\irr$} has no cycles.
     \qcomment{mmm}{not standard!}
\par Then in each class $[R]$ either all elements are acyclic
\par or all are cyclic.

% (find-dn4ex "edrx08.sty" "diagprep")
% (find-dn4ex "edrxdnt.tex" "defdiag")
% (find-dn5file "preamble.lua")
% (find-dn5file "README")
% (find-LATEXfile "2011ebl-slides.dnt")
% (find-LATEXfile "2010diags.dnt" "{dict-1}")
% (find-LATEXfile "2011ebl-slides.dnt" "{loops-are-evil}")



% --------------------
% «dags-are-good»  (to ".dags-are-good")
% (s "DAGs are good" "dags-are-good")
\myslide {DAGs are good} {dags-are-good}
\msk
\par ``Acyclic'' for us is ``acyclic modulo reflexive arrows''...
\par Consider the set of DAGs on a finite set of vertices $A$.
\par The equivalence relation $R \sim S \iff R^*=S^*$
\par partitions it into equivalent classes that are ``diamond-shaped'',
\par i.e., ``everything between a top and a bottom element'':
\par $[R] = \sst{R'}{R^\ess \subseteq R' \subseteq R^*}$.
\par To build $R^\ess$ from $R$ we drop all ``non-essential arrows''.
\par (This is the dual of the saturation $R \mto R^*$).
\msk
\par Moral: we can represent finite partial orders canonically
\par by their minimal DAGs (that only have ``essential arrows'').
\par ZDags are finite, acyclic, and minimal. 8-)



% --------------------
% «fav-top-space»  (to ".fav-top-space")
% (s "Our favorite topological space: $\bbV$" "fav-top-space")
\myslide {Our favorite topological space: $\bbV$} {fav-top-space}
\msk
%
\par Here it is:
\par as a DAG, $\bbV = (V, \BPM{V}) = (\{\aa,\bb,\cc\}, \{(\aa\to\cc),(\bb\to\cc)\})$
\par as a partial order, $\bbV = (V, \BPM{V}^*)$
\par as a top. space, $\bbV = (X, \Opens(X))$
     \qcomment{mmm}{note the renaming!}
\par \lph{mm} $= (X, \{\{\aa,\bb,\cc\}, \{\aa,\cc\}, \{\bb,\cc\}, \{\cc\}, \{\}\})$
\par \lph{mm} $= (X, \{X, U, V, W, \emp\})$
     \qcomment{mmmmmi}{names for the open sets}
\par \lph{mm} $= (X, \{\dagVee111, \dagVee101, \dagVee011, \dagVee001, \dagVee000\})$
     \qcomment{mmmmn}{positional notation!}
\msk
\par We can think of it as a quotient topology on $\R$...

%D diagram V-as-quot
%D 2Dx     100 +15 +15     +30 +15 +15      +30 +15 +15 
%D 2D  100 \aa     \bb     qaa     qbb      paa     pbb 
%D 2D                                                   
%D 2D  +15     \cc             qcc              pcc     
%D 2D                                                   
%D 2D  +15     X               QX               pX      
%D 2D                                                   
%D 2D  +15 U       V       QU      QV       pU      pV  
%D 2D                                                   
%D 2D  +15     W               QW               pW      
%D 2D                                                   
%D 2D  +15    \emp             Qemp             pemp    
%D (( \aa \cc -> \bb \cc ->
%D ))
%D (( qaa .tex= (-,3]
%D    qbb .tex= [2,+)
%D    qcc .tex= (2,3)
%D    qaa qcc -> qbb qcc ->
%D ))
%D (( paa .tex= \dagVee¢¢{}
%D    pbb .tex= \dagVee¢¢{}
%D    pcc .tex= \dagVee¢¢{}
%D    paa pcc -> pbb pcc ->
%D ))
%D (( X U -> X V ->  U W -> V W ->  W \emp ->
%D ))
%D (( QX .tex= (-,+)
%D    QU .tex= (-,3)
%D    QV .tex= (2,+)
%D    QW .tex= (2,3)
%D    Qemp .tex= \emp
%D    QX QU -> QX QV ->  QU QW -> QV QW ->  QW Qemp ->
%D ))
%D (( pX .tex= \dagVee111
%D    pU .tex= \dagVee101
%D    pV .tex= \dagVee011
%D    pW .tex= \dagVee001
%D    pemp .tex= \dagVee000
%D    pX pU -> pX pV ->  pU pW -> pV pW ->  pW pemp ->
%D ))
%D enddiagram
%D
$\diag{V-as-quot}$
\msk
\par I draw $X$ on top because it ``covers'' the other open sets,
\par and because $\dagVee111$ is $§$ (``Top'') in the Heyting algebra
\par (but $§$ is also the terminal... the HA must $\bbK^\op$).
\par Surprise: $(\Opens(X), \supseteq^\ess)$ is a ZDag!



% --------------------
% «fav-sh-and-presh»  (to ".fav-sh-and-presh")
% (s "Our favorite sheaves and presheaves" "fav-sh-and-presh")
\myslide {Our favorite sheaves and presheaves} {fav-sh-and-presh}
\msk
\par Let's write $\Opens(\R)$ for $(\Opens(\R), \subseteq)$  \qcomment{mmn}{a category ($\nearrow\nwarrow$)}
\par and $\Opens(\R)^\op$ for $(\Opens(\R), \supseteq)$.     \qcomment{mmmmm}{another \;\;\;\;($\swarrow\searrow$)}
\par Then $\calC^ Ý \Set^{\Opens(\R)^\op}$ is a \red{sheaf}.
\par Bad news: it is too big to visualize.
\msk
\par We write $\bbV \equiv \dagVee$ and $\bbK = \bbV' \equiv \dagKite$.
\par Let's define presheaves $C^, E Ý \Set^\bbK$.
\par A {\bf} presheaf in $\Set^\bbD$ is just a functor from $\bbD$ to $\Set$.
\par \red{Sheafness} is \red{separatedness} plus \red{collatedness}.
\par $C^$ will obey both, and $E$ will fail both.
\par
\msk 
%D diagram Cfo
%D 2Dx     100 +15 +15
%D 2D  100     \foX
%D 2D
%D 2D  +15 \foU    \foV
%D 2D
%D 2D  +15     \foW
%D 2D
%D 2D  +15     \foe
%D 2D
%D (( \foX \foU -> \foX \foV ->
%D    \foU \foW -> \foV \foW ->
%D    \foW \foe ->
%D ))
%D enddiagram
%D
\def\diagCfo#1#2#3#4#5{%
  \def\foX{#1}%
  \def\foU{#2}%
  \def\foV{#3}%
  \def\foW{#4}%
  \def\foe{#5}%
  \diag{Cfo}}
%
$ C^
  \;\; = \;\;
  \diagCfo{C^(X)}{C^(U)}{C^(V)}{C^(W)}{C^(\emp)}
  \;\; = \;\;
  \diagCfo{\calC^(\R)}{\calC^((-,1))\phantom{mm}}{\phantom{mm}\calC^((0,+))}{\calC^((0,1))}{\calC^(\emp)}
$

% --------------------
% «compatibility»  (to ".compatibility")
% (s "Compatibility" "compatibility")
\myslide {Compatibility} {compatibility}
\msk
\par Let $U=(-,3)$ and $V=(2,)$ (temporarily).
\par Let $f_U Ý \calC^(U,\R)$ and $f_V Ý \calC^(V,\R)$, in:
\bsk
\par
$ \diagCfo{\calC^(\R,\R)}
          {\calC^((-,3),\R)\phantom{mmmm}}
          {\phantom{mmmm}\calC^((2,+),\R)}
          {\calC^((2,3),\R)}
          {\calC^(\emp,\R)}
$
\bsk
\par We say that two ``locally defined functions'', $f_U$ and $f_V$,
\par are {\bf compatible} iff they ``coincide wherever they're both
\par defined'' (in the example: on $(2,3)$).
\par More precisely: $f_U$ and $f_V$ are compatible iff $f_U|_{UÌV} = f_V|_{UÌV}$.
% \par (To generalize, use the morphisms: $^U_{U´V}(f_U) = ^V_{U´V}(f_V)$).
\par Sheafness means that every {\bf compatible family} $\{f_U, \ldots, f_V\}$
\par has exactly one glueing to an $f_{Uþ\ldotsþV}$
\par (collatedness guarantees existence of a glueing,
\par separatedness guarantees that there is at most one).

% --------------------
% «evil-presheaf»  (to ".evil-presheaf")
% (s "The evil presheaf" "evil-presheaf")
\myslide {The evil presheaf} {evil-presheaf}
% \msk
\par Here is the ``evil presheaf'', $E:\dagKite \to \Set$.
\par Note that everything here is given explicitly ---
\par restriction functions that are the images of black pawn's moves,
\par e.g., $^X_V:E(X) \to E(V)$, are {\sl drawn};
\par restriction functions like $^U_U$ are necessarily $= \id_{E(U)}$, and
\par restriction functions like $^X_W$ are obtained by composition.
\par Note (again!) that $E$ is a {\sl functor}.
\msk
\par
%
% (find-dn4 "experimental.lua" "relphantom")
%L forths[".xtag="] = function ()
%L     local x, y = ds:pick(1).x, ds:pick(1).y
%L     local dx, tag = getwordasluaexpr(), getword()
%L     tex = "\\ph{"..tag.."}"
%L     ds[1] = storenode {x=x+dx, y=y, tex=tex, tag=tag}
%L   end
%
%D diagram evil-presheaf
%D 2Dx     100 +20 +20  +30 +20 +20
%D 2D  100     A0           B0     
%D 2D         /  \         /  \    
%D 2D        v    v       v    v   
%D 2D  +20 A1      A2   B1      B2 
%D 2D        \    /       \    /   
%D 2D         v  v         v  v    
%D 2D  +20     A3           B3     
%D 2D          |            |      
%D 2D          v            v      
%D 2D  +20     A4           B4     
%D 2D
  %D (( A0 .tex= E(X)
  %D    A1 .tex= E(U)
  %D    A2 .tex= E(V)
  %D    A3 .tex= E(W)
  %D    A4 .tex= E(\emp)
  %D    A0 A1 ->
  %D    A0 A2 ->
  %D    A1 A3 ->
  %D    A2 A3 ->
  %D    A3 A4 ->
  %D ))
%D (( B0 .tex= \{e_X,e'_X\}  place  .xtag= -6 e_X  .xtag= 12 e'_X
%D  # B1 .tex= \{e_U,e'_U\}  place  .xtag= -5 e_U  .xtag= 10 e'_U
%D    B1 .tex= \{e_U\}       place  .xtag=  0 e_U  .xtag=  0 e'_U
%D    B2 .tex= \{e_V,e'_V\}  place  .xtag= -5 e_V  .xtag= 11 e'_V
%D    B3 .tex= \{e_W\}
%D    B4 .tex= \{e_\emp\}
%D    e_X e_U ->  e'_X e'_U ->
%D    e_X e_V ->  e'_X e_V  ->
%D    e_U B3  ->  e'_U B3   ->
%D    e_V B3  ->  e'_V B3   ->
%D    B3 B4 ->
%D ))
%D enddiagram
%D
$ E
  \;\; = \;\;
  \diagCfo{E(X)}{E(U)}{E(V)}{E(W)}{E(\emp)}
  \;\; = \;\;
  % (find-LATEXgrep "grep -nH -e color *.tex")
  \def\ph#1{{\color{red}#1}}
  \def\ph#1{\phantom{#1}}
  \diag{evil-presheaf}
$
\msk
\par Then $\{e_U, e_V\}$ is a compatible family,
\par because $e_U|_{UÌV} := ^U_W(e_U) = e^W$ and $e_V|_{UÌV} := ^V_W(e_V) = e^W$,
\par but $\{e_U, e_V\}$ has two different glueings, $e_X$ and $e'_X$,
\par so separatedness doesn't hold in $E$...
\par Also, $\{e_U, e'_V\}$ is another compatible family,
\par and this one has {\sl no glueings}.
\par So collatedness also doesn't hold in $E$.




% --------------------
% «stack-ops»  (to ".stack-ops")
% (s "Stack operations" "stack-ops")
\myslide {Stack operations} {stack-ops}
\msk
\par The fastest way to formalize all this is by using {\bf stacks}.
\par (This is not the standard way at all! I learned it from
\par Harold Simmons's ``The point-free approach to sheafification''.)
\msk
\par This is $E$ as a stack:
\par $ÆE = E(X)÷E(U)÷E(V)÷E(W)÷E(\emp)$
\par We have an operation called ``extent'', $[e_U] = U$,
\par going from $ÆE$ to $Ø=\{X,U,V,W,\emp\}$,
\par and a non-commutative `$·$', heavily overloaded,
\par that behaves as {\sl restriction} when its left arg is in $ÆE$
\par and as {\sl intersection} when its left arg is in $Ø$:
\msk
\par
$\begin{array}{lrl}
   U·V     &:=& U´V \\
            &=& W   \\
   U·e_V   &:=& U·[e_V] \\
            &=& U·V \\
            &=& W \\
   e_U·V   &:=& e_U|_{([e_U]·V)} \\
            &=& e_W \\
   e_U·e_V &:=& e_U|_{([e_U]·[e_V])} \\
            &=& e_W \\
 \end{array}
$

% --------------------
% «stack-ops-2»  (to ".stack-ops-2")
% (s "Stack operations (2)" "stack-ops-2")
\myslide {Stack operations (2)} {stack-ops-2}
\msk
\par The `$·$' also accepts sets as arguments,
\par with the usual conventions:
\par $\{a,b\}·\{c,d\} = \{a·c, a·d, b·c, b·d\}$,
\par $a·\{b,c\} = \{a·b, a·c\}$,
\par $\{a,b\}·c = \{a·c, b·c\}$.
\par (Also: $[\{a,b\}] = \{[a],[b]\}$).
\msk


% --------------------
% «covers-and-families»  (to ".covers-and-families")
% (s "Covers and families" "covers-and-families")
\myslide {Covers and families} {covers-and-families}
\msk
\par Def: a {\bf cover} is a subset of $Ø$. (Example: $\{U,V\}$)
\par Def: a {\bf family} is a subset of $ÆE$ ``where $[·]$ is injective''.
\par Def: a {\bf compatible family} is a family ``where `$·$' commutes''.
\par Example 1: $\{e_V,e'_V\}$ is not a family.
\par Example 2: $\{e_U,e_V\}$ is a compatible family.
\par Example 3: $\{e_X,e'_V\}$ is non-compatible family.
\msk
\par $\def\ph#1{\phantom{#1}}
      \diag{evil-presheaf}
     $
\msk
\par Notation for covers: $\calU, \calV, \ldots$, where $\bigcup\calV = V$.
\par Notation for families: $e_\calU$, where $[e_\calU] = \calU$.
\par Def: a cover $\calU$ is (downward) {\bf saturated} when $\calU·Ø=\calU$.
\par Def: a family $e_\calU$ is (downward) {\bf saturated} when $e_\calU·Ø=e_\calU$.
\par Example 4: $\{U,V\}·Ø = \{U,V,W,\emp\}$.
\par Example 5: $\{e_U,e'_V\}·Ø = \{e_U,e'_V,e_W,e_\emp\}$.
\par Example 6: $e_X·Ø = \{e_X, e_U, e_V, e_W, e_\emp\}$.
\par Example 7: $e_X·\{U,V\}·Ø = \{e_U, e_V, e_W, e_\emp\}$.



% --------------------
% «saturated-families»  (to ".saturated-families")
% (s "Saturated families" "saturated-families")
\myslide {Saturated families} {saturated-families}
\msk
\par Let's annotate saturated covers with a `$$'.
\par So: $\calU$, $\calU'$, $\calU^$, $\calU^{\prime}$ are saturated families, 
\par possibly different, all ``covering $U$''.
\msk
\par Let's write the saturation operation, `$·Ø$', as `$()^$',
\par and let's say that $\calU \approx \calV$ when $(\calU)^=(\calV)^$,
\par and write the equivalence classes as $[\calU]$.
\msk
\par On \red{finite DAGs} each equivalence class has both a top element
\par and a bottom element:
\par $[\calU] = \sst{\calU'}{(\calU)^¢ \subseteq \calU' \subseteq (\calU)^}$.
\par The operation $(\calU)^¢$, that drops all ``non-essential open sets''
\par in a cover, is new...
\par and it also makes sense for families.
% \par Each \red{compatible} family can be saturated in a unique way
\msk
\par Examples:
\par $\{U,V,W\}^ = \{U,V,W,\emp\}$
\par $\{U,V,W\}^¢ = \{U,V\}$
\par $\{e_U,e_V,e_W\}^ = \{e_U,e_V,e_W,e_\emp\}$
\par $\{e_U,e_V,e_W\}^¢ = \{e_U,e_V\}$



% «.adding-unions»	(to "adding-unions")
% --------------------
% «adding-unions»  (to ".adding-unions")
% (s "Adding unions" "adding-unions")
\myslide {Adding unions} {adding-unions}
\msk
\par In a \red{sheaf} $F:\bbK \to \Set$ every compatible family
\par $f_\calU$ can be glued in a unique way to obtain a $f_U$,
\par and we can obtain $f_\calU$ back from $f_U$: $f_\calU = f_U·\calU$.
\msk
\par To understand what is going on here we need
\par another notion of saturation...
\msk
\par The `$$' saturation adds {\sl smaller opens sets} to a cover;
\par The `$$' saturation also adds {\sl unions} to a cover.
\msk
%D diagram X**
%D 2Dx     100     +30        +50        +35     +25
%D 2D  100 X ----> {X} --*--> {X}*	 dX      dX*
%D 2D	     <----     <-o---  |^	 
%D 2D	                     *o||** 
%D 2D	                       v|	 
%D 2D  +30        {U,V} --*-> {U,V}*     dUV     dUV*
%D 2D	                <-o--       
%D ((   X   .tex= X
%D     {X}  .tex= \{X\}
%D     {X}* .tex= \{X,U,V,W,\emp\}
%D   {U,V}  .tex= \{U,V\}
%D   {U,V}* .tex= \{U,V,W,\emp\}
%D    X    {X}   -> sl^
%D    X    {X}   <- sl_
%D   {X}   {X}*  -> sl^ .plabel= a 
%D   {X}   {X}*  <- sl_ .plabel= b ¢
%D   {X}* {U,V}* --> sl_ .plabel= l ¢
%D   {X}* {U,V}* <-- sl^ .plabel= r 
%D  {U,V} {U,V}* -> sl^ .plabel= a 
%D  {U,V} {U,V}* <- sl_ .plabel= b ¢
%D ))
%D (( dX   .tex= \dagKite10000
%D    dX*  .tex= \dagKite11111
%D    dUV  .tex= \dagKite01100
%D    dUV* .tex= \dagKite01111
%D    dX  dX* -> sl^ .plabel= a 
%D    dX  dX* <- sl_ .plabel= b ¢
%D    dX* dUV* .> sl_ .plabel= l ¢
%D    dX* dUV* <. sl^ .plabel= r 
%D    dUV dUV* -> sl^ .plabel= a 
%D    dUV dUV* <- sl_ .plabel= b ¢
%D ))
%D enddiagram
%D
\par $\diag{X**}$


% (find-34page 10 "Quotient topologies")
% (find-34     "" "quotient")
% (find-34page 12 "set of saturated covers")
% (find-34        "set of saturated covers")


% --------------------
% «priming»  (to ".priming")
% (s "Priming" "priming")
\myslide {Priming} {priming}
\msk

\input 2011ebl-defs.tex

\def\G#1#2#3#4#5#6{\dagGuill{#1}{#2}{#3}{#4}{#5}{#6}}
\def\A{\bigGuill 123456}
\def\B{\hugeGuillPrime
  {\G 111111}  % 12
 {(\G 101111)} % 11
  {\G 011111}  % 10
  {\G 001111}  % 8
 {(\G 010111)} % 9
  {\G 001011}  % 7
 {(\G 000111)} % 5
 {(\G 001010)} % 6
  {\G 000011}  % 4
 {(\G 000010)} % 3
 {(\G 000001)} % 2
  {\G 000000}  % 1
}
% $$
% \bhbox{$\A$} \to \bhbox{$\B$}
% $$
%
%D diagram guill-priming
%D 2Dx     100   +70
%D 2D  100 A     B
%D 2D
%D 2D  +50 C     D
%D 2D
%D 2D  +20 E     F
%D 2D
%D (( A .tex= \A
%D    B .tex= \B
%D    C .tex= \dagGuill
%D    D .tex= (\dagGuill)'=\dagGuillPrime
%D    A B `-> # .plabel= a \aa|->\{\aa\}^\coint
%D    C D `->
%D ))
%D enddiagram
%D
$\diag{guill-priming}$

\msk
\par To understand ``topological sheaves'' we take a DAG (e.g., $\bbV$)
\par and prime it \red{twice}; the operations `$$' and `$¢$' work on $\bbV''$.
\msk
\par For ``generic'' sheaves (``sheaves on a site'') we take any DAG $\bbD$
\par to play the role of $\bbV'$ and an operation `$*$' on $\bbD$
\par that obeys three rules (obeyed by `$$', of course),
\par and from there on we treat what were ``open sets''
\par as ``truth-values'' (!!!), and the `$*$' as a modality (!!!!!).


% --------------------
% «what-next»  (to ".what-next")
% (s "What next?" "what next")
\myslide {What next?} {what next}
\msk
\par ...but that doesn't fit in 20 minutes! 8-(
\par Look for the complete version of these slides in my home page!
\msk
\par \red{Goodbye! 8-)} 


%:|-\vdash 
%:
%:  ------   --------
%:  P|-P^*   P^*|-Q^*
%:
%:
%:
%:
%:
%:




% (find-34     "" "priming")
% (find-34page  5 "priming")

% (find-854     "" "prop-calc-in-a-hyp")
% (find-854page 88 "prop-calc-in-a-hyp")



% (find-34     "" "primingp")
% (find-34page 5 "priming")



% (find-34        "presheaves")
% (find-34page 14 "presheaves")
% (find-LATEX "2008graphs.tex")



% (find-LATEX "2011ebl-abs.tex")






%

\end{document}

% Local Variables:
% coding:           raw-text-unix
% ee-anchor-format: "«%s»"
% End:
