Sheaves and presheaves
Sheaves and presheaves are important structures at the intersection of logic and geometry. Presheaves fit into categorical logic as a relatively inexpressive logic, less expressive than algebraic theories, yet they still encompass many important examples. Presheaves are equivalent to discrete fibrations.
Theory
General
- Tennison, 1975: Sheaf theory (doi)
- Commentary on my blog
- Reyes, Reyes, Zolfaghari, 2004: Generic figures and their glueings: A constructive approach to functor categories (online , pdf)
- Borceux, 1994: Handbook of categorical algebra, Vol 3: Categories of sheaves
- Mac Lane & Moerdijk, 1992: Sheaves in geometry and logic: A first introduction to topos theory (doi, nLab )
- Ramanan, 2005: Global calculus
- Textbook on differential geometry from the sheaf-theoretic viewpoint
Relational presheaves, the relational counterpart of presheaves
A lax functor \(B \to \mathbf{Rel}\) is variously known as a relational presheaf, relational variable set, specification structure, or dynamic set. Likewise, a lax functor \(B \to \mathbf{Par}\) is a partial presheaf or partial variable set.
- Rosenthal, 1996: The theory of quantaloids, Sec. 3.3: Categories enriched in
a free quantaloid
- Based on Rosenthal, 1991: Free quantaloids (doi, pdf)
- The paper uses the term nondeterministic functor
- For related references, see quantaloids
- Abramsky, Gay, Nagarajan, 1996: Specification structures and propositions-as-types for concurrency (doi)
- Ghilardi and Meloni, 1996: Relational and partial variable sets and basic predicate logic (doi, jstor )
- Niefield, 2004: Change of base for relational variable sets (pdf)
- Theorem 3.1: Equivalence between relational variable sets and full subcategory \(\mathbf{Cat}_f/B\) of \(\mathbf{Cat}/B\) consisting of faithful functors over \(B\)
- Niefield, 2010: Lax presheaves and exponentiability (pdf)
- Studies lax presheaves valued in \(\mathbf{Rel}\), \(\mathbf{Par}\), and \(\mathbf{Span}\)
- Sec. 3: Further equivalences between lax functors and subcategories of \(\mathbf{Cat}/B\)
- Sobociński, 2015: Relational presheaves, change of base and weak simulation (doi, pdf)
Displayed categories
Closely related to a relational presheaf, a displayed category is a lax functor \(B \to \mathbf{Span}\). Displayed categories over \(B\) are equivalent to slice categories over \(B\):
\[ \mathrm{Lax}(B,\mathbf{Span}) \simeq \mathbf{Cat}/B. \]
Examples
Presheaf toposes
Every category of presheaves is an elementary topos, known as a presheaf topos. Much of the literature on topos theory is about sheaves and presheaves.
Graphs
The category of graphs is an important example of a “combinatorial” presheaf topos.
- Lawvere, 1989: Qualitative distinctions between some toposes of generalized
graphs (pdf)
- Lawvere, 1991: More on graphic toposes (online , pdf)
- Context and further references on nLab pages for graphic category and, bizarrely, Hegelian tacos
- Vigna, 2003: A guided tour of the topos of graphs (arxiv, pdf)
- Sebastiano Vigna’s personal page on graph fibrations
- Boldi & Vigna, 2002: Fibrations of graphs (doi, pdf)
- Boldi, Lonati, Santini, Vigna, 2006: Graph fibrations, graph isomorphism, and PageRank (doi, pdf)
- Ronnie Brown’s papers on graphs of graph morphisms, which explicitly invoke the topos of graphs
Not only do graphs form a category of presheaves; there are also sheaves on graphs.
- Hansen, 2019: A gentle introduction to sheaves on graphs (pdf)
- A very nice introduction, both readable and rigorous
- Covers sheaves of vector spaces on graphs, their morphisms and Laplacians, and hints at possible applications
- Hansen & Ghrist, 2018: Towards a spectral theory of cellular sheaves (arxiv, pdf)
- Friedman, 2015: Sheaves on graphs, their homological invariants, and a proof of the Hanna Neumann conjecture (doi, arxiv)
Simplicial and cubical sets
Simplicial sets and semi-simplicial sets form presheaf toposes, generalizing (reflexive) graphs to dimension greater than one. Likewise for cubical sets. For references, see simplicial stuff and cubical stuff.
Applications
Presheaves as models of networks
- Spivak, 2009: Higher-dimensional models of networks (arxiv)
- Network models as categories of presheaves, with functorial changes of model
- Main examples: graphs, hypergraphs, semi-simplicial sets, simplicial sets
Sheaves in topological data analysis
- Robinson, 2014: Topological signal processing (doi)
- DARPA tutorial on sheaves in data analytics , including slides and video
- Robinson, 2018: Assignments to sheaves of pseudometric spaces (arxiv)
- Curry, 2014, PhD thesis: Sheaves, cosheaves and applications (arxiv)
- Thesis by student of Robert Ghrist developing “cellular sheaves”
- Sec 4.2, relating classical and cellular sheaves, presents an alternate proof of: Ladkani, 2008: On derived equivalences of categories of sheaves over finite posets (doi, arxiv)
- Curry, 2018: Dualities between cellular sheaves and cosheaves (doi, arxiv)
- Partly extracted from Curry’s thesis
- Correction issued in: Curry, 2019: Functors on posets left Kan extend to cosheaves: An erratum (arxiv)
- Vepstas, 2017: Sheaves: A topological approach to big data (doi, arxiv,
GitHub )
- A gentle, informal introduction to graphs and cellular sheaves, motivated by data analysis
- Plenty of good intuition but certain analogies make little sense to me, e.g., comparing graphs and lambda calculus as “similar concepts”
- Also lots of mistakes, not merely typographical: assuming an adjacency list representation when claiming that graphs have bad computational properties compared to sections; claiming that contractions are what make tensor algebras into a monoidal category, rather than a compact closed category; claiming that “simply typed” means there is only one type; and so on
Sheaves in systems theory
- Goguen, 1992: Sheaf semantics for concurrent interacting objects (doi)
- Brief exposition in Spivak, 2014: Category Theory for the Sciences, Sec. 7.2.3: Sheaves, especially Sec 7.2.3.13: Time
- Robinson, 2017: Sheaves are the canonical datastructure for sensor integration (doi, arxiv)
- Schultz & Spivak, 2019: Temporal type theory: A topos-theoretic approach to systems and behavior (doi, arxiv)