% -*- coding: raw-text-unix -*-
% (find-angg "LATEX/2008sheaves.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008sheaves.tex && latex    2008sheaves.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008sheaves.tex && pdflatex 2008sheaves.tex"))
% (eev "cd ~/LATEX/ && Scp 2008sheaves.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (find-dvipage "~/LATEX/2008sheaves.dvi")
% (find-pspage  "~/LATEX/2008sheaves.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2008sheaves.ps 2008sheaves.dvi")
% (find-pspage  "~/LATEX/2008sheaves.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage  "~/LATEX/tmp.ps")

% (find-pen-links)
% (find-sh0 "cd ~/LATEX/; sudo cp -v 2008sheaves.{tex,dvi,pdf} /tmp/pen/")
% http://angg.twu.net/LATEX/2008sheaves.pdf

\documentclass[oneside]{book}
\usepackage[latin1]{inputenc}
\usepackage{edrx08}       % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty"  -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex   % (find-dn4ex "edrxheadfoot.tex")
\begin{document}

\input 2008sheaves.dnt

% «.dags»			(to "dags")
% «.dags-as-topspaces»		(to "dags-as-topspaces")
% «.compact-diagrams»		(to "compact-diagrams")
% «.motivation-for-logicians»	(to "motivation-for-logicians")
% «.topologies-on-dags»		(to "topologies-on-dags")
% «.a-presheaf-on-a-dag»	(to "a-presheaf-on-a-dag")
% «.presheaf-on-a-dag-germs»	(to "presheaf-on-a-dag-germs")
% «.archetypical-sheaf»		(to "archetypical-sheaf")
% «.saturated-coherent-fams»	(to "saturated-coherent-fams")
% «.logic-on-tss-sc-1»		(to "logic-on-tss-sc-1")
% «.logic-on-tss-sc-2»		(to "logic-on-tss-sc-2")
% «.logic-on-tss-s-and-c»	(to "logic-on-tss-s-and-c")
% «.modalities»			(to "modalities")
% «.modalities-more-theorems»	(to "modalities-more-theorems")
% «.modalities-alt-axioms»	(to "modalities-alt-axioms")
% «.double-neg-by-hand-1»	(to "double-neg-by-hand-1")
% «.double-neg-by-hand-2»	(to "double-neg-by-hand-2")
% «.downcasing-closure-op»	(to "downcasing-closure-op")
% «.sat-cov-fibration»		(to "sat-cov-fibration")
% «.saturated-covers»		(to "saturated-covers")
% «.adjunctions»		(to "adjunctions")
% «.saturation-in-prestacks»	(to "saturation-in-prestacks")
% «.algebra-of-covers-lemma»	(to "algebra-of-covers-lemma")
% «.algebra-of-covers-bottom»	(to "algebra-of-covers-bottom")
% «.geometric-morphisms»	(to "geometric-morphisms")
% «.geometric-morphisms-2»	(to "geometric-morphisms-2")
% «.johnstone-filter-powers»	(to "johnstone-filter-powers")
% «.note-on-filter-powers»	(to "note-on-filter-powers")

% I have always found the definition of ``sheaf'' incredibly hard to
% understand, and it was only a few months ago that I discovered why:
% it involves many different kinds of objects --- open sets, sets of
% opens sets, sets of sets of open sets, ``saturated'' sets of open
% sets, etc... however, if we allow certain names of variables to
% include ``annotations'' indicating where the values of those
% variables live, then the definitions become much simpler, and some
% adjunctions between the set of open sets (the topology) and the set
% of sets of open sets (the set of covers and precovers) appear ---
% and they turn out to be fibrations.

% In the first part of these notes we will see how each directed graph
% has a natural topology, and how the open sets of a topological space
% can play the role of the truth-values of an intuitionistic logic;
% our ``archetypical'' topological space for understanding sheaves
% will be the directed graph with only three vertices, seen as a
% topological space.

% The operation that takes the union of the open sets in a cover can
% be seen as a logical operation: a ``modality''. Other modalities are
% the double negation, ``$\aa$-implies'', and ``$\aa$-or'', and
% modalities can be composed in several ways, and they can be used for
% Forcing.

% The real objective of these notes is to show techniques for studying
% filter-powers, and for showing how proofs done in the
% ``calculational fragment'' of Non-Standard Analysis can be
% translated to proofs done in a filter-power, getting rid of the
% ultrafilters needed for of NSA; and then these proofs can be
% translated quite easily to standard proofs in terms of continuity.

% Be warned, though: these notes are a work in progress --- very few
% of the slides are complete, some are obsolete, and some contain
% errors...


%
% (eedn4-51-bounded)
% \catcode`Î=13 \defÎ{\exists}
% \catcode`Î=13 \defÎ{\exists}
% \catcode`Ý=13 \defÝ{\in}
% \def\cded#1{\begin{matrix}\ded{#1}\end{matrix}}
% \def\cded#1{\begin{matrix}\ded{#1}\end{matrix}}
% \def\vbij{\updownarrow}


Index of the slides:
\msk
% To update the list of slides uncomment this line:
\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")
\tocline {DAGs} {2}
\tocline {DAGs as topological spaces} {3}
\tocline {Compact diagrams} {4}
\tocline {Motivation for Logicians} {5}
\tocline {Topologies on (directed) graphs} {6}
\tocline {A (bad) presheaf on a DAG} {7}
\tocline {A presheaf on a DAG: its space of germs} {8}
\tocline {An archetypical example of a sheaf} {9}
\tocline {Saturated coherent families} {10}
\tocline {Logic on topological spaces: sequent calculus (1)} {11}
\tocline {Logic on topological spaces: sequent calculus (2)} {12}
\tocline {Logic on topological spaces: soundness and completeness} {13}
\tocline {Modalities} {14}
\tocline {Modalities: more theorems} {15}
\tocline {Modalities: alternative axioms} {16}
\tocline {Double negation is a modality, by hand (1)} {17}
\tocline {Double negation is a modality, by hand (2)} {18}
\tocline {Downcasing the closure operator} {19}
\tocline {Saturated covers} {20}
\tocline {Adjunctions between categories of covers} {21}
\tocline {Saturation in prestacks} {22}
\tocline {The algebra of covers: a lemma} {23}
\tocline {The algebra of covers: an (imaginary) finest cover} {24}
\tocline {Geometric Morphisms} {25}
\tocline {Geometric morphisms (2)} {26}
\tocline {Johnstone: filter-powers} {27}
\tocline {A note on filter-powers} {28}


\newpage
% --------------------
% «dags»  (to ".dags")
% (s "DAGs" "dags")
\myslide {DAGs} {dags}

{\myttchars
\footnotesize
\begin{verbatim}
A ``DAG'', for us, will have unlabelled arrows, at most one arrow from
a given vertex to another, and stationary arrows in it do not count as
cycles; so we can represent a DAG as a pair (X,R), where R<=X×X, and R
may have elements in the diagonal of X×X. We will write (a,b) in R as
a->b in R, and we will write the transitive-reflexive closure of R as
R^*. A ``never-stationary path'' from a to d in R may have length 0,
but it may not have stationary arrows; so, in the DAG below,

      aa -<
    <- |
  bb   |
    -> v
      cc -> dd

aa->bb->cc->dd and a->c->d are never-stationary paths from a to d, and
a is a never-stationary path from a to a. We define the length of a
never-stationary path in the obvious way, and we define ``R-length''
of an arrow a->d in R^* as the maximum length of never-stationary
paths from a to d in R. The numbers on the arrows of the DAG above are
their R-lengths, and the R-length of a->d in R^* is 3. Note that in a
DAG like (\R,{(a,b) in R^2|a<=b}) all the non-stationary arrows have
infinite length.

Fact (easy): if (X,R) is a finite DAG then there is exactly one
minimal R'<=R such that R'*=R*:

  R' := {a->b in R | the R-length of a->b is 1}.

Aciclity is needed because a DAG like ({0,1,2},{0,1,2}^2) is the
transitive-reflexive closure of two disjoint -- and minimal --
triangles of arrows: 0->1->2->0 and 0->2->1-0.
\end{verbatim}
}


\newpage
% --------------------
% «dags-as-topspaces»  (to ".dags-as-topspaces")
% (s "DAGs as topological spaces" "dags-as-topspaces")
\myslide {DAGs as topological spaces} {dags-as-topspaces}

{\myttchars
\footnotesize
\begin{verbatim}
Our archetypical DAG -- see [DS] for the meaning of ``archetypical''
-- will be D:=V, where V:=({aa,bb,cc},{aa->cc,bb->cc}); `V' will
always stand for that particular V-shaped DAG, but `D' will have the
connotation of a DAG that may be different in the general case.

We will call the vertices of V ``worlds'', and we will ``pronounce''
an arrow aa->cc in D as ``aa goes to cc'' or as ``cc is after aa''. We
will represent this DAG V bidimensionally as:

  aa      bb
    ->  <-
      cc

One benefit of using a fixed bidimensional representation for our DAGs
is that it will give us a very compact positional way of representing
subsets of the set of worlds: for example, {aa,cc}==101 -- a `1' at a
position means ``that vertex belongs to the subset'', a `0' means
``that vertex does not belong to the subset'', and `==' will always
mean ``change of notation''.

The arrows in R induce an ``order topology'' on X -- the idea is that
an arrow aa->cc says: ``any open set containing aa also contains cc''.
So the subsets of X that respect that arrows aa->cc and bb->cc are
{000, 001, 011, 101, 111}, and these are the open sets of ``D seen as
a topological space''; note that 100=={aa} is not open because it
violates the (condition given by the) arrow aa->cc, 010={bb} is not
open because it violates bb->cc, and 110={aa,bb} is not open because
it violates both.

We are mainly interested in using DAGs to represent their
(order-)induced topological spaces, and DAGs with fewer arrows are
easier to draw, so the fact (1) is quite handy.

Not all topologies are order topologies. The topology of (X,O(X))
comes from an DG on X if and only if arbitrary intersections of open
sets are open -- i.e, if (X,O(X)) is an ``Alexandroff space'' --, and
it comes from a DAG if and only if also any two different points in X
are topologically distinguishable -- i.e., if (X,O(X)) is T^0.
\end{verbatim}
}


(Point to Jibladze and Simmons)

% (find-angg ".emacs.papers" "jibladze")
% (find-angg ".emacs.papers" "simmons")

\newpage
% --------------------
% «compact-diagrams»  (to ".compact-diagrams")
% (s "Compact diagrams" "compact-diagrams")
\myslide {Compact diagrams} {compact-diagrams}

\def\threemadj{\;\three/|->`<-|`|->/\;}
\def\threeadj{\;\three/->`<-`->/\;}
\def\bbD{\mathbb{D}}
\def\bbV{\mathbb{V}}
\def\leaves{\mathrm{leaves}}
\def\2{\mathbf{2}}

Double negation:

$\dagSeven···1100 \threemadj \dagSeven0?01100$,

$\2^{\leaves(\bbD)} \threeadj \2^\bbD$

\msk

Saturated covers:

$X \threemadj \dagKite?1111$,

$\Opens(\bbV) \threeadj \Opens(\Opens(\bbV)^\op)$

\msk

Necessary:

$\dagReh0010 \threemadj \dagReh??10$,

$\2^\bbD \threeadj \2^D$

%D diagram geo-kitetopology
%D 2Dx     100    +15   +15
%D 2D  100      \d?1111
%D 2D
%D 2D  +15 \d01011   \d00111
%D 2D
%D 2D  +15      \d00011
%D 2D
%D 2D  +25      \d0000?
%D 2D
%D (( \d?1111   \d01011 \d00111   \d00011 \d0000?
%D    @ 0 @ 1 - @ 0 @ 2 -
%D    @ 1 @ 3 - @ 2 @ 3 -
%D    @ 3 @ 4 -
%D ))
%D enddiagram

%D diagram geo-kitenec
%D 2Dx     100    +15  +15
%D 2D  100      \d111
%D 2D
%D 2D  +15 \d101     \d011
%D 2D
%D 2D  +15      \d001
%D 2D
%D 2D  +20      \d??0
%D 2D
%D (( \d111   \d101 \d011   \d001 \d??0
%D    @ 0 @ 1 - @ 0 @ 2 -
%D    @ 1 @ 3 - @ 2 @ 3 -
%D    @ 3 @ 4 -
%D ))
%D enddiagram

%D diagram geo-rehnec
%D 2Dx      100  +15   +15  +15
%D 2D  100      \d1111
%D 2D
%D 2D  +20      \d0111
%D 2D
%D 2D  +15 \d?101    \d?011
%D 2D
%D 2D  +15      \d?001    \d??10
%D 2D
%D 2D  +15           \d??00
%D 2D
%D ((     \d1111
%D        \d0111
%D     \d?101 \d?011
%D         \d?001 \d??10
%D            \d??00
%D    @ 0 @ 1 -   @ 1 @ 2 - @ 1 @ 3 -
%D    @ 2 @ 4 - @ 3 @ 4 - @ 3 @ 5 -
%D    @ 4 @ 6 - @ 5 @ 6 -
%D ))
%D enddiagram

%D diagram geo-squareunkite
%D 2Dx     100   +15  +15
%D 2D  100      \d?11
%D 2D
%D 2D  +15 \d010     \d001
%D 2D
%D 2D  +15      \d000
%D 2D
%D (( \d?11   \d010 \d001   \d000
%D    @ 0 @ 1 - @ 0 @ 2 - @ 1 @ 3 - @ 2 @ 3 -
%D ))
%D enddiagram

$$\def\d{\dagKite}
  \diag{geo-kitetopology}
% $$
% $$
  \def\d{\dagVee}
  \diag{geo-kitenec}
% $$
% $$
  \def\d{\dagReh}
  \diag{geo-rehnec}
% $$
% $$
  \def\d{\dagPyr}
  \diag{geo-squareunkite}
$$


\newpage
% --------------------
% «motivation-for-logicians»  (to ".motivation-for-logicians")
% (s "Motivation for Logicians" "motivation-for-logicians")
\myslide {Motivation for Logicians} {motivation-for-logicians}

We can interpret intuitionistic propositional calculus on topological
spaces.

Fix a topological space $(X, \Opens(X))$ -- its open sets will play
the role of

truth values.

For $P, Q \in \Opens(X)$, define:

$$\begin{array}{rcl}
  § & := & X \\
  PQ & := & PþQ \\
  P´Q & := & PÌQ \\
  P¶Q & := & (P^\compl þ Q)^\interior \\
  ® & := & \emptyset \\
 \end{array}
$$

We will regard $X$ as a set of ``worlds'', and each open set $P \in
\Opens(X)$

as a proposition that is true at the worlds for which $x \in P$,

false at the others.

\smallskip

If the topology is discrete then $\Pts(X) = \Opens(X)$:

all subsets of $X$ are truth values,

and all the worlds are independent.

\smallskip

For some non-discrete topological spaces we may have $¬¬P \neq P$,

$¬(P´Q) \neq ¬P¬Q$, etc.

For example: take $X := \R$, with the usual topology, and

take $P := (0,1) þ (1,2)$. 

Then:

$\begin{array}{rcrcrcl}
  ¬P &=&  P¶® &=&  (P^\compl)^\interior &=& (-\infty,0)þ(2,\infty), \\
 ¬¬P &=& ¬P¶® &=& (¬P^\compl)^\interior &=& (0,2) \\
                          &&&& &\supsetneq& P. \\
 \end{array}
$

\medskip

\fbox{
\begin{tabular}{l}
Some operations on sheaves will be related to \\
forcing the logic to become boolean. \\
\end{tabular}
}

\newpage
% --------------------
% «topologies-on-dags»  (to ".topologies-on-dags")
% (s "Topologies on (directed) graphs" "topologies-on-dags")
\myslide {Topologies on (directed) graphs} {topologies-on-dags}

For some examples it will be convenient to use very small

(i.e., finite) topological spaces.

We will never need non-directed graphs here...

so let's say just ``graph'' to mean ``directed graph''.

Actually we are interested in the {\sl category} generated by a graph:

the transitive closure of the graph, plus the identity arrows.

\medskip

This will be one of our favourite graphs:

%D diagram fav-dag
%D 2Dx     100 +15 +15
%D 2D  100 \aa     \bb
%D 2D
%D 2D  +20     \cc
%D 2D
%D (( \aa \cc -> \bb \cc -> ))
%D enddiagram
%D
$$\mathbbold{3} \quad := \diag{fav-dag}$$

We can use `0's and `1's at the right places to denote

subsets of the set of ``worlds'' (points) of a graph.

In the ``natural topology'' of a graph the open sets

are be the subsets associated to non-decreasing functions

from the set of worlds to $\{0, 1\}$.

% (find-es "tex" "dags")
% (find-dn4ex "edrx08.sty" "dags")

The ``natural'' topology on $\mathbbold{3}$, $\Opens(\mathbbold{3})$, has
five open sets:

%D diagram nat-top-on-3
%D 2Dx     100        +15     +15        +30       +15      +15  
%D 2D  100        \dagVee111                \{\aa,\bb,\cc\}
%D 2D
%D 2D  +20 \dagVee101   \dagVee011   \{\aa,\cc\}    \{\bb,\cc\}
%D 2D
%D 2D  +20        \dagVee001                    \{\cc\}
%D 2D
%D 2D  +20        \dagVee000                     \{\,\}
%D 2D
%D 2D  +20
%D 2D
%D ((        \dagVee111           
%D    \dagVee101   \dagVee011   
%D           \dagVee001           
%D           \dagVee000           
%D    @ 0 @ 1 <- @ 0 @ 2 <-
%D    @ 1 @ 3 <- @ 2 @ 3 <-
%D    @ 3 @ 4 <-
%D ))
%D ((      \{\aa,\bb,\cc\}	    
%D    \{\aa,\cc\}    \{\bb,\cc\}
%D             \{\cc\}	    
%D              \{\,\}          
%D    @ 0 @ 1 <- @ 0 @ 2 <-
%D    @ 1 @ 3 <- @ 2 @ 3 <-
%D    @ 3 @ 4 <-
%D ))
%D enddiagram
%D
$$\diag{nat-top-on-3}$$

They are naturally ordered by inclusion, so $\Opens(\mathbbold{3})$

is another graph, with five points...

The cover of $\mathbbold{3}$

\medskip

$\begin{array}{lccc}
 \text{by:  } & \dagVee 101 \,\, \equiv \{\aa, \cc\} \\
 \text{and: } & \dagVee 011 \,\, \equiv \{\bb, \cc\} \\
 \end{array}
$

\medskip

can be denoted by:

$$\dagKite 01100 \quad \equiv \quad \{\{\aa, \cc\}, \{\bb, \cc\}\}.$$ 

\edrxcolors
\def\bhbox{\bicolorhbox}
% Test: a\bhbox{\dagKite 01100}b


\newpage
% --------------------
% «a-presheaf-on-a-dag»  (to ".a-presheaf-on-a-dag")
% (s "A (bad) presheaf on a DAG" "a-presheaf-on-a-dag")
\myslide {A (bad) presheaf on a DAG} {a-presheaf-on-a-dag}

\def\emp{\emptyset}

Here are shorter names for the open sets of $\Opens(X) =
\Opens(\mathbbold{3})$,

and a way to imagine $\Opens(X)$ as a subtopology of $\Opens(\R)$:

%D diagram UVW-and-R
%D 2Dx     100 +15 +15  +30 +15 +15  
%D 2D  100     X            X'     
%D 2D        /   \        /   \   
%D 2D  +20 U       V    U'      V'  
%D 2D        \   /        \   /   
%D 2D  +20     W            W'      
%D 2D          |            |      
%D 2D  +20   \emp         \emp{}
%D 2D
%D 2D  +20
%D 2D
%D ((    X           
%D    U     V   
%D       W
%D      \emp           
%D    @ 0 @ 1 <- @ 0 @ 2 <-
%D    @ 1 @ 3 <- @ 2 @ 3 <-
%D    @ 3 @ 4 <-
%D ))
%D ((      X' .tex= (-,)
%D    U' .tex= (-,1)    V' .tex= (0,)
%D         W' .tex= (0,1)   
%D              \emp{}          
%D    @ 0 @ 1 <- @ 0 @ 2 <-
%D    @ 1 @ 3 <- @ 2 @ 3 <-
%D    @ 3 @ 4 <-
%D ))
%D enddiagram
%D
$$\diag{UVW-and-R}$$

Here is a presheaf over $(X,\Opens(X))$ (``$P$'') that is

not a sheaf - it violates the two sheaf conditions.

$P$ is not collated - because

$\{p_U, p_{V'}\}$ is a coherent family (on $\{U,V\}$)

that cannot be collated to a global function.

$P$ is not separated - because

there are two different collations for $\{p_U, p_V\}$.

% (find-dn4file "dednat41.lua" "forths[\".PLABEL=\"] =")
% (find-dn4file "dednat41.lua" "storenode =")

%L thereplusxy = function (dx, dy, tag)
%L     ds[1] = storenode({x = ds[1].x + dx, y = ds[1].y + dy, tag = tag})
%L     return ds[1]
%L   end
%L forths["there+xy:"] = function ()
%L     thereplusxy(getword(), getword(), getword())
%L   end

\def\ph#1{\phantom{O}}
\def\ph#1{#1}
\def\ph#1{O}
\def\ph#1{{\color{red}#1}}
\def\ph#1{\phantom{#1}}

%D diagram bad-presheaf
%D 2Dx     100 +15 +15  +30 +15  +15  
%D 2D  100     X            X'     
%D 2D        /   \        /   \    
%D 2D  +20 U       V    U'      V'  
%D 2D        \   /        \   /    
%D 2D  +20     W            W'      
%D 2D          |            |      
%D 2D  +20   \emp         \emp{}
%D 2D
%D ((         X .tex= P(X)          
%D    U .tex= P(U)    V .tex= P(V)  
%D            W .tex= P(W)
%D         \emp .tex= P(\emp)          
%D    @ 0 @ 1 -> @ 0 @ 2 ->
%D    @ 1 @ 3 -> @ 2 @ 3 ->
%D    @ 3 @ 4 ->
%D ))
%D (( X' there+xy: -6 0 X'L .tex= \ph{p_X}
%D    X' there+xy:  6 0 X'R .tex= \ph{p'_X}
%D    V' there+xy: -6 0 V'L .tex= \ph{p_V}
%D    V' there+xy:  6 0 V'R .tex= \ph{p'_V}
%D ))
%D ((          X' .tex= \{p_X,p'_X\}
%D    U' .tex= \{p_U\}   V' .tex= \{p_V,p'_V\}
%D             W' .tex= \{p_W\}
%D         \emp{} .tex= \{p_\emp\}       
%D    # @ 0 @ 1 -> @ 0 @ 2 ->
%D    # @ 1 @ 3 -> @ 2 @ 3 ->
%D    # @ 3 @ 4 ->
%D                         X' place
%D    X'L U' -> X'R U' ->           X'L V'L -> X'R V'L ->
%D                                    V' place
%D                U' W' ->         V'L W' -> V'R W' ->
%D                       W' \emp{} ->
%D ))
%D enddiagram
%D
$$\diag{bad-presheaf}$$


\newpage
% --------------------
% «presheaf-on-a-dag-germs»  (to ".presheaf-on-a-dag-germs")
% (s "A presheaf on a DAG: its space of germs" "presheaf-on-a-dag-germs")
\myslide {A presheaf on a DAG: its space of germs} {presheaf-on-a-dag-germs}


Its space of germs is built like this:

for each point in $X$ - i.e., for $\aa, \bb, \gg$; let's look

at $\aa$ - look at all open sets containing $\aa$ (namely:

$U=\{\aa,\cc\}, X=\{\aa,\bb,\cc\}$) and take the colimit of $P$

on these open sets as they get smaller and smaller.

As there is a smallest open set containing $\aa$ - and $\bb$,

and $\cc$ - these colimits/germs are very easy to calculate:


%D diagram bad-presheaf-germs
%D 2Dx     100 +15 +15  +30 +15  +15  
%D 2D  100 \aa     \bb  \aa'     \bb'  
%D 2D         \   /        \    /  
%D 2D  +20     \cc          \cc'      
%D 2D
%D (( \aa \cc -> \bb \cc ->
%D ))
%D (( \bb' there+xy: -6 0 \bb'L .tex= \ph{p_\bb}
%D    \bb' there+xy:  6 0 \bb'R .tex= \ph{p'_\bb}
%D ))
%D (( \aa' .tex= \{p_\aa\}
%D    \bb' .tex= \{p_\bb,p'_\bb\}
%D    \cc' .tex= \{p_\cc\}
%D    \aa' \cc' ->
%D    \bb' place   \bb'L \cc' -> \bb'R \cc' ->
%D ))
%D enddiagram
%D
$$\begin{matrix}
  p_\aa  := p_U  \\
  p_\bb  := p_V  \\
  p'_\bb := p'_V \\
  p_\cc  := p_W  \\
  \end{matrix}
  \qquad
  \cdiag{bad-presheaf-germs}
$$

\msk

The projection map $E \to X$ is the obvious one.

We need to put a topology to $E$; it turns out (why?) that the

right topology is the one induced by the obvious graph.

Now this induces a sheaf of sections...

{\bf (I am skipping some steps -)}

%D diagram bad-presheaf-sheaf
%D 2Dx     100 +15 +15  +30 +15  +15  
%D 2D  100     X            X'     
%D 2D        /   \        /   \    
%D 2D  +20 U       V    U'      V'  
%D 2D        \   /        \   /    
%D 2D  +20     W            W'      
%D 2D          |            |      
%D 2D  +20   \emp         \emp{}
%D 2D
%D 2D  +20
%D 2D
%D ((         X .tex= S(X)          
%D    U .tex= S(U)    V .tex= S(V)  
%D            W .tex= S(W)
%D         \emp .tex= S(\emp)          
%D    @ 0 @ 1 -> @ 0 @ 2 ->
%D    @ 1 @ 3 -> @ 2 @ 3 ->
%D    @ 3 @ 4 ->
%D ))
%D (( X' there+xy: -5 0 X'L .tex= \ph{s_X}
%D    X' there+xy:  5 0 X'R .tex= \ph{s'_X}
%D    V' there+xy: -5 0 V'L .tex= \ph{s_V}
%D    V' there+xy:  5 0 V'R .tex= \ph{s'_V}
%D ))
%D ((          X' .tex= \{s_X,s'_X\}
%D    U' .tex= \{s_U\}   V' .tex= \{s_V,s'_V\}
%D             W' .tex= \{s_W\}
%D         \emp{} .tex= \{s_\emp\}       
%D    # @ 0 @ 1 -> @ 0 @ 2 ->
%D    # @ 1 @ 3 -> @ 2 @ 3 ->
%D    # @ 3 @ 4 ->
%D                         X' place
%D    X'L U' -> X'R U' ->           X'L V'L -> X'R V'R ->
%D                                    V' place
%D                U' W' ->         V'L W' -> V'R W' ->
%D                       W' \emp{} ->
%D ))
%D enddiagram
%D
$$\diag{bad-presheaf-sheaf}$$




\newpage
% --------------------
% «archetypical-sheaf»  (to ".archetypical-sheaf")
% (s "An archetypical example of a sheaf" "archetypical-sheaf")
\myslide {An archetypical example of a sheaf} {archetypical-sheaf}

Take $X := \R$, and:

$\begin{array}{rrcl}
 C: & \Opens(\R) &  \to & \Sets \\
    &          U & \mto & C(U) := \setofst{f: U \to \R}{\text{$f$ is continuous}} \\
 \end{array}
$

Now take a cover for $X = \R$:

$\begin{array}{rcl}
 W & := & (\infty, 1) \\
 V & := & (0, \infty) \\
 \U & := & \{W, V\} \\
 \end{array}
$

and look at a ``coherent family of functions'', $a_\U$, defined on $\U$:

$\begin{array}{rcl}
 a_\U & := & \{(W, a_W), \\
      &    & \;(V, a_V)\}
 \end{array}
$

where:

$\begin{array}{rrcl}
 a_W: & W & \to & \R \\
      & x & \mto & 2x \\
 a_V: & V & \to & \R \\
      & x & \mto & 2x \\
 \end{array}
$

Being ``coherent'' means that $ýV,W \in \U. (a_V|_{VÌW} = a_W|_{VÌW})$.

It is only for coherent families that we can have hope of being able to ``glue''

all the ``locally defined functions'' of the family into a sigle ``global function'',

$\begin{array}{rrcl}
 a: & X & \to & \R \\
    & x & \mto & 2x \\
 \end{array}
$

that generates them all, by restriction.

\medskip

A {\sl presheaf} on a topological space $\Opens(X)$ is a contravariant functor

$\Opens(X)^\op \to \Set$:

%D diagram restriction
%D 2Dx       100       +40
%D 2D  100 C(V) <--- C(U)
%D 2D        ^    ^    ^
%D 2D        |    |    |
%D 2D        -    -    -
%D 2D  +30   V ------> U
%D 2D
%D (( C(V) C(U)
%D      V    U
%D    @ 0 @ 1 <- .plabel= a C(V->U)
%D    @ 0 @ 2 <-| @ 1 @ 3 <-| @ 2 @ 3 ->
%D    @ 0 @ 3 varrownodes nil 20 nil <-|
%D ))
%D enddiagram
%D
$$\diag{restriction}$$

that is, for any $U \in \Opens(X)$ a set of ``locally defined functions''

(with support $U$), plus ``restriction functions'' between these sets.

\medskip

A {\sl sheaf} is a presheaf in which all coherent families defined on

covers can be glued well.

\newpage
% --------------------
% «saturated-coherent-fams»  (to ".saturated-coherent-fams")
% (s "Saturated coherent families" "saturated-coherent-fams")
\myslide {Saturated coherent families} {saturated-coherent-fams}

A ``continuous function'' defined on an open set $U$

induces a coherent family defined on all open sets contained in $U$...

Look at the graph $\Opens(\mathbbold{3})^\op$:

%D diagram nat-top-on-3-inv
%D 2Dx     100       +15     +15        +30       +15      +15  
%D 2D  100        \dagVee111                \{\aa,\bb,\cc\}
%D 2D
%D 2D  +20 \dagVee101   \dagVee011   \{\aa,\cc\}    \{\bb,\cc\}
%D 2D
%D 2D  +20        \dagVee001                    \{\cc\}
%D 2D
%D 2D  +20        \dagVee000                     \{\,\}
%D 2D
%D 2D  +20
%D 2D
%D ((        \dagVee111           
%D    \dagVee101   \dagVee011   
%D           \dagVee001           
%D           \dagVee000           
%D    @ 0 @ 1 -> @ 0 @ 2 ->
%D    @ 1 @ 3 -> @ 2 @ 3 ->
%D    @ 3 @ 4 ->
%D ))
%D ((      \{\aa,\bb,\cc\}	    
%D    \{\aa,\cc\}    \{\bb,\cc\}
%D             \{\cc\}	    
%D              \{\,\}          
%D    @ 0 @ 1 -> @ 0 @ 2 ->
%D    @ 1 @ 3 -> @ 2 @ 3 ->
%D    @ 3 @ 4 ->
%D ))
%D enddiagram
%D
$$\diag{nat-top-on-3-inv}$$

A ``continuous function'' defined on $\{\aa,\cc\}$ induces a coherent family

with support $\dagKite 01011$.

\newpage
% --------------------
% «logic-on-tss-sc-1»  (to ".logic-on-tss-sc-1")
% (s "Logic on topological spaces: sequent calculus (1)" "logic-on-tss-sc-1")
\myslide {Logic on topological spaces: sequent calculus (1)} {logic-on-tss-sc-1}

Topological spaces are a very good setting for understanding

intuitionistic propositional calculus - especially because they

let us show that some sentences can {\sl not} be proved.

\medskip

A topology $\Opens(X)$ will be seen as a category;

a morphism $P \to R$ exists iff, as open sets, $P \subseteq Q$ --

that is, if $P$ implies $Q$ ``in each world'' (i.e., $ýx \in X.(xÝP)¶(xÝQ)$);

this will also be our notion of $P$ implying $Q$ ``globally''.

\medskip

The sequent (with one hypothesis) $P \vdash Q$ will mean

``the morphism $P \to Q$ exists''.

\medskip

Fact: look at $\Opens(X)$ as a category; it is a cartesian closed category,

and the topological definitions of $§$, $´$, $¶$, $$, $®$ coincide

with the obvious corresponding categorical operations on objects --

\medskip

$\begin{array}{|c|l|}
 \hline
 § & \text{terminal object} \\
 ´ & \text{binary product} \\
 ¶ & \text{exponential} \\
  & \text{binary coproduct} \\
 ® & \text{initial object} \\
 \hline
 \end{array}
$

\medskip

The categorical definitions of $§$, $´$, $¶$, $$, $®$ suggest some rules

for building some sequents from others (or from nothing):

%D diagram O(X)-structure
%D 2Dx    100     +25     +25  +15  +20      +25
%D 2D 100     --| p0 |-	       t0   a0 <==== a1
%D 2D	     /    -    \       -     -        -
%D 2D	    /     |	\      |     |  <-->  |
%D 2D	   v      v	 v     v     v	      v
%D 2D +25 p1 <--| p2 |--> p3   t1   a2 ====> a3
%D 2D
%D 2D +15 c0 |--> c1 <--| c2   i0              
%D 2D	   -      -       -    -               
%D 2D	    \     |	 /     |               
%D 2D	     \    v	/      v               
%D 2D +25     --> c3 <--       i1              
%D 2D
%D ((            p0 .tex=  P
%D    p1 .tex= Q p2 .tex= Q´R p3 .tex= R
%D    @ 0 @ 1 |-> @ 0 @ 2 |-> @ 0 @ 3 |->
%D    @ 1 @ 2 <-| @ 2 @ 3 |->
%D ))
%D (( c0 .tex= P c1 .tex= PQ c2 .tex= Q
%D               c3 .tex=  R
%D    @ 0 @ 1 |-> @ 1 @ 2 <-|
%D    @ 0 @ 3 |-> @ 1 @ 3 |-> @ 2 @ 3 |->
%D ))
%D (( t0 .tex= P t1 .tex= §
%D    @ 0 @ 1 |->
%D ))
%D (( i0 .tex= ® i1 .tex= P
%D    @ 0 @ 1 |->
%D ))
%D (( a0 .tex= P´Q a1 .tex= P
%D    a2 .tex=  R  a3 .tex= Q¶R
%D    @ 0 @ 1 <= @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 =>
%D    @ 0 @ 3 harrownodes nil 20 nil <->
%D ))
%D enddiagram

$$\diag{O(X)-structure}$$

%:  P|-Q  P|-R                           P´Q|-R
%:  ----------  ------   ------   ----   ------(\vbij)
%:    P|-Q´R    Q´R|-Q   Q´R|-R   P|-§   P|-Q¶R
%:  
%:    ^O(X)-1   ^O(X)-2  ^O(X)-3  ^O(X)-4 ^O(X)-5
%:  
%:  P|-R  Q|-R
%:  ----------  ------   ------   ----
%:    PQ|-R    P|-PQ   Q|-PQ   ®|-P
%:  
%:    ^O(X)-6   ^O(X)-7  ^O(X)-8  ^O(X)-9
%:
$\begin{array}{ccccc}
 \ded{O(X)-1} & \ded{O(X)-2} & \ded{O(X)-3} & \ded{O(X)-4} & \ded{O(X)-5} \\ \\
 \ded{O(X)-6} & \ded{O(X)-7} & \ded{O(X)-8} & \ded{O(X)-9} \\
 \end{array}
$

\newpage
% --------------------
% «logic-on-tss-sc-2»  (to ".logic-on-tss-sc-2")
% (s "Logic on topological spaces: sequent calculus (2)" "logic-on-tss-sc-2")
\myslide {Logic on topological spaces: sequent calculus (2)} {logic-on-tss-sc-2}

We will work with four different ``languages'':

$\bullet$ categories,

$\bullet$ sequents with one hypothesis,

$\bullet$ sequents with a finite number of hypotheses,

$\bullet$ Natural Deduction.

\medskip

An example of translation

(between sequents with one hypothesis and categories):

%:                    ----  ----             ------       
%:    P|-Q            P|-§  P|-P   §|-P¶Q    §´P|-P  P|-Q 
%:   ======(\vbij)    ----------   ------    ------------ 
%:   §´P|-Q	        P|-§´P     §´P|-Q       §´P|-Q    
%:   ======(\vbij)      -----------------       ------    
%:   §|-P¶Q	             P|-Q               §|-P¶Q    
%:		                                          
%:   ^*transl-1	             ^*transl-2         ^*transl-3
%:
$$\ded{*transl-1} \qquad \ded{*transl-2} \qquad \ded{*transl-3}$$

%D diagram *transl-2
%D 2Dx     100      +30       +30
%D 2D  100 P <---> §´P <===== §
%D 2D       -       -         -
%D 2D        \ <->  |   <->   |
%D 2D         \     v         v
%D 2D  +30     ---> Q =====> P¶Q
%D 2D
%D (( P §´P §
%D       Q P¶Q
%D    @ 0 @ 1 <-> @ 1 @ 2 <=
%D    @ 0 @ 3 |-> @ 1 @ 3 |-> @ 2 @ 4 |->
%D    @ 3 @ 4 =>
%D    @ 0 @ 3 harrownodes 15 17 nil <->
%D    @ 1 @ 4 harrownodes nil 20 nil <->
%D enddiagram
%D
$$\diag{*transl-2}$$

\bigskip

{\bf A technicality:}

\medskip

%:   P|-Q         
%:   ----        --------
%:   R|-S        P¶Q|-R¶S
%:
%:   ^techPQRS   ^techPQRS-2
%:
$§ \vdash (P¶Q)¶(R¶S)
 \quad \Bij \quad
 P¶Q \vdash R¶S
 \quad \funto \quad
 \cded{techPQRS}
$

\medskip

Proof of the implication at the right:

%:  P|-Q
%:  ----
%:  §|-P¶Q  P¶Q|-R¶S
%:  ----------------
%:      §|-R¶S
%:      ------
%:       R|-S
%:
%:       ^techPQRS-3
%:
$$\ded{techPQRS-3}$$

\def\pileThree#1#2#3{\begin{smallmatrix}#1 \\ #2 \\ #3\end{smallmatrix}}

But the converse does not hold.

The case where it fails is when we have neither $P \vdash Q$ nor $R
\vdash S$.

Then, ``semantically'', 

$\cded{techPQRS}$ \quad holds, in a sense,

and we could expect this to be reflected in the existence of a

morphism $P¶Q \vdash R¶S$...

But try $P:=\pileThree 111$, $Q:=\pileThree 011$, $R:=\pileThree 011$,
$S:=\pileThree 001$ ---

then $(P¶Q)¶(R¶S) = \pileThree 001$, which is weaker than $§$.

\newpage
% --------------------
% «logic-on-tss-s-and-c»  (to ".logic-on-tss-s-and-c")
% (s "Logic on topological spaces: soundness and completeness" "logic-on-tss-s-and-c")
\myslide {Logic on topological spaces: soundness and completeness} {logic-on-tss-s-and-c}

Fact (for logicians; ``soundness''):

If
%:
%:  \aa_1|-\bb_1  \ldots  \aa_n|-\bb_n
%:  ==================================
%:               \cc|-\dd
%:
%:               ^soundness
%:
$$\ded{soundness}$$

is provable intuitionistically (i.e., in the system above),

then in any HA where $\aa_1 \vdash \bb_1, \ldots, \aa_n \vdash \bb_n$ hold,

the conclusion $\cc \vdash \dd$ also holds.

Proof: induction, trivial. Look at the full derivation,

starting from the top, and check that each bar constructs

a new sequent that holds.

\bigskip

Fact (for logicians; ``completeness''):

If
%:
%:  \aa_1|-\bb_1  \ldots  \aa_n|-\bb_n
%:  ==================================
%:               \cc|-\dd
%:
%:               ^completeness
%:
$$\ded{completeness}$$

is {\sl not} provable intuitionistically,

then there is a directed graph $D$,

and choices of truth values in $\Opens(D)$ for the

atomic propositions in $\aa_i, \bb_i, \cc, \dd$,

such that the hypotheses $\aa_1 \vdash \bb_1, \ldots, \aa_n \vdash \bb_n$ hold,

but the conclusion $\cc \vdash \dd$ does not hold.

Proof: hard, and non-categorical... uses tableau methods.

%:**^{**}
%:*^*
%:<=>\Bij 
\catcode`Î=13 \defÎ{\exists}
\def\vbij{\updownarrow}
\def\cded#1{\begin{matrix}\ded{#1}\end{matrix}}

\newpage
% --------------------
% «modalities»  (to ".modalities")
% (s "Modalities" "modalities")
\myslide {Modalities} {modalities}


Examples of modalities:

$P^* := ¬¬P$

$P^* := \aa  P$

$P^* := \aa ¶ P$

\medskip

Axioms:

%:                 P|-Q         
%:   ----         ------        -------
%:   |-§*         P*|-Q*        P**|-P*
%:
%:   ^ax*-1       ^ax*-2        ^ax*-3
%:
$$\ded{ax*-1} \qquad \ded{ax*-2} \qquad \ded{ax*-3}$$

First theorems:

\smallskip

$P \vdash P^*$

\smallskip

$(P´Q)^* \vdash P^*´Q^*$

\smallskip

$P´Q^* \vdash (P´Q)^*$

$P^*´Q^* \vdash (P´Q)^*$

\medskip

Proofs:

%:                --------
%:                P|-§<=>P
%:  --------     ----------
%:  |-§<=>§*     P|-§*<=>P*
%:  -----------------------
%:     P|-§<=>P*
%:     ---------
%:       P|-P*
%:
%:       ^and*-1
%:
%:                              ------------ 
%:			        P|-Q<=>(P´Q) 
%:    ------       ------      --------------
%:    P´Q|-P       P´Q|-Q      P|-Q*<=>(P´Q)*
%:  ----------	 ----------    --------------
%:  (P´Q)*|-P*	 (P´Q)*|-Q*     P|-Q*¶(P´Q)* 
%:  -----------------------     ------------ 
%:       (P´Q)*|-P*´Q*	        P´Q*|-(P´Q)*
%:
%:       ^and*-2                ^and*-3
%:
%:                     ============
%:                     P*´Q|-(P´Q)*
%:  ==============   ----------------   ---------------
%:  P*´Q*|-(P*´Q)*   (P*´Q)*|-(P´Q)**   (P´Q)**|-(P´Q)*
%:  ---------------------------------------------------
%:                    P*´Q*|-(P´Q)*
%:   
%:                    ^and*-4
%:
$$\ded{and*-1}$$
$$\ded{and*-2} \qquad \ded{and*-3}$$
$$\ded{and*-4}$$

\medskip

Consequence:

%D diagram and-cube
%D 2Dx     100  +20  +25  +20
%D 2D  100 (0)       (1)
%D 2D  +20      (2)       (3)
%D 2D      
%D 2D  +20 (4)       (5)
%D 2D  +20      (6)       (7)
%D 2D
%D (( (0) .tex= P´Q
%D    (1) .tex= P*´Q
%D    (2) .tex= P´Q*
%D    (3) .tex= P*´Q*
%D    (4) .tex= (P´Q)*
%D    (5) .tex= (P*´Q)*
%D    (6) .tex= (P´Q*)*
%D    (7) .tex= (P*´Q*)*
%D    @ 0 @ 1 |-> @ 2 @ 3 |->
%D    @ 0 @ 2 |-> @ 1 @ 3 |->
%D    @ 4 @ 5 <-> @ 6 @ 7 <->
%D    @ 4 @ 6 <-> @ 5 @ 7 <->
%D    @ 0 @ 4 |-> @ 1 @ 5 |->
%D    @ 2 @ 6 |-> @ 3 @ 7 <->
%D ))
%D enddiagram
%D
$$\diag{and-cube}$$

\newpage
% --------------------
% «modalities-more-theorems»  (to ".modalities-more-theorems")
% (s "Modalities: more theorems" "modalities-more-theorems")
\myslide {Modalities: more theorems} {modalities-more-theorems}

Implication:
%:
%:  ----------
%:  (P¶Q)´P|-Q
%:  --------------
%:  ((P¶Q)´P)*|-Q*
%:  --------------    -----------   ------------- 
%:  (P¶Q)*´P*|-Q*     P¶Q|-(P¶Q)*   (P¶Q)*|-P*¶Q* 
%:  -------------     ---------------------------  
%:  (P¶Q)*|-P*¶Q*            P¶Q|-P*¶Q*           
%:                                                
%:  ^imp*-1                  ^imp*-2              
%:
%:                     ---------------   -------     
%:                     P*´(P¶Q*)*|-Q**   Q**|-Q* 
%:  -------------      ------------------------- 
%:  (P¶Q)*|-P*¶Q*           P*´(P¶Q*)*|-Q*       
%:  -------------           --------------       
%:  P*´(P¶Q)*|-Q*           (P¶Q*)*|-P*¶Q*       
%:                    
%:  ^imp*-3                 ^imp*-4
%:
$$\ded{imp*-1} \qquad \ded{imp*-2}$$
$$\ded{imp*-3} \qquad \ded{imp*-4}$$

Disjunction:
%:  
%:    ------       ------          -------------
%:    P|-PQ       Q|-PQ          P*Q*|-(PQ)*
%:  ----------   ----------      -----------------
%:  P*|-(PQ)*   Q*|-(PQ)*      (P*Q*)*|-(PQ)**
%:  -----------------------      -----------------
%:       P*Q*|-(PQ)*            (P*Q*)*|-(PQ)*
%:
%:       ^or*-1                   ^or*-2
%:
$$\ded{or*-1} \qquad \ded{or*-2}$$

Quantifiers:
%:
%:     -------          --------------
%:     P|-Îx.P          Îx.P*|-(Îx.P)*
%:   -----------      ------------------
%:   P*|-(Îx.P)*      (Îx.P*)*|-(Îx.P)**
%:  --------------    ------------------
%:  Îx.P*|-(Îx.P)*    (Îx.P*)*|-(Îx.P)*
%:
%:  ^ex*-1            ^ex*-2
%:
%:
%:     -------
%:     ýx.P|-P
%:   -----------      ----------------
%:   (ýx.P)*|-P*      (ýx.P*)*|-ýx.P**
%:  --------------    ----------------
%:  (ýx.P)*|-ýx.P*    (ýx.P*)*|-ýx.P*
%:
%:  ^fa*-1            ^fa*-2
%:
$$\ded{ex*-1} \qquad \ded{ex*-2}$$
$$\ded{fa*-1} \qquad \ded{fa*-2}$$

Consequences:

%D diagram imp-cube
%D 2Dx     100  +20  +25  +20
%D 2D  100 (0)       (1)
%D 2D  +20      (2)       (3)
%D 2D      
%D 2D  +20 (4)       (5)
%D 2D  +20      (6)       (7)
%D 2D
%D (( (0) .tex= P¶Q
%D    (1) .tex= P*¶Q
%D    (2) .tex= P¶Q*
%D    (3) .tex= P*¶Q*
%D    (4) .tex= (P¶Q)*
%D    (5) .tex= (P*¶Q)*
%D    (6) .tex= (P¶Q*)*
%D    (7) .tex= (P*¶Q*)*
%D    @ 0 @ 1 <-| @ 2 @ 3 <->
%D    @ 0 @ 2 |-> @ 1 @ 3 |->
%D    @ 4 @ 5 <-| @ 6 @ 7 <->
%D    @ 4 @ 6 |-> @ 5 @ 7 |->
%D    @ 0 @ 4 |-> @ 1 @ 5 |->
%D    @ 2 @ 6 <-> @ 3 @ 7 <->
%D ))
%D enddiagram
%D
%D diagram or-cube
%D 2Dx     100  +20  +25  +20
%D 2D  100 (0)       (1)
%D 2D  +20      (2)       (3)
%D 2D      
%D 2D  +20 (4)       (5)
%D 2D  +20      (6)       (7)
%D 2D
%D (( (0) .tex= PQ
%D    (1) .tex= P*Q
%D    (2) .tex= PQ*
%D    (3) .tex= P*Q*
%D    (4) .tex= (PQ)*
%D    (5) .tex= (P*Q)*
%D    (6) .tex= (PQ*)*
%D    (7) .tex= (P*Q*)*
%D    @ 0 @ 1 |-> @ 2 @ 3 |->
%D    @ 0 @ 2 |-> @ 1 @ 3 |->
%D    @ 4 @ 5 <-> @ 6 @ 7 <->
%D    @ 4 @ 6 <-> @ 5 @ 7 <->
%D    @ 0 @ 4 |-> @ 1 @ 5 |->
%D    @ 2 @ 6 |-> @ 3 @ 7 |->
%D ))
%D enddiagram
%D
$$\diag{imp-cube} \qquad \diag{or-cube}$$

%D diagram ex-square
%D 2Dx      100       +40
%D 2D  100  Îx.P      Îx.P*
%D 2D
%D 2D  +40 (Îx.P)*   (Îx.P*)*
%D 2D
%D ((  Îx.P    Îx.P*   |->
%D    (Îx.P)* (Îx.P*)* <->
%D     Îx.P   (Îx.P)*  |->
%D     Îx.P*  (Îx.P*)* |->
%D ))
%D enddiagram
%D
%D diagram fa-square
%D 2Dx      100       +40
%D 2D  100  ýx.P      ýx.P*
%D 2D
%D 2D  +40 (ýx.P)*   (ýx.P*)*
%D 2D
%D ((  ýx.P    ýx.P*   |->
%D    (ýx.P)* (ýx.P*)* |->
%D     ýx.P   (ýx.P)*  |->
%D     ýx.P*  (ýx.P*)* <->
%D ))
%D enddiagram
%D
$$\diag{ex-square} \qquad \diag{fa-square}$$

\newpage
% --------------------
% «modalities-alt-axioms»  (to ".modalities-alt-axioms")
% (s "Modalities: alternative axioms" "modalities-alt-axioms")
\myslide {Modalities: alternative axioms} {modalities-alt-axioms}

A {\sl Lawvere-Tierney topology} is an arrow $j: Ø \to Ø$ such that

these three diagrams commute:

%:`\ign 
\def\ign#1{}

%D diagram LT-topology
%D 2Dx     100     +30   +20       +30      +30          +35
%D 2D          t               j                   /\
%D 2D  100 1 ----> Ø`0   Ø`2 ----> Ø`3      Ø×Ø -------> Ø
%D 2D        \      |        \      |        |           |
%D 2D       t \     | j     j \     | j  j×j |           | j
%D 2D          \    v          \    v        v     /\    v
%D 2D  +30      -> Ø`1          -> Ø`4     {Ø×Ø} -----> {Ø}
%D 2D
%D (( 1 Ø`0 Ø`1
%D    @ 0 @ 1 -> .plabel= a t
%D    @ 0 @ 2 -> .plabel= l t
%D    @ 1 @ 2 -> .plabel= r j
%D ))
%D (( Ø`2 Ø`3 Ø`4
%D    @ 0 @ 1 -> .plabel= a j
%D    @ 0 @ 2 -> .plabel= l j
%D    @ 1 @ 2 -> .plabel= r j
%D ))
%D (( Ø×Ø Ø {Ø×Ø} {Ø}
%D    @ 0 @ 1 -> .plabel= a {´}
%D    @ 0 @ 2 -> .plabel= l j×j
%D    @ 1 @ 3 -> .plabel= r j
%D    @ 2 @ 3 -> .plabel= a {´}
%D ))
%D enddiagram
%D
$$\diag{LT-topology}$$

Which means:
$$ Ï[§]=Ï[§^*] \qquad Ï[P^*]=Ï[P^{**}] \qquad Ï[P^*´Q^*]=Ï[(P´Q)^*] $$
%:
%:  -----     -------   -------   -------------  -------------
%:  §|-§*     P*|-P**   P**|-P*   P*´Q*|-(P´Q)*  (P´Q)*|-P*´Q*
%:
%:  ^LT-ax-1  ^LT-ax-2  ^LT-ax-3  ^LT-ax-4       ^LT-ax-5
%:
$$\ded{LT-ax-1} \qquad \ded{LT-ax-2} \qquad \ded{LT-ax-3}$$

$$\ded{LT-ax-4} \qquad \ded{LT-ax-5}$$

\medskip

It is not clear that these axioms (``LT axioms'')

are equivalent to the three axioms (``modality axioms'')

that we were using before...

We know that the modality axioms imply all the LT axioms,

but it is not obvious that the modality axioms $§ \vdash §^*$

and \quad $\cded{ax*-2}$

can be proved from the LT axioms...

\medskip

Here are the proofs:
%:
%:                     P|-Q
%:                    ------
%:                    §|-P¶Q
%:   --------       ------------
%:   P|-§<=>P       §|-P<=>(P´Q)
%:  ----------    ---------------
%:  P|-§*<=>P*    §|-P*<=>(P*´Q*)
%:  ----------    ---------------
%:  P|-§<=>P*        §|-P*¶Q*
%:  ---------        --------
%:    P|-P*           P*|-Q*
%:
%:    ^LT-equiv-1     ^LT-equiv-2
%:
$$\ded{LT-equiv-1} \qquad \ded{LT-equiv-2}$$

\newpage
% --------------------
% «double-neg-by-hand-1»  (to ".double-neg-by-hand-1")
% (s "Double negation is a modality, by hand (1)" "double-neg-by-hand-1")
\myslide {Double negation is a modality, by hand (1)} {double-neg-by-hand-1}

We need to see that $¬¬(P´Q) \Bij ¬¬P´¬¬Q$.

One direction is easy, and is a consequence of $(¬)$ being

a contravariant functor:

%D diagram notnot-categorically
%D 2Dx      100       +40        +45           +45
%D 2D  100  P ======> ¬P ====================> ¬¬P
%D 2D	    ^          -                 /--->  ^
%D 2D	    |   |->    |      |->       /       |
%D 2D	    -          v               -        -
%D 2D  +30 P´Q ===> ¬(P´Q) ===> ¬¬(P´Q) |--> ¬¬P´¬¬Q
%D 2D	    -          ^               -        -
%D 2D	    |   |->    |      |->       \       |
%D 2D	    v          -                 \--->  v
%D 2D  +30  Q ======> ¬Q ====================> ¬¬Q
%D 2D
%D ((  P    ¬P             ¬¬P      # 0 1   2
%D    P´Q ¬(P´Q) ¬¬(P´Q) ¬¬P´¬¬Q    # 3 4 5 6
%D     Q    ¬Q             ¬¬Q      # 7 8   9
%D    @ 0 @ 1 =>  @ 1 @ 2 =>
%D    @ 0 @ 3 <-| @ 1 @ 4 |-> @ 2 @ 5 <-| @ 2 @ 6 <-|
%D    @ 0 @ 4 harrownodes nil 20 nil |->
%D    @ 1 @ 5 harrownodes  15 20 nil |->
%D    @ 3 @ 4 =>  @ 4 @ 5 =>  @ 5 @ 6 |->
%D    @ 3 @ 7 |-> @ 4 @ 8 <-| @ 5 @ 9 |-> @ 6 @ 9 |->
%D    @ 3 @ 8 harrownodes nil 20 nil |->
%D    @ 8 @ 5 harrownodes  15 20 nil |->
%D    @ 7 @ 8 =>  @ 8 @ 9 =>
%D ))
%D enddiagram
%D
$$\diag{notnot-categorically}$$

We can convert this to natural deduction and normalize:

%:     =====         =====
%:     P´Q¶P	     P´Q¶Q
%:   =========	   =========
%:   ¬P¶¬(P´Q)	   ¬Q¶¬(P´Q)
%:  ===========	  ===========
%:  ¬¬(P´Q)¶¬¬P   ¬¬(P´Q)¶¬¬Q
%:  =========================
%:      ¬¬(P´Q)¶¬¬P´¬¬Q
%:
%:      ^notnot-and-1
%:
$$\ded{notnot-and-1}$$

%:  [P´Q]^1                [P´Q]^3
%:  -------                -------
%:     P     [¬P]^2           Q     [¬Q]^4
%:     ------------           ------------
%:         ®                      ®
%:       ------1                ------1
%:       ¬(P´Q)    ¬¬(P´Q)      ¬(P´Q)    ¬¬(P´Q)
%:       -----------------      -----------------
%:              ®                      ®
%:             ---2                   ---2
%:             ¬¬P                    ¬¬Q
%:             --------------------------
%:                      ¬¬P´¬¬Q
%:
%:                      ^notnot-and-1-nd
%:
$$\ded{notnot-and-1-nd}$$


\newpage
% --------------------
% «double-neg-by-hand-2»  (to ".double-neg-by-hand-2")
% (s "Double negation is a modality, by hand (2)" "double-neg-by-hand-2")
\myslide {Double negation is a modality, by hand (2)} {double-neg-by-hand-2}

The converse, $(¬¬P´¬¬Q)¶¬¬(P´Q)$, is much harder

(it was for me, at least...)

We start with two lemmas:
%:
%:  ¬¬¬P                ¬¬P,Q|-®
%:  ====(\vbij)		========(\vbij)
%:   ¬P			 P,Q|-®
%:
%:   ^notnot-lemma31	 ^notnot-lemma0
%:
$$\ded{notnot-lemma31} \qquad \ded{notnot-lemma0}$$

Proofs:
%:
%:                     [P]^2  [¬P]^1
%:		       -------------
%:		            ®
%:		           ---1
%:  ¬P  [¬¬P]^1	           ¬¬P  ¬¬¬P
%:  -----------	           ---------
%:      ®	               ®
%:    ----1	              --2
%:    ¬¬¬P     	              ¬P
%:
%:    ^notnot-n-to-nnn        ^notnot-nnn-to-n
%:
$$\ded{notnot-n-to-nnn} \qquad \ded{notnot-nnn-to-n}$$
%:
%:                       P
%:           		===
%:  ¬¬P  Q   		¬¬P  Q
%:    ::::   		  ::::
%:     ®     		    ®
%:
%:     ^notnot-lemma1       ^notnot-lemma2
%:
%:                     [P]^1  Q
%:                     ::::::::
%:                         ®
%:           		  --1
%:    P  Q   		  ¬P   ¬¬P
%:    ::::   		  --------
%:     ®     		    ®
%:
%:     ^notnot-lemma3       ^notnot-lemma4
%:
$$
 \def\higharrow{
   \begin{matrix}
     \funto \\ {} \\ {}
   \end{matrix}
 }
 \begin{array}{rcl}
   \ded{notnot-lemma1} & \higharrow & \ded{notnot-lemma2} \\
   \ded{notnot-lemma3} & \higharrow & \ded{notnot-lemma4} \\
 \end{array}
$$

\noindent
Now we can prove $(¬¬P´¬¬Q)¶-¬¬(P´Q)$ by reducing a ``hard'' sequent
to several simpler ones, then convert the simplest one to a small ND
proof (the bottom sequent at the left corresponds to the three top
lines at the right), then build bigger trees corresponding to more
complex sequents.
%:
%:                          [P]^2  [Q]^1
%:			    ------------
%:			        P´Q       [¬(P´Q)]^3
%:			        --------------------
%:			               ®
%:			              --1
%:			              ¬Q   ¬¬Q
%:			              --------
%:  ¬¬P,¬¬Q|-¬¬(P´Q)	                  ®
%:  =================(\vbij)             --2
%:  ¬¬P,¬¬Q,¬(P´Q)|-®	                 ¬P   ¬¬P
%:  =================(\vbij)             --------
%:   P,¬¬Q,¬(P´Q)|-®	                    ®
%:   ===============(\vbij)              -------3
%:    P,Q,¬(P´Q)|-®	                 ¬¬(P´Q)
%:
%:    ^notnot-lemma5	                 ^notnot-lemma5-nd
%:
$$\ded{notnot-lemma5} \ded{notnot-lemma5-nd}$$

\newpage
% --------------------
% «downcasing-closure-op»  (to ".downcasing-closure-op")
% (s "Downcasing the closure operator" "downcasing-closure-op")
\myslide {Downcasing the closure operator} {downcasing-closure-op}

\def\ovl{\overline}

\def\bP{\setofst{b}{P(b)}}
\def\aP{
  \begin{array}{l}
    f^{-1}(\setofst{b}{P(b)}) \\
    = \setofst{a}{P(f(a))} \\
  \end{array}
  }
\def\bovlP{
  \begin{array}{l}
    \ovl{\setofst{b}{P(b)}} \\
    = \setofst{b}{P(b)^*)} \\
  \end{array}
  }
\def\aovlP{
  \begin{array}{l}
    f^{-1}(\ovl{\setofst{b}{P(b)}}) \\
    = f^{-1}(\setofst{b}{P(b)^*}) \\
    = \setofst{a}{P(f(a))^*} \\
    = \ovl{\setofst{a}{P(f(a))}} \\
    = \ovl{f^{-1}(\setofst{b}{P(b)})} \\
  \end{array}
  }

%D diagram closure-1
%D 2Dx     100      +45     +40       +45
%D 2D  100 \aP              \bP
%D 2D
%D 2D  +45         \aovlP           \bovlP
%D 2D
%D 2D  +45 A                B
%D 2D
%D (( \aP       \bP
%D       \aovlP    \bovlP
%D         A          B
%D    @ 0 @ 1 ->  @ 2 @ 3 ->  @ 4 @ 5 -> .plabel= b f
%D    @ 0 @ 4 >->  @ 0 @ 2 >->  @ 2 @ 4 >->
%D    @ 1 @ 5 >->  @ 1 @ 3 >->  @ 3 @ 5 >->
%D ))
%D enddiagram
%D
%D diagram closure-2
%D 2Dx     100      +15     +20       +15
%D 2D  100 a|_P             b|_P
%D 2D
%D 2D  +20      a|_{\ovl{P}}       b|_{\ovl{P}}
%D 2D
%D 2D  +20 a                b
%D 2D
%D (( a|_P         b|_P
%D      a|_{\ovl{P}}   b|_{\ovl{P}}
%D        a            b
%D    @ 0 @ 1 |->  @ 2 @ 3 |->  @ 4 @ 5 |->
%D    @ 0 @ 4 `->  @ 0 @ 2 `->  @ 2 @ 4 `->
%D    @ 1 @ 5 `->  @ 1 @ 3 `->  @ 3 @ 5 `->
%D ))
%D enddiagram
%D
$$\diag{closure-1}$$
$$\diag{closure-2}$$


%%
%%
% (eedn4-51-bounded)


\newpage
% --------------------
% «saturated-covers»  (to ".saturated-covers")
% (s "Saturated covers" "saturated-covers")
\myslide {Saturated covers} {saturated-covers}

% (find-symbolspage 44 "\\blacktriangle")
% (find-symbolspage 54 "\\FilledSmallTriangleUp")
% (find-symbolstext)
%
\def\dbul{{\bullet\bullet}}
\def\bul{\bullet}
\def\bol{\circ}
\def\dtri{{\blacktriangle\blacktriangle}}
\def\tri{\blacktriangle}
\def\tro{\vartriangle}
\def\V{{\mathcal{V}}}
\def\W{{\mathcal{W}}}
\def\Opens {{\mathcal{O}}}
\def\OX    {{\Opens(X)}}
\def\OXop  {{\Opens(X)^\op}}

% (find-fline "~/LATEX/2005oct20-seminar.tex")
\catcode`=13 \def{\llbracket}
\catcode`=13 \def{\rrbracket}
\catcode`Ý=13 \defÝ{\in}

%D diagram U
%D 2Dx     100           +35          +35
%D 2D  100 \U^\dbul `--> \U^\bul `--> \U^\bol
%D 2D         /             /           /
%D 2D         |             |           |
%D 2D         v             v           v
%D 2D  +25 \U^\dtri `--> \U^\tri `--> \U^\tro
%D 2D
%D (( \U^\dbul \U^\bul \U^\bol
%D    \U^\dtri \U^\tri \U^\tro
%D    @ 0 @ 1 `-> @ 1 @ 2 `->
%D    @ 0 @ 3 `-> @ 1 @ 4 `-> @ 2 @ 5 `->
%D    @ 3 @ 4 `-> @ 4 @ 5 `->
%D ))
%D enddiagram
%D
$$\diag{U}$$

%D diagram Om
%D 2Dx        100            +35            +35
%D 2D  100 Ø^\dbul(U) >--> Ø^\bul(U) >--> Ø^\bol(U)
%D 2D          v              v              v
%D 2D          |              |              |
%D 2D          v              v              v
%D 2D  +25 Ø^\dtri(U) >--> Ø^\tri(U) >--> Ø^\tro(U)
%D 2D
%D (( Ø^\dbul(U) Ø^\bul(U) Ø^\bol(U)
%D    Ø^\dtri(U) Ø^\tri(U) Ø^\tro(U)
%D    @ 0 @ 1 >-> @ 1 @ 2 >->
%D    @ 0 @ 3 >-> @ 1 @ 4 >-> @ 2 @ 5 >->
%D    @ 3 @ 4 >-> @ 4 @ 5 >->
%D ))
%D enddiagram
%D
$$\diag{Om}$$

%D diagram om
%D 2Dx     100             +35           +35
%D 2D  100 Ï_U^\dbul `--> Ï_U^\bul `--> Ï_U^\bol
%D 2D         /              /             /
%D 2D         |              |             |
%D 2D         v              v             v
%D 2D  +25 Ï_U^\dtri `--> Ï_U^\tri `--> Ï_U^\tro
%D 2D
%D (( Ï_U^\dbul Ï_U^\bul Ï_U^\bol
%D    Ï_U^\dtri Ï_U^\tri Ï_U^\tro
%D    @ 0 @ 1 `-> @ 1 @ 2 `->
%D    @ 0 @ 3 `-> @ 1 @ 4 `-> @ 2 @ 5 `->
%D    @ 3 @ 4 `-> @ 4 @ 5 `->
%D ))
%D enddiagram
%D
$$\diag{om}$$

Notes:

$
\begin{array}{ll}
  Ø^\dbul(U) & \text{supersaturated, covering $U$, singleton} \\
  Ø^\bul(U)  & \text{saturated covering $U$} \\
  Ø^\bol(U)  & \text{covering $U$} \\
  Ø^\dtri(U) & \text{supersaturated or empty, subcovering $U$} \\
  Ø^\tri(U)  & \text{saturated, subcovering $U$} \\
  Ø^\tro(U)  & \text{subcovering $U$} \\
\end{array}
$

\smallskip

Comparison of notations:

Harold Simmons (p.5):

$
\begin{array}{ll}
  Ø[U]     & Ø^\dbul(U) \\
  Ø\ang{U} & Ø^\bul(U)  \\
  Ø(U)     & Ø^\tri(U)  \\
\end{array}
$

MacLane/Moerdijk:

$
\begin{array}{ll}
  Ø(U)     & Ø^\tri(U)  \\
\end{array}
$

\smallskip

% (find-angg "LATEX/edrxdnt.tex" "diagxy")
% (find-dn4file "dednat41.lua" "`->")
% (find-dn4file "dednat41.lua" "forths[\"`->\"] =")

\def\monic{\diagxyto/^{ (}->/}
\def\epic{\diagxyto/|->>/}
\def\diagxybij{\diagxyto/<->/}

Let $A(·)$ be a presheaf.

$
\begin{array}{ll}
  \text{$A$ is {\sl separated} when:} & ý\U^\bul.(a_U \monic     a_{\U^\bul}) \\
  \text{$A$ is {\sl collated} when:}  & ý\U^\bul.(a_U \epic      a_{\U^\bul}) \\
  \text{$A$ is a {\sl sheaf} when:}   & ý\U^\bul.(a_U \diagxybij a_{\U^\bul}) \\
\end{array}
$

\newpage
% --------------------
% «adjunctions»  (to ".adjunctions")
% (s "Adjunctions between categories of covers" "adjunctions")
\myslide {Adjunctions between categories of covers} {adjunctions}

\def\dbul{{\bullet\bullet}}
\def\bul{\bullet}
\def\bol{\circ}
\def\dtri{{\blacktriangle\blacktriangle}}
\def\tri{\blacktriangle}
\def\tro{\vartriangle}
\def\U{{\mathcal{U}}}
\def\V{{\mathcal{V}}}
\def\W{{\mathcal{W}}}

%D diagram adjs-betw-cats-of-covers
%D 2Dx     100    +35      +35     +35   +25      +30     +30
%D 2D                  uu       u                             
%D 2D  100 V <--| Vuu <--| Vu <--| Vo    vuu <=== vu <=== vo 
%D 2D      |       |        |       |     -        -       -
%D 2D      |  <->  |  <->   |  <->  |     |  <->   |  <->  | 
%D 2D      v       v        v       v     v        v       v 
%D 2D  +30 U |--> Uuu |--> Uu |--> Uo    uuu ===> uu ===> uo 
%D 2D                                                        
%D 2D          	        uu       u                           
%D 2D  +20     	  Øuu() <- Øu() <- Øo()                      
%D 2D      	        >->     >->                          
%D 2D		                                             
%D 2D          U       uu       u                            
%D 2D  +20 Ø <--- Øuu <--- Øu <--- Øo			      
%D 2D        >-->     >-->    >-->                           
%D 2D
%D (( V  Vuu .tex= \V^\dbul  Vu .tex= \V^\bul  Vo .tex= \V^\bol
%D    U  Uuu .tex= \U^\dbul  Uu .tex= \U^\bul  Uo .tex= \U^\bol
%D    @ 0 @ 1 <-| .plabel= a \bigcup
%D    @ 1 @ 2 <-| .plabel= a \dbul
%D    @ 2 @ 3 <-| .plabel= a \bul
%D    @ 0 @ 4 -> @ 1 @ 5 -> @ 2 @ 6 -> @ 3 @ 7 ->
%D    @ 0 @ 5 harrownodes nil 20 nil <->
%D    @ 1 @ 6 harrownodes nil 20 nil <->
%D    @ 2 @ 7 harrownodes nil 20 nil <->
%D    @ 4 @ 5 |-> .plabel= b \dbul @ 5 @ 6 |-> @ 6 @ 7 |->
%D ))
%D (( vuu .tex= \dagKite11111  vu .tex= \dagKite01111  vo .tex= \dagKite01100
%D    uuu .tex= \dagKite11111  uu .tex= \dagKite11111  uo .tex= \dagKite11111
%D    @ 0 @ 1 <-| .plabel= a \dbul  @ 1 @ 2 <-| .plabel= a \bul
%D    @ 0 @ 3 -> @ 1 @ 4 -> @ 2 @ 5 ->
%D    @ 0 @ 4 harrownodes nil 20 nil <->
%D    @ 1 @ 5 harrownodes nil 20 nil <->
%D    @ 3 @ 4 |-> @ 4 @ 5 |->
%D ))
%D (( Øuu() .tex= Ø^\dbul(U)  Øu() .tex= Ø^\bul(U)  Øo() .tex= Ø^\bol(U)
%D    @ 0 @ 1 <- sl^ .plabel= a \dbul   @ 0 @ 1 >-> sl_
%D    @ 1 @ 2 <- sl^ .plabel= a \bul    @ 1 @ 2 >-> sl_
%D ))
%D (( Ø  Øuu .tex= Ø^\dbul  Øu .tex= Ø^\bul  Øo .tex= Ø^\bol
%D    @ 0 @ 1 <- sl^ .plabel= a \bigcup @ 0 @ 1 >-> sl_
%D    @ 1 @ 2 <- sl^ .plabel= a \dbul   @ 1 @ 2 >-> sl_
%D    @ 2 @ 3 <- sl^ .plabel= a \bul    @ 2 @ 3 >-> sl_
%D ))
%D enddiagram
%D
$$\diag{adjs-betw-cats-of-covers}$$

Note that the inclusion arrows between covers run in the opposite

direction than the restrictions or coherent families...



\newpage
% --------------------
% «saturation-in-prestacks»  (to ".saturation-in-prestacks")
% (s "Saturation in prestacks" "saturation-in-prestacks")
\myslide {Saturation in prestacks} {saturation-in-prestacks}

Notation: $a_{\U^\bul} \subseteq A$ is a saturated, coherent family,

with support $\U^\bul$.

A family $a_{\U^\bul} \subseteq A$ in a prestack $A$ is:

{\sl saturated} when $ýV \in \U^\bul.ýW.(a_V·W \in a_{\U^\bul})$,

{\sl coherent} when $·: a_{\U^\bul} \to \U^\bul$ is a bijection.

\medskip

A prestack $A$ is:

$
\begin{array}{ll}
  \text{{\sl separated} when:} & ýa_U.ý\U^\bul.(a_U \monic     a_{\U^\bul}) \\
  \text{{\sl collated} when:}  & ýa_U.ý\U^\bul.(a_U \epic      a_{\U^\bul}) \\
  \text{a {\sl stack} when:}   & ýa_U.ý\U^\bul.(a_U \diagxybij a_{\U^\bul}) \\
\end{array}
$

where $a_{\U^\bul} := a_U · \U^\bul$.


%D diagram foo-J
%D 2Dx      100    +45         +40        +20            +35         +20
%D 2D  100                            Ø^\bul(V) ------------------> 1{}
%D 2D  +10  J ---> {1}            <----   v                <------   v
%D 2D  +10  v _|    v      Ø^\bul(W) ------------------> 1           |
%D 2D	    |       |          v          |              v           |
%D 2D	    |       | t        |          |              |           |
%D 2D	    |       |          |          v              |           v
%D 2D  +20  v  j    v          |      Ø^\tri(V) ---\dtri-|----> Ø^\tri(V){}
%D 2D  +10  Ø ---> {Ø}         v  <----                  v <-----
%D 2D  +10                 Ø^\tri(W) ----\dtri----> Ø^\tri(W){}
%D 2D
%D 2D
%D 2D  +20                                V                         V{}
%D 2D  +10                        ----->                     ---->
%D 2D  +10                     W                        W{}
%D 2D
%D (( J {1} Ø {Ø}
%D    @ 0 @ 1 -> @ 0 @ 2 >-> @ 1 @ 3 >-> .plabel= r t
%D    @ 2 @ 3 -> .plabel= a j
%D    @ 0 _|
%D ))
%D ((        Ø^\bul(V)              1{}
%D    Ø^\bul(W)               1
%D            Ø^\tri(V)          Ø^\tri(V){}
%D    Ø^\tri(W)           Ø^\tri(W){}
%D
%D    @ 0 @ 1 -> @ 2 @ 3 ->
%D    @ 4 @ 5 -> .plabel= a \dtri
%D    @ 6 @ 7 -> .plabel= a \dtri
%D
%D    @ 0 @ 2 -> @ 1 @ 3 ->
%D    @ 4 @ 6 -> @ 5 @ 7 ->
%D
%D    @ 0 @ 4 >-> @ 1 @ 5 >->
%D    @ 2 @ 6 >-> @ 3 @ 7 >->
%D    @ 0 relplace 8 8 \pbsymbol{7}
%D    @ 2 relplace 8 8 \pbsymbol{7}
%D ))
%D ((   V    V{}
%D    W    W{}
%D    @ 2 @ 0 -> @ 3 @ 1 ->
%D ))
%D enddiagram
%D
$$\diag{foo-J}$$

The classifier object:

$\begin{array}{rcl}
 Ø: \OX^\op & \to  & \Set \\
          U & \mto & Ø(U) \equiv Ø^\tri(U) \\
 \end{array}
$

A covering system, a.k.a.\ a Grothendieck topology:

$\begin{array}{rcl}
 K: \OX^\op & \to  & PØ^\tri(X) \\
          U & \mto & K(U) \equiv
                     \text{a family of ``covering sieves'' on $U$} \\
          U & \mto & Ø^\bul(U) \subseteq Ø^\tri(U) \\
 \end{array}
$

A site:

$(\OX, K)$

A covering system gives us a notion of ``sheaf'':

an object $A \in \Set^\OXop$

is a presheaf:
$\begin{array}[t]{rcl}
 A: \OXop & \to  & \Set \\
    U^\op & \mto & A(U) \\
 \end{array}
$

$A$ is a sheaf when $ýU.ý\U^\bul.(a_U \mto a_{\U^\bul} \text{ is a bijection})$



\newpage
% --------------------
% «algebra-of-covers-lemma»  (to ".algebra-of-covers-lemma")
% (s "The algebra of covers: a lemma" "algebra-of-covers-lemma")
\myslide {The algebra of covers: a lemma} {algebra-of-covers-lemma}

Theorem: for all $\W^\bul$ and $\V^\bul$,

$\W^\bul ´ \V^\bul$ is a saturated cover of $W´V$.

\smallskip

The saturation part is obvious; what is tricky there

is to see that
$\bigcup(\W^\bul ´ \V^\bul) = (\bigcup\W^\bul) ´ (\bigcup\V^\bul)$.

This only happens because $Ø$ is a frame.

\medskip

We will prove something stronger:

$\bigcup(\W^\tro ´ \V^\tro) = (\bigcup\W^\tro) ´ (\bigcup\V^\tro)$

for a harder definition of $\W^\tro ´ \V^\tro$ (not $(´)=(Ì)$).

\medskip

Definitions:

$\W^\tro ´ \V^\tro := \setofst{ W'´V' }{ W' Ý \W^\tro, V' Ý \V^\tro }$

$\W^\tro ´ V := \setofst{ W'´V }{ W' Ý \W^\tro }$

$W ´ \V^\tro := \setofst{ W´V' }{ V' Ý \V^\tro }$

When $\W^\tro$ and $\V^\tro$ are saturated, $(´)=(Ì)$.

\medskip

Lemma: when $\W^\tro = \{W_1, W_2\}$,

then $(\bigcup \W^\tro) ´ V = \bigcup (\W^\tro ´ V)$.

Proof: as $(´V) \vdash (V¶)$, the functor $(´V)$ preserves colimits:

%D diagram prescolims-UVW
%D 2Dx           100          +50           +45             +50                  +70
%D 2D  100 (W_1W_2)´V <--| W_1W_2 <--| (W_1,W_2) |--> (W_1´V,W_2´V) |--> (W_1´V)(W_2´V)
%D 2D	         |             |             |                |                   |
%D 2D	         |     <-->    |    <-->     |      <-->      |       <-->        |
%D 2D	         v             v             v                v                   v
%D 2D  +30       U |--------> V¶U |----> (V¶U,V¶U) <------| (U,U) <------------| U{}
%D 2D
%D (( (W_1W_2)´V W_1W_2 (W_1,W_2) (W_1´V,W_2´V) (W_1´V)(W_2´V)
%D        U         V¶U   (V¶U,V¶U)     (U,U)           U{}
%D    @ 0 @ 1 <-| @ 1 @ 2 <-| @ 2 @ 3 |-> @ 3 @ 4 |->
%D    @ 5 @ 6 |-> @ 6 @ 7 |-> @ 7 @ 8 <-| @ 8 @ 9 <-|
%D    @ 0 @ 5 -> @ 1 @ 6 -> @ 2 @ 7 -> @ 3 @ 8 -> @ 4 @ 9 ->
%D    @ 0 @ 6 harrownodes nil 20 nil <->
%D    @ 1 @ 7 harrownodes nil 20 nil <->
%D    @ 2 @ 8 harrownodes nil 20 nil <->
%D    @ 3 @ 9 harrownodes nil 20 nil <->
%D ))
%D enddiagram
$$\diag{prescolims-UVW}$$

Lemma: for any $\W^\tro$ and $V$,

$(\bigcup \W^\tro)´V = \bigcup (\W^\tro´V)$

Proof: generalize the diagram above.

\medskip

Theorem: for any $\W^\tro$ and $V^\tro$,

$\bigcup(\W^\tro ´ \V^\tro) = (\bigcup\W^\tro) ´ (\bigcup\V^\tro)$

Proof:

$\bigcup(\W^\tro ´ \V^\tro) =
 \bigcup_{V'Ý\V^\tro}(\bigcup(\W^\tro ´ V')) =
 (\bigcup\W^\tro) ´ (\bigcup\V^\tro)
$

{\it (wrong; check and correct)}





\newpage
% --------------------
% «algebra-of-covers-bottom»  (to ".algebra-of-covers-bottom")
% (s "The algebra of covers: an (imaginary) finest cover" "algebra-of-covers-bottom")
\myslide {The algebra of covers: an (imaginary) finest cover} {algebra-of-covers-bottom}

Definition: $\U^\bul \land \V^\bul := \U^\bul \cap \V^\bul$

Lemma: $\bigcup (\U^\bul \land \V^\bul) = \bigcup \U^\bul \land \bigcup \V^\bul = U \land V$

\smallskip

Definition: $§_U := \colim \,\, \U^\bul = \bigvee \Omega^\bul(U) = \U^\dbul$

Definition: $\bot_U := \lim \,\, \U^\bul = \bigwedge \Omega^\bul(U)$

\smallskip

$§_U$ is the biggest possible cover for $U$,

$\bot_U$ is the finest possible saturated cover for $U$.

\smallskip

Trick: sometimes $F(\bot_U)$ will make sense, but $\bot_U$ will not exist.

Motivation: notation for preservation of limits (as below).

% (even when $\bot_U$ does not exist!)

% (eedn4-51-bounded)
% (find-anggfile "LATEX/edrxdednat.tex" "forths[\"_|\"] =")

\def\foo{
  \begin{array}{c}
  F(A ×_C B)
  \cong \\
  F(A)×_{F(C)}F(B) \\
  \end{array}
}

%D diagram preslim
%D 2Dx        100       +35   +45      +55
%D 2D  100 A×_{C}B ---> B    \foo ---> F(B)
%D 2D         |  _|     |      | _|     |
%D 2D         |         |      |        |
%D 2D         v         v      v        v
%D 2D  +35    A ------> C    F(A) ---> F(C)
%D 2D
%D (( A×_{C}B B A C
%D    @ 0 @ 1 -> @ 0 @ 2 -> @ 1 @ 3 -> @ 2 @ 3 ->
%D    @ 0 relplace 8 8 \pbsymbol{7}
%D ))
%D (( \foo F(B) F(A) F(C)
%D    @ 0 @ 1 -> @ 0 @ 2 -> @ 1 @ 3 -> @ 2 @ 3 ->
%D    @ 0 relplace 18 14 \pbsymbol{7}
%D ))
%D enddiagram
%D
$$\diag{preslim}$$

Definition: $A^+(U) := \colim_{\U^\bul} A(\U^\bul)$

We will write this as: $A^+(U) := A(\bot_U) = A(\lim_{\U^\bul} \U^\bul)$

More explicitly: an $a^+_U = a_{\bot_U}$ is a pair $(\U^\bul, a_{\U^\bul})$

modulo an equivalence relation:
$({\U^\bul}',  a'_{{\U^\bul}'}) \sim
 ({\U^\bul}'', a''_{{\U^\bul}''})
$

when the set of indices where $a'_{{\U^\bul}'}$ and $a''_{{\U^\bul}''}$ coincide

is a (saturated) cover of $U$.

\newpage
% --------------------
% «geometric-morphisms»  (to ".geometric-morphisms")
% (s "Geometric Morphisms" "geometric-morphisms")
\myslide {Geometric Morphisms} {geometric-morphisms}

% (find-es "xypic" "two-and-three")

\def\tE{\mathscr{E}}
\def\tF{\mathscr{F}}
\def\Shv{\mathrm{Shv}}
\def\Psh{\mathrm{Psh}}
\def\Opens{\mathcal{O}}
\catcode`Î=13 \defÎ{\exists}
\catcode`Ý=13 \defÝ{\in}
\catcode`¨=13 \def¨{{:}}

A geometric morphism, $f: \tF \to \tE$,

is an adjunction, $\tF \two/<-`->/^{f^*}_{f_*} \tE$,

where $f^* \dashv f_*$ and $f^*$ is ``left exact'',

i.e., preserves finite limits.

\medskip

$f^*$ is called the {\sl inverse image}, and

$f_*$ is called the {\sl direct image} of $f$.

\medskip

If $f^*$ has a left adjoint, $f_!$ (i.e., $f_! \dashv f^* \dashv f_*$)

which is a stronger condition than $f^*$ being left exact,

then we say that $f$ is {\sl essential}.


$$ \tF  \three/->`<-`->/^{f_!}|{f^*}_{f_*}
   \tE
$$


\bigskip

Facts:

Each continuous map $f: X \to Y$ induces a

geometric morphism $\Shv(X) \to \Shv(Y)$.

(Does it extend to $\Psh(X) \to \Psh(Y)$?)

For a topological space $X$,

the inclusion $\Shv(X) \to \Set^{\Opens(X)^\op}$

is (the direct image of) a geometric morphism.

\medskip

What happens in the case of discrete topological spaces?

$\Shv(X) \cong \Set^X$,

where the $X$ in $\Set^X$ is a the set of points of the topological
space,

seen as a discrete category.


\newpage
% --------------------
% «geometric-morphisms-2»  (to ".geometric-morphisms-2")
% (s "Geometric morphisms (2)" "geometric-morphisms-2")
\myslide {Geometric morphisms (2)} {geometric-morphisms-2}

Two examples, associated to maps between discrete topological spaces:

%D diagram Set1->Set2
%D 2Dx     100     +35         +30        +30
%D 2D  100 A |---> (A,0)       a ======> (a;®)	
%D 2D	   |         |         -           -	
%D 2D	   |  <-->   |	       |    <->    |	
%D 2D	   v         v	       v           v	
%D 2D  +30 B <---| (B,B')      b <====== (b;b')	
%D 2D	   |         |         -           -	
%D 2D	   |  <-->   |         |    <->    |	
%D 2D	   v         v         v           v	
%D 2D  +30 C |---> (C,1)       c ======> (c;*)	
%D 2D	                                        
%D 2D  +18 Set1 -> Set12                                     
%D 2D  +8  {1} --> {1,2}                        
%D (( A (A,0)       
%D    B (B,B')      
%D    C (C,1)       
%D    Set1  .tex= \Set^{\{\aa\}}
%D    Set12 .tex= \Set^{\{\aa,\bb\}}
%D    {1}   .tex= \{\aa\}
%D    {1,2} .tex= \{\aa,\bb\}
%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 ->
%D    @ 8 @ 9 ->
%D ))
%D (( a (a;®)
%D    b (b;b')
%D    c (c;*)
%D    @ 0 @ 1 =>  @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 <=
%D    @ 2 @ 4 |-> @ 3 @ 5 |-> @ 4 @ 5 =>
%D    @ 0 @ 3 harrownodes nil 20 nil <->
%D    @ 2 @ 5 harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
$$\diag{Set1->Set2}$$

Another one:

%D diagram SetN->Set1
%D 2Dx          100            +35         +30          +30
%D 2D  100 (A_i)_{iÝ\N} |-> Æi¨\N.A_i     i;a_i ====> i,a_i 
%D 2D	        |              |            -           -   
%D 2D	        |     <-->     |            |    <->    |   
%D 2D	        v              v            v           v   
%D 2D  +30  (B)_{iÝ\N} <-----| B           i;b <======= b   
%D 2D	        |              |            -           -   
%D 2D	        |     <-->     |            |    <->    |   
%D 2D	        v              v            v           v   
%D 2D  +30 (C_i)_{iÝ\N} |-> åi¨\N.C_i     i;c_i ===> i|->c_i
%D 2D	                                                                                         
%D 2D  +18    SetN ---------> Set1
%D 2D  +8       N -----------> 1
%D (( (A_i)_{iÝ\N} Æi¨\N.A_i
%D     (B)_{iÝ\N}      B    
%D    (C_i)_{iÝ\N} åi¨\N.C_i
%D    SetN  .tex= \Set^\N
%D    Set1  .tex= \Set
%D    N     .tex= \N
%D    1     .tex= \{1\}
%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 ->
%D    @ 8 @ 9 ->
%D ))
%D (( i;a_i i,a_i
%D     i;b    b
%D    i;c_i i|->c_i
%D    @ 0 @ 1 =>  @ 0 @ 2 |-> @ 1 @ 3 |-> @ 2 @ 3 <=
%D    @ 2 @ 4 |-> @ 3 @ 5 |-> @ 4 @ 5 =>
%D    @ 0 @ 3 harrownodes nil 20 nil <->
%D    @ 2 @ 5 harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
$$\diag{SetN->Set1}$$

\newpage
% --------------------
% «johnstone-filter-powers»  (to ".johnstone-filter-powers")
% (s "Johnstone: filter-powers" "johnstone-filter-powers")
\myslide {Johnstone: filter-powers} {johnstone-filter-powers}

\catcode`Î=13 \defÎ{\exists}
\catcode`Ý=13 \defÝ{\in}
\catcode`¨=13 \def¨{{:}}
\def\tE{\mathscr{E}}
\def\tF{\mathscr{F}}

Johnstone, 9.41: We start with a left exact morphism $L$ between
toposes. In the case that interests us it is the direct image of an
essential geometric morphism; moreover, its inverse image is logical.
Diagram:

%D diagram 9.41
%D 2Dx         100             +40
%D 2D  100 (A_i)_{iÝ\N} |--> Æ_iA_i
%D 2D          |               |
%D 2D          |      <-->     |
%D 2D          v               v
%D 2D  +30  (B)_{iÝ\N} <-----| B
%D 2D          |               |
%D 2D          |      <-->     |
%D 2D          v               v
%D 2D  +30 (C_i)_{iÝ\N} |-> å_iC_i
%D 2D
%D 2D  +20    \tE ----L-----> \tF
%D 2D
%D (( (A_i)_{iÝ\N} Æ_iA_i
%D      (B)_{iÝ\N}   B
%D    (C_i)_{iÝ\N} å_iC_i
%D        \tE       \tF
%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 |-> .plabel= b L
%D    @ 6 @ 7 ->  .plabel= b L
%D ))
%D enddiagram
%D
$$\diag{9.41}$$

% (find-fline "~/LATEX/2008sheaves.tex" "diagram foo-J")

A filter on $L$ is a morphism $\Phi: L(Ø_\tE) \to Ø_\tF$ that is an
$´$-semilattice morphism, i.e., it respects $´$ and $§$. In our
archetypical case it is a morphism $\Phi: Ø^\N \to Ø$ that looks at
each point of $Ø^\N$ as if were a characteristic function of a subset
of $\N$, and then returns 1 when that subset is $\F$-big, and 0 when
not, where $\F$ is our filter on $\N$.

%D diagram 9.41b
%D 2Dx         100          +40              +30             +40
%D 2D  100     U --------> 1_\tE{}     (U_i)_{iÝ\N} ---> (1)_{iÝ\N}{}
%D 2D          v _|          v               v _|            v
%D 2D          |             | t_\tE         |               | (t)_{iÝ\N}
%D 2D          v      u      v               v       u       v
%D 2D  +30   1_\tE ------> Ø_\tE         (1)_{iÝ\N} ---> (Ø)_{iÝ\N}
%D 2D
%D 2D               L(u)                            L(u)
%D 2D  +20 L(1_\tE) ---> L(Ø_\tE)            1 -----------> Ø^\N
%D 2D              \         |                 \             |
%D 2D             t \        | \Phi           t \            | \Phi
%D 2D                \       v                   \           v
%D 2D  +30            ---> Ø_\tF                  ---------> Ø
%D 2D                                          
%D ((     U      1_\tE{}     
%D      1_\tE    Ø_\tE       
%D    L(1_\tE) L(Ø_\tE)      
%D               Ø_\tF       
%D    @ 0 @ 1 -> @ 0 @ 2 >-> @ 1 @ 3 >-> .plabel= r t_\tE
%D    @ 2 @ 3 -> .plabel= a u
%D    @ 0 _|
%D    @ 4 @ 5 -> .plabel= a L(u)
%D    @ 4 @ 6 -> .plabel= l t
%D    @ 5 @ 6 -> .plabel= r \Phi
%D ))
%D (( (U_i)_{iÝ\N} (1)_{iÝ\N}{}
%D      (1)_{iÝ\N} (Ø)_{iÝ\N}	 
%D           1      Ø^\N		                                           
%D                  Ø              
%D    @ 0 @ 1 -> @ 0 @ 2 >-> @ 1 @ 3 >-> .plabel= r t_\tE
%D    @ 2 @ 3 -> .plabel= a u
%D    @ 0 _|
%D    @ 4 @ 5 -> .plabel= a L(u)
%D    @ 4 @ 6 -> .plabel= l t
%D    @ 5 @ 6 -> .plabel= r \Phi
%D ))
%D
%D enddiagram
%D
$$\diag{9.41b}$$

A subobject $U \monicto 1_\tE$, and its characteristic morphism $u$,
are said to be {\sl $\Phi$-dense} (note the correspondence between
Johnstone's $\Phi$ and our filter $\F$ on $\N$) when $\Phi¢L(u) = t$,
i.e., in our archetypical case, when it takes 1 to a point of $Ø^\N$
that represents an $\F$-big set.

\newpage
% --------------------
% «note-on-filter-powers»  (to ".note-on-filter-powers")
% (s "A note on filter-powers" "note-on-filter-powers")
\myslide {A note on filter-powers} {note-on-filter-powers}

Now for each $\Phi$-dense subobject $U \monicto 1_\tE$ (in the
archetypical case: for $\F$-big subsets of the index set $\N$) there
is a pullback functor $U^*: \tE \to \tE/U$; and each monic $V \monicto
U$ between $\Phi$-dense subobjects induces a functor $\tE/U \to
\tE/V$. The (filtered) colimit of all these functors is a functor
$P_\Phi: \tE \to \tE_\Phi$; it turns out that $\tE_\Phi$ is a topos,
and that all these pullback functors are logical morphisms; I {\sl
think} that they are also the inverse images of essential geometric
morphisms, but I am not totally sure; and $P_\Phi$ is also logical
(but not usually a direct image of an essential geometric morphism).

%

\end{document}
