Let be a Topological Space and a Presheaf on its poset of opens: is the set of sections over and for the restriction is written .
- Let cover . A matching family is a choice of for each with for all .
- A gluing of is an with for all .
- satisfies the sheaf condition for the cover if every matching family has a unique gluing; is a sheaf if it satisfies the sheaf condition for every cover.
Morphisms of sheaves are natural transformations of the underlying presheaves; the category of sheaves on is a Topos.
Sources: 7 Sketches §7.3 (“a sheaf on a space is roughly ‘a sort of thing that can happen on the space’”), §7.3.3, Definition 7.35, Examples 7.36, 7.45, 7.46, 7.48, Exercises 7.42–7.44, 7.47, 7.49, 7.80; §7.4.1; §7.5.2; CTfS §5.2.3 (Application 5.2.3.1, Definitions 5.2.3.2, 5.2.3.5, Examples 5.2.3.4, 5.2.3.6, Applications 5.2.3.7, 5.2.3.9, Example 5.2.3.10, §5.2.3.11–5.2.3.13, Example 5.2.3.14)
Sheaves in science (Category Theory for Scientists §5.2.3)
“Sheaves allow us to consider the local-global nature of such maps, taking into account reparable discrepancies in data gathering tools.”
- A consistent translation system (CTfS Application 5.2.3.1). Cover the earth with 10 000 overlapping regions , each with its own temperature recorder . On an overlap two devices disagree, but by a known translation (” reads 3° warmer than ”). “A consistent system of translation formulas is called a sheaf. It does not demand a universal ‘true’ temperature function, but only a consistent translation system between them.”
- Gluing measurements (CTfS Examples 5.2.3.4, 5.2.3.6): is covered by , , with overlaps , , ; measurements on the that agree on the overlaps glue to one measurement on . Assigning to a region all temperature assignments between two bounds gives a sheaf; restricting to continuous assignments gives a sub-sheaf (CTfS Exercise 5.2.3.3).
- The night sky (CTfS Application 5.2.3.7): functions from regions of outer space to visible wavelengths nm form a sheaf; the sheaf condition is “the taken-for-granted fact that we can patch together different observations of space” — three overlapping telescope views glue into one image.
- Prediction (CTfS Application 5.2.3.9): knowledge of the temperatures on pulls back along restriction and pushes forward to ; the image is what can be predicted about (“warm in Texas, Arkansas and Kansas ⇒ not cold in Oklahoma”). Laws that agree on the overlap of two jurisdictions (“no hunting near rivers” on , “no hunting in public areas” on , where public areas and river banks coincide) glue to one law on (CTfS Example 5.2.3.10).
- Shared worldviews (CTfS §5.2.3.11): on a Simplicial Complex of people, assign to every simplex the Olog of concepts its members share; a face inclusion gives a schema morphism, and after passing to the Alexandrov topology this is a sheaf of categories. Over the union of the simplices and one gets the concepts shared by on which agree with .
- Valid time (CTfS §5.2.3.13, Example 5.2.3.14): information holding throughout a time interval restricts to subintervals and glues along overlaps, so a time-varying database is a sheaf of -sets on . In a maternity ward, nurses on overlapping 8-hour shifts (00–08, 04–12, 08–16) record only patients present throughout; a baby born at 05:00 appears in the overlap but not in . Compare the Topos of Behavior Types.
Remarks and examples
- Empty cover (Example 7.36): the empty family covers , and the empty tuple is its only matching family; so a sheaf must have — a necessary but rarely sufficient condition.
- Sections of a function/bundle (Example 7.45): for continuous , is a sheaf on ; see Sheaf of Sections. Vector fields on a manifold are the sections of the tangent bundle (Example 7.46); this is one sheaf among a proper class of sheaves on (7S Exercise 7.47).
- Constant sheaf (Example 7.78): for a set — behaviours that never change. (Strictly, this is a sheaf on spaces whose opens are connected, like basic opens of .)
- Local functions (Example 7.79, 7S Exercise 7.80): and, for a subspace , are sheaves: continuous functions agreeing on overlaps glue.
- Trivial covers: if every object covers only itself, sheaves = presheaves; so presheaf categories (-, C-sets, graphs) count as sheaf toposes (footnote 10). (Example 7.48, 7S Exercise 7.52).
- The Subobject Classifier of is the sheaf ; sheaves on the Interval Domain are behavior types.
- On the Sierpinski Space, a sheaf is just a function (7S Exercise 7.49).
Docs: Vignette: sheaves
# the sheaf of sections of a finite function f : X → Y on the discrete space Y (Example 7.45)
X = ["a1","a2","b1","b2","b3","c1","e1","e2"]
f = Dict("a1"=>"a","a2"=>"a","b1"=>"b","b2"=>"b","b3"=>"b","c1"=>"c","e1"=>"e","e2"=>"e")
fiber(y) = [x for x in X if f[x] == y]
sections(U) = [Dict(zip(U, c)) for c in Iterators.product((fiber(y) for y in U)...)] # Sec_f(U)
restrict(s, V) = Dict(v => s[v] for v in V)
length(sections(["a","b"])) # 6 sections, Eq. (7.39)
length(sections(["a","b","c","d"])) # 0: the fiber over d is empty
# gluing: two sections over U1, U2 agreeing on the overlap glue uniquely over U1 ∪ U2
s1 = Dict("a"=>"a1","b"=>"b2"); s2 = Dict("b"=>"b2","e"=>"e1")
restrict(s1, ["b"]) == restrict(s2, ["b"]) # matching family
merge(s1, s2) # the glued sectionimport Mathlib
#check @TopCat.Presheaf -- (Opens X)ᵒᵖ ⥤ C
#check @TopCat.Presheaf.IsSheaf
#check @TopCat.Sheaf -- the category Shv(X)
#check @TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing -- matching families glue uniquely
#check @TopCat.Presheaf.IsCompatible -- matching family
#check @TopCat.Presheaf.IsGluing
#check @CategoryTheory.Sheaf -- sheaves for a Grothendieck topology J on a site-- a presheaf on a finite poset of opens, with a brute-force sheaf check on one cover
import qualified Data.Map as M
data Presheaf u s = Presheaf { sections :: u -> [s], restrict :: u -> u -> s -> s }
-- unique gluing of a matching family (s_i) over a cover (u_i) of u
sheafCond :: (Eq s) => Presheaf u s -> u -> [u] -> [s] -> Bool
sheafCond p u cover fam = length [ s | s <- sections p u, and (zipWith (\ui si -> restrict p u ui s == si) cover fam) ] == 1