% (find-angg "LATEX/2013sheaves-for-children.tex")
% (find-dn4tex-links "2013sheaves-for-children")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2013sheaves-for-children.tex && latex    2013sheaves-for-children.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2013sheaves-for-children.tex && pdflatex 2013sheaves-for-children.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && latex    2013sheaves-for-children.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && pdflatex 2013sheaves-for-children.tex"))
% (defun d () (interactive) (find-dvipage "~/LATEX/2013sheaves-for-children.dvi"))
% (find-dvipage "~/LATEX/2013sheaves-for-children.dvi")
% (find-xpdfpage "~/LATEX/2013sheaves-for-children.pdf")
% http://angg.twu.net/LATEX/2013sheaves-for-children.pdf

% (find-LATEXgrep "grep -nH -e BPM *.tex")
% (find-LATEX "2011ebl-slides.tex")
% (find-LATEX "2012minicats.tex")
% (find-dn4ex "edrxdefs.tex")


\documentclass[oneside]{article}
\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}

\def\BPM{\mathsf{BPM}}
\def\S{\mathsf{S}}
\def\catV{\mathbf{V}}
\def\nec{\Box}
\def\poss{\lozenge}
\def\toM{\to_{\scriptscriptstyle\mathsf{M}}}
\def\dagThreeH  #1#2#3{[\text{ThreeH }#1#2#3]}
\def\dagSquare#1#2#3#4{[\text{Square }#1#2#3#4]}
\def\L{\Lambda}


\input 2013sheaves-for-children.dnt


Title: Sheaves for Children

Author: Eduardo Ochs (eduardoochs@gmail.com)

{\bf INCOMPLETE VERSION - 2013dec22 23:50}

% {\bf Sheaves for children}

\bigskip

\begin{abstract}
First-year university students -- the ``children'' of the title --
often prefer to start from an interesting particular case, and only
then proceed to general statements. How can we make intuitionistic
logic, toposes, and sheaves accessible to them?

Let $D$ be a finite subset of $\N^2$. Draw arrows for all the ``black
pawns moves'' between points of $D$, and let $\catD$ be the poset
generated by that graph; $\catD$ is what we call a ``ZDAG'', and
$\Set^\catD$ is a ``ZDAG-topos''. It turns out that the truth-values
of a $\Set^\catD$ can be represented in a very nice way as
two-dimensional ascii diagrams, and that all the operations leading to
sheaves and geometric morphisms can be understood via algorithms on
diagrams.

In this talk we will present a computer library for performing
computations interactively on the truth-values of ZDAG-toposes. The
diagrams are rendered in ascii by default, but there is a module that
typesets them in LaTeX.
\end{abstract}

\bigskip


Let's start with some definitions. A non-empty subset of $\N^2$ is
{\sl well-positioned} when it touches both axes; a {\sl Z-set} is a
finite, non-empty, well-positioned subset of $\N^2$; a {\sl black
pawn's move} is an arrow between points of $\N^2$ that moves one unit
down and -1, 0 or 1 units horizontally; $\BPM(D)$ is the set of black
pawns' moves between point of $D$; a {\sl ZDAG} is a graph $(D,
\BPM(D))$ where $D$ is a Z-set. We will use the notation $R^*$ for the
transitive-reflexive closure of the relation $R$, $\bbD$ for the graph
$(D, \BPM(D)^*)$, and $\catD$ for $\bbD$ seen as a category.

% (find-dn4exfile "edrx08.sty" "dagKite")

A nice thing about Z-sets is that they can be ``named'' unambigously
by a positional notation with bullets. Four of our favourite Z-sets
--- $\dagVee***$ (``vee''), $\dagVee***$ (``lambda''), $\dagKite*****$
(``kite''), and $\dagHouse*****$ (``house'') --- also deserve
letter-like names: $V$, $\L$, $K$, and $H$; by a slight abuse of
language, the same diagrams will sometimes stand for $\bbV$, $\catV$,
and so on.

