|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (setenv "TEXINPUTS" "~/LATEX:")
% (setenv "TEXINPUTS" nil)
% (defun c () (interactive) (find-LATEXsh "run-latex 'stem=2014sfc-slides2;pla'"))
% (defun c () (interactive) (find-LATEXsh "run-latex 'stem=2014sfc-slides2;d4;pla'"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2014sfc-slides2.pdf"))
% (defun fra () (interactive) (insert "\n% <>\n%\n\\begin{frame}\n\\frametitle{}\n\\end{frame}\n"))
% (find-pen-links)
% (find-sh0 "cp -v ~/LATEX/2014sfc-slides2.pdf /tmp/pen/")
% (find-sh0 "cp -v ~/LATEX/2014sfc-slides2h.pdf /tmp/pen/")
% (eev "cp -v /tmp/2014sfc-slides2.pdf /tmp/pen/ebl2014-ochs.pdf")
% (find-TH "math-b" "sheaves-for-children")
% (eev "Scp ~/LATEX/2014sfc-slides2.pdf $TWUS/LATEX/2014sfc-slides2.pdf")
% (eev "Scp ~/LATEX/2014sfc-slides2h.pdf $TWUS/LATEX/2014sfc-slides2h.pdf")
% (eev "Scp ~/LATEX/2014sfc-slides2h.pdf $TWUP/LATEX/2014sfc-slides2h.pdf")
% «.title-page» (to "title-page")
% «.where-sheaves-stand» (to "where-sheaves-stand")
% «.CT-why» (to "CT-why")
% «.CT-why-now» (to "CT-why-now")
% «.CT-should-be» (to "CT-should-be")
% «.CT-lambda-calculus» (to "CT-lambda-calculus")
% «.ZSets» (to "ZSets")
% «.ZDAGs» (to "ZDAGs")
% «.truth-values» (to "truth-values")
% «.intuitionistic-truth-values» (to "intuitionistic-truth-values")
% «.the-order-topology» (to "the-order-topology")
% «.priming» (to "priming")
% «.unpriming» (to "unpriming")
% «.priming-theorems» (to "priming-theorems")
% «.glueing-functions» (to "glueing-functions")
% «.sheafness» (to "sheafness")
% «.topological-sheafness» (to "topological-sheafness")
% «.the-evil-presheaf» (to "the-evil-presheaf")
% «.dual-operations» (to "dual-operations")
% «.where-are-the-theorems» (to "where-are-the-theorems")
% «.ZHAs-introduction» (to "ZHAs-introduction")
% «.ZHA-definition» (to "ZHA-definition")
% «.definitions-for-ZHAs» (to "definitions-for-ZHAs")
% «.definitions-for-ZHAs-2» (to "definitions-for-ZHAs-2")
% «.definition-of-ZHA» (to "definition-of-ZHA")
% «.Dminus-as-a-DAG» (to "Dminus-as-a-DAG")
% «.Dminus-as-generators» (to "Dminus-as-generators")
% «.ZHAs-are-sets-of-truth-values» (to "ZHAs-are-sets-of-truth-values")
%
% «.closure-and-ess» (to "closure-and-ess")
% (find-LATEX "README")
% (find-dn4file ".files.sh" "cptexinputs")
% (find-sh "pwd; ~/dednat4/.files.sh -n rmtexinputs")
% (find-sh "pwd; ~/dednat4/.files.sh -n cptexinputs")
% (find-sh "pwd; ~/dednat4/.files.sh rmtexinputs")
% (find-sh "pwd; ~/dednat4/.files.sh cptexinputs")
% (find-BEAMERfile "foo-ornate.tex")
% (find-BEAMERfile "foo.tex")
% (find-node "(kpathsea)Index" "TEXINPUTS")
% (find-es "tex" "TEXINPUTS")
% (find-LATEXfile "" "edrx08.sty")
\documentclass[hyperref=colorlinks]{beamer}
% \usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
\usepackage{etex} % (find-es "tex" "no-room-for-a-new-dimen")
\mode<presentation>
{
% \usetheme{Warsaw}
\usetheme{Boadilla}
\useinnertheme{default}
\useinnertheme{rectangles}
\setbeamercovered{transparent}
% or whatever (possibly just delete it)
}
\usepackage[english]{babel}
\usepackage[latin1]{inputenc}
\usepackage{times}
\usepackage[T1]{fontenc}
\usepackage{edrx08}
\input 2011ebl-defs.tex
% (find-LATEX "2011ebl-abs.tex" "priming")
%L process "edrx08.sty" -- (find-dn4ex "edrx08.sty")
\input 2014sfc-slides2.dnt
\def\BPM{\mathsf{BPM}}
\def\bbK{\mathbb{K}}
\def\dn{{\dnto}}
\def\Cont{\mathcal{C}}
\def\Cinfty{\mathcal{C}^‚}
\def\ctor#1{\mathcal{C}^‚(#1,\R)}
\def\ctos#1{C(#1)}
\def\bigdagop{
\def\searrow{\nwarrow}
\def\swarrow{\nearrow}
\def\downarrow{\uparrow}
}
\def\bigdagnoarrows{
\def\searrow{}
\def\swarrow{}
\def\downarrow{}
}
\def\Dn{{\Downarrow}}
\defÐ{\mathsf}
\def\ZHAC#1{$Ð{ZHA}_{#1}$}
%
\begin{document}
% (find-beamerugpage 73 "\\setbeamertemplate{navigation symbols}{}")
% (find-beamerugtext 73 "\\setbeamertemplate{navigation symbols}{}")
\setbeamertemplate{navigation symbols}{}
% «title-page» (to ".title-page")
%
\title{Sheaves for Children}
\author{Eduardo Ochs}
\institute[PURO/UFF]{
Departmento de Física e Matemática\\
Pólo Universitário de Rio das Ostras\\
UFF\\
% \footnotesize
\scriptsize
\url{http://angg.twu.net/math-b.html\#sfc} \\
\url{http://angg.twu.net/ferramentas-para-ativistas.html} \\
\tiny \phantom{a}
{\color{gray}(Version: 2014may19)} \\
}
\date{IFCS 2014may19}
\begin{frame}
\titlepage
\end{frame}
% «where-sheaves-stand» (to ".where-sheaves-stand")
%
\begin{frame}[fragile]
\frametitle{Where sheaves stand}
{\footnotesize
\begin{verbatim}
____________________
| |
| Category Theory | Cartesian Closed Categories,
| ________________ | Lambda-Calculus,
| | | | Intuitionistic Logic
| | Topos Theory | |
| | ____________ | |
| | | | | | Modal Logic (S4)
| | | Sheaves | | |
| | |____________| | | Topology
| |________________| |
|____________________| Algebraic Geometry
\end{verbatim}
}
\end{frame}
% «CT-why» (to ".CT-why")
%
\begin{frame}[fragile]
\frametitle{CT: Why?}
\par Category Theory is fascinating (for some people!),
\par but (usually) too abstract...
\msk
\par The right level of abstraction
\par makes lots of proofs {\it almost} automatic:
\par {\it proving} something in CT means
\par {\it constructing} something (CT is constructive!), and
\par all ``natural'' constructions are equivalent (``coherence'').
\msk
\par More or less like this:
\begin{quote}
\par Let A and B be (arbitrary) sets.
\par Then there is an ``obvious'' function $\text{flip}: A×B \to B×A$.
\end{quote}
% \msk
\par This {\sl ought} to make some parts of CT {\sl easy}!!!
\msk
\par (Long story... see ``Internal Diagrams and Archetypal Reasoning
in Category Theory'')
\end{frame}
% «CT-why-now» (to ".CT-why-now")
%
\begin{frame}
\frametitle{Why study CT {\sl now}?}
\includegraphics[width=8.5cm]{garota_de_ipanema.jpg}
\par Public education in Brazil is being dismantled -
\par maybe we should be doing better things than studying
\par very technical \& inaccessible subjects
\par with no research grants -
\end{frame}
% «CT-should-be» (to ".CT-should-be")
%
\begin{frame}
\frametitle{Category theory should be more accessible}
\par Most texts about CT are for specialists in research universities...
\par {\sl Category theory should be more accessible.}
\msk
\par To whom?...
\begin{itemize}
\item Non-specialists (in research universities)
\item Grad students (in research universities)
\item Undergrads (in research universities)
\item Non-specialists (in conferences - where we have to be quick)
\item Undergrads (e.g., in CompSci - in teaching colleges) - (``Children'')
\end{itemize}
\end{frame}
% «ZSets» (to ".ZSets")
%
\begin{frame}
\frametitle{ZSets}
\par Take a finite, non-empty subset of $\N^2$;
\par translate it lowerleftwards as most as possible in $\N^2$,
\par until you get something that touches both axes.
\msk
\par Subsets of $\N^2$ obtained in this way are said to be
\par ``well-positioned'', and we call them {\sl ZSets}.
\msk
\par We can use a positional notation with bullets
\par to denote our favourite ZSets (unambiguously!)...
\msk
\begin{tabular}{|l|l|c|l|} \hline
% Lambda & $\dagLambda***$ & \\ \hline
$V$ & Vee & $\dagVee***$ & $\{(0,1),\, (2,1),\, (1,0)\}$ \\ \hline
$K$ & Kite & $\dagKite*****$ & $\{(1,3),\, (0,2),\, (2,2),\, (1,1),\, (1,0)\}$ \\ \hline
$H$ & House & $\dagHouse*****$ & $\{(1,2),\, (0,2),\, (2,2),\, (0,1),\, (2,1)\}$ \\ \hline
\end{tabular}
\msk
\par $\uparrow$ Some of my favorite ZSets -
\par note that they have both short, one-letter names
\par and long, pronounceable names.
\msk
\end{frame}
% «ZDAGs» (to ".ZDAGs")
%
\begin{frame}
\frametitle{ZDAGs}
\par An arrow between points of $\N^2$ that goes one unit down
\par and 0/1/-1 units horizontally is called a {\sl black pawn's move}.
\msk
\par Take a ZSet, $D$, and draw all possible black pawns moves
\par between its points; this gives us a set of arrows, $\BPM(D)$,
\par that turns $D$, a ZSet, into a directed, acyclical, graph, $\bbD$,
\par in a canonical way: $\bbD = (D, \BPM(D)).$
\msk
\par Note the change of font!!!: \quad $D \dashrightarrow \bbD$
%Notation (note the change of font):
% D is a ZSet,
% bbD = (D, BPM(D)) is a _ZDAG_.
\msk
Example:
$$\def\ph{\phantom{m}}
K \;\; = \;\; \dagKite***** \;\; = \quad
{\bigdagnoarrows
\bigKite {(1,3)} {(0,2)\ph} {\ph(2,2)} {(0,1)} {(0,0)}
}
\qquad
\qquad
\bbK \;\; = \quad
\bigKite {(1,3)} {(0,2)\ph} {\ph(2,2)} {(0,1)} {(0,0)}
$$
\end{frame}
% «truth-values» (to ".truth-values")
%
\begin{frame}[fragile]
\frametitle{Truth-values}
\par A function from a ZSet $D$ to $\{0,1\}$ is a {\color{red}\sl
modal truth-value}.
\msk
\par The positional notation gives us a way to write modal
truth-values very compactly, and the points on a ZSet have a natural
order - the ``reading order'', in which we read them line by line,
left to right in each line. \msk \par This gives us a way to {\sl read
aloud} modal truth-values - \par and to list all modal truth-values
in order.
$$\bigKite abcde
\qquad
\bigKite 00110
\;\; = \;\; \dagKite00110 \;\; = \;\; P
\qquad
(\text{``Kite 00110''})
$$
\msk
Notation: $\Pts(\bbD)$ is the set of modal truth-values on $\bbD$
We use ``$\Pts(\bbD)$'' because $\dagKite00110$ ``is'' $\{c,d\}$ ($\subset K$)
\end{frame}
% «intuitionistic-truth-values» (to ".intuitionistic-truth-values")
%
\begin{frame}
\frametitle{Intuitionistic truth-values}
\msk
$$\bigKite a b c d e \qquad \bigKite 0 0 1 1 0 \;\; = P \qquad (\text{``Kite 00110''})
$$
\msk
\par Now consider that each 1 in $P$ is covered with (wet) black paint.
\par Then $P$ (``Kite 00110'') is not {\sl stable}, because the paint
\par of the 1 in position $d$ will flow down into the 0 of position $e$,
\par and paint it black.
\msk
\par {\color{red}\sl Stable} modal truth-values are called
{\color{red}\sl intuitionistic truth-values}.
\msk
\par Notation: $\dn P$ is $P$ after letting the black paint flow down.
\par Example: $\dn \dagKite 00110 = \dagKite 00111$
\end{frame}
% «the-order-topology» (to ".the-order-topology")
%
\begin{frame}
\frametitle{The order topology}
\par
$$\dn \dagKite 00110 = \dagKite 00111$$
\bsk
\par Notation: $\Pts(\bbD)$ is the set of modal truth-values on $\bbD$
\par Notation: $\Opens(\bbD)$ is the set of intuitionistic truth-values on $\bbD$
%\msk
$$\dn: \Pts(\bbD) \to \Opens(\bbD)$$
\par The topology $\Opens(\bbD)$ is the {\sl order topology} -
\par an arrow $\aa \to \bb$ in $\bbD$ means that
\par if an open set contains $\aa$ it has to contain $\bb$ too.
\msk
\par {\footnotesize (Order topologies are Alexandroff.)}
\end{frame}
% «priming» (to ".priming")
%
\begin{frame}[fragile]
\frametitle{Priming}
\par Amazing fact: very often $\Opens(\bbD)$ can be represented as a ZDAG too!
\par $\Opens(\bbD)$ has a natural order:
\par $P \to Q$ means
$P \le Q$,
$P \subseteq Q$,
$P \vdash Q$,
\par and $§ = \dagVee111$ (``Top'') is the terminal of the category...
\msk
\par But if we draw $\Opens(\bbD)^\op$ instead of $\Opens(\bbD)$
\par we can see clearly how $\bbD \ito \Opens(\bbD)^\op$:
\msk
$$\bigVee a b c
\qquad
\bigKite {\dagVee111} {\dagVee101} {\dagVee 011} {\dagVee 001} {\dagVee 000}
\qquad
\bigKite {\dn ab} {\dn a} {\dn b} {\dn c} {\emp}
$$
\msk
\par Note that $\dn ab = \dn \{a,b\} = \dn \dagVee110 = \dagVee111$.
\par Def: $\bbD' = \Opens(\bbD)^\op$.
\par $\bbV' \cong \bbK$ - and, by abuse of language, $\bbV' = \bbK$.
\end{frame}
% «unpriming» (to ".unpriming")
%
\def\G#1#2#3#4#5#6{\dagGuill{#1}{#2}{#3}{#4}{#5}{#6}}
%
\begin{frame}
\frametitle{Unpriming}
\par If $\bbC' = \bbD$ can we recover $\bbC$ from $\bbD$?
\par Better: if $\bbD$ is a ZDAG that is a Heyting algebra
\par can we find a $\bbC \subset \bbD$ such that $\bbC' = \bbD$?
\par Can we use that to determine quickly whether
\par an arbitrary $\bbD$ is a Heyting algebra?
\par Yes, yes, \& yes!
% Look at the elements of $\left(\dagGuill******\right)'$
% that have exactly one arrow leaving them...
$$\left(
\bigGuill abcdef
\right)'
\quad \cong \quad
\hugeGuillPrime
{\G 111111} % 12
{\G 101111} % 11
{\G 011111} % 10
{\G 001111} % 8
{\G 010111} % 9
{\G 001011} % 7
{\G 000111} % 5
{\G 001010} % 6
{\G 000011} % 4
{\G 000010} % 3
{\G 000001} % 2
{\G 000000} % 1
\qquad
\hugeGuillPrime
{\Dn ab} % 111111
{\Dn a} % 101111
{\Dn bc} % 011111
{\Dn cd} % 001111
{\Dn b} % 010111
{\Dn cf} % 001011
{\Dn d} % 000111
{\Dn c} % 001010
{\Dn ef} % 000011
{\Dn e} % 000010
{\Dn f} % 000001
{\emptyset } % 000000
$$
\end{frame}
% «priming-theorems» (to ".priming-theorems")
%
\begin{frame}
\frametitle{Priming: theorems}
% \par For each ZDAG $\bbD$, let $\catD$ be $\bbD^*$ seen as a category.
% \par We say that $\bbC \subset \bbD$ when there is a
% \par proper inclusion $\catC \ito \catD$.
\par We say that $\bbD$ is {\em 3-thin} when $\dagHthree*** \not\subset \bbD$.
\par We say that $\bbD$ is {\em square-thin} when $\dagVV**** \not\subset \bbD$.
\par We say that $\bbD$ is {\em thin} when it is both 3-thin and square-thin.
\par Fact: if $\bbD$ is 3-thin then $\bbD'$ is a ZDAG.
\par Fact: if $\bbD$ is thin then $\bbD'$ is a thin ZDAG.
\msk
Fact: every topology - whether planar or not - is a
Heyting algebra - i.e., we can interpret $T$, $F$, $\land$, $\lor$, $\to$,
$\neg$ on it, and every $\bbD'$ is a topology...
\msk
{\color{red}
\par Priming gives us LOTS of Heyting algebras,
\par and lots of {\sl planar} Heyting algebras!
}
\bsk
{\sl Topological} sheaves are defined on diagrams like
$\bbD \ito \bbD' \ito \bbD''$.
\end{frame}
% «glueing-functions» (to ".glueing-functions")
% (find-LATEX "2011ebl-abs.tex" "quotient")
%
\begin{frame}
\frametitle{Glueing locally-defined functions}
\par Let $U$ be $(-‚,1)$
\par and $V$ be $(0,‚)$...
\par Consider these open sets in $\R$,
$$\def\ph{\phantom{m}}
{\bigdagop
\bigKite {(-‚,‚)} {(-‚,1)\ph} {\ph(0,‚)} {(0,1)} {\emp}
\qquad
% \quad
\bigKite {UþV} {U} {V} {UÌV} {\emp}
\qquad
\bigKite {X} {U} {V} {W} {\emp}
}
\qquad
\qquad
\bigKite {\ctor X} {\ctor U\ph\ph} {\ph\ph\ctor V} {\ctor W} {\ctor\emp}
\qquad
\qquad
\bigKite {\ctos X} {\ctos U} {\ctos V} {\ctos W} {\ctos\emp}
$$
\par and the sheaf $C$ of $\Cinfty$ functions from them to $\R$.
\msk
\par Upward arrows are {\sl inclusions} (of an open set into another).
\par Downward arrows are {\sl restrictions} (of domains).
\msk
\par Two functions $f_U$ and $f_V$ are {\sl compatible}
\par if their restrictions to $UÌV$ coincide.
\msk
\par Each compatible family $\{f_U, f_V\}$ in $C$ has a unique glueing $f_X$.
\par Generalize that, and you get the definition of {\sl sheafness}.
\end{frame}
% «sheafness» (to ".sheafness")
%
\begin{frame}
\frametitle{Sheafness}
\par A compatible family $\{f_U, f_V\}$ is defined on $\{U, V\} = \dagKite01100$,
\par and it can be extended, using the restriction maps $\rho_{UW}:FU \to FW$ etc,
\par to a downward-closed compatible family $\{f_U, f_V, f_W, f_\emp\}$,
\par defined on $\{U, V, W, \emp\} = \dagKite01111$...
\msk
\par The ``unique glueing'' $f_X$ of $\{f_U, f_V\}$ can be extended
\par to a downward-closed compatible family $\{f_X, f_U, f_V, f_W, f_\emp\}$,
\par defined on $\{X, U, V, W, \emp\} = \dagKite11111$.
\msk
\par The restriction
$$\{f_X, f_U, f_V, f_W, f_\emp\}
\;\; \mton{\rho} \;\;
\{f_U, f_V, f_W, f_\emp\}
$$
\par is trivial to define -
\par {\color{red}sheafness means that maps like these are bijections.}
\end{frame}
% «topological-sheafness» (to ".topological-sheafness")
%
\begin{frame}
\frametitle{Topological sheafness}
\par A closure operator:
$$÷ \{U, V, W, \emp\} = \{X, U, V, W, \emp\}$$
\par it takes the union $U þ V þ W þ \emp = X$
\par and then all subsets of that.
\par It acts on $\bbV''$: \quad $÷: \dagVee***'' \to \dagVee***''$
$$÷ \dagKite01111 = \dagKite11111$$
\par Which elements of $\bbV''$ are stable by $÷$?
\par Only $\dn\{U,V\} \mto \dn \{X\}$ ($\dagKite01111 \mapsto \dagKite11111$)
and $\emp \mto \{\emp\}$ ($\dagKite00000 \mapsto \dagKite00001$)
\par are {\sl not} stable by $÷$.
\par The stable elements of $\bbV''$ are these: $\dagKitePrime1011110$.
\par {\color{red}These diagrams of stable elements are what we need to
\par define sheaves ``in general''.}
\end{frame}
% «the-evil-presheaf» (to ".the-evil-presheaf")
% (find-LATEXfile "2011ebl-abs.tex" "evil-presheaf")
%
\begin{frame}
\frametitle{The evil presheaf}
A presheaf $F$ in $\Set^{\Opens(\bbV)^\op}$
is simply a functor $F: \Opens(\bbV)^\op \to \Set$.
%
% (find-dn4 "experimental.lua" "relphantom")
%L forths[".xtag="] = function ()
%L local dx, tag = getwordasluaexpr(), getword()
%L tex = "\\ph{"..tag.."}"
%L ds[1] = storenode{x=ds[1].x+dx, y=ds[1].y, tex=tex, tag=tag}
%L end
%
%D diagram evil-presheaf
%D 2Dx 100 +20 +20 +30 +20 +20
%D 2D 100 A0 B0
%D 2D / \ / \
%D 2D v v v v
%D 2D +20 A1 A2 B1 B2
%D 2D \ / \ /
%D 2D v v v v
%D 2D +20 A3 B3
%D 2D | |
%D 2D v v
%D 2D +20 A4 B4
%D 2D
%D (( A0 .tex= E(X)
%D A1 .tex= E(U)
%D A2 .tex= E(V)
%D A3 .tex= E(W)
%D A4 .tex= E(\emp)
%D A0 A1 ->
%D A0 A2 ->
%D A1 A3 ->
%D A2 A3 ->
%D A3 A4 ->
%D ))
%D (( B0 .tex= \{e_X,e'_X\} place .xtag= -6 e_X .xtag= 12 e'_X
%D # B1 .tex= \{e_U,e'_U\} place .xtag= -5 e_U .xtag= 10 e'_U
%D B1 .tex= \{e_U\}
%D B2 .tex= \{e_V,e'_V\} place .xtag= -5 e_V .xtag= 11 e'_V
%D B3 .tex= \{e_W\}
%D B4 .tex= \{e_\emp\}
%D # e_X e_U -> e'_X e'_U ->
%D # e_X e_V -> e'_X e_V ->
%D # e_U B3 -> e'_U B3 ->
%D # e_V B3 -> e'_V B3 ->
%D # B3 B4 ->
%D e_X B1 -> e'_X B1 ->
%D e_X e_V -> e'_X e_V ->
%D B1 B3 ->
%D e_V B3 -> e'_V B3 ->
%D B3 B4 ->
%D ))
%D enddiagram
%D
$$
% (find-LATEXgrep "grep -nH -e color *.tex")
% \def\ph#1{{\color{red}#1}}
% \def\ph#1{\phantom{#1}}
\def\ph{\phantom}
\diag{evil-presheaf}
$$
The {\color{red}evil presheaf} $E: \Opens(\bbV)^\op \to \Set$, above,
fails to be in a sheaf in two ways:
the compatible family $\{e_U, e_V\}$ has two different glueings,
the compatible family $\{e_U, e'_V\}$ doesn't have a glueing.
\end{frame}
% «dual-operations» (to ".dual-operations")
%
\begin{frame}
\frametitle{Dual operations}
\par Due to we being in a finite / planar / etc case,
\par several interesting operations have duals (adjoints):
\msk
\begin{itemize}
\item In finite DAGs the transitive-reflexive closure $(A,R) \mto (A,R^*)$
\par has an adjoint that keeps only the ``essential arrows'' of the graph;
\item The ``let the paint flow down'' operation $\dn \dagKite00110=\dagKite00111$
\par has an adjoint $\dagKite 00111 \mto \dagKite 00100$ that returns
the ``generators''of an open set;
\item Each closure operator like $\calU \mto ÷\calU$ has an adjoint that
returns the smallest equivalent cover...
\end{itemize}
%\par In finite DAGs the transitive-reflexive closure $(A,R) \mto (A,R^*)$
%\par has an adjoint that keeps only the ``essential arrows'' of the graph;
%\msk
%\par The ``let the paint flow down'' operation $\dn \dagKite00110=\dagKite00111$
%\par has an adjoint $\dagKite 00111 \mto \dagKite 00100$ that returns
% the ``generators''of an open set;
%\msk
%\par Each closure operator like $\calU \mto ÷\calU$ has an adjoint that
% returns the smallest equivalent cover...
\end{frame}
% «where-are-the-theorems» (to ".where-are-the-theorems")
%
\begin{frame}
\frametitle{Where are the theorems?}
\par {\color{red}Not here! Why???}
\par Because this is ``for children'' -
\par we are focusing on the tools to let people check particular cases...
\par and this {\sl complements} [Bell 1988] and my IDARCT paper,
\par that explains how to do theorems and archetypal cases in parallel
\msk
\par Slightly more advanced things:
\begin{itemize}
\item CCCs and Heyting Algebras; $(∧Q) \dashv (Q{\to})$
\item presheaves of the form $\Set^\bbD$ as toposes
\item the classifier object of a $\Set^\bbD$
\item other modalities (besides $÷$) in a $\Set^\bbD$
\item all logical properties of modalities follow from three axioms
\item operations on the lattice of modalities
\item forcing
\item sheafification
\item geometric morphisms between toposes - I need help here ${=}($
\end{itemize}
\end{frame}
% o o
% o o o o o
% o o o o
% o o o o o o
% o o o o o o
% o o o o o o o
% o o o o o o o
% o o o o o o
% o o o o o o
% o o o o o o
% o o o
%
% This is This is This is
% a ZHA a ZHA NOT a ZHA
% «ZHAs-introduction» (to ".ZHAs-introduction")
%
\begin{frame}[fragile]
\frametitle{ZHAs}
\par A {\sl ZHA} is a ZSet that is a Heyting Algebra -
\par i.e., one whose points are intuitionistic truth-values,
\par and where we have the logical operations $\land$, $\lor$, $\to$, etc
\par defined on them, obeying the right equations...
\msk
\par ...but this is how we want to {\sl use} ZHAs.
\par Let's see a {\sl visual} characterization of ZHAs.
\bsk
\bsk
\par (See the handouts)
\usebox{\myboxa}
\end{frame}
% ¬ZHA1: The non-empty lines of D are not sequential - this is a gap
% ¬ZHA2: This D has more than one top element
% ¬ZHA3L: this is not a black pawn's move
% ¬ZHA4: This line is not made of consecutive same-parity points
% ¬ZHA5: This wide region has points of opposite parities
% o o
% o o o o o ¬ZHA2
% o o o o ¬ZHA1
% o o o o o o ¬ZHA3R
% o o o o o o ¬ZHA4
% o o o o o o o
% o o o o o o o
% o o o o o o
% o o o o o o ¬ZHA5
% o o o o o o
% o o o
%
% A ZHA (D_1) A ZHA (D_2) Not a ZHA (D_3)
%
%
%
% B B y=10
% o o B y=9
% o o o B y=8 \
% o o o o o y=7 | (6,8) in DCB_D_2
% o o o B y=6 \ /
% o o o o o y=5 |
% o o o o o o y=4 | (3,6) in DCB_D_2
% o o o o B y=3 /
% o o o B y=2 \
% o o o o y=1 | (0,2) in DCB_D_2
% B B y=0 /
%
% A ZHA with one A ZHA with
% wide region three wide
% regions
%
%
%
% B B
% L R B
% L o R B
% L o R L R
% L o R B
% L o R L R
% L o o R L R
% L o o R B
% L o R B
% L R L R
% B B
%
% The left wall and the right walls
% of D_1 and D_2; the bottlenecks
% belong to both walls
%
%
%
% o G .
% o o G . .
% G o o o G . .
% G o o G G G . .
% o o G o \ . G
% o o o G o . \ /
% o o o G G G . . X G
% G o o G G G . / G
% G o G o G / G
% G G G G G G
% o o .
%
% The generators of D_1 and D_2,
% and the inter-wall arrows of D_1
%
%
%
%
%
%
%
%
%
%
%
%
%
% The generators of D_1 and D_2
% «ZHA-definition» (to ".ZHA-definition")
%
\begin{frame}
\frametitle{ZHAs: definition}
\msk
\par Def: a ZSet $D$ is a ZHA iff it obeys these five conditions:
\msk
\par
% \par \ZHAC{1}: The non-empty lines of $D$ are sequential
% \par \ZHAC{2}: $D$ has a top element and a bottom element
% \par \ZHAC{3L}: The left wall of $D$ can be traversed by black pawns moves.
% \par \ZHAC{3R}: The right wall of $D$ can be traversed by black pawns moves.
% \par \ZHAC{4}: Each line of $D$ is made of consecutive same-parity points
% \par \ZHAC{5}: All points in each wide region of $D$ have the same parity
\begin{tabular}{ll}
\ZHAC{1} & The non-empty lines of $D$ are sequential \\
\ZHAC{2} & $D$ has one top element and one bottom element \\
\ZHAC{3L} & The left wall of $D$ can be traversed by black pawns moves \\
\ZHAC{3R} & The right wall of $D$ can be traversed by black pawns moves \\
\ZHAC{4} & Each line of $D$ is made of consecutive same-parity points \\
\ZHAC{5} & All points in each wide region of $D$ have the same parity \\
\end{tabular}
\msk
\par (The bottlenecks of $D$ divide it into regions with a top element
\par and a bottom element. A region whose lines are a bottleneck,
\par one or more non-bottlenecks, and another bottleneck is a
\par ``wide region'').
\msk
\par (If these look like six conditions, let \ZHAC3 be ``both the left
wall and the right wall of $D$ can be traversed by black pawns moves'')
\end{frame}
% «definitions-for-ZHAs» (to ".definitions-for-ZHAs")
%
\begin{frame}[fragile]
\frametitle{Definitions for ZHAs}
% {\footnotesize (``lines'' here are horizontal lines in $\N^2$)}
% \par
% \msk
% \par
\begin{tabular}{ll}
$Ð{height}_D$ & is the $y$ coordinate of the uppermost points of $D$. \\
$Ð{Line}_D(y)$ & is all points of $D$ whose $y$ coordinate is the given $y$. \\
$Ð{Lines}_D$ & is the set of all $y$s such that $Ð{Line}_D(y)$ is non-empty. \\
$Ð{L}_D(y)$ & is the $x$ coordinate of the leftmost point in $Ð{Line}_D(y)$. \\
$Ð{R}_D(y)$ & is the $x$ coordinate of the rightmost point in $Ð{Line}_D(y)$. \\
$Ð{W}_D(y)$ & is $ÐR_D(y)-ÐL_D(y)$. \\
$Ð{B}_D$ & is the set of all ys such that $Ð{Lines}_D(y)$ has exactly one \\
& point; these points are the {\color{red}bottlenecks} of $D$. \\
$Ð{LW}_D$ & is the {\color{red}left wall} - the set of points of the form $(y,ÐL_D(y))$ \\
$Ð{RW}_D$ & is the {\color{red}right wall} - the set of points of the form $(y,ÐR_D(y))$ \\
$D^-$ & is the set of {\color{red}generators} of $D$ - formally, the points \\
& $(x,y) \in D$ such that exactly one of the points \\
& $(x-1,y-1)$, $(x,y-1)$, $(x+1,y-1)$ belongs to $D$. \\
\end{tabular}
\msk
\par $ÐL_D, ÐR_D, ÐW_D: Ð{Lines}_D \to \N$.
\par ``Lines'' here are horizontal lines in $\N^2.$
% \par The functions $L_D$, $R_D$, $W_D$ above are partial on $\N$ -
% \par they are defined exactly on $Ð{Lines}_D$.
\end{frame}
% «definitions-for-ZHAs-2» (to ".definitions-for-ZHAs-2")
%
\begin{frame}[fragile]
\frametitle{Definitions for ZHAs (2)}
\par The line $y$ is a {\color{red}bottleneck} (of $D$) when $Ð{Lines}_D(y)$ has exactly one point
\par The line $y$ is a {\color{red}wide} when $Ð{Lines}_D(y)$ has more than one point
\msk
\par
\begin{tabular}{ll}
$Ð{B}_D$ & is the set of the ($y$ coordinates of) bottlenecks of $D$. \\
$Ð{CB}_D$ & is the set of ($y$ coords of pairs of) \\
& {\color{red}consecutive bottlenecks} of $D$ \\
& Formally: $(y_0,y_1) \in Ð{CB}_D$ iff $([y_0,y_1] \cap Ð{B}_D) = \{y_0,y_1\}$ \\
$Ð{CCB}_D$ & is the of {\color{red}close consecutive bottlenecks} of $D$ \\
& Formally: $(y_0,y_1) \in Ð{CCB}_D$ iff \\
& $(y_0,y_1) \in Ð{CB}_D$ and $y_1-y_0=1$ \\
$Ð{DCB}_D$ & is the of {\color{red}distant consecutive bottlenecks} of $D$ \\
& Formally: $(y_0,y_1) \in Ð{CCB}_D$ iff \\
& $(y_0,y_1) \in Ð{CB}_D$ and $y_1-y_0 \ge 2$ \\
$Ð{Reg}_D(y0,y1)$ & is the {\color{red}region} of all points $(x,y) \in D$ with $y_0 \le y \le y_1$. \\
$Ð{WideRegs}_D$ & is the set of all {\color{red}wide regions} of $D$ \\
& Formally: $Ð{WideRegs}_D = Ð{Reg}_D(Ð{DCB}_D)$ \\
\end{tabular}
\end{frame}
% (setq last-kbd-macro (kbd "C-a $ M-, ss{ M-z SPC C-y } M-f M-b & SPC C-a <down>"))
% (setq last-kbd-macro (kbd "C-a <right> M-, ss{ M-f } C-a <down>"))
% (setq last-kbd-macro (kbd "M-, ss{ M-f }"))
% (setq last-kbd-macro (kbd "{ \\ color{red} M-f }"))
% «definition-of-ZHA» (to ".definition-of-ZHA")
%
\begin{frame}[fragile]
\frametitle{ZHAs: definition (again, but this time formally)}
\par Def: a ZSet $D$ is a ZHA iff it obeys these conditions:
\par
\msk
\par
\begin{tabular}{ll}
\ZHAC{1} & The non-empty lines of $D$ are sequential \\
& Formally: $Ð{Lines}_D = \{0, 1, ..., Ð{height}_D\}$ \\
\ZHAC{2} & $D$ has one top element and one bottom element \\
& Formally: $\{0, Ð{height}_D\} \subset B_D$ \\
\ZHAC{3L} & The left wall of $D$ can be traversed by black pawns moves \\
& Formally: $Ð{L}_D(y+1)-Ð{L}_D(y) \in \{-1,0,1\}$ whenever defined \\
\ZHAC{3R} & The right wall of $D$ can be traversed by black pawns moves \\
& Formally: $Ð{R}_D(y+1)-Ð{R}_D(y) \in \{-1,0,1\}$ whenever defined \\
\ZHAC{4} & Each line of $D$ is made of consecutive same-parity points \\
& Formally: $Ð{Line}_D(y) =$ \\
& $\phantom{m} \{(a=Ð{L}_D(y),y), (a+2,y), (a+4,y), ..., (Ð{R}_D(y),y)\}$ \\
\ZHAC{5} & All points in each wide region of $D$ have the same parity \\
\end{tabular}
\end{frame}
% «Dminus-as-a-DAG» (to ".Dminus-as-a-DAG")
%
\begin{frame}
\frametitle{$D^-$ as a DAG (not necessarily a ZDAG)}
\par For each ZDAG $D$ its subset of generators, $D^-$
\par (the points of $D$ with exactly one black pawn move going out)
\par has a natural partial order in it, obtained by restricting
\par the partial order in $D$...
\msk
$$(D, \BPM^*(D) \quad \mto \quad (D^-, \BPM(D)^* \cap (D^- × D^-)$$
% \msk
\par When $D$ is a ZHA this order on $D^-$ is generated by a
\par set of arrows that is very easy to draw -
\par draw an arrow from each point of the left wall to the next one,
\par draw an arrow from each point of the right wall to the next one,
\par draw inter-wall arrows (which will always be $45^\circ$) like this:
\msk
\par [See the handouts]
\end{frame}
% «Dminus-as-generators» (to ".Dminus-as-generators")
%
\begin{frame}
\frametitle{$D^-$ as generators}
\par This gives us a notion of stable subsets of $D^-$,
\par and thus a topology on $D^-$.
\par $(D^-, \Opens(D^-))$ is a topological space,
\par which lets us construct $(D^-)'$...
\msk
\par When $D$ is a ZHA we have $(D^-)' \cong D$.
\par How?
\msk
\par We have
\par a natural function from $D^-$ to $D$,
\par a natural function from $\Opens(D^-)$ to $D$,
\par a natural function from $D$ to $\Opens(D^-)$,
\msk
\par [See the handouts]
\end{frame}
% «ZHAs-are-sets-of-truth-values» (to ".ZHAs-are-sets-of-truth-values")
%
\begin{frame}[fragile]
\frametitle{ZHAs are sets of truth-values}
Theorem 1: every ZHA $D$ is isomorphic to $\Opens(D^-)$.
Theorem 2: every ZHA $D$ is a Heyting Algebra.
Theorem 3: a ZSet $D$ is a Heyting Algebra iff it is isomorphic to $\Opens(D^-)$.
Theorem 4: a ZSet $D$ is a Heyting Algebra iff it is a ZHA ``with some
(or no) corners tucked in''.
\msk
[To do: describe the iso in theorem 1]
% {\footnotesize
% \scriptsize
% \begin{verbatim}
% Theorem 1: every ZHA D is isomorphic to O(D^-).
% Theorem 2: every ZHA D is a Heyting Algebra.
% Theorem 3: a ZSet D is a Heyting Algebra iff it is isomorphic to O(D^-).
% Theorem 4: a ZSet D is a Heyting Algebra iff it is a ZHA "with some
% (or no) corners tucked in."
%
% [To do: describe the iso in theorem 1]
% \end{verbatim}
% }
\end{frame}
%
%
%\section*{Summary}
%
%\begin{frame}{Summary}
%\end{frame}
%
%
%
%% All of the following is optional and typically not needed.
%\appendix
%\section<presentation>*{\appendixname}
%\subsection<presentation>*{For Further Reading}
%
\begin{frame}[allowframebreaks]
% \frametitle<presentation>{For Further Reading}
\frametitle{For Further Reading}
\begin{thebibliography}{10}
\beamertemplatebookbibitems
% Start with overview books.
\bibitem{Bell1988}
J.L.~Bell.
\newblock {\em Toposes and Local Set Theories}.
\newblock Oxford, 1988 (re-ed: Dover, 2007).
\beamertemplatearticlebibitems
% Followed by interesting articles. Keep the list short.
\bibitem{Ochs2013}
E.~Ochs.
\newblock{\em Internal Diagrams and Archetypal Reasoning in Category Theory}
\newblock Logica Universalis, 2013
\newblock{\url{http://angg.twu.net/math-b.html}}.
% (find-TH "math-b" "sheaves-on-zdags")
% (find-TH "math-b" "internal-diags-in-ct")
\end{thebibliography}
\end{frame}
\end{document}
% «closure-and-ess» (to ".closure-and-ess")
%
%\begin{frame}
%\frametitle{Closure and essentiality}
%\par If $(A,R)$ is a graph,
%\par then $(A,R^*)$ is its transitive-reflexive closure.
%\msk
%\par Notation and terminology:
%\par $\bbD = (D, \BPM(D))$
%\par $\bbD^* = (D, \BPM(D)^*)$
%\par $\catD$ is $\bbD^*$ seen as a category ($\catD$ a poset)
%\par $\Set^\catD$ is a ZDAG-topos
%\msk
%\par $\Opens(\bbD)$ are opens sets of the order topology on $\bbD$
%\par $\bbD' = \Opens(\bbD)$
%\msk
%\par We ${\color{red}\heartsuit}$ transitive and reflexive relations
%\par (and categories, and posets).
%\msk
%\par The operation $R \mapsto R^*$ is well-known.
%\msk
%\par If $(A,R)$ is a finite DAG,
%\par look for the smallest set of arrows, $R^-$,
%\par such that $(R^-)^* = R^*$.
%\par Fact 1: on finite DAGs this $R^-$ is unique.
%\par Fact 2: for any ZDAG $\bbD$ we have $\bbD^- = (\bbD^*)^- = \bbD$.
%\par {\sl This is not well-known.}
%
%
% \msk
% \par Example: $\bbK \to \bbK^* \to (\bbK^*)^-$
\end{frame}
%D diagram miniadj
%D 2Dx 100 120
%D 2D 100 a^L <= a
%D 2D - -
%D 2D | |
%D 2D v v
%D 2D 120 b => b^R
%D a^L a <= a^L b |-> a b^R |-> b b^R =>
%D enddiagram
%$$\diag{miniadj}$$
%: [a,b]^1
%: -------
%: [a,b]^1 b b|->c
%: ------- ------------
%: a c
%: ---------------
%: a,c
%: ---------1
%: a,b|->a,c
%:
%: ^tree1
%:
%$$\ded{tree1}$$
% «CT-lambda-calculus» (to ".CT-lambda-calculus")
%
\begin{frame}[fragile]
\frametitle{CT and $\lambda$-calculus}
\msk
\par Again:
\begin{quote}
\par Let A and B be (arbitrary) sets.
\par Then there is an ``obvious'' function $\text{flip}: A×B \to B×A$.
\end{quote}
\par This idea can be formalized in (typed, polymorphic) $\lambda$-calculus -
\par because $\lambda$-calculus is {\sl made} for expressing computations.
\par Roughly, we have this parallel:
\begin{tabular}{|l|l|} \hline
$\lambda$-calculus & Categories \\ \hline
computations & constructions \\
$\lambda$-terms & diagrams \\ \hline
\end{tabular}
Sales pitch:
{\sl Come learn CT, diagrammatic reasoning, $\lambda$-calculus and
functional languages at the same time!}
\end{frame}
% \section{Motivation}
% \subsection{The Basic Problem That We Studied}
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
#*
# (eev-bounded)
# (defun d () (interactive) (find-xpdfpage "/tmp/tmp.pdf"))
cd /tmp/
cat > /tmp/print.css <<'%%%'
@page { size: A4 }
body { font-size: 10pt !important }
%%%
cat > tmp.blogme <<'%%%'
[htmlize0 [J]
<pre>
Sheaves for Children - handouts
Seminário Carioca de Lógica, 2014may19
Eduardo Ochs
ZHAs - examples
===============
o o y=10
o o o o o <-- ¬ZHA2 y=9
o o o o <-- ¬ZHA1 y=8
o o o o o o <-- ¬ZHA3R y=7
o o o o o o <-- ¬ZHA4 y=6
o o o o o o o y=5
o o o o o o o y=4
o o o o o o \ y=3
o o o o o o | <-- ¬ZHA5 y=2
o o o o o o | y=1
o o o / y=0
A ZHA (D_1) A ZHA (D_2) Not a ZHA (D_3)
A ZSet D is a ZHA iff it obeys these conditions:
ZHA1: The non-empty lines of D are sequential
ZHA2: D has a top element and a bottom element
ZHA3L: The left wall of D can be traversed by black pawns moves
ZHA3R: The right wall of D can be traversed by black pawns moves
ZHA4: Each line of D is made of consecutive same-parity points
ZHA5: All points in each wide region of D have the same parity
D_3 violates all the ZHA conditions...
¬ZHA1: The non-empty lines of D_3 are not sequential - y=8 is a gap
¬ZHA2: D_3 has more than one top element
¬ZHA3R: this is not a black pawn's move (from y=7 to y=6)
¬ZHA4: This line is not made of consecutive same-parity points (y=6)
¬ZHA5: This wide region has points of opposite parities
B B y=10
o o B y=9
o o o B y=8 \
o o o o o y=7 | (6,8) in DCB_D_2
o o o B y=6 \ /
o o o o o y=5 |
o o o o o o y=4 | (3,6) in DCB_D_2
o o o o B y=3 /
o o o B y=2 \
o o o o y=1 | (0,2) in DCB_D_2
B B y=0 /
A ZHA with one A ZHA with
wide region three wide
regions
</pre>
<pre style="page-break-before: always">
B B
L R B
L o R B
L o R L R
L o R B
L o R L R
L o o R L R
L o o R B
L o R B
L R L R
B B
The left wall and the right walls
of D_1 and D_2; the bottlenecks
belong to both walls
o G .
o o G . .
G o o o G . .
G o o G G G . .
o o G o \ . G
o o o G o . \ /
o o o G G G . . X G
G o o G G G . / G
G o G o G / G
G G G G G G
o o .
The generators of D_1 and D_2,
and the inter-wall arrows of D_1
The intuitionistic implication:
0 0 0 0 int
0 1 -> 1 0 = ( 0 1 -> 1 0 ) P Q P&Q P\/Q P->Q
1 I 1 1 M 1 ---------------------
0 0 0 0 1
1 int 0 1 0 1 1
= ( 1 0 ) 1 0 0 1 0
1 1 1 1 1 1
0
= 1 0
1
</pre>
]
%%%
# cd
lua51 ~/blogme3/blogme3.lua -o /tmp/tmp.html -i /tmp/tmp.blogme
prince -s /tmp/print.css -o /tmp/tmp.pdf /tmp/tmp.html
cp -v /tmp/tmp.pdf ~/LATEX/2014sfc-slides2h.pdf
#*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Just after the presentation
Semantics of propositional calculus
This is a(n example of) a (T,F,&,or,->)-proposition on P and Q:
(P -> Q) or (Q -> P)
If we know the values of P and Q, and we know how to interpret
T, F, &, or, ->, we know how to calculate its value.
In the ``usual'' semantics we have P, Q in {0,1}, T=1, F=0,
and the behavior of &, or, -> is given by their tables:
P Q P&Q P\/Q P->Q
---------------------
0 0 0 0 1
0 1 0 1 1
1 0 0 1 0
1 1 1 1 1
When P=0 and Q=1 we can calculate the value of (P -> Q) or (Q -> P) as this:
(0->1) or (1->0)
1 0
1
Semantics of propositional calculus: not
By convention ¬P is always the same as P->F, so even when we attribute
stranger meanings to T, F, &, or, -> we can calculate the table for ¬
from T and the table for ->.
Semantics of propositional calculus: tautologies
We can express the behavior of (P -> Q) or (Q -> P) as a table, too:
P Q P->Q Q->P (P->Q)or(Q->P) P Q (P->Q)or(Q->P)
-------------------------------- --------------------
0 0 1 1 1 0 0 1
0 1 1 0 1 0 1 1
1 0 0 1 1 1 0 1
1 1 1 1 1 1 1 1
A proposition is a tautology when it answers T for all inputs.
We have a partial order on our truth-values: 0->1 (0<=0, 0<=1, 1<=1)
It induces a partial order on propositions on, say, P, Q and R...
F(P,Q,R) <= G(P,Q,R) iff ýP,Q,R in {0,1}. F(P,Q,R) <= G(P,Q,R)
So, for example, F <= P&Q <= P <= PorQ <= PorQorR <= T
P Q R F P&Q P PorQ PorQorR T
-------------------------------------
0 0 0 0 0 0 0 0 1
0 0 1 0 0 0 0 1 1
0 1 0 0 0 0 1 1 1
0 1 1 0 0 0 1 1 1
1 0 0 0 0 1 1 1 1
1 0 1 0 0 1 1 1 1
1 1 0 0 1 1 1 1 1
1 1 1 0 1 1 1 1 1
The notion of _theorem_
_tries_ to be equivalent to the notion of tautology...
but, conceptually, tautology and the the partial order on propositions
come first.
We saw how to use {0,1} as our set of truth-values.
Now we will learn how to use Pts(D) and Opens(D) instead -
for example,
Pts(Vee) = (modal)
Opens(Vee) = (intuitionistic)
We could give tables for and, or, ... on Pts(Vee),
but the tables would be too large...
instead we will describe how to calculate PandQ by an algorithm,
We can regard a (T,F,&,or,->)-proposition
/o
/o.o
<o o.o
\o o.o
>o o.o
/o o o<
/o o o o>
<o o o o/
\o o o/
\o o/
\o/
% Local Variables:
% coding: raw-text-unix
% End: