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