Finite models for the modal logic $\S4$ use valuations on systems of
``worlds'' (Kripke frames) whose visibility relations are partial
orders. So, we have a model of $\S4$ on $\dagHouse*****$;
$\dagHouse01101$ is a truth-value on it, and $\nec\dagHouse01101 =
\dagHouse00101$, and $\poss\dagHouse01101 = \dagHouse01111$. Note how
a lot of information can be recovered from the shapes of our diagrams.
{\sl Modal truth-values} are ZDAG bullet diagrams with `0's and `1's
in place of `*'s.

There is a well-known translation of intuitionistic logic into $\S4$
([1]), in which the ``intuitionistic truth-values'' correspond to
$\nec$-stable modal truth-values. When we put this in terms of Z-sets,
we get the following: the modal truth-values on a Z-set $D$ are
exactly (the characteristic functions of elements of) $\Pts(D)$, and
the intuitionistic truth-values on $D$ are a subset of that --- if we
consider the order topology on $D$ induced by $\BPM(D)$ we get a
topological space $(D, \Opens(D))$, and the intuitionistic
truth-values on $D$ are exacty the (characteristic functions of)
elements of $\Opens(D)$. So, for each Z-set $D$ we have a finite
Heyting algebra associated to it, whose elements have a very nice
diagrammatic representation --- and, using `$\to$' for the
intuitionistic implication and `$\toM$' for the modal implication, we
can say things like this:
%
  $$    (\dagHouse00111 \to  \dagHouse01011) =
    \nec(\dagHouse00111 \toM \dagHouse00111) =
    \nec \dagHouse01011 =
         \dagHouse01011
  $$

Anyone with a lot of practice in Topos Theory may find all this
trivial --- we are only establishing a nice notation for working with
the truth-values of a topos $\Set^\bbD$, which would be standard if
the \LaTeX{} macros for Z-sets and valuations on Z-sets were in wide
use. The only things here that may be new theorems are these: call a
ZDAG ``thin'' if it doesn't have $\dagThreeH***$ as a subgraph; then
$(\Opens(D), \subseteq)$ is isomorphic to a ZDAG iff $D$ is thin, and
that ZDAG is thin iff $D$ doesn't contain $\dagSquare****$ as a
subgraph...

{\sl ...but mathematics also has a social side} --- and when we take
it into account we become able to admit that {\sl theorems are of
little use when too few people are able to understand them.} ZDAGs are
tools for {\it social} mathematics --- they can be used to analyze
particular cases of many theorems, and to let people understand the
general theorems from these particular cases. In the paper [2] I have
laid down some a method for doing that precisely, in which the
particular and the general cases are written down in parallel, and I
have had this conjecture for several years:
%
\begin{quote}
  Categories of the form $\Set^\catD$ are the archetypal models for a
  sizeable fragment of basic sheaf theory,
\end{quote}
%
but {\sl what fragment}? I have since then realized that I won't be
able to answer that by working alone ---





\end{document}


% ----------------------------------------------------------------------------
\documentclass[oneside]{book}
\usepackage{amssymb}
\begin{document}

\def\N{\mathbb{N}}
\def\Set{\mathbf{Set}}
\def\catD{\mathbf{D}}

{\bf Sheaves for children}

\medskip

First-year university students -- the ``children'' of the title --
often prefer to start from an interesting particular case, and only
then proceed to general statements. How can we make intuitionistic
logic, toposes, and sheaves accessible to them?

Let $D$ be a finite subset of $\N^2$. Draw arrows for all the ``black
pawns moves'' between points of $D$, and let $\catD$ be the poset
generated by that graph; $\catD$ is what we call a ``ZDAG'', and
$\Set^\catD$ is a ``ZDAG-topos''. It turns out that the truth-values
of a $\Set^\catD$ can be represented in a very nice way as
two-dimensional ascii diagrams, and that all the operations leading to
sheaves and geometric morphisms can be understood via algorithms on
diagrams.

In this talk we will present a computer library for performing
computations interactively on the truth-values of ZDAG-toposes. The
diagrams are rendered in ascii by default, but there is a module that
typesets them in LaTeX.

\end{document}

% Local Variables:
% coding:           raw-text-unix
% ee-anchor-format: "«%s»"
% End: