|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2011ebl-abs.tex")
% (find-angg ".emacs" "eblsheaves")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (find-angg ".zshrc" "makebbl")
% (defun b () (interactive) (find-zsh "makebbl 2011ebl-abs.bbl catsem,filters"))
% (defun b () (interactive) (find-zsh "bibtex 2011ebl-abs"))
% (defun b () (interactive) (find-zsh "bibtex 2011ebl-abs; makeindex 2011ebl-abs"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2011ebl-abs.tex && latex 2011ebl-abs.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2011ebl-abs.tex && latex 2011ebl-abs.tex" 1 '(eek "M->")))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2011ebl-abs.tex && pdflatex 2011ebl-abs.tex"))
%
% (defun c () (interactive) (find-LATEXsh "dednat4 2011ebl-abs.tex && latex 2011ebl-abs.tex"))
% (defun c () (interactive) (find-LATEXsh "dednat4 2011ebl-abs.tex && latex 2011ebl-abs.tex" 1 '(eek "M->")))
% (defun c () (interactive) (find-LATEXsh "dednat4 2011ebl-abs.tex && pdflatex 2011ebl-abs.tex"))
%
% (eev "cd ~/LATEX/ && Scp 2011ebl-abs.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (defun d () (interactive) (find-dvipage "~/LATEX/2011ebl-abs.dvi"))
% (find-xdvipage "~/LATEX/2011ebl-abs.dvi")
% (find-pspage "~/LATEX/2011ebl-abs.ps")
% (find-pspage "~/LATEX/2011ebl-abs.pdf")
% (find-xpdfpage "~/LATEX/2011ebl-abs.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvipdf 2011ebl-abs.dvi 2011ebl-abs.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2011ebl-abs.ps 2011ebl-abs.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2011ebl-abs.ps 2011ebl-abs.dvi && ps2pdf 2011ebl-abs.ps 2011ebl-abs.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2011ebl-abs.pdf" (ee-twupfile "LATEX/2011ebl-abs.pdf") 'over)
% (ee-cp "~/LATEX/2011ebl-abs.pdf" (ee-twusfile "LATEX/2011ebl-abs.pdf") 'over)
% (find-twusfile "LATEX/" "2011ebl-abs")
% http://angg.twu.net/LATEX/2011ebl-abs.pdf
% «.2011ebl-defs» (to "2011ebl-defs")
%
% «.positional» (to "positional")
% «.zdags» (to "zdags")
% «.priming» (to "priming")
% «.essential» (to "essential")
% «.diamond» (to "diamond")
% «.continuity» (to "continuity")
% «.quotient» (to "quotient")
% «.covers» (to "covers")
% «.thinness» (to "thinness")
% «.presheaves» (to "presheaves")
% «.prestacks» (to "prestacks")
% «.HAs» (to "HAs")
% «.MHAs» (to "MHAs")
% «.FMHAs» (to "FMHAs")
% «.FHAs» (to "FHAs")
% «.omega» (to "omega")
% «.etale» (to "etale")
% «.geometric-morphs» (to "geometric-morphs")
% «.geometric-discr» (to "geometric-discr")
% «.geometric-epi» (to "geometric-epi")
% «.geometric-monic» (to "geometric-monic")
% «.right-example» (to "right-example")
% «.old-intro» (to "old-intro")
% «.old-abstract» (to "old-abstract")
%\documentclass[oneside]{book}
\documentclass[oneside]{article}
\usepackage[latin1]{inputenc}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
\usepackage{breakurl}
\usepackage{edrx08} % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty" -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex % (find-dn4ex "edrxheadfoot.tex")
\begin{document}
\input 2011ebl-abs.dnt
%*
% (eedn4-51-bounded)
% «2011ebl-defs» (to ".2011ebl-defs")
% (find-angg "LUA/canvas3.lua")
% (find-angg "LUA/canvas3.lua" "2011ebl-defs")
\input 2011ebl-defs.tex
%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")
% 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}}
\def\int {{\mathsf{int}}}
% \def\und {{\mathsf{und}}}
\def\discr{{\mathsf{discr}}}
\def\antidiscr{{\mathsf{ad}}}
\def\coint{{\mathsf{coint}}}
\def\costar{{\mathsf{co}*}}
\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\calU{\mathcal{U}} \def\Ubu{\calU^\bu} \def\Ububu{\calU^\bubu}
\def\calV{\mathcal{V}} \def\Vbu{\calV^\bu} \def\Vbubu{\calV^\bubu}
\def\calW{\mathcal{W}} \def\Wbu{\calW^\bu} \def\Wbubu{\calW^\bubu}
\def\calX{\mathcal{X}} \def\Xbu{\calX^\bu} \def\Xbubu{\calX^\bubu}
\def\Xbubo{\calX^\bubo}
\def\bfA{{\mathbf{A}}}
\def\bfB{{\mathbf{B}}}
\def\D{\mathbb{D}}
\def\V{\mathbb{V}}
\def\Sh{\mathbf{Sh}}
\def\ess{{\mathsf{ess}}}
\def\irr{{\mathsf{irr}}}
\def\refl{{\mathsf{refl}}}
\def\trans{{\mathsf{trans}}}
\def\paths{{\mathsf{paths}}}
\def\Paths{{\mathsf{Paths}}}
\def\Repls{{\mathsf{Repls}}}
\def\Basic{{\mathsf{Basic}}}
\def\NonBasic{{\mathsf{NonBasic}}}
\def\length{{\mathsf{length}}}
\def\replace{{\mathsf{replace}}}
\def\longpaths{{\mathsf{longpaths}}}
\def\Longpaths{{\mathsf{LongPaths}}}
\def\LongPaths{{\mathsf{LongPaths}}}
\def\endpoints{{\mathsf{endpoints}}}
\def\dists{{\mathsf{dists}}}
\def\maxdist{{\mathsf{maxdist}}}
\def\natindex{{\mathsf{index}}}
\def\H{{\mathsf{H}}}
\def\PL{{\mathsf{PL}}}
\def\SPL{{\mathsf{SPL}}}
\def\ind{{\mathsf{ind}}}
\def\epi{\twoheadrightarrow}
\def\mepi{\mapstochar\twoheadrightarrow}
\def\bu{\bullet}
\def\bo{\circ}
\def\bubu{{\bullet\bullet}}
\def\bubo{{\bullet\circ}}
\title{Sheaves over finite DAGs may be archetypal (working draft)}
\author{Eduardo Ochs (LLaRC, PURO, UFF) \\
{\tt eduardoochs@gmail.com} \\
{\url{http://angg.twu.net/}}}
\date{Version: 2011mar08}
\maketitle
\fbox{\parbox{4.25in}{\small
Beware: {\color{red}{\sl These notes are still being written!}} My
plan is to give a presentation based on them at
\url{http://www.cle.unicamp.br/ebl2011/}, but whether that it is going
to be official or just to a few colleagues is something that depends
on the goodwill of the organizers (yeah, I would give less rank-points
to incomplete sumbissions, too!). {\sl You are not allowed to blame me
too hard for holes \& faults at this moment} --- please send
comments instead!
}}
\bsk
These notes are a follow-up to \cite{OchsIDCT}, where, in section 18,
we hinted at a notion of ``obviousness'' for definitions and theorems
that should be (or rather, that {\sl ought to be}!) formalizable.
Roughly speaking, a way to present a theorem makes that theorem
``obvious'' if 1) the reader can complete all the details omitted from
the presentation by himself, 2) the reader can store the theorem
itself in his memory using very little ``mental space''. In order to
formalize that we analyzed how discarding, or forgetting, information
acts as a kind of {\sl projection}, and how reconstructing the missing
information is akin to {\sl lifting}. By using diagrams and
well-chosen notations --- and bordering on ambiguity in the right way
--- it becomes possible to infer quite a lot from the names of the
objects and operations. A ``well-chosen notation'' for a general
structure --- i.e., one that allows us to commit to memory just a few
diagrams, and from them reconstruct all the rest --- usually comes
from an elementary particular case for that structure; we call that
particular case, and the language and notation coming from it, the
``archetypal model'' for that structure (see \cite{OchsIDCT}, section
15, for the details). Here we will discuss a very surprising
``well-chosen notation'' for sheaves.
% The ``right notation'' for a general structure --- the one that
% allows us to commit to memory just a few diagrams, and from them
% reconstruct all the rest --- usually comes from an elementary
% particular case for that structure; we call that particular case,
% and the language and notation coming from it, the ``archetypal
% model'' for that structure (see \cite{OchsIDCT}, section 15, for the
% details). Here we will discuss
{\sl (This introduction will not be convincing until I formalize how
to interpret diagrams formally... and the case of hyperdoctrines is
much easier, and will probably be done before sheaves).}
\msk
Now consider the following question, which at first sight may seem
to be impossible to treat mathematically:
%
\begin{quote}
{\sl Why are sheaves and sheafification hard to understand?}
\end{quote}
%
and the following conjecture:
\begin{quote}
{\sl Categories of the form $\Set^\bbD$, where $\bbD$ is a finite
poset, form an archetypal model for basic sheaf theory.}
\end{quote}
%
% One of the main motivating ideas for these notes is this conjecture:
% {\sl categories of the form $\Set^\bbD$, where $\bbD$ is a finite
% poset, are an archetypal model for basic sheaf theory}.
%
For ``basic sheaf theory'' we understand the contents of, for example,
chapter 5 (?) of \cite{BellLST} or chapter 21 of \cite{McLarty}; that
is, not current research topics, but just the difference between
knowing the fundamentals of sheaves as they are viewed in Topos Theory
and knowing nothing about them at all. To prove that conjecture
completely we would have to: 1) present all the definitions and
theorems of basic sheaf theory in the language of categories of the
form $\Set^\bbD$; 2) show how to lift these constructions to the
general case; 3) sketch a translation between the language coming from
the archetype and the language and notations from standard
presentations --- say, the above-mentioned \cite{BellLST} and
\cite{McLarty}, plus \cite{Elephant1} and \cite{MacLaneMoerdijk}. And
ideally all that should be done in enough details to make it obvious
how to translate all the constructions into, say, Agda [ref?] (with an
extension to let any piece of \LaTeX{} code, even a diagram, stand for
an identifier). Then we would have a first answer for our initial
question: sheaves and sheafification are ``hard'' because they need
all those many constructions and lifting steps; basic sheaf theory can
indeed be reconstructed from just a few core ideas and ``hints'', but
the number of reconstruction steps is huge.
Sheaves may be ``hard'' for still another reason. The archetypal model
proposed here, which focuses on finite and discrete objects given
explicitly, is quite different from the standard,approach (e.g., the
one in chapters II, III, V of \cite{MacLaneMoerdijk}), that uses
infinite, ``continuous'' objects all the time, and is very generic.
% as it is based on categories of the form $\Set^\bbD$,
This is a paragraph from \cite{Byers} (p.204):
\begin{quote}
For a subject that revels in the abstract, mathematical ideas are
often very concrete. Think of the discussion of ``variables'' in
Chapter 1. The domain of a variable may include an infinite range of
values, but when a variable is used we think of it as having a
definite and particular value. This enables us to think concretely.
This mental technique is used very generally in mathematics. We want
to understand some mathematical phenomenon that arises in a wide
variety of circumstances. How is one to think about such a general
phenomenon? Often one thinks in depth about some particular but
generic example --- some computation or picture. Of course the genius
is in picking the right example or examples. One looks for some
specific example that captures all the subtleties of the general
situation. Thus ``what is going on'' is often revealed within the
specificity of a particular example. The task of extending and
abstracting that understanding is often secondary. The role of
specific counterexamples in establishing the boundaries of some
mathematical theory is balanced by the role of specific generic
examples for which one can say that they illustrate the ``general
case.''
\end{quote}
It should be possible to formalize Byers's notion of ``right example''
precisely in the framework of \cite{OchsIDCT} --- and basic sheaf
theory may be a good case to study with that goal in view, because it
can be reconstructed from {\sl two} different families of ``right
examples'', one discrete, one continuous.
\msk
So far, so good: we have delineated a big project, whose interest and
relevance should be hard to deny. However, these notes are just the
first steps towards that --- we are only going to present the basic
tools for working on toposes of the form $\Set^\bbD$, and show what
the basic definitions and constructions for sheaves become in that
case. These notes can be considered as a complement and an
introduction for \cite{Simmons} and \cite{BellLST} (its chapter 5(?));
I wrote them for an audience of logicians and computer scientists who are
neither categorists, nor topologists, and who may have struggled with
Category Theory (...)
% and we can consider that they are mainly dydactical in purpose:
% we are not even going to delimit completely what ``basic sheaf
% theory'' is, and all the more advanced topics will be left for future
% work.
% The main ``practical'' intent of these notes
% {\sl This is a work in progress.}
% --------------------
% «positional» (to ".positional")
% (sec "Positional notation" "positional")
\mysection {Positional notation} {positional}
We will say that a subset $A$ of $\Z^2$ is {\sl well-positioned} when
$\inf(\sst{x}{(x,y)ÝA}) = \inf(\sst{y}{(x,y)ÝA}) = 0$; a {\sl
well-positioned rectangle} (of width $w$ and height $h$) is a subset
of $\Z^2$ of the form $\{0,\ldots,w-1\}×\{0,\ldots,h-1\}$. We can use
a positional notation to represent functions from well-positioned
rectangles to $\N$. For example:
%
$$\begin{array}{rccl}
\sm{4567\\0123}: & \{0,1,2,3\}×\{0,1\} & \to & \N \\
& (x,y) & \mto & x+4y \\
\end{array}
$$
We will use bullet diagrams, like $\dagVee***$, to denote
well-positioned finite subsets of $\Z^2$. For typographical
convenience we will draw these bullet diagrams by squeezing them a bit
horizontally: $\dagVee***$, instead of $\proportionalVee***$.
The set $\dagVee***$ is a subset of a well-positioned rectangle; its
characteristic function is $\sm{101\\010}$. We can adapt the idea of a
positional notation to represent functions whose domains are arbitrary
well-positioned finite subsets of $\Z^2$ to $\N$. For example:
%
% $\dagVee241$ is a function:
%
$$\begin{array}{rccl}
\dagVee241: & \dagVee*** & \to & \N \\
& (x,y) & \mto & x+2y \\
\end{array}
$$
So, $\dagVee101$ is a characteristic function with domain
$\dagVee***$, and by abuse of language we will sometimes denote
subsets of well-positioned subsets of $\Z^2$ by their characteristic
functions.
Also, a notation like $(\dagVee255 \to \dagWdot123456)$ will
stand for a function between two well-positioned subsets of $\Z^2$,
%
$$\begin{array}{rccl}
(\dagVee255 \to \dagWdot123456): & \dagVee*** & \to & \dagWdot****** \\
& (x,y) & \mto & (\frac{x-y+5}2,\frac{-x+y+1}2) \\
\end{array}
$$
%
that can be defined formally as composite, $(\dagVee255 \to
\dagWdot123456) := (\dagWdot123456)^{-1} ¢ (\dagVee255)$:
%
%D diagram composite
%D 2Dx 100 +40 +45 +55
%D 2D 100 A -> B -> C -> D
%D 2D
%D 2D +10 A' ----------> D'
%D 2D
%D (( A .tex= \dagVee***
%D B .tex= \{2,5\}
%D C .tex= \{1,2,3,4,5\}
%D D .tex= \dagWdot******
%D A B -> .plabel= a \textstyle(\dagVee255)
%D B C `-> # .plabel= a \textstyle\dagVee255
%D C D -> .plabel= a \textstyle(\dagWdot123456)^{-1}
%D # A D -> .slide= -7.5pt .plabel= b \textstyle(\dagVee255\to\dagWdot123456)
%D ))
%D (( A' .tex= \dagVee255
%D D' .tex= \dagWdot123456
%D A' D' ->
%D ))
%D enddiagram
%D
$$\diag{composite}$$
The {\sl natural indexing} on a well-positioned finite subset $A$ of
$\Z^2$ is the bijection $\natindex_A: A \to \{1, \ldots, |A|\}$ that
enumerates all elements in $A$ in ``reading order'', starting from the
top line and traversing the elements in each line from left to right.
For example, the natural indexing on $\dagVee***$ is $\dagVee123$.
% --------------------
% «zdags» (to ".zdags")
% (sec "ZDAGs" "zdags")
\mysection {ZDAGs} {zdags}
A characteristic function like $\dagVee100$ gives me the impression of
something unstable: it has an element, at the `1', immediately above
an empty position, indicated by the `0' at the bottom; `1's feel
heavier than `0's, and the `1' wants to fall, and to change places
with the `0'... It turns out that there are {\sl two} good ways to
formalize that idea: by order-preserving functions and by topology.
Let's see this.
\msk
We say that an arrow $(x_0,y_0) \to (x_1,y_1)$ in $\Z^2×\Z^2$ is a
{\sl black pawn's move} when it is of the form $(x_0,y_0) \to (x_0+\DD
x,y_0-1)$, for $\DD xÝ\{-1,0,1\}$. Each subset $\Z^2$ can be endowed
with a natural directed (acyclical) graph structure, whose arrows are
the black pawn's moves over its points. By an abuse of language our
bullet diagrams will sometimes stand for DAGs, instead of for just
subsets of $\Z^2$; the arrows are the black pawn's moves. For example,
$\dagKite*****$ will stand for the DAG at the left below; and by using
the natural indexing we can obtain an equivalent DAG, drawn at the
right, whose explicit description is much shorter --- namely, $(\{1,
2, 3, 4, 5\}, \{(1 \to 2), (1 \to 3), (2 \to 4), (3 \to 4), (4 \to
5)\})$.
%
$$\bigKite {(1,3)} {(0,2)} {(2,2)} {(1,1)} {(1,0)}
\qquad
\bigKite 12345
$$
A {\sl $\Z^2$-DAG}, or simply a {\sl ZDAG}, is a pair made of a finite
well-positioned subset of $\Z^2$ and its black pawn's moves.
From now let be $\bbD=(D_0, D_1)$ be a ZDAG --- but the definitions
and theorems below also work when $\D$ is an arbitrary directed graph.
If $f:D_0 \to \N$, we say that $f$ {\sl decreases} on an arrow $(\aa
\to \bb) \in D_1$ when $f(\aa) \ge f(\bb)$; we say that $f$ is {\sl
non-decreasing} when it does not decrease for any $(\aa \to \bb) \in
D_1$. For example: $\dagVee255$ is non-decreasing, but $\dagVee010$ is
not --- it decreases on the right arm of the `V'.
A subset of $D_0$ is {\sl open} if and only if its characteristic
function is non-decreasing. So, $\dagVee000$, $\dagVee001$,
$\dagVee011$, $\dagVee101$, $\dagVee111$ are open sets of
$\dagVee***$, and $\dagVee010$, $\dagVee100$, $\dagVee110$ are not
open.
The {\sl order topology} on $\bbD$, denoted by $\Opens_{D_1}(D_0)$,
$\Opens(D_0)$, or $\Opens(\bbD)$, is the set of open sets of $\bbD$.
For example, $\Opens(\dagVee***) = \{\dagVee000, \dagVee001,
\dagVee011, \dagVee101, \dagVee111\}$.
An {\sl Alexandroff Topology} is one in which the family of open sets
is also closed by arbitrary intersections, not only by arbitrary
unions; order topologies are Alexandroff.
The {\sl interior} of a set $A \subset D_0$ is the union of all open
sets contained in $A$. The {\sl cointerior} of a set $A \subset D_0$
is the intersection of all open sets containing $A$; in Alexandroff
spaces $A^\coint$ is always an open set. We say that a subset $A
\subset D_0$ is {\sl representable} when it is of the form
$\{\aa\}^\coint$ for some $\aa \in D_0$.
Each ZDAG $\D=(D_0, D_1)$ has a natural topology; and the points of
$D_0$ are in bijection with the representable open sets of
$\Opens(\D)$.
% --------------------
% «priming» (to ".priming")
% (sec "Priming" "priming")
\mysection {Priming} {priming}
For any directed graph $\D=(D_0, D_1)$ the structure $(\Opens(\D),
\supsetneq)$ is a DAG. We are going to use this way of generating new
DAGs so much that we need a short name for it: we will call it
``priming''. The figure below shows what happens in the case when $\D
= \dagGuill******$; the representable open sets are marked with
parentheses. We are abusing the positional notation a bit more at the
right, and using it to denote a function from $(\dagGuill******)' =
\dagGuillPrime ****** ******$ to $\Opens(\dagGuill******)$ --- we are
indexing the points of $(\dagGuill******)'$ not by numbers, but by the
opens sets of $\Opens(\dagGuill******)$.
%
\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 +100
%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}$$
The structure $(\Opens(\D), \supsetneq)$ has many more arrows than
we've drawn above. The diagram shows only the black pawn's moves, and
`$\supsetneq$' is actually the transitive closure of that. However,
the black pawn's moves are exactly the ``essential'' arrows in
`$\supsetneq$', in a sense that we shall now make precise.
% --------------------
% «essential» (to ".essential")
% (sec "Essential arrows" "essential")
\mysection {Essential arrows} {essential}
We start with some notation and definitions (on a directed graph $(A,
R)$).
A {\sl reflexive arrow} of $R$ is an arrow of the form $(\aa \to
\aa)$; $R^\irr$ is $R$ minus its reflexive arrows, and a relation $R$
is {\sl irreflexive} when $R=R^\irr$.
% A relation $R$ is {\sl acyclic} when $R^\irr$ has no cycles. Note
% that this is a non-standard definition; we choose it so that posets
% will be acyclic.
$R^\refl$ and $R^\trans$ are the reflexive and the transitive closures
of $R$. As we are working on $(A,R)$, $R^\refl$ is $R \cup \sst{(\aa
\to \aa)}{\aa \in A}$. We write $R^*$ for the reflexive-transitive
closure of $R$.
Two relations $R,S \subseteq A×A$ are {\sl equivalent} when $R^*=S^*$
(or: when they generate the same order topology).
An arrow $(\aa \to \bb) \in R$ is {\sl inessential} when $(R^*
\setminus \{\aa \to \bb\})^* = R^*$. The set of essential (i.e.,
non-inessential) arrows of $R$ will by denoted by $R^\ess$.
A directed graph is {\sl good} when $R^* = (R^\ess)^*$. It is easy to
see that all the ZDAGs mentioned explicitly in examples above are
``good'', and that their black pawn's moves are essential. However, if
$(A,R) = (\{1,2,3\},\{(1 \to 2),(2 \to 3),(3 \to 1)\})$ then $R$,
$R^*$ and $R^{-1}$ are equivalent, and $R \cap R^{-1} = \emp$, so in
this case all arrows are inessential; and in $(\R,<)$ all arrows are
again inessential. So, {\sl very} roughly, loops are evil, and
loopless ``dense'' situations in which every arrow is the composite of
others are also evil. It will turn out that all finite DAGs are good,
and ZDAGs are finite DAGs, and therefore good. We will sketch a
constructive proof of that.
\msk
The {\sl length} of a path $\aa_0 \to \aa_1 \to \ldots \to \aa_n$ is
$n$. We write $\Paths_R$ for the set of all paths all of whose arrows
are in $R$, and $\LongPaths_R$ for the subset of $\Paths_R$ with just
the paths of length $\ge 2$. If $(A, R)$ is a finite DAG then
$\Paths_R$ is a finite set of finite paths. We define the functions
$\endpoints_R: \Paths_R \to R^*$ and $\length_R: \Paths_R \to \N$ in
the obvious way; note that the subscript `$R$' indicates their domain.
A {\sl possible replacement} in $R$ is a pair $\rho = ((\aa \to \bb),
\pi)$, where $(\aa \to \bb) Ý R$ and $\pi$ is a path in $R$ with
$\endpoints_R(\pi) = (\aa \to \bb)$ and $\length_R(\pi) \ge 2$. If
$(A, R)$ is a DAG then in a replacement $((\aa \to \bb), \pi)$ the
path $\pi$ cannot have repeated arrows, and $\endpoints_R(\pi)$ cannot
be an arrow of $\pi$. We write $\Repls_R$ for the set of possible
replacements in $R$.
A replacement $\rho = ((\aa \to \bb), \pi) \in \Repls_R$ induces a
function $\replace_\rho: \Paths_R \to \Paths_{R \setminus \{(\aa \to
\bb)\}}$, that expands every occurrence of an arrow $\aa \to \bb$ in
a path by its expansion, $\pi$. The function $\replace_\rho$ does not
change endpoints, and it is non-decreasing on lengths.
Let's write $\Paths_R(\aa \to \bb)$ for $\sst{\pi Ý
\Paths_R}{\endpoints_R(\pi)=\aa \to \bb}$. For any $(\aa \to \bb) Ý
R^*$ and $\rho Ý \Repls_R$ the function $\replace_\rho$ restricts to a
function from $\Paths_R(\aa \to \bb)$ to $\Paths_R(\aa \to \bb)$. If
$(A,R)$ is a finite DAG, then for each $\aa \to \bb Ý R^*$ the set
$\Paths_R(\aa \to \bb)$ is finite and non-empty, and we can define the
function
%
$$\begin{array}{rccl}
\maxdist_R: & R^* & \to & \N \\
& (\aa \to \bb) & \mto & \sup \, \sst{\length_R(\pi)}{\pi Ý \Paths_R(\aa \to \bb)}, \\
\end{array}
$$
%
which turns out to be invariant by replacements: for any $\rho = ((\aa
\to \bb), \pi) \in \Repls_R$ the domains of $\maxdist_R$ and
$\maxdist_{R \setminus \{(\aa \to \bb)\}}$ are equal, and so are the
values that these functions return --- even though $\Paths_R(\aa \to
\bb)$ may be a bigger set than $\Paths_{R \setminus \{(\aa \to
\bb)\}}(\aa \to \bb)$. The function $\maxdist_R$ gives an upper
bound for how lengths are changed by replacements: we have, for any
$\pi \in \Paths_R$ and $\rho \in \Repls_R$,
%
$$\length_R(\pi) \le \length_R(\replace_\rho(\pi)) \le \maxdist_R(\endpoints_R(\pi)).$$
It also turns out that $\maxdist_R$ split $R$ in a very nice way: the
arrows of $R$ which have replacements (i.e., which are the first
component of some $\rho \in \Repls_R$) are exactly the ones in
$\maxdist_R^{-1}(\{2, 3, \ldots\}) \cap R$, and the arrows of $R$
which have no replacements are exactly $\maxdist_R^{-1}(\{1\})$. Let's
give names to these sets: $R$ is the disjoint union of $\Basic_R$ and
$\NonBasic_R$, where:
%
$$\begin{array}{rcl}
\Basic_R &=& \maxdist_R^{-1}(\{1\}) \cap R \;\; = \;\; \maxdist_R^{-1}(\{1\}) \\
\NonBasic_R &=& \maxdist_R^{-1}(\{2, 3, \ldots\}) \cap R \\
\end{array}
$$
\def\Rmab{{R \setminus \{(\aa \to \bb)\}}}
These sets change in a very simple way after a replacement. If $((\aa
\to \bb), \pi) \in \Repls_R$, then
%
$$\begin{array}{rcl}
\Basic_\Rmab &=& \Basic_R \\
\NonBasic_\Rmab &=& \NonBasic_R \setminus \{(\aa \to \bb)\} \\
\end{array}
$$
This means that we can delete the ``non-basic'' arrows of a finite DAG
$(A, R)$ in any order. Take a bijection between $\NonBasic_R$ and a
set of the form $\{1, \ldots, n\}$; this gives us a sequence $(\aa_1
\to \bb_1), \ldots, (\aa_n \to \bb_n)$. Let $R_0=0$, and define $R_1,
\ldots, R_n$ by making each $R_i$ be $R_{i-1}$ minus the arrow $(\aa_i
\to \bb_i)$. For each $i$, choose any $\pi_i \in
\Paths_{R_{i-1}}(\aa_i \to \bb_i)$, and define $\rho_i = ((\aa_i \to
\bb_i), \pi_i)$. Now $\rho_1, \ldots, \rho_n$ is a sequence of
replacements, that can be used to shrink the relation $R=R_0$ to an
equivalent relation $R_n=\Basic_R=R^\ess$: using the composite
$\replace_n ¢ \ldots ¢ \replace_1: \Paths_R \to \Paths_{R^\ess}$ we
can see that $R^* = (R^\ess)^*$. The relation $R_n$ is minimal, and
cannot be shrunk anymore.
It is clear from that argument that a relation $R$ is good if and only
if the relations equivalent to it are exactly the ones in the set
$\sst{S}{R^\ess \subseteq S \subseteq R^*}$; and then $R^\ess =
\bigcap \sst{S}{S^* = R^*}$, and the intersection of two relations
equivalent to $R$ is again equivalent to $R$.
Every ZDAG $\D=(A,R)$ is a finite DAG, and so is good. Also, if
$((x,y) \to (x',y')) Ý R^*$ then $\maxdist_R((x,y) \to (x',y')) =
y-y'$, and so the essential/basic arrows of $R^*$ are exactly the
black pawn's moves. All relations equivalent to $R$ induce the same
order topology on $A$. As ZDAGs are good, we have two canonical ways
to represent $(\D,\Opens(\D))$ by an relation on $A$: $R^*$ and
$R^\ess$, and $R^\ess$ is by far more economical.
\msk
Here is a slightly more general result (for details, see [some
topology book]):
{\sl Theorem.} If $A$ is a finite set, then there is a bijection
between: $T_0$ topologies on $A$, partial orders on $A$, and DAGS on
$A$ having only essential arrows.
Some $T_0$ topologies (and, equivalently, partial orders) on finite
sets, {\sl but not all,} are equivalent to ones coming from ZDAGs; for
example, add the arrow $3 \to 5$ to $\dagO 1234{}5$ and you get
something that is not equivalent to a ZDAG. But topologies coming from
ZDAGs will be enough for our purposes, and we will represent them by
bullet diagrams.
% --------------------
% «diamond» (to ".diamond")
% (sec "Diamond-shaped regions" "diamond")
\mysection {Diamond-shaped regions} {diamond}
If $(A,R^*)$ is a preorder, we say that a set $S \subseteq A$ is a
{\sl diamond-shaped region} if it is of the form $\sst{\bb Ý
A}{\text{$(\aa \to \bb) \in R^*$ and $(\bb \to \cc) \in R^*$}}$, for
some $\aa, \cc \in A$. We saw that if $(A,R)$ is a finite DAG then the
set of the relations equivalent to $R$ is diamond-shaped in
$(\Pts(A^2), \subseteq)$, with extremities $R^\ess$ and $R^*$.
If $(A,R)$ is a finite DAG then the subsets of $A$ whose cointerior is
a given open set $U$ form a diamond-shaped region. One of the
extremities of the diamond is $U$ itself; the other extremity can be
calculated by intersections, and, as we will not use that operation
much, let's also call it `$\ess$' --- $U^\ess$ is the set of
``essential points'', or ``generators'', for $U$.
Formally, we can define the set of essential points of $B$ as $B^\ess
:= \bigcap \sst{C \subseteq A}{C^\coint = B^\coint}$, and, for
example, $\dagGuill011111^\ess = \dagGuill011000$. On a finite DAG
$(A,R)$, the subsets of $A$ whose cointerior is a given open set $U$
are exactly the ones between $U^\ess$ and $U$; and the representable
open sets are the ones such that $|U^\ess| = 1$. Note that the
operation $B \mto B^\ess$ gives us a minimal way to express each open
set on a finite DAG as a union of representable open sets: $U =
\bigcup \sst{\{\aa\}^\coint}{\aa \in U^\ess}$. An example should make
this less abstract:
%
$$\def\ph{\phantom{\dagKite*****}}
\begin{array}{rcl}
\dagGuill011111 &=& \bigcup \; \sst{\{\aa\}^\coint}{\aa \in \dagGuill011111^\ess} \ph \\
&=& \bigcup \; \sst{\{\aa\}^\coint}{\aa \in \dagGuill011000} \ph \\
&=& \bigcup \; \setof{\dagGuill010000^\coint, \dagGuill001000^\coint} \ph \\
&=& \bigcup \; \setof{\dagGuill010111, \dagGuill001010} \ph \\
&=& \dagGuill010111 \cup \dagGuill001010 . \ph \\
\end{array}
$$
Another way to state this is: ``The operation $(·^\coint)^{-1}$
partitions $\Pts(A)$ into diamond-shaped regions''. We shall see soon
that if $(·^*):\bbH \to \bbH$ is any Lawvere-Tierney modality on a
finite Heyting algebra, then $(·^*)^{-1}$ also partitions $\bbH$ into
diamond-shaped regions.
% {\myttchars
% \footnotesize
% \begin{verbatim}
% 1 0 0
% 0 0 0
% 1 0 0 coint 1 0 0 1 0 0
% | 0 0 0 |--> 1 0 0 1 1 0
% |
% v | | |
% | <-> | |
% 1 0 0 v v v
% 1 0 0
% 1 0 0 und 1 0 0 1 0 0
% 1 1 0 <--| 1 1 0 1 1 0
% 1 1 0
% 1 1 0 | | |
% | <-> | |
% | v v v
% |
% v 1 1 1 int 1 1 0 1 0 0
% 1 1 0 |--> 1 1 0 1 1 0
% 1 1 1
% 1 1 0
% \end{verbatim}
% }
% --------------------
% «continuity» (to ".continuity")
% (sec "Continuity" "continuity")
\mysection {Continuity} {continuity}
A directed graph $(A,R^*)$, where $R^*$ is a reflexive and transitive
relation on $A$, may be regarded as a category (a ``preorder''),
$\bfA$; we can define formally $\Hom_\bfA(\aa, \bb)$ as $\{(\aa \to
\bb)\} \cap R$. We will sometimes write $\bfA_R$ instead of $\bfA$ for
clarity.
A function $f:A \to B$ may be seen as a map $f:(A,R) \to (B,S)$ or
$f:(A,R^*) \to (B,S^*)$ between DAGs, which may or may not repect the
order, or as a map $f:(A,\Opens_R(A)) \to (B,\Opens_R(B))$ between
topological spaces, which may or may not be continuous, or as a map
$f:|\bfA| \to |\bfB|$, which may or may not be extendable to (i.e., be
the action on objects of) a functor $f:\bfA \to \bfB$. Note that we
always use the name `$f$' for the map; when we want to regard it in a
specific way we write it as $f:\_\_ \to \_\_$, and give the rest of
the information in the way we write its domain and codomain.
{\sl Theorem.} The following conditions are equivalent:
1) $f:(A,R) \to (A,S^*)$ is order-preserving,
2) $f:(A,R^*) \to (A,S^*)$ is order-preserving,
3) $f:(A, \Opens_R(A)) \to (B, \Opens_S(B))$ is continuous,
4) $f:|\bfA_R| \to |\bfB_S|$ is the object part of a functor (or, more
shortly: ``$f:\bfA_R \to \bfB_S$ is a functor'').
\msk
Here is a very interesting example. Take any ZDAG $\bbD = (A, R)$, and
consider the transformation on $A$ that duplicates the $y$-coordinate
of each point; the resulting ZDAG, $\bbD^\discr = (\psm{1& \\ &2}A,
\emp)$, has no black pawn's moves, and so is discrete. The obvious
``anti-discretization'' function $\antidiscr_\bbD: \bbD^\discr \to
\bbD$ is continuous.
Let's look at a concrete case for clarity: $\antidiscr:
\dagWdotT****** \to \dagWdot******$. It induces a map
$\antidiscr^{-1}: \Opens(\dagWdot******) \to \Opens(\dagWdotT******)$,
that, modulo a factor of 2 in the $y$ coordinate, is exactly the
inclusion of $\Opens(\dagWdot******)$ in $\Pts(\dagWdot******)$. We
can regard $\antidiscr^{-1}$ as a functor, and it turns out that is
has both adjoints, which are exactly the ``interior'' and
``cointerior'' operations defined in section \ref{zdags}; the diagram
below --- an ``internal diagram'', as in \cite{OchsIDCT} --- should
convince the reader of the truth of this. We actually have more: $\ess
\dashv \coint \dashv \discr \dashv \int$, but the operation $\ess$ is
not going to be important.
%
$$\def\W #1#2#3#4#5#6{(\dagWdot {#1}{#2}{#3}{#4}{#5}{#6})}
\def\WW#1#2#3#4#5#6{(\dagWdotT{#1}{#2}{#3}{#4}{#5}{#6})}
\diag{adjs-to-discr}
$$
The adjoints associated to arbitrary continuous functions between DAGs
will be discussed in section \ref{geometric-morphs}.
% --------------------
% «quotient» (to ".quotient")
% (sec "Quotient Topologies" "quotient")
\mysection {Quotient Topologies} {quotient}
Let $q$ (for ``quotient'') be the following surjective function, going
from $\R$ to a set of three symbols:
%
$$\begin{array}{rccl}
q: & \R & \to & \{\aa,\bb,\cc\} \\
& x & \mto & \begin{cases}
\aa & \text{when $x \in (-\infty, 0]$} \\
\cc & \text{when $x \in (0,1)$} \\
\bb & \text{when $x \in [1,\infty)$} \\
\end{cases}
\end{array}
$$
%
There are eight subsets $A \subseteq \R$ such that $q^{-1}(q(A)) = A$;
only five of them are open. Here they are, ordered by reverse
inclusion:
%
$$\def\ph{\phantom{m}}
\bigKite {(-‚,‚)} {(-‚,1)\ph} {\ph(0,‚)} {(0,1)} {\emp}
\qquad
\two/->`<-/^q_{q^{-1}}
\qquad
\bigKite {\{\aa,\bb,\cc\}} {\{\aa,\cc\}} {\{\bb,\cc\}} {\{\cc\}} {\emp}
$$
The five sets at the right form a topology on $\{\aa,\bb,\cc\}$ ---
the {\sl quotient topology} induced by $q$. The general definition is
this: if $(X,\Opens(X))$ is a topological space, then the topology on
$Y$ induced by the function $q:X \to Y$ is $\Opens(Y) := \sst{B
\subseteq Y}{q^{-1}(B) \in \Opens(X)}$. The induced order relation
on $Y$, $R \subseteq Y×Y$, is defined by: $\aa R \bb$ iff every open
set of $Y$ that contains $\aa$ also contains $\bb$. In the case of our
$q$, this is:
%
$$\def\ph{\phantom{m}}
\bigVee {(-‚,0]\ph} {\ph[1,‚)} {(0,1)}
\qquad
\bigVee \aa \bb \cc
$$
When $Y$ is finite (or, more generally, when $\Opens{Y}$ is
Alexandroff) we can reconstruct $\Opens(Y)$ from its order relation:
$\Opens(Y) := \Opens_R(Y)$. When $Y$ is not Alexandroff --- for
example,if $q:= \id : \R \to \R$ --- then we have $\Opens(Y)
\subsetneq \Opens_R(Y)$.
We are going to use that order topology on $\{\aa, \bb, \cc\}$ in our
archetypal definition for sheaves, Note that $(Y, \Opens(Y))$ is
$(\dagVee***, \Opens(\dagVee***))$, but we are using $\aa$, $\bb$,
$\cc$ as names for its points --- $\dagVee\aa\bb\cc$, instead of
$\dagVee123$.
We will need a pronounceable name for $\dagVee***$; let's call it
$\bbV$. It will also be convenient to have names for its five open
sets. They will be $X$, $U$, $V$, $W$, $\emp$:
%
$$\def\ph{\phantom{m}}
\bigKite {(-‚,‚)} {(-‚,1)\ph} {\ph(0,‚)} {(0,1)} {\emp}
\qquad\quad
% \two/->`<-/^q_{q^{-1}}
% \qquad
\bigKite {\{\aa,\bb,\cc\}} {\{\aa,\cc\}} {\{\bb,\cc\}} {\{\cc\}} {\emp}
\qquad
\bigKite XUVW\emp
$$
Sometimes $U$, $V$, $W$ will stand for $\{\aa,\cc\}$, $\{\bb,\cc\}$,
$\{\cc\}$ --- then we will have $UþV=X$ and $UÌV=W$ ---, sometimes for
arbitrary open sets (as variables). Similarly, $X$ will stand for the
``top'' open set.
% So sometimes $U$, $V$, $W$ will stand for arbitrary open sets (as
% variables), and sometimes for $\{\aa,\cc\}$, $\{\bb,\cc\}$,
% $\{\cc\}$; similarly, $X$ stands for the ``top'' open set.
In the next sections we will work on a fixed topological space ---
$\bbV$ --- but the way to generalize that should be obvious.
% --------------------
% «covers» (to ".covers")
% (sec "Covers" "covers")
\mysection {Covers} {covers}
A {\sl cover} (in $\bbV$) is a subset of $\Opens(X)$; a cover for
$UÝ\Opens(X)$ is a subset of $\Opens(X)$ whose union is $U$. We will
use a notational convention to reduce the use of `$\bigcup$'s: $\calU$
denotes a cover for $U$, $\calV$ a cover for $V$, $\calX$ a cover for
$X$ (the whole space), and so on; so we have $\bigcup\calU=U$,
$\bigcup\calV=V$, etc. As we may have different covers for the same
open set we will use {\sl annotations} to distinguish them: for
example, $\calU''$, $\calU^*$.
We can use subsets of $\dagKite*****$ to denote covers in $\bbV$. For
example, $\dagKite01100$ ($=\{U,V\}$) is a cover for $X$.
Covers may be (downward) saturated, in the sense that if $\calU \ni V$
and we have an arrow $V \to W$ --- i.e., if $V \supset W$ --- then we
also have $\calU \ni W$. For example, $\dagKite01100$ is not
saturated, but $\dagKite01111$ is. Saturated covers correspond to open
sets of $\dagKite*****$.
We will use the annotation `${}^\bu$' to indicate that a cover is
saturated: $\calU^\bu$ denotes a saturated cover for $U$, $\calU$ an
arbitrary one. Type-theoretically, a $\calU^\bu$ is (dependent) pair
made of a cover $\calU$ and a proof (or witness) that it is saturated;
and a $\calU$ is a triple composed of an open set $U$, a family of
open subsets of $X$ (or of $U$), and a proof that the union of that
family is $U$.
\msk
We have a natural operation that takes a saturated cover and forgets
the proof that it is saturated; that operation goes from the set of
saturated covers to the set of all covers. We also have a natural
operation that takes an arbitrary cover and saturates it. In the
spirit of \cite{OchsIDCT}, we can name these operations $\calU^\bu
\ito \calU$ and $\calU \mepi \calU^\bu$, where `$\ito$' is an
injective `$\mapsto$' and `$\mepi$' a surjective `$\mapsto$'. The
composite $\calU^\bu \ito \calU \mepi \calU^\bu$ is the identity, but
the composite $\calU \mepi \calU^\bu \ito \calU$ is not:
%
%D diagram isnot
%D 2Dx 100 +30 +30
%D 2D 100 A B C
%D 2D
%D 2D +20 D E F
%D 2D
%D (( A .tex= \Pts(\dagKite*****)
%D B .tex= \Opens(\dagKite*****)
%D C .tex= \Pts(\dagKite*****)
%D D .tex= \dagKite01100
%D E .tex= \dagKite01111
%D F .tex= \dagKite01111
%D A B ->> .plabel= a \coint
%D B C >->
%D D E |->>
%D E F `->
%D ))
%D enddiagram
%D
$$\diag{isnot}$$
It is a kind of closure operation, as we shall see soon. Clearly,
$\calU \mepi \calU^\bu \ito \calU$ is a weird name for it, as the last
`$\calU$' may be different from the first. We will fix that later.
A stronger kind of saturatioon is the following: we say that a cover
$\calU$ is {\sl doubly saturated} if it contains all the subsets of
$\bigcup\calU$. We will annotate doubly saturated covers with a
`${}^\bubu$', and besides the obvious forgetful operations
$\calU^\bubu \ito \calU^\bu$ and $\calU^\bubu \ito \calU$ we also have
``double saturation'' operations, $\calU \mepi \calU^\bubu$ and
$\calU^\bu \mepi \calU^\bubu$. For example, to calculate
$(\dagKite01100)^\bubu$ we need to add to $\dagKite01100 = \{U,V\}$
all the subsets of $\bigcup\{U,V\} = UþV = X$; the result is
$\dagKite11111$. The doubly-saturated covers are exactly the {\sl
representable} open sets of $\dagKite*****$.
The closure operation $\calU^\bu \epito \calU^\bubu \ito \calU^\bu$
will be one of our main objects of interest here. It will be a key
ingredient in defining sheaves and sheafification in the most natural
setting, which is this: we start with an arbitrary DAG $\bbV$, prime
it once to obtain the topology $\Opens(\bbV)$ (which will be a Heyting
algebra), and prime that to obtain the set of saturated covers:
%D diagram V-prime-prime
%D 2Dx 100 +40 +65
%D 2D 100 A ---> A' ---> A''
%D 2D
%D 2D +70 B ---> B' ---> B''
%D 2D
%D 2D +15 C ---> C' ---> C''
%D 2D
%D (( A .tex= \bigVee\aa\bb\cc
%D A' .tex= \bigKite{X}{(U)}{(V)}{(W)}{\emp}
%D A'' .tex= \phantom{m}\AAA\phantom{m}
%D @ 0 @ 1 -> @ 1 @ 2 ->
%D ))
%D (( B .tex= \dagVee345
%D B' .tex= \dagKite13456
%D B'' .tex= \dagKitePrime1234567
%D @ 0 @ 1 -> @ 1 @ 2 ->
%D ))
%D (( C .tex= \bbV
%D C' .tex= \bbV'
%D C'' .tex= \bbV''
%D @ 0 @ 1 -> @ 1 @ 2 ->
%D ))
%D enddiagram
%D
$$\def\Def #1#2{{#1{=}#2}}
\def\PDef#1#2{{#1{=}\left(#2\right)}}
\def\Def #1#2{{\phantom{mm}#2{=}#1}}
\def\PDef#1#2{{\phantom{mm}\left(#2\right){=}#1}}
\def\AAA{\hugeKitePrime
{\PDef{\calX^\bubu}{\dagKite11111}}
{\Def {\calX^\bubo}{\dagKite01111}}
{\PDef{\calU^\bubu}{\dagKite01011}}
{\PDef{\calV^\bubu}{\dagKite00111}}
{\PDef{\calW^\bubu}{\dagKite00011}}
{\PDef{ \emp^\bubu}{\dagKite00001}}
{\Def { \emp^\bubo}{\dagKite00000}}
}
\diag{V-prime-prime}
$$
In the diagram above the representables are marked in parentheses, and
we give names to the seven saturated covers. It turns out that for any
starting DAG $\bbD$ and any open set $U \in \Opens(\bbD)$ the set
$\sst{\calU^\bu}{\text{$\calU^\bu$ is a saturated cover for $U$}}$ is
diamond-shaped; we mark with a `${}^\bubu$' its maximal element --- a
doubly saturated cover --- and with a `${}^\bubu$' its minimal element
--- the smallest saturated cover for $U$. Here's why this happens.
{\sl Theorem}. For any topological space $(X, \Opens(X))$ and covers
$\calU$, $\calV$, $\calU^\bu$, $\calV^\bu$, $\calU^\bubu$,
$\calV^\bubu$ on it,
(i) $\bigcup(\calUþ\calV) = \bigcup\calUþ\bigcup\calV$,
(ii) $\calU^\buþ\calV^\bu$ is saturated,
(iii) $\calU^\bubuþ\calV^\bubu$ is not necessarily doubly saturated,
(iv) $\bigcup(\calUÌ\calV) \subseteq \bigcup\calUÌ\bigcup\calV$
(v) $\bigcup(\calU^\buÌ\calV^\bu) = \bigcup\calU^\buÌ\bigcup\calV^\bu$
(vi) $\calU^\buÌ\calV^\bu$ is saturated,
(vii) $\calU^\bubuÌ\calV^\bubu$ is doubly saturated.
Proof. The only non-trivial part is $\bigcup(\UbuÌ\Vbu) \supseteq
\bigcup\UbuÌ\bigcup\Vbu$. Take any point $\cc \in
\bigcup\UbuÌ\bigcup\Vbu$; there are open sets $W'$, $W''$ with $\cc Ý
W' Ý \Ubu$ and $\cc Ý W'' Ý \Vbu$. Define $W := W'ÌW''$; we have $\cc
Ý W Ý \Ubu$ and $\cc Ý W Ý \Vbu$, so $\cc Ý W Ý \UbuÌ\Vbu$ and $\cc
\in \bigcup(\UbuÌ\Vbu)$.
\def\Ubup{\calU^{\bu\prime}}
\def\Ubupp{\calU^{\bu\prime\prime}}
\def\satcovers{\mathsf{satcovers}}
An easy corollary of this is that if $\Ubup$ and $\Ubupp$ are two
saturated covers of $U$, then $\UbupÌ\Ubupp$ is still a saturated
cover of $U$. Let's write $\satcovers(U)$ for the set of saturated
covers of $U$. We know that $\satcovers(U)$ is closed by arbitrary
unions and finite intersections, and has $\Ububu$ as its top element;
if $\satcovers(U)$ is finite then the intersection of all saturated
covers of $U$ is a still a cover of $U$, and is the minimal one; so:
{\sl Theorem.} If $\bbD$ is finite then for each set $\satcovers(U)$,
for $U \in \Opens(\bbD)$, is a finite diamond-shaped region.
% --------------------
% «thinness» (to ".thinness")
% (sec "Thinness" "thinness")
\mysection {Thinness} {thinness}
% (find-cwmpage (+ -4 14) "full functor")
If $\bbC = (A, R)$ and $\bbD = (B, S)$ are directed graphs, we say
that a function $f:A \to B$ is an {\sl inclusion} of $\bbC$ in $\bbD$
if for all points $\aa, \bb \in A$ we have $\aa R^* \bb$ iff $f(\aa)
S^* f(\bb)$; for example, $f = (\dagVee154 \to \dagWdot123456)$ is not
an inclusion because $4 \to 5 \in R$ but $4 \in 5 \notin S$. An
equivalent, but less elementary, characterization of inclusions is the
following: $f: A \to B$ is an inclusion iff $f^{-1}(\Opens(\bbD)) =
\Opens(\bbC)$. Note that being an inclusion is a stricter condition
than being continuous.
We say the $\bbC$ is {\sl contained in} $\bbD$ (notation: $\bbC \le
\bbD$) when there is some inclusion $f:\bbC \to \bbD$.
\msk
It is easy the characterize those ZDAGs $\bbD$ such that $\bbD',
\bbD'', \ldots$ can all be represented as ZDAGs.
\msk
{\sl Definition.} A directed graph $\bbD$ is {\sl thin} when
$\dagVV**** \not\le \bbD$ and $\dagHthree*** \not\le \bbD$.
{\sl Theorem.} If $\bbD$ is not thin then $\bbD''$ cannot be
represented as a ZDAG. The proof follows immediately from the
following five easy lemmas.
{\sl Lemma.} $\bbD \le \bbD'$. This generalizes the figure in section
\ref{priming}.
{\sl Lemma.} If $\bbC \le \bbD$ then $\bbC' \le \bbD'$.
{\sl Lemma.} If $(\dagHthree***)' \le \bbD$ then $\bbD$ cannot be
represented as a ZDAG.
{\sl Lemma.} $\dagHthree*** \le \bbD$ implies $(\dagHthree***)' \le
\bbD'$, which implies that $\bbD'$ cannot be a ZDAG.
{\sl Lemma.} $\dagVV**** \le \bbD$ implies $\dagHthree*** \le
\bbD'$, which implies that $\bbD''$ cannot be a ZDAG.
The following diagram explains some of the lemmas above. The
horizontal `$\monicto$' arrows are primings.
%
%D diagram thinness-diagram
%D 2Dx 100 +55 +50
%D 2D 100 Three >-> Cube
%D 2D
%D 2D +10 Three'
%D 2D |
%D 2D v
%D 2D +40 VV >-> Lozenge
%D 2D
%D (( Three .tex= \left(\bigHthree124\right)
%D Three' .tex= \left(\bigHthree456\right)
%D Cube .tex= \left(\bigCube7"356"124"0\right)
%D Lozenge .tex= \left(\bigLozengeThree1"23"456"78"9\right)
%D VV .tex= \left(\bigVV4678\right)
%D Three Cube >->
%D Three' Lozenge >->
%D VV Lozenge >->
%D ))
%D enddiagram
%D
$$\diag{thinness-diagram}$$
\msk
We also have a kind of a converse for the theorem above.
{\sl Lemma.} If a ZDAG $\bbD$ has three or more connected components
then $\dagHthree*** \le \bbD$, and so $\bbD$ it is not thin.
{\sl Lemma.} If a ZDAG $\bbD$ has two connected components and each of
them has more than one vertex, then $\bbD$ is not thin.
{\sl Lemma.} A thin ZDAG with exactly two connected components is
isomorphic to a isolated point plus a tower with $n$ points.
{\sl Lemma.} If the ZDAG $\bbD$ is (isomorphic to) an isolated point
plus a tower of $n$ points then $\bbD'$ is a tilted $2×(n+1)$
rectangle. For example: $(\dagTwoOne***)' = \dagTwoOnePrime******$.
{\sl Lemma.} If $\bbD$ is a thin ZDAG with a single connected
component then $\bbD'$ is also a thin ZDAG with a single connected
component.
{\sl Theorem.} If $\bbD$ is a thin ZDAG then $\bbD'$ is also a thin
ZDAG.
\msk
We can combine both theorems: let $\bbD$ be a ZDAG; then $\bbD',
\bbD'', \ldots$ are all ZDAGs iff $\bbD$ is thin --- and if $\bbD$ is
a thin ZDAG then $\bbD', \bbD'', \ldots$ are all thin ZDAGs, with a
single connected component each.
\msk
We saw how thin ZDAGs are {\sl nice}. Now we will see that they are
{\sl useful}.
% http://en.wikipedia.org/wiki/Local_homeomorphism
% Two of the main figures of the proof (both are primings):
%
% $$
% \bhbox{$\bigHthree124$}
% \to
% \bhbox{$\bigCube 7 356 124 0$}
% $$
%
% $$
% \bhbox{$\bigVV4678$}
% \to
% \bhbox{$\bigLozengeThree 1 23 456 78 9$}
% $$
% --------------------
% «presheaves» (to ".presheaves")
% (sec "Presheaves" "presheaves")
\mysection {Presheaves} {presheaves}
% Classifier object
\def\Cinfty{\calC^\infty}
\def\Cinftyp{\calC^{\infty\prime}}
A {\sl proto-presheaf} $F$ on a directed graph $\D=(A,R)$ is a pair
$(F_0,F_1)$, where $F_0$ is the ``action on objects'' of $F$, which
receives points of $A$ and returns sets, and $F_1$ is the ``action on
morphisms'' of $F$, that takes each arrow $\aa \to \bb$ of $A$ to a
map from $F(\aa)$ to $F(\bb)$. For example, a proto-presheaf on
$\dagKite*****$ can be drawn as:
%
$$\bigKite12345 \qquad \bigKite {F(1)} {F(2)} {F(3)} {F(4)} {F(5)}$$
A {\sl presheaf} $F$ on a directed graph $\D=(A,R^*)$ --- note that
now we are using $R^*$, not $R$ --- is a proto-presheaf $F$ on $\D$
plus the assurance that $F$ is functorial, i.e., that for reflexive
arrows $\aa\to\aa$ the associated function $F(\aa\to\aa):F(\aa) \to
F(\aa)$ is the identity, and that for composable arrows $\aa\to\bb$
and $\bb\to\cc$ we have $F_1(\aa\to\bb);F_1(\bb\to\cc) =
F_1(\aa\to\bb;\bb\to\cc)$.
\msk
This is a classical example of a presheaf. Let $\bbD$ be
$(\Opens(\R),\supseteq)$ --- a huge poset --- and set $\Cinfty_0(U)$
to the set $\sst{f:U \to R}{\text{$f$ is $\Cinfty$}}$ and $\Cinfty_1$
to the operation that restricts the domain of those functions; for
each reverse inclusion $U \supseteq V$ in $\bbD$, $\Cinfty_1$ applied
to the arrow $U \to V$ yields the restriction function
%
$$\begin{array}{rrcl}
\Cinfty_1(U \to V): & \Cinfty_0(U) & \to & \Cinfty_0(V) \\
& f_U & \mto & f_U|_V \\
& (f_U: U \to \R) & \mto & (f_U|_V: V \to \R) \\
\end{array}
$$
Now define a presheaf $\Cinftyp$ on $\dagKite*****$ by composing
$\Cinfty$ with the quotient $q$ of section \ref{quotient}:
%
$$\def\ph{\phantom{mmmm}}
\bigKite {\Cinfty((-‚,‚))}
{\Cinfty((-‚,1))\ph}
{\ph\Cinfty((0,‚))}
{\Cinfty((0,1))}
{\Cinfty(\emp)}
\qquad
\qquad
\qquad
\qquad
\def\ph{\phantom{mm}}
\bigKite {\Cinftyp(X)}
{\Cinftyp(U)\ph}
{\ph\Cinftyp(V)}
{\Cinftyp(W)}
{\Cinftyp(\emp)}
% \two/->`<-/^q_{q^{-1}}
% \qquad
% \bigKite {\{\aa,\bb,\cc\}} {\{\aa,\cc\}} {\{\bb,\cc\}} {\{\cc\}} {\emp}
$$
\bsk
And this will be our other favorite example; we will call it the {\sl
evil presheaf}, and we will see soon that it fails the two
conditions that a presheaf must obey to be a sheaf.
%
% (find-dn4 "experimental.lua" "relphantom")
%L forths[".xtag="] = function ()
%L local dx, tag = getwordasluaexpr(), getword()
%L tex = "\\ph{"..tag.."}"
%L ds[1] = storenode{x=ds[1].x+dx, y=ds[1].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 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
$$
% (find-LATEXgrep "grep -nH -e color *.tex")
\def\ph#1{{\color{red}#1}}
\def\ph#1{\phantom{#1}}
\diag{evil-presheaf}
$$
Let's set, temporarily, $U:=(-‚,1)$ and $V:=(0,‚)$. If we start with
any two functions $f_U Ý \Cinfty(U)$ and $f_V Ý \Cinfty(V)$ that are
``compatible'', in the sense that $f_U|_{UÌV} = f_V|_{UÌV}$, then
there exists exactly one ``glueing'' for them, i.e., a function
$f_{UþV} Ý \Cinfty(UþV)$ such that $f_U = f_{UþV}|_U$ and $f_V =
f_{UþV}|_V$. The same happens in $\Cinftyp$, but now $U=\{\aa,\cc\}$
and $V=\{\bb,\cc\}$, and so the notion of ``restriction'' is a bit
more abstract; now to obtain $f_U|_{UÌV}$ from $f_U$ we have to do
$f_U|_{UÌV} := F(U \to W)(f_U)$.
In the evil presheaf $E$ the sets $E(X), \ldots, E(\emp)$ and the
``restriction functions'' $E(X \to U), \ldots, E(W \to \emp)$ were
chosen arbitrarily. They obey functoriality (because $E(X\to U);E(U
\to W) = E(X \to V);E(V \to W)$), but not the idea that ``compatible
functions must have exactly one glueing'': $e_U$ and $e_V$ are
compatible yet they have two different glueings, $e_X$ and $e'_X$;
$e'_U$ and $e'_V$ are compatible but can't be glued.
The best way to formalize the glueing condition in its general form is
by using {\sl prestacks} (as in \cite{Simmons}, sections 3--5).
% --------------------
% «prestacks» (to ".prestacks")
% (sec "Prestacks" "prestacks")
\mysection {Prestacks} {prestacks}
\def÷{\amalg}
Let's write $ÆA$ for the disjoint union of all the ``fibers'' in a
presheaf $A$; example, $ÆE=E(X) ÷ \ldots ÷ E(\emp)$. We can define a
function $\dbr{·}: ÆA \to Ø$, that returns for each $a_U \in A(U)
\subset ÆA$ the corresponding $U$ --- the ``extent'' of $a_U$. We can
also define a binary operation, `$·$', usually non-commutative, that
in reality will be several different operations packed into one, and
that will sometimes behave as {\sl intersection}, sometimes as {\sl
restriction}. We start by defining what happens when the `$·$'
receives two elements from the disjoint union $Ø÷ÆA$. There are four
cases:
$$\begin{array}{rcl}
U·V &:=& UÌV \\
U·b_V &:=& U·\dbr{b_V} \\
&=& UÌV \\
a_U·V &:=& A(\dbr{a_U} \to \dbr{a_U}·V)(a_U) \\
&=& A(U \to UÌV)(a_U) \\
&=& a_U|_{UÌV} \\
a_U·b_V &:=& A(\dbr{a_U} \to \dbr{a_U}·\dbr{b_V})(a_U) \\
&=& A(U \to UÌV)(a_U) \\
&=& a_U|_{UÌV} \\
\end{array}
$$
Note that $a_U · b_V = b_V · a_U$ exactly when $a_U$ and $b_V$ are
compatible, and that the operation `$·$' is associative; also our
discipline of always writing the ``extent'' of a point of $ÆA$ as its
subscript is paying off!
\msk
Now we will extend that operation to let it receive and return
elements from $Ø÷ÆA÷\Pts(Ø)÷\Pts(ÆA)$ --- but to avoid confusion we
will not go beyond single applications of `$\Pts$'. We use the
standard trick: if $x$ and $y$ are elements and $X$ and $Y$ are sets,
then:
%
$$\begin{array}{rcl}
x·Y &:=& \sst{x·y}{yÝY} \\
X·y &:=& \sst{x·y}{xÝX} \\
X·Y &:=& \sst{x·y}{xÝX, yÝY} \\
\end{array}
$$
By doing that we get an operation `$·$' that is in fact 16 different
operations being treated as one. If $a_\calU$ and $b_\calV$ stand for
subsets of $ÆA$, then...
%
$$\def\inW{ÝØ}
\def\inSA{ÝÆA}
\def\inPtsW{Ý\Pts(Ø)}
\def\inPtsSA{Ý\Pts(ÆA)}
\begin{array}{c|cccc}
· & V & b_V & \calV & b_\calV \\ \hline
U & U·V \inW & U·b_V \inW & U·\calV \inPtsW & U·b_\calV \inPtsW \\
a_U & a_U·V \inSA & a_U·b_V \inSA & a_U·\calV \inPtsSA & a_U·b_\calV \inPtsSA \\
\calU & \calU·V \inPtsW & \calU·b_V \inPtsW & \calU·\calV \inPtsW & \calU·b_\calV \inPtsW \\
a_\calU & a_\calU·V \inPtsSA & a_\calU·b_V \inPtsSA & a_\calU·\calV \inPtsSA & a_\calU·b_\calV \inPtsSA \\
\end{array}
$$
(...)
A {\sl compatible family} is a set $a_\calU \subset ÆA$ such that all
its elements commute. If $a_\calU$ is a compatible family then we
can't have $a_V, b_V Ý a_\calU$ with $\dbr{a_V} = \dbr{b_V}$ and $a_V
\neq b_V$; so $\dbr{·}$ is injective on $a_\calU$, and establishes a
bijection between $a_\calU$ and $\calU := \dbr{a_\calU} =
\sst{\dbr{a_V}}{a_VÝa_\calU}$. Let's establish a convention: from now
on, when we write a subset of $ÆA$ as $a_\calU$ that will mean that it
is a compatible family, with $\dbr{a_\calU} = \calU$; subsets of $ÆA$
that are not necessarily compatible families will be written as $A'$,
$B$, etc. Also, we will denote the element of $a_\calU$ over $VÝ\calU$
as $(a_\calU)(V)$, or simply as $a_V$.
\msk
A cover $\calU \subset Ø$ is saturated iff $\calU·Ø = \calU$.
A coherent family $a_\calU$ is saturated iff $a_\calU·Ø = a_\calU$.
If $\calU^\bu$ and $\calV^\bu$ are saturated covers then
$\calU^\bu·\calV^\bu = \calU^\bu Ì \calV^\bu$.
A cover $\calU$ is representable iff there exists a $U$ with $\calU =
U·Ø$.
If $\calU^\bu \supset \calV^\bu$ then $a_{\calU^\bu}·\calV^\bu$ is the
restriction of $a_{\calU^\bu}$ to $\calV^\bu$.
% --------------------
% «HAs» (to ".HAs")
% (sec "Heyting Algebras" "HAs")
\mysection {Heyting Algebras} {HAs}
Every $\Opens(X)$ is a Heyting Algebra.
When $X$ is Alexandroff $\Opens(X)$ is even bi-Heyting.
Every $\bbD'$ is a Heyting Algebra.
Diagram and example:
% (find-LATEX "2010diags.tex" "CCCs")
%D diagram HA-1
%D 2Dx 100 +35 +35 +25 +30 +40 +25
%D 2D 100 P0 T0 E0 E1
%D 2D
%D 2D +30 P1 P2 P3 T1 E2 E3
%D 2D
%D 2D +20 p0 t0 e0 e1
%D 2D
%D 2D +30 p1 p2 p3 t1 e2 e3
%D 2D
%D 2D +20 p4 e4 e5
%D 2D
%D (( P0 .tex= P P1 .tex= Q P2 .tex= Q∧R P3 .tex= R
%D P0 P1 ->
%D P0 P2 ->
%D P0 P3 ->
%D P1 P2 <-
%D P2 P3 ->
%D ))
%D (( T0 .tex= P T1 .tex= § ->
%D ))
%D (( E0 .tex= P∧Q E1 .tex= P
%D E2 .tex= R E3 .tex= Q⊃R
%D E0 E1 <-|
%D E0 E2 ->
%D E1 E3 ->
%D E0 E3 harrownodes nil 20 nil <->
%D E2 E3 |->
%D ))
%D (( p0 .tex= \W000110
%D p1 .tex= \W011111 p2 .tex= \W011111∧\W110110 p3 .tex= \W110110
%D p0 p1 ->
%D p0 p2 ->
%D p0 p3 ->
%D p1 p2 <-
%D p2 p3 ->
%D p4 .tex= \W010110 p2 p4 =
%D ))
%D (( t0 .tex= \W000110 t1 .tex= \W111111 ->
%D ))
%D (( e0 .tex= \W000110∧\W000011 e1 .tex= \W000110
%D e2 .tex= \W010110 e3 .tex= (\W000011⊃_{¯C}\W010110)^\int
%D e0 e1 <-|
%D e0 e2 ->
%D e1 e3 ->
%D e0 e3 harrownodes nil 20 nil <->
%D e2 e3 |->
%D e4 .tex= \W111110^\int e5 .tex= \W110110
%D e3 e4 = e4 e5 =
%D ))
%D enddiagram
%D
$$\def\W{\dagWdot}
\diag{HA-1}
$$
Explain that we are now using the arrows in the standard direction
(inclusion). The $§$ (``top'') is terminal. Suggestion to the reader:
change the values of $P$, $Q$, $R$ above; when one of the vertical
arrows of the adjunction disappears the other also does.
% --------------------
% «MHAs» (to ".MHAs")
% (sec "Modalized Heyting Algebras" "MHAs")
\mysection {Modalized Heyting Algebras} {MHAs}
A.k.a. Lawvere-tierney topologies (\cite{MacLaneMoerdijk}, section
V.1), or local operators (\cite{Elephant1}, section A4.4)
Look at the space of saturated covers as a HA.
Rename it to $Ø$; then $Ø=\{\emp^\bubo, \ldots, \calX^\bubu\}$
(in the archetypal case).
The saturated covers will play the role of truth-values.
Let's loot at the operation $·^*:Ø \to Ø$ (double saturation, with a new name).
Important properties: $P \vdash P^* = P^{**}$, $P \vdash Q$ implies
$P^* \vdash Q^*$, $P^*∧Q^*=(P∧Q)^*$.
From just these properties we can prove all these about how the
modality interacts with $∧$, $∨$, $⊃$:
% (find-books "__cats/__cats.el" "johnstone")
% (find-books "__cats/__cats.el" "moerdijk")
% Other modalities:
% (find-LATEX "2008graphs.tex" "a-presheaf-on-a-dag")
% (find-dvipage "2008graphs.dvi" 17 "a-presheaf-on-a-dag")
%D diagram op-cube2
%D 2Dx 100 +20 +25 +20 +40 +20 +25 +20
%D 2D 100 A000 A020 a000 a020
%D 2D +20 A004 A024 a004 a024
%D 2D
%D 2D +20 A100 A120 a100 a120
%D 2D +20 A104 A124 a104 a124
%D 2D
%D (( A000 .tex= P∧Q
%D A004 .tex= (P∧Q)^*
%D A020 .tex= P∧Q^*
%D A024 .tex= (P∧Q^*)^*
%D A100 .tex= P^*∧Q
%D A104 .tex= (P^*∧Q)^*
%D A120 .tex= P^*∧Q^*
%D A124 .tex= (P^*∧Q^*)^*
%D A000 A004 -> A020 A024 -> A100 A104 -> A120 A124 =
%D A000 A020 -> A004 A024 = A100 A120 -> A104 A124 =
%D A000 A100 -> A004 A104 = A020 A120 -> A024 A124 =
%D ))
%D (( a000 .tex= \dagVee001
%D a004 .tex= \dagVee101
%D a020 .tex= \dagVee011
%D a024 .tex= \dagVee111
%D a100 .tex= \dagVee111
%D a104 .tex= \dagVee111
%D a120 .tex= \dagVee111
%D a124 .tex= \dagVee111
%D a000 a004 -> a020 a024 -> a100 a104 -> a120 a124 =
%D a000 a020 -> a004 a024 = a100 a120 -> a104 a124 =
%D a000 a100 -> a004 a104 = a020 a120 -> a024 a124 =
%D ))
%D enddiagram
%D
$$\diag{op-cube2}$$
% (find-854 "" "LT-intro")
(Insert the diagrams for $∨$ and $⊃$)
(Prove and explain everything)
% --------------------
% «FMHAs» (to ".FMHAs")
% (sec "Finite Modalized Heyting Algebras" "FMHAs")
\mysection {Finite Modalized Heyting Algebras} {FMHAs}
We have a kind of dual to $*$ (minimal saturated cover).
The sets of the form $\sst{Q}{Q^*=P^*}$ are diamond-shaped.
Show the adjunction and examples.
Show how to recover $*$ from the set of $*$-stable truth-values.
The set of $*$-stable truth-values is a HA.
Each $*$ induces a quotient.
A definition of sheaf.
% --------------------
% «FHAs» (to ".FHAs")
% (sec "Finite Heyting Algebras" "FHAs")
\mysection {Finite Heyting Algebras} {FHAs}
% (find-angg "LUA/distributivity.lua")
Def: the evil DAG, $\bbE$ is the one pictured below:
%D diagram evil-dag
%D 2Dx 100 +15 +15
%D 2D 100 \aa
%D 2D +10 \bb
%D 2D +10 \cc
%D 2D +10 \dd
%D 2D +10 \ee
%D 2D
%D # (( \aa \bb -> \bb \dd -> \dd \ee ->
%D # \aa \cc -> \cc \ee ->
%D # ))
%D (( \aa \bb <- \bb \dd <- \dd \ee <-
%D \aa \cc <- \cc \ee <-
%D ))
%D enddiagram
%D
$$\diag{evil-dag}$$
[It is not a HA; explain why. Three reasons: 1) it is not ``graded'',
i.e., the operation that calculates the $y$-coordinate gives
incoherent results for $\aa$; 2) it is not distributive; 3) ...]
{\color{red}Update, 2011mar08:} \cite{Gratzer} has a {\sl lot} about
that! I'm reading it --- and I need to change a lot of the terminology
here.
\msk
(An interesting theorem, quite non-trivial: a ZDAG that is a Heyting
Algebra $\bbD$ is always a $\bbC'$. To locate the points of $\bbD$
that are in the image of $\bbC$ we take each {\sl essential} arrow
$\aa \to \bb$ in $\bbD$ and we check that the ``difference set''
associated to $\aa \to \bb$, $\dnto\aa \bsl \dnto\bb$ has a lower
element...)
% --------------------
% «omega» (to ".omega")
% (sec "Subobject Classifiers" "omega")
\mysection {Subobject Classifiers} {omega}
Let 1 be the singleton set $\{*\}$ in $\Set$, let $ØÝ\Set$ be the set
$\{0,1\}$, and let $§:1 \to Ø$ be the morphism that takes $*$ to
$1Ý\{0,1\}$. Then $§$ has this very nice property: for every monic $A'
\monicto A$ there is exactly one map $\chi_{A'}:A \to Ø$ --- the
characteristic function of the image of $A'$ in $A$ --- that makes
this square a pullback:
%D diagram omega
%D 2Dx 100 +25
%D 2D 100 A' --> 1
%D 2D v v
%D 2D | |
%D 2D v v
%D 2D +25 A ---> Ø
%D 2D
%D (( A' 1 -> .plabel= a !
%D A' A >->
%D 1 Ø >-> .plabel= r §
%D A Ø -> .plabel= b \chi_{A'}
%D A' relplace 7 7 \pbsymbol{7}
%D A relplace 8 -8 \searrow
%D ))
%D enddiagram
%D
$$\diag{omega}$$
We will see how to generalize this a bit, to categories of the form
$\Set^\bbC$, where $\bbC$ is a poset; the main aim of this section is
to show how to ``understand'' (in the sense of \cite{OchsIDCT}) the
following statement:
\begin{quote}
Let $ØÝ\Set^\bbC$ be the functor whose action on objects is $U \mto
\Sub(\Hom_\bbC(U,-))$, and let $§:1 \to Ø$ be the natural
transformation defined by $§(U)(*) = \Hom_\bbC(U,-) Ý
\Sub(\Hom_\bbC(U,-))$. Then for every monic $A' \monicto A$ in
$\Set^\bbC$ there is exactly one morphism $\chi_{A'}:A \to Ø$ making
the square $(*)$ a pullback.
\end{quote}
Our archetypal case will be $\bbC := \bbK = \dagKite*****$, with
arrows going down. The objects of $\bbK$ are named $X$, $U$, $V$, $W$,
$\emp$, and, for example, $\Hom_\bbK(U, W) = \{\rho_{UW}\}$ and
$\Hom_\bbK(U, X) = \{\}$.
\msk
\def\HU#1{\Hom_\bbK(U,#1)}
\def\ru#1{\{\rho_{U#1}\}}
\def\SHK#1{\Sub(\Hom_\bbK(#1,-))}
\def\SHV#1{\Sub(\Hom_\bbV(#1,-))}
The functor $\HU-$ acts on objects as $V \mto \HU{v}$, i.e., it is:
%
$$\def\m{\phantom{n.}}
\bigKite {\HU{X}} {\HU{U}\m\m\m\m} {\m\m\m\m\HU{V}} {\HU{W}} {\HU{\emp}}
\qquad\qquad
=
\qquad
\bigKite {\{\}} {\ru{U}\m} {\{\}} {\ru{W}} {\ru{\emp}}
$$
It acts on morphisms like this: for a morphism $\rho_{VW}: V \to W$,
%
$$\begin{array}{rccl}
\HU{\rho_{VW}}: & \HU{V} & \to & \HU{W} \\
& \rho_{UV} & \mto & \rho_{VW}¢\rho_{UV}. \\
\end{array}
$$
For each $UÝ\bbK$, $\Sub(\HU-)$ is the set of subfunctors of $\HU-$,
i.e., of those $S:\bbK \to \Set$ such that: 1) for each $V \in \bbK$
we have $S(V) \subseteq \HU{V}$, and 2) $S$ is a functor. Note that
%
$$\def\m{\phantom{n.}}
\bigKite {\{\}} {\ru{U}\m} {\{\}} {\{\}} {\ru{\emp}}
$$
%
is not a functor; using the language of section \ref{prestacks}, if
$sÝÆS$ then all the points of $s·Ø$ are forced to belong to $ÆS$ too
--- otherwise $S$ can't be a functor.
We can use the following notation for an element $S$ of $\Sub(\HU-)$:
a `$·$' marks each object of $\bbK$, e.g. $X$, for which $\HU{X} =
\{\}$; in the other positions we use `0's and `1's to denote the
characteristic function of $S \monicto \HU-$. So $\dagKite·0·11$ is
this subfunctor of $\HU-$:
%
$$\def\m{\phantom{n.}}
\bigKite {\{\}} {\{\}} {\{\}} {\ru{W}} {\ru{\emp}}
\quad
\monicto
\qquad
\bigKite {\{\}} {\ru{U}\m} {\{\}} {\ru{W}} {\ru{\emp}}
% \qquad
% \text{is}
% \qquad
$$
{\def\K#1#2#3#4#5{\dagKite#1#2#3#4#5}
Let's write $Ø_\bbK$ for the functor from $\bbK$ to $\Set$ whose
action on objects is $U \mto \SHK{U}$; so $Ø_\bbK(U) =
\Big\{\K·0·00,\K·0·01,\K·0·11,\K·1·11\Big\}$. We can picture $Ø_\bbV$
and $Ø_\bbK$ as:
}
%
%D diagram classiKite
%D 2Dx 100 +25 +25 +30 +20 +20
%D 2D 100 X B0
%D 2D / \ / \
%D 2D v v v v
%D 2D +25 U V
%D 2D \ / \ /
%D 2D v v v v
%D 2D +25 W B3
%D 2D | |
%D 2D v v
%D 2D +25 emp B4
%D 2D
%D (( X .tex= \Big\{\K00000,\K00001,\K00011,\K00111,\K01011,\K01111,\K11111\Big\}
%D U .tex= \Big\{\K·0·00,\K·0·01,\K·0·11,\K·1·11\Big\}
%D V .tex= \Big\{\K··000,\K··001,\K··011,\K··111\Big\}
%D W .tex= \Big\{\K···00,\K···01,\K···11\Big\}
%D emp .tex= \Big\{\K····0,\K····1\Big\}
%D ))
%D (( X U -> X V -> U W -> V W -> W emp ->
%D ))
%D enddiagram
%D
%D diagram classiVee
%D 2Dx 100 +20 +20
%D 2D 100 A B
%D 2D \ /
%D 2D v v
%D 2D +25 C
%D 2D
%D (( A .tex= \{\V0·0,\V0·1,\V1·1\}
%D B .tex= \{\V·00,\V·01,\V·11\}
%D C .tex= \{\V··0,\V··1\}
%D ))
%D (( A C -> B C ->
%D ))
%D enddiagram
%D
$$\def\V#1#2#3{\dagVee#1#2#3}
\diag{classiVee}
\qquad
\def\K#1#2#3#4#5{\dagKite#1#2#3#4#5}
\diag{classiKite}
$$
[The action on objects of $Ø$ is graphically obvious, but how do we
formalize it?]
[Show that these `$Ø$'s obey the axiom]
[Show how to represent $Ø_j$ and $J$ graphically for a modality $j$]
% --------------------
% «etale» (to ".etale")
% (sec "Étale spaces" "etale")
\mysection {Étale spaces} {etale}
% ****************
% Discuss with gf:
% (find-LATEX "2010sheaves.tex")
% (find-dvipage "~/LATEX/2010sheaves.dvi")
\def\colim{\mathop{\mathstrut\rm colim}\limits}
\def\colimxU{\colim_{U \to x}}
\def\colimxU{\colim_{x \ot U}}
\def\UxU{\bigcup\limits_{xÝX}}
\def\UxU{\bigcup\limits_{X \ni x}}
\def\Ucolim{\UxU\!\colimxU}
\def\suto#1{\{s:U \to #1\}}
\def\Top{¦{Top}}
\def\slice#1#2{\begin{pmatrix} #1 \\ \dnto \\ #2 \end{pmatrix}}
On the top square: the adjunction $\LL \dashv \GG$;
On the lower $|·|$: the counit $\ee_Y$ (etalification),
and the unit $\eta_P$ (sheafification).
%D diagram etale-1
%D 2Dx 100 +75
%D 2D 100 LA A
%D 2D
%D 2D +50 B RB
%D 2D
%D 2D +35 LRB A'
%D 2D
%D 2D +50 B' RLA
%D 2D
%D 2D +25 CatB CatA
%D (( LA .tex= \slice{\Ucolim{P(U)}}{X} A .tex= (U^\op\mapsto"P(U))
%D B .tex= \slice{Y}{X} RB .tex= (U^\op\mapsto\suto{Y})
%D LA A <-| .plabel= a \Lambda
%D LA B -> A RB ->
%D B RB |-> .plabel= b \GG
%D @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D (( LRB .tex= \slice{\Ucolim{\suto{Y}}}{X}
%D B' .tex= \slice{Y}{X}
%D @ 0 @ 1 -> .plabel= l \ee_Y
%D ))
%D (( A' .tex= (U^\op\mapsto"P(U))
%D RLA .tex= (U^\op\mapsto\suto{\Ucolim{P(U)}})
%D @ 0 @ 1 -> .plabel= r \eta_P
%D ))
%D (( CatB .tex= \Top/X
%D CatA .tex= \Set^{\Opens(X)^\op}
%D @ 0 @ 1 <- sl^ .plabel= a \Lambda
%D @ 0 @ 1 -> sl_ .plabel= b \GG
%D ))
%D enddiagram
%D
$$\diag{etale-1}$$
% (find-books "__cats/__cats.el" "moerdijk")
% (find-maclanemoerdijkpage (+ -39 89) "II.6 Sheaves as Étale Spaces")
If $X = \bbV = \dagVee***$ then this gives an adjunction
between $\Top/\bbV$ and $\Set^{\Opens(\bbV)^\op} = \Set^\bbK$.
I know how the sheafification $\eta$ acts on the evil presheaf,
but not yet how $\LL$, $\GG$, $\ee$ work.
\msk
\def\upto{\uparrow}
\def\udto{\uparrow\downarrow}
$\dnto\aa = \dagVee101 = U$
$\dnto\bb = \dagVee011 = V$
$\dnto\cc = \dagVee001 = W$
$\udto\aa = \upto U = \dagKite11000 = \{X,U\}$
$\udto\bb = \upto V = \dagKite10100 = \{X,V\}$
$\udto\cc = \upto W = \dagKite11110 = \{X,U,V,W\}$
$\colim_{\aa\ot U'} P(U') = \colim_{(\udto\aa)\ni U'} P(U') = \colim_{(\upto U)\ni U'} P(U') = P(U)$
$\colim_{\bb\ot U'} P(U') = \colim_{(\udto\bb)\ni U'} P(U') = \colim_{(\upto V)\ni U'} P(U') = P(V)$
$\colim_{\cc\ot U'} P(U') = \colim_{(\udto\cc)\ni U'} P(U') = \colim_{(\upto W)\ni U'} P(U') = P(W)$
\msk
Note that if $x \in \R$ then $\udto x$ is the filter of neighbourhoods
of $x$, which is not a principal filter; the operation `$\udto$'
cannot be factored as $\upto(\dnto x)$.
% --------------------
% «geometric-morphs» (to ".geometric-morphs")
% (sec "Geometric Morphisms" "geometric-morphs")
\mysection {Geometric Morphisms} {geometric-morphs}
Every continuous map of
Every continuous map of finite dags induces...
The ``anti-discretization'' map, $a:\dagWdotT****** \to
\dagWdot******$, is continuous, and it induces a map
$\und:\Opens(\dagWdot******) \to \Opens(\dagWdotT******) =
\Pts(\dagWdotT******)$
% (find-LATEXfile "2010diags.tex" "diagram 3-pi")
% (find-dn4 "experimental.lua" "thereplusxy")
% «geometric-discr» (to ".geometric-discr")
%D diagram adjs-to-discr
%D 2Dx 100 +20 +40 +20 +35 +25 +35 +30
%D 2D 100 A0. A0 A1 A1. B0. B0 B1 B1.
%D 2D
%D 2D +20 A2. A2 A3 A3. B2. B2 B3 B3.
%D 2D
%D 2D +20 A4. A4 A5 A5. B4. B4 B5 B5.
%D 2D
%D 2D +20 A6 A7 B6 B7
%D 2D
%D 2D +15 A8 B8
%D 2D
%D 2D +15 A6. A7. B6. B7.
%D 2D
%D (( A0. y+= -6 A2. y+= -6 there+xy: 0 10 A2.. A4. y+= 6
%D B0. y+= -6 B2. y+= -6 there+xy: 0 10 B2.. B4. y+= 6
%D ))
%D (( A0 .tex= \WW100000 A1 .tex= \W100100
%D A2 .tex= \WW100110 A3 .tex= \W100110
%D A4 .tex= \WW111110 A5 .tex= \W110110
%D A6 .tex= \Opens\WW****** A7 .tex= \Opens\W******
%D A8 .tex= \Pts\W******
%D A6. .tex= \WW****** A7. .tex= \W****** -> .plabel= a \antidiscr
%D ))
%D (( A0. .tex= \WW100000 A2. .tex= \WW100100 ->
%D A2.. .tex= \WW110110 A4. .tex= \WW111110 ->
%D A1. .tex= \W100110 A3. .tex= \W100110 ->
%D A3. A5. .tex= \W100110 ->
%D ))
%D (( B0 .tex= A B1 .tex= A^\coint
%D B2 .tex= B^\discr B3 .tex= B
%D B4 .tex= C B5 .tex= C^\coint
%D B6 .tex= \Opens(\bbD^\discr) B7 .tex= \Opens(\bbD)
%D B8 .tex= \Pts(\bbD_0)
%D B6. .tex= \bbD^\discr B7. .tex= \bbD -> .plabel= a \antidiscr
%D ))
%D (( B0. .tex= A
%D B2. .tex= (A^\coint)^\discr
%D B2.. .tex= (C^\int)^\discr
%D B4. .tex= C
%D B0. B2. ->
%D B2.. B4. ->
%D B1. .tex= (B^\discr)^\coint
%D B3. .tex= B
%D B5. .tex= (B^\discr)^\int
%D B1. B3. -> .plabel= r (\cong)
%D B3. B5. -> .plabel= r (\cong)
%D ))
%D (( A0 A1 A2 A3 A4 A5 A6 A7 A8
%D @ 0 @ 1 |-> .plabel= a \coint
%D @ 0 @ 2 -> @ 1 @ 3 -> @ 0 @ 3 harrownodes nil 20 nil <->
%D @ 2 @ 3 <-| .plabel= a \discr
%D @ 2 @ 4 -> @ 3 @ 5 -> @ 2 @ 5 harrownodes nil 20 nil <->
%D @ 4 @ 5 |-> .plabel= a \int
%D @ 6 @ 7 ->> sl^^
%D @ 6 @ 7 <-<
%D @ 6 @ 7 ->> sl__
%D @ 6 @ 8 =
%D ))
%D (( B0 B1 B2 B3 B4 B5 B6 B7 B8
%D @ 0 @ 1 |-> # .plabel= a \coint
%D @ 0 @ 2 -> @ 1 @ 3 -> @ 0 @ 3 harrownodes nil 20 nil <->
%D @ 2 @ 3 <-| # .plabel= a \und
%D @ 2 @ 4 -> @ 3 @ 5 -> @ 2 @ 5 harrownodes nil 20 nil <->
%D @ 4 @ 5 |-> # .plabel= a \int
%D @ 6 @ 7 ->> sl^^
%D @ 6 @ 7 <-<
%D @ 6 @ 7 ->> sl__
%D @ 6 @ 8 =
%D ))
%D enddiagram
%D
%$$\def\W #1#2#3#4#5#6{(\dagWdot {#1}{#2}{#3}{#4}{#5}{#6})}
% \def\WW#1#2#3#4#5#6{(\dagWdotT{#1}{#2}{#3}{#4}{#5}{#6})}
% \diag{adjs-to-discr}
%$$
% «geometric-epi» (to ".geometric-epi")
%D diagram adjs-to-epi
%D 2Dx 100 +25 +40 +25 +35 +25 +35 +25
%D 2D 100 A0. A0 A1 A1. B0. B0 B1 B1.
%D 2D
%D 2D +20 A2. A2 A3 A3. B2. B2 B3 B3.
%D 2D
%D 2D +20 A4. A4 A5 A5. B4. B4 B5 B5.
%D 2D
%D 2D +20 A6 A7 B6 B7
%D 2D
%D 2D +15 A6. A7. B6. B7.
%D 2D
%D (( A0. y+= -5 A2. y+= -5 there+xy: 0 10 A2.. A4. y+= 5
%D B0. y+= -5 B2. y+= -5 there+xy: 0 10 B2.. B4. y+= 5
%D ))
%D (( A0 .tex= \Rft00001000 A1 .tex= \Rfo1000
%D A2 .tex= \Rft11001100 A3 .tex= \Rfo1100
%D A4 .tex= \Rft11101111 A5 .tex= \Rfo1110
%D A6 .tex= \Opens\Rft******** A7 .tex= \Opens\Rfo****
%D # A8 .tex= \Pts\W******
%D A6. .tex= \Rft******** A7. .tex= \Rfo**** ->>
%D ))
%D (( A0. .tex= \Rft00001000 A2. .tex= \Rft10001000 ->
%D A2.. .tex= \Rft10001000 A4. .tex= \Rft11111110 ->
%D A1. .tex= \Rfo1100 A3. .tex= \Rfo1100 -> .plabel= r \cong
%D A3. A5. .tex= \Rfo1100 -> .plabel= r \cong
%D ))
%D (( B0 .tex= A B1 .tex= f^ÎA
%D B2 .tex= f^{-1}B B3 .tex= B
%D B4 .tex= C B5 .tex= f^ýC
%D B6 .tex= \Opens(\bbD) B7 .tex= \Opens(\bbE)
%D B6. .tex= \bbD B7. .tex= \bbE ->> .plabel= a f
%D ))
%D (( B0. .tex= A
%D B2. .tex= f^{-1}f^ÎA
%D B2.. .tex= f^{-1}f^ýC
%D B4. .tex= C
%D B0. B2. ->
%D B2.. B4. ->
%D B1. .tex= f^Îf^{-1}B
%D B3. .tex= B
%D B5. .tex= f^ýf^{-1}B
%D B1. B3. -> .plabel= r \cong B3. B5. -> .plabel= r \cong
%D ))
%D (( A0 A1 A2 A3 A4 A5 A6 A7 # A8
%D @ 0 @ 1 |-> .plabel= a f^Î
%D @ 0 @ 2 -> @ 1 @ 3 -> @ 0 @ 3 harrownodes nil 20 nil <->
%D @ 2 @ 3 <-| .plabel= a f^{-1}
%D @ 2 @ 4 -> @ 3 @ 5 -> @ 2 @ 5 harrownodes nil 20 nil <->
%D @ 4 @ 5 |-> .plabel= a f^ý
%D @ 6 @ 7 ->> sl^^
%D @ 6 @ 7 <-<
%D @ 6 @ 7 ->> sl__
%D ))
%D (( B0 B1 B2 B3 B4 B5 B6 B7 # B8
%D @ 0 @ 1 |->
%D @ 0 @ 2 -> @ 1 @ 3 -> @ 0 @ 3 harrownodes nil 20 nil <->
%D @ 2 @ 3 <-|
%D @ 2 @ 4 -> @ 3 @ 5 -> @ 2 @ 5 harrownodes nil 20 nil <->
%D @ 4 @ 5 |->
%D @ 6 @ 7 ->> sl^^
%D @ 6 @ 7 <-<
%D @ 6 @ 7 ->> sl__
%D ))
%D enddiagram
%D
%$$\def\Rft#1#2#3#4#5#6#7#8{(\dagRft{#1}{#2}{#3}{#4}{#5}{#6}{#7}{#8})}
% \def\Rfo#1#2#3#4{(\dagRfo{#1}{#2}{#3}{#4})}
% \diag{adjs-to-epi}
%$$
% «geometric-monic» (to ".geometric-monic")
%D diagram adjs-to-monic
%D 2Dx 100 +25 +40 +25 +35 +25 +35 +25
%D 2D 100 A0. A0 A1 A1. B0. B0 B1 B1.
%D 2D
%D 2D +20 A2. A2 A3 A3. B2. B2 B3 B3.
%D 2D
%D 2D +20 A4. A4 A5 A5. B4. B4 B5 B5.
%D 2D
%D 2D +20 A6 A7 B6 B7
%D 2D
%D 2D +15 A6. A7. B6. B7.
%D 2D
%D (( A0. y+= -7 A2. y+= -7 there+xy: 0 14 A2.. A4. y+= 7
%D B0. y+= -7 B2. y+= -7 there+xy: 0 14 B2.. B4. y+= 7
%D ))
%D (( A0 .tex= \D00001 A1 .tex= \DW00000001
%D A2 .tex= \D00011 A3 .tex= \DW00001011
%D A4 .tex= \D00111 A5 .tex= \DW01011111
%D A6 .tex= \Opens\D***** A7 .tex= \Opens\DW********
%D A6. .tex= \D***** A7. .tex= \DW******** >->
%D ))
%D (( A0. .tex= \D00001 A2. .tex= \D00001 -> .plabel= l \cong
%D A2.. .tex= \D00111 A4. .tex= \D00111 -> .plabel= l \cong
%D A1. .tex= \DW00000011 A3. .tex= \DW00001011 ->
%D A3. A5. .tex= \DW00001111 ->
%D ))
%D (( B0 .tex= A B1 .tex= f^{Ð{min}}A
%D B2 .tex= f^{-1}B B3 .tex= B
%D B4 .tex= C B5 .tex= f^{Ð{max}}C
%D B6 .tex= \Opens(\bbD) B7 .tex= \Opens(\bbE)
%D B6. .tex= \bbD B7. .tex= \bbE >-> .plabel= a f
%D ))
%D (( B0. .tex= A
%D B2. .tex= f^{-1}f^{Ð{min}}A
%D B2.. .tex= f^{-1}f^{Ð{max}}C
%D B4. .tex= C
%D B0. B2. -> .plabel= l \cong
%D B2.. B4. -> .plabel= l \cong
%D B1. .tex= f^{Ð{min}}f^{-1}B
%D B3. .tex= B
%D B5. .tex= f^{Ð{max}}f^{-1}B
%D B1. B3. -> B3. B5. ->
%D ))
%D (( A0 A1 A2 A3 A4 A5 A6 A7 # A8
%D @ 0 @ 1 |-> .plabel= a f^{Ð{min}}
%D @ 0 @ 2 -> @ 1 @ 3 -> @ 0 @ 3 harrownodes nil 20 nil <->
%D @ 2 @ 3 <-| .plabel= a f^{-1}
%D @ 2 @ 4 -> @ 3 @ 5 -> @ 2 @ 5 harrownodes nil 20 nil <->
%D @ 4 @ 5 |-> .plabel= a f^{Ð{max}}
%D @ 6 @ 7 >-> sl^^
%D @ 6 @ 7 <<-
%D @ 6 @ 7 >-> sl__
%D ))
%D (( B0 B1 B2 B3 B4 B5 B6 B7 # B8
%D @ 0 @ 1 |->
%D @ 0 @ 2 -> @ 1 @ 3 -> @ 0 @ 3 harrownodes nil 20 nil <->
%D @ 2 @ 3 <-|
%D @ 2 @ 4 -> @ 3 @ 5 -> @ 2 @ 5 harrownodes nil 20 nil <->
%D @ 4 @ 5 |->
%D @ 6 @ 7 >-> sl^^
%D @ 6 @ 7 <<-
%D @ 6 @ 7 >-> sl__
%D ))
%D enddiagram
%D
%$$\def\DW#1#2#3#4#5#6#7#8{(\smashDeeWide{#1}{#2}{#3}{#4}{#5}{#6}{#7}{#8})}
% \def\D#1#2#3#4#5{(\smashDee{#1}{#2}{#3}{#4}{#5})}
% \diag{adjs-to-monic}
%$$
% --------------------
% «right-example» (to ".right-example")
% (sec "The ``right example''" "right-example")
\mysection {The ``right example''} {right-example}
{\sl Is there still something that I want to save from this section?}
% This is a paragraph from \cite{Byers} (p.204):
%
% \begin{quote}
% For a subject that revels in the abstract, mathematical ideas are
% often very concrete. Think of the discussion of ``variables'' in
% Chapter 1. The domain of a variable may include an infinite range of
% values, but when a variable is used we think of it as having a
% definite and particular value. This enables us to think concretely.
% This mental technique is used very generally in mathematics. We want
% to understand some mathematical phenomenon that arises in a wide
% variety of circumstances. How is one to think about such a general
% phenomenon? Often one thinks in depth about some particular but
% generic example --- some computation or picture. Of course the genius
% is in picking the right example or examples. One looks for some
% specific example that captures all the subtleties of the general
% situation. Thus ``what is going on'' is often revealed within the
% specificity of a particular example. The task of extending and
% abstracting that understanding is often secondary. The role of
% specific counterexamples in establishing the boundaries of some
% mathematical theory is balanced by the role of specific generic
% examples for which one can say that they illustrate the ``general
% case.''
% \end{quote}
[Byers's] idea of ``right example'' is very close to the idea of
``archetypal model'' in \cite{OchsIDCT}, but an underlying theme in
\cite{OchsIDCT} is that internal diagrams, downcasing types and
archetypal models can be used to {\sl formalize} the idea of ``right
example'', in two senses: 1) it should be possible to work using a
notation that suggests that we are in the archetypal case, and then,
by a ``dictionary trick'', lift our proofs to the general case; 2) ...
Even though sheaves on ZDAGs are much simpler than general sheaves (I
will show, in one of the yet-unwritten sections, how the colimits that
are used to define spaces of germs can be calculated explicitly on
presheaves on ZDAGs), most of ``basic sheaf theory'' can be defined on
sheaves and ZDAGs and then lifted to the general case... However, I
still need to {\sl define} what is ``basic sheaf theory'' --- which
definitions and proofs are conatined in it... This is a work in
progress!
(Many ideas here came from \cite{Simmons})
% % --------------------
% % «old-intro» (to ".old-intro")
% % (sec "Old intro" "old-intro")
% \mysection {Old intro} {old-intro}
%
% This paper is a sequel to \cite{OchsIDCT}, where we introduced a
% (tentative) definition for what is an archetypal model, $A$, for a
% structure $S$. Roughly, $A$ is an archetypal model for $S$ when: 1)
% $A$ is a particular case for $S$; 2) the notation (the ``language'')
% that we use for $A$ is ``intuitive'', in the sense that it lets us
% formulate good conjectures about $A$ and check them quickly; 3) the
% definitions, constructions, and statements of $S$ can be
% ``reconstructed'', by a lifting process like the ones in [1], from the
% particular case $A$ and relatively few extra hints.
%
% The paper \cite{OchsIDCT} --- that we will refer to as IDCT from here
% on --- discussed mathematical intuition, reasoning processes, and how
% we forget the details of parts of a structure that are not central,
% and later reconstruct them from the ``core''. In order to do so, it
% used a narrative trick: it was written in the first person, from the
% point of view of a (semi-fictional) ``I'', who thinks mostly
% diagrammatically and has a very bad memory. We will do the same here.
%
%
% % --------------------
% % «old-abstract» (to ".old-abstract")
% % (sec "Old abstract" "old-abstract")
% \mysection {Old abstract} {old-abstract}
%
% % {\bf On sheaves over finite DAGs}
%
% Let $D_0$ be a subset of $\Z^2$, and $D_1$ be the set of ``black
% pawn's moves'' on it. Then $\D=(D_0, D_1^*)$, where $D_1^*$ is the
% reflexive-transitive closure of $D_1$, is a poset, and $D_1$ is the
% minimal set of arrows generating it. By putting the Alexandroff
% topology on $\D$ we can form another poset, $\D'=(\Opens(\D),
% \subseteq)^\op$, and if $D_0$ obeys some simple conditions (is finite
% and ``thin enough'') then $\D', \D'', \ldots$ are all ``$\Z^2$-DAGs''.
%
% The two two-dimensional structure of a $D_0$ allows a very compact
% positional notation for functions from $D_0$ to $\N$ --- in
% particular, for characteristic functions for open subsets, i.e., for
% the points in $\D'$. That positional notation makes it easy to
% describe explicitly {\sl particular} open sets, covers, Grothendieck
% and Lawvere-Tierney topologies, presheaves, sheaves, classifier
% objects, truth-values, geometric morphisms, etc.
%
% In \cite{OchsIDCT} there is a (somewhat tentative) definition for what
% is an {archetypal model} $A$ for a structure $S$. Here we take $S$ as
% being the (type-theoretical) structure for basic sheaf theory; we have
% diagrams for its definitions, constructions, and statements.
% Apparently, when we specialize a structure $S$ to a particular case,
% $A$, we only lose information; but sometimes the diagrams for the case
% $A$ are ``intuitive enough'' (in a precise sense), and from them and a
% few ``hints'' we can reconstruct the general case, $S$. When this
% happens we say that $A$ is an {archetypal model} for $S$.
%
% The categories of the form $\Set^{\D}$ seem to be archetypal for basic
% sheaf theory in the following sense. Take $\V$ as the three-point,
% V-shaped DAG, and build the toposes $\Set^{\V}$, $\Set^{\V'}$,
% $\Set^{\V''}$, and $\Sh(\V)$. Essentially all the definitions,
% statements and constructions of basic topos and sheaf theory have very
% nice, concrete diagrams on those toposes, and using the ``dictionary
% tricks'' of \cite{OchsIDCT} we can lift these diagrammatical
% constructions from the particular to the general case. The archetypal
% diagrams for the logical view of sheaves in \cite{BellLST} require
% only slightly bigger $\Z^2$-DAGs.
%
% ({\sl This is a work in progress.} Sheafification works well on the
% presheaf side of the adjunction, but the diagrams for étale maps may
% be problematic.)
%
% \msk
% (find-LATEX "2009-planodetrabalho.tex" "bibliography")
% (find-angg ".zshrc" "makebbl")
\bibliography{catsem,filters}
\bibliographystyle{alpha}
\end{document}
% (find-LATEX "2010diags.tex" "archetypal")
%*
\end{document}
% http://www.cle.unicamp.br/ebl2011/
% http://www.cle.unicamp.br/ebl2011/call_papers.php
% http://www.cle.unicamp.br/ebl2011/submissions.php
diagrammatical representations in those particular cases,
% (find-books "__phil/__phil.el" "byers")
CT is diagrammatic, constructive, powerful, and CT theorems are
usually published in a very abstract way that hides the intuition; the
right examples are mentioned in passing.
In IDCT I showed how to connect ``intuitive thought'' and ``algebraic
thought'' in CT. ``Intuitive'' is related to the right examples
(archetypal); algebraic is axiomatic, but especially connected to how
things are published, how to read the literature, and how to prove
using type theory
Use the language of the archetypal case to formalize the diagrams, to
build a bridge between the right example and the axiomatic; the acid
test would be a formalization in type theory.
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: