Sheaves and Gluing

Appendix B

2 min read

Text size

A presheaf assigns data to contexts and specifies how data restricts to sub-contexts (Appendix A). A sheaf is a presheaf with a coherence guarantee: local data that agree on overlaps glue into global data, uniquely.

The Sheaf Condition

Sheaf

Let $(\mathcal{C}, J)$ be a site (Appendix A). A presheaf $F : \mathcal{C}^{\mathrm{op}} \to \mathbf{Set}$ is a sheaf if for every cover $\{U_i \to U\}_{i \in I}$ in $J$ :

Locality. If $s, t \in F(U)$ satisfy $s|_{U_i} = t|_{U_i}$ for all $i$ , then $s = t$ .

Gluing. If sections $s_i \in F(U_i)$ satisfy the matching condition:

s_i|_{U_i \times_U U_j} = s_j|_{U_i \times_U U_j} \quad \text{for all } i, j

then there exists a unique $s \in F(U)$ with $s|_{U_i} = s_i$ for all $i$ .

Diagram form. The sheaf condition is an equalizer:

F(U) \xrightarrow{\text{restrict}} \prod_{i} F(U_i) \rightrightarrows \prod_{i,j} F(U_i \times_U U_j)

Sections over $U$ correspond exactly to matching families over the cover.

Locality prevents invisible global distinctions; gluing prevents orphaned local data. Together: global sections are completely determined by local restrictions, and compatible local data always has a global origin.

Sheafification

Given a presheaf $F$ , its sheafification $aF$ has a map $F \to aF$ through which every map from $F$ to a sheaf factors uniquely. This notation distinguishes sheafification from a single application of the usual plus construction, which need not already be a sheaf.

The usual plus construction uses matching families modulo agreement after refinement. It produces a separated presheaf; applying it again gives a sheaf. The construction adds exactly the global sections that should exist and identifies those indistinguishable locally.

Summary

Concept	Role in Coherence
Presheaf	Local data with restriction
Locality	Global sections determined by local restrictions
Gluing	Compatible local data assembles uniquely
Matching condition	Local sections agree on overlaps
Sheafification	Universal map to a sheaf, adding amalgamations and identifying locally equal sections

The sheaf condition formalizes the exact-gluing case of A5 and is stated precisely as A13. A verified unequal pair rules out an amalgamation of that family. In an arbitrary presheaf, a matching family can also lack an amalgamation or have several; the sheaf hypothesis is what excludes those other failures. A computable disagreement report additionally requires effective comparisons.

← Back to Appendices Back to The Proofs →

Explore Res Agentica

Reading

Sheaves and Gluing

The Sheaf Condition

Sheafification

Summary

Search the book

In this chapter