|
|
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!):
|
|