The Sheaf Condition: Gluing as the meaning of coherence

A13Machine-checkedThe central theorem: local data that agrees on overlaps determines global data.

Concordia discordantium canonum — The Harmony of Discordant Canons.
— Gratian, Concordia discordantium canonum (c. 1140)

This chapter formalizes coherence as the sheaf condition, defining Anchor A13: a presheaf on the site structure of Chapter 10 is a sheaf when it satisfies locality (no hidden globals) and gluing (matching local sections amalgamate to a unique global section). The equalizer characterization is stated, failure modes are classified as locality violations or gluing failures, and obstruction witnesses are introduced to record structured conflict. Sheafification is presented as the canonical extraction of coherent data from incoherent local claims. The touchstones resolved here -- contradiction (T1), reference (T2), and contextual equivalence (T7) -- correspond to the narrative treatments in Vol I, Chapters 5 ("The Empire of Tables") and 6 ("Evidence without Custody").

The Promise of Gluing

You have local measurements, local claims, local truths. You want a global picture. When is that possible?

Consider a patchwork quilt. Each patch has a color, a texture, a position. The quilt as a whole has a pattern, but only if the patches are stitched correctly at boundaries. A loose thread, a misaligned edge, and the pattern breaks. The global exists only when the locals agree where they meet.

Consider a git merge. Two developers modify the same file. The merge succeeds only if their changes to overlapping lines are compatible. Otherwise, conflict markers appear: <<<<<<< and >>>>>>>, the system's admission that it cannot glue. No global file exists until the conflict is resolved.

Consider map tiles. A cartographer divides a region into squares. Each square is drawn independently. Adjacent squares must match at edges: roads must connect, rivers must flow continuously, elevations must agree. A global map exists only when tiles glue seamlessly.

These are the same problem. Coherence is the stitching condition. The sheaf condition is the formal statement of what "correctly stitched" means(Lane 1992, ch. II).

Remark(Intuition: The Google Doc Merge Conflict)

You and a colleague edit the same Google Doc simultaneously. You change paragraph 3; they change paragraph 7. The system merges automatically—no conflict, because the edits don't overlap.

Now suppose you both edit paragraph 5. You write "the project succeeded"; they write "the project failed." The system cannot merge. It shows both versions and asks a human to resolve.

This is the sheaf condition in miniature:

