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: