|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% -*- 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 \\
P∨Q & := & 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= P∨Q 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
%: ---------- ------ ------ ----
%: P∨Q|-R P|-P∨Q Q|-P∨Q ®|-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|-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*)*|-(P∨Q)*
%:
%: ^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= 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{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_1∨W_2)∧V <--| W_1∨W_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_1∨W_2)∧V W_1∨W_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}