Local edits are your changes and their changes.
Overlaps are paragraphs you both touched.
Matching means your overlapping edits agree (or at least don't contradict).
Gluing is the merged document that incorporates both contributions.

If overlaps match, a global document exists. If overlaps disagree, no global document exists until a human resolves the conflict. The system cannot pretend coherence where there is none.

The sheaf condition says: local truths glue into global truth if and only if they agree where they overlap. Every distributed system faces this problem—databases, blockchains, version control, sensor networks. The mathematics of sheaves is the general theory of when gluing is possible.

Locality: No Hidden Globals

The first axiom is locality: a global section is determined by its local restrictions.

For presheaf F on site (C, J): if s, t ∈ F(U) and $s|_{U_i} = t|_{U_i}$ for all $U_i$ in a cover of U, then s = t.

If two global sections restrict to the same locals everywhere, they are equal. There is no "extra" global information beyond the locals. No hidden state, no privileged vantage point, no God's-eye view that differs from what the local observers see.

A global claim is fully determined by its local appearances. If you know what the claim says in every context of the cover, you know everything. The system cannot appeal to a "global database" that lives outside the views.

Example

In a build system, treat the project context U as covered by the module contexts $\{U_\text{auth}, U_\text{payments}, \ldots\}$ . A global "dependency resolved" claim is determined by the per-module resolution. If every module reports success on the same version configuration, the project is resolved. There is no separate "project-level" truth that differs from the modules. If the build server claims success but a module claims failure, the locality axiom is violated. Something is hiding information.

Locality prevents systems from asserting global facts that have no local evidence. It is a sanity check: every global claim must be grounded in locals.

Gluing: Matching Locals Produce Unique Globals

The second axiom is gluing: if local sections agree on overlaps, they amalgamate to a unique global.

For cover $\{U_i \to U\}$ , a matching family is a collection $\{s_i \in F(U_i)\}$ such that for all pairs i, j:

s_i|_{U_i \wedge U_j} = s_j|_{U_i \wedge U_j}

where $U_i \wedge U_j$ is the overlap (pullback in general; meet in the poset simplification). When working in the general categorical setting, we write $U_i \times_U U_j$ for the fiber product; in poset examples, $\wedge$ denotes the meet.

A presheaf F satisfies gluing iff every matching family has a unique amalgamation: a section s ∈ F(U) such that $s|_{U_i} = s_i$ for all i. We call this the glued global section.

If all views agree on the overlaps, you can construct a global. If they don't agree, you cannot. The sheaf condition blocks incoherent claims from pretending to be global.

Example

Three merchants cover a fashion catalog. Each asserts a color for item X:

Merchant A: "navy"
Merchant B: "dark blue"
Merchant C: "navy"

On overlap A ∧ B, merchant A's "navy" and merchant B's "dark blue" must agree. Do they? If the system has a witness navy ∼ dark_blue in that scope (from A10), yes. The matching condition holds. The amalgamation is the global color claim "navy/dark_blue" (equivalence class). In this presheaf, values are taken modulo the witnessed equivalence relation in the relevant scope.

If no such witness exists, the matching condition fails. The system cannot assert a global color for X. It records three local claims and a conflict on A ∧ B.

Gluing is the license to "promote" local claims to global. Without it, you can only speak locally. With it, coherent locals become global.

The Sheaf Condition

A13

A presheaf F : C^op → Set on site (C, J) is a sheaf iff for every cover $\{U_i \to U\}$ (Lane 1992, ch. II, §1):

Locality: s = t whenever $s|_{U_i} = t|_{U_i}$ for all i
Gluing: Every matching family has a unique amalgamation

Equivalently: F(U) is the equalizer(Lane 1971, ch. III, §4) of the diagram

F(U) \to \prod_i F(U_i) \rightrightarrows \prod_{i,j} F(U_i \wedge U_j)

The two parallel arrows restrict sᵢ and sⱼ to their common overlap. The equalizer is the set of tuples where both arrows agree: exactly the matching families, with unique amalgamation.

The equalizer diagram is compact, but its meaning is plain: global = exactly those local tuples that agree on overlaps. No more, no less.

A sheaf is a data structure where the only global facts you are allowed to assert are the ones you can reconstruct from agreeing local facts. A13 is the rule that decides when "local" is allowed to become "global."

Remark(Scope: Set-valued presheaves)

The definition uses Set-valued presheaves: F assigns to each context a set of claims, and matching requires exact equality on overlaps. This suffices for discrete, exact-equality claims (type checks, schema validation, deterministic assertions). For probabilistic claims (where "matching" is approximate), continuous values (where equality must be replaced by tolerance), or temporal claims (whose truth changes), the sheaf machinery requires extension to presheaves valued in richer categories (topological spaces, probability spaces, or filtered colimits). The framework does not develop these extensions; the core results apply to the discrete case. Extending to graded or approximate matching is a natural direction for future work.

Example

Let F(U) = "color claims for item X in context U."

F(catalog) = global color claim
F(merchant_A), F(merchant_B), F(merchant_C) = local claims
F(A ∧ B), F(B ∧ C), F(A ∧ C) = claims on overlaps

The first arrow restricts a hypothetical global "navy" to the tuple ("navy", "dark blue", "navy"). The two parallel arrows compare: restrict "navy" from A to A∧B versus restrict "dark blue" from B to A∧B. If these disagree, that tuple is not a matching family, so it cannot be the restriction of any global section. No global color exists given those locals without additional witnesses or coarsening.

A global claim is not one that holds everywhere. It is one whose local forms agree wherever the views meet.

Failure Modes

A presheaf assigns data to contexts with restriction maps, but it may fail to be a sheaf. There are two ways to fail:

Fail locality (hidden global): There exist distinct global sections with identical local restrictions. The system has information that no view can see. This is the "God's-eye view" anti-pattern. A master record differs from all local views; no one can access the truth.

Fail gluing (orphan locals): Matching families exist but do not amalgamate. Local claims agree on overlaps, yet the system cannot construct a global. This happens when "global" requires an identification or constraint not present in any single view: the locals match pairwise, but there is no consistent object that realizes them all. This is a coverage failure: the cover is insufficient, or the gluing mechanism is missing.

Systems that fail the sheaf condition are either hiding information (locality failure) or dropping information (gluing failure). Neither is coherent.

When matching or gluing fails, the system should not merely return an error. For cover $\{U_i \to U\}$ , an obstruction witness records:

The family $\{s_i\}$ of local sections
The minimal overlaps $U_i \wedge U_j$ where agreement fails
Provenance for each conflicting claim
Allowed remediation: refine cover, produce equivalence witness, approximate via adjunction, or isolate

A gluing failure is not an error code—it is a structured object that downstream processes can act on.

Theorem: Obstruction Localization

The following theorem establishes that gluing failures are not merely detectable but precisely localizable. The obstruction set exactly identifies which pairs of contexts disagree and on what.

If $\{s_i\}$ is not a matching family (some $s_i|_{U_i \times_U U_j} \neq s_j|_{U_i \times_U U_j}$ ), we say there is an obstruction to gluing. Define:

\mathrm{Obs}(\{s_i\}) := \{(i, j) \mid s_i|_{U_i \times_U U_j} \neq s_j|_{U_i \times_U U_j}\}

This is the set of disagreeing pairs.

Theorem(Obstruction Localization)

Let $F$ be a presheaf on a site $(\mathbf{Ctx}, J)$ . Let $\{U_i \to U\}_{i \in I}$ be a covering family and $\{s_i \in F(U_i)\}_{i \in I}$ a collection of local sections.

Either:

$\{s_i\}$ is a matching family, in which case there exists at most one $s \in F(U)$ with $s|_{U_i} = s_i$ for all $i$ , or
$\{s_i\}$ is not a matching family, in which case $\mathrm{Obs}(\{s_i\}) \neq \emptyset$ , and this set exactly identifies the pairs $(i, j)$ where the obstruction occurs.

Moreover, if $F$ is a sheaf, case (1) guarantees existence and uniqueness of the gluing.

Proof

We prove each part.

Part 1: Matching implies at-most-one gluing.

Suppose $\{s_i\}$ is a matching family and $s, s' \in F(U)$ both satisfy $s|_{U_i} = s_i$ and $s'|_{U_i} = s_i$ for all $i$ .

Consider the equalizer diagram:

F(U) \xrightarrow{e} \prod_{i \in I} F(U_i) \xrightarrow[\rho_2]{\rho_1} \prod_{i,j \in I} F(U_i \times_U U_j)

where $e(s) = (s|_{U_i})_{i \in I}$ , and $\rho_1, \rho_2$ are the restriction maps to overlaps.

By assumption, $e(s) = e(s') = (s_i)_{i \in I}$ .

The map $e$ is injective for separated presheaves (and hence for sheaves). This separation property is precisely what distinguishes separated presheaves from arbitrary presheaves; for a sheaf, it holds by definition. Since we are proving uniqueness for sheaves, separation applies, and therefore $s = s'$ .

Part 2: Non-matching implies nonempty obstruction set.

Suppose $\{s_i\}$ is not a matching family. Then by definition, there exist $i, j$ such that $s_i|_{U_i \times_U U_j} \neq s_j|_{U_i \times_U U_j}$ . Hence $(i, j) \in \mathrm{Obs}(\{s_i\})$ , so $\mathrm{Obs}(\{s_i\}) \neq \emptyset$ .

Part 3: Obstruction set exactly identifies disagreements.

By construction, $(i, j) \in \mathrm{Obs}(\{s_i\})$ if and only if $s_i|_{U_i \times_U U_j} \neq s_j|_{U_i \times_U U_j}$ . The set contains no spurious pairs and omits no actual disagreements.

Part 4: Sheaf implies existence.

If $F$ is a sheaf and $\{s_i\}$ is a matching family, the sheaf condition guarantees existence of $s \in F(U)$ with $s|_{U_i} = s_i$ . Combined with Part 1, the gluing is unique.

∎

The Obstruction Localization theorem is why the Third Mode can promise auditable failure. The failure is not "something went wrong." It is "contexts $U_i$ and $U_j$ disagree on the overlap $U_i \times_U U_j$ , with these specific values." The ObstructionWitness artifact is the operational realization of $\mathrm{Obs}(\{s_i\})$ .

Touchstones Transformed

The touchstones from Part I are now legible as sheaf-theoretic phenomena.

T1 (Contradiction) becomes overlap disagreement. A claim P and ¬P coexist in different views. On their overlap, both restrictions must agree. They cannot. The matching condition fails. There is no global P(x) or ¬P(x). The system records the obstruction: the views, the overlap, the conflicting claims, the remediation options.

T1 is not a bug to fix—it is the sheaf condition doing its job, blocking incoherent gluing.

T2 (Reference) becomes identity as gluing problem. "Morning Star" and "Evening Star" are different names in different views. On the overlap, the identity must be witnessed. Without the witness from A10, the local identity claims do not match: different names imply different referents. With the witness, they glue. Reference resolution is a matching condition.

T7 (Contextual Equivalence) becomes scoped gluing. "NYC" in the tax context and "NYC" in the shipping context are different entities. They share a name, but their restrictions to any common overlap (say, "locations in New York State") do not agree on boundaries. There is no global "NYC" that restricts consistently to both. The sheaf condition blocks the false merge. If you want a global "NYC," you must define the overlap carefully and produce a witness that the meanings agree there. They probably do not, which is the point.

CAP as Operational Corollary

The CAP theorem says you cannot have Consistency, Availability, and Partition tolerance simultaneously in a distributed system(Brewer 2000)(Lynch 2002). Read this as an operational corollary of the sheaf condition.

Consistency corresponds to enforcing the matching+gluing discipline
Availability means every query returns a result (a local section always exists)
Partition tolerance means the system survives network splits (communication needed to check overlaps may be unavailable)

Under partition, you cannot check overlap agreement in real time. Either sacrifice availability (wait for the partition to heal before answering) or sacrifice consistency (return a local result without matching guarantees).

CAP is a theorem about the cost of maintaining the matching condition under partitions, not about whether the matching condition is correct. The sheaf condition defines what coherence means; CAP says when you can afford to check it.

Distributed consensus protocols (Paxos(Lamport 2001), Raft(Ousterhout 2014)) are precisely the machinery for establishing that matching holds despite partitions. Eventual consistency is the admission that matching is only checked eventually, not synchronously. The sheaf framework does not judge these tradeoffs. It names them.

Sheafification

What if your presheaf is not a sheaf? Sheafification is the process of turning a presheaf into "the best sheaf approximation"(Lane 1992, ch. III, §5).

The idea: take the set of all matching families as the new F(U). Quotient by an equivalence that identifies families which would have glued to the same global. The result is a sheaf: the canonical coherent core of your incoherent data.

Remark

Sheafification is "coherence enforcement." You take incoherent local data and force it through the matching filter. What survives is the coherent part; what does not is either dropped or flagged as conflict.

Example

Your three merchants have conflicting colors. Sheafification would:

Keep the agreements (A and C both say "navy")
Flag A ∧ B as a conflict (no matching)
Produce a "sheafified" color that is partial: defined on A, C, undefined on B until reconciled

The global color exists only where the locals cohere.

Sheafification is not always what you want. Sometimes you want the conflict explicit, with its full provenance and remediation options.

A mathematical note: the general "plus construction" for sheafification can freely add structure, not just truncate. In topos theory, sheafifying a presheaf may create complex objects over overlaps rather than simply deleting rows. What we describe here—keeping coherent data, flagging or dropping the rest—is more precisely the maximal consistent sub-presheaf or separated presheaf that agrees with the original where possible. For engineering purposes, this truncation strategy is usually what you want: extract the largest coherent subset, record the obstruction for the remainder. The general plus construction matters when you need to freely generate glue where none exists; in data integration, you typically want to discover that glue is missing, not manufacture it.

Sheafification (in this truncation sense) maximizes coherence, not fidelity: it keeps what can be justified as global and forces the rest into explicit partiality or conflict. It is the canonical way to extract coherence from incoherence, the mathematical analog of "merge what you can, flag what you cannot."

A5 Fulfilled

A5 (Chapter 5) asked preformally: local definability, overlap agreement, invariant preservation. A12 and A12b (Chapter 10) built the site structure: contexts, covers, restriction maps. A13 delivers the formal content.

Theorem

For the presheaves of interest (claims, attributes, witnesses), coherence is precisely sheafiness relative to the chosen topology, with invariants enforced locally (in each T(U)) and preserved under restriction and gluing.

Proof

The proof has two directions.

Sheaf implies coherence. If $F$ is a sheaf on the site $(\mathbf{Ctx}, J)$ and $\{U_i \to U\}$ is a cover, any family of local claims $\{s_i \in F(U_i)\}$ satisfying the matching condition $s_i|_{U_i \times_U U_j} = s_j|_{U_i \times_U U_j}$ for all $i, j$ amalgamates to a unique global section $s \in F(U)$ . Uniqueness follows from the locality axiom (the restriction map $F(U) \to \prod_i F(U_i)$ is injective for sheaves). Existence follows from the gluing axiom. Together: $F(U)$ is the equalizer of $\prod_i F(U_i) \rightrightarrows \prod_{i,j} F(U_i \times_U U_j)$ . This is precisely A5's requirement: local definability (each $s_i$ is well-formed in $U_i$ ), overlap agreement (matching condition), and unique global amalgamation.

Coherence implies sheaf. Conversely, if every locally defined, overlap-compatible family of claims amalgamates uniquely to a global claim, then $F$ satisfies both locality and gluing. The invariant preservation condition (Obligation 3 from A17) enters at the gluing step: the amalgamation $s$ must satisfy the constraint set $I_U$ . If it does not, gluing fails and an obstruction witness is produced. The sheaf condition thus subsumes A5 with invariants treated as an additional coherence check at the gluing boundary.

∎

Theorem: Gluing Correctness

The following theorem, drawn from standard sheaf theory(Lane 1992, ch. II), establishes the precise guarantee underlying the glue operation.

Theorem(Gluing Correctness)

Let $F : \mathbf{Ctx}^{\mathrm{op}} \to \mathbf{Set}$ be a sheaf on the context site $(\mathbf{Ctx}, J)$ . Let $\{U_i \to U\}$ be a cover of $U$ .

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 \forall\, i, j

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

Proof

The sheaf condition states that $F(U)$ is the equalizer of:
$\prod_i F(U_i) \xrightarrow[\rho_2]{\rho_1} \prod_{i,j} F(U_i \times_U U_j)$
where $\rho_1$ restricts the $i$ -th component to $U_i \times_U U_j$ , and $\rho_2$ restricts the $j$ -th component.
A family $(s_i) \in \prod_i F(U_i)$ is in the equalizer iff $\rho_1(s_i) = \rho_2(s_i)$ , i.e., $s_i|_{U_i \times_U U_j} = s_j|_{U_i \times_U U_j}$ for all $i, j$ .
Existence: The matching condition says $(s_i)$ is in the equalizer. Therefore there exists $s \in F(U)$ that maps to $(s_i)$ under restriction.
Uniqueness: The equalizer is a limit; the map $F(U) \to \prod_i F(U_i)$ is injective (this is the locality condition). Therefore $s$ is unique.

Failure mode: If the matching condition fails (some $s_i|_{U_i \times_U U_j} \neq s_j|_{U_i \times_U U_j}$ ), the family is not in the equalizer, and no global section exists. The failure is localized to the specific overlap(s) where disagreement occurs, producing an obstruction witness per the definition above.

∎

A claim is coherent over a cover iff:

It restricts to well-formed locals (local definability)
The restrictions agree on overlaps (matching condition = overlap agreement)
The amalgamation respects constraints (invariants checked at gluing time)

This is the complete picture. Coherence is not a vibe but the sheaf condition: matching on overlaps, gluing to global, with no hidden extras.

But the picture assumes something it has not examined. When two views overlap and we check agreement, we compare claims of the same type. What happens when the type itself changes across views — when "best" means something different depending on the market segment, when "affordable" varies with currency and context, when the predicate's signature depends on where you are standing? The sheaf condition handles claims that live in a fixed type. It does not yet handle claims whose type varies with context. That variation is not an edge case; it is the common case for any predicate involving preference, value, or evaluation.