Quick
index
main
eev
maths
blogme
dednat4
littlelangs
PURO
(GAC2,
λ, etc)
(Chapa 1)

emacs
lua
(la)tex
fvwm
tcl
forth
icon
debian
irc
contact

Sheaves for children

1. Sheaves for Children

Category Theory     <->  lambda calculus
  Topos Theory
    Sheaves
2. Why?

Category theory fascinates many people, but is usually done in a level
that is too abstract...

At the same time, that level of abstraction is exactly what is needed
to make lots of proofs be _almost_ automatic: _proving_ something in
CT means _constructing_ something, and all ``natural'' constructions
are equivalent. More or less like this:

  Let A and B be (arbitrary) sets. Then there is an ``obvious''
  function flip:A×B->B×A.

This idea can be formalized in (typed, polymorphic) lambda-calculus -
because lambda-calculus is made for expressing computations. Roughly,
we have this parallel:

  lambda-calculus:
    computations
    lambda-terms

  categories:
    constructions
    diagrams
3. Why? (2)

The new Girl from Ipanema

2012: 4-month long strike involving almost all federal universities in
Brazil

2013: many protests in Brazil, with many demands

Public education being dismantled.

Clear split between ``research universities'' and ``teaching
colleges''

Most texts about CT are for specialists in research universities...

Category theory should be more accessible.

To whom?...

Non-specialists (in research universities)
Grad students (in research universities)
Undergrads (in research universities)
Non-specialists (in conferences - where we have to be quick)
Undergrads (e.g., in CompSci - in teaching colleges)
(``Children'')
4. ZSets

Take a finite, non-empty subset of Nē;
translate it lowerleftwards as most as possible in Nē,
until you get something some touches both axes.
Subsets of Nē obtained in this way are said to be
"well-positioned", and we call them _ZSets_.

We can use a positional notation with bullets
to denote our favourite ZSets (unambiguously!)...

  V
  Lambda
  Kite
  House
5. ZDAGs

An arrow between points of Nē that goes one unit down
and 0/1/-1 units horizontally is called a _black pawn's move_.

Take a ZSet, D, and draw all possible black pawns moves
between its points; that gives us a set of arrows BPM(D),
that turns D, a ZSet, into a directed, acyclical, graph
in a canonical way.

Notation (note the change of font):
  D is a ZSet,
  bbD = (D, BPM(D)) is a _ZDAG_.

Example: K and bbK.
6. Closure and essentiality

We usually prefer transitive and reflexive relations.

If (A,R) is a graph,
then (A,R*) is its transitive-reflexive closure.

The operation R |-> R^* is well-known.
Now look for the smallest set of arrows, R^-,
such that (R^-)^* = R^*.

Example: bbK <==> bbK*

Fact: this generalizes to _any_ ZSet -
on ZSets/ZDAGs the dual operation to "*" is well defined!
For any ZSet D, (D, BPM(D)) is canonical in another sense -
the set BPM(D) has only the arrows that are "essential" to
generate bbD = (D, BPM(D)^*).

Duals of closure operations are usually _partial_ functions...

Magic fact: in the world of ZSets and ZDAGs _many_ closure
operations - many more that expected - have duals!

_Some people hate this_ - they seem to believe that a family
of particular cases in which some bonus properties hold
is useless for understanding the general case...

_They are wrong._
7. Truth-values

A function from a ZSet D to {0,1} is a _modal truth-value_.

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.
This gives us a way to _read aloud_ modal truth-values.
Example:

    1           0
   2 3         0 1
    4           1
    5           0

  reading      P:K->{0,1}
  order on K   "0,0,1,1,0"

Now consider that each 1 is covered with black paint.
Then Kite 00110 is not _stable_, because the paint on position 4
may flow into the 0 of position 5.

_Stable_ modal truth-values are called
_intuitionistic truth-values_.
8. Priming

For any ZDAG D, write Omega(D) (supset Pts(D)) for the set of all
intuitionistic truth-values on D.

Example: Omega(V) = {...}
Diagram:

             1 1                (1,3)
              1                 /   \
           /     \             /     \
          v       v           v       v
      1 0           0 1	  (0,2)       (2,2)
       1	     1	      \       /
          \       /	       \     /
	   v     v	       	v   v
	     0 0                (1,1)
	      1                   |
              |                   |
              v                   v
             0 0                (1,0)
              0

   (Omega(V), supseteq) iso (K, BPM(K)) = V'

Some Omega(D)s are (isomorphic to) ZDAGs!
Which ones?
9. Priming: theorems

For each ZDAG bbD, let catD be bbD^* seen as a category.
We say that bbC subset bbD when there is a
proper inclusion catC `-> catD.
We say that bbD is 3-thin when 3 notsubseq bbD.
We say that bbD is square-thin when square notsubseq bbD.
We say that bbD is thin when it is both 3-thin and square-thin.
Fact: is bbD is 3-thin then Omega(D) is (iso to) a ZDAG.
Fact: is bbD is thin then Omega(D) is (iso to) a ZDAG.

Fact: every D' = (Omega(D), supseteq) - whether planar or not -
is a Heyting algebra - i.e., we can interpret T, F, and, or, imp,
not on it.

So: priming gives us LOTS of Heyting algebras.
10. Modal logic

On any ZDAG D the directed graph bbD^* = (D, BPM(D)^*)
is a Kripke frame, and Pts(D) is a model of S4;
also, Omega(D) is a Heyting algebra, and a model of
IPL (intuitionistic propositional logic); the Tarski
translation holds, with these definitions (where "M"
means the "modal" operation, and "I" the "intuitionistic"
operation): if P,Q in Omega(D), then

  T_I = T_M
  F_I = F_M
  P and_I Q = P and_M Q
  P or_I Q  = P or_M Q
  P imp_I Q = nec (P imp_M Q)
  not_I P = nec (not_M P)

Amazing fact: for any wff E in IPL that is not
a theorem, the method of tableaux can find a finite
countermodel for it, using a tree-like frame; By making
a ZDAG with that shape - with possibly more points -
we can make a ZDAG-countermodel for E.

Example: let E be ... .
Let P = ..., Q = ... .
Then: ... = ... = ... != T
Thus E = ... is not a tautology in IPL,
and can't be a theorem of IPL -
but E' = ... is a theorem...

So ZDAGs can give people a concrete feeling of how
intuitionistic propositional logic works - which WFFs
can be theorems, which ones can't be, and why.
11. Categories

Remember: each catD - i.e., (D, BPM(D)^*) can be seen as a category -
the identity maps and the composition of morphisms is trivial
to define.

Each D' is a Heyting Algebra - a cartesian closed category -, and we
have nice names for its objects - for example, V' is (the
transitive-reflexive closure of) this:

We can explain the operations and, or, imp, not, plus T and F, and
their properties, by their categorical definitions (via diagrams!):