The Sheaf Condition

Exact matching and unique amalgamation

14 min read

Text size

A13Written accountFor a sheaf, matching local sections have a unique gluing; existence and uniqueness require their stated hypotheses.

Concordia discordantium canonum — The Harmony of Discordant Canons.
— Title of Gratian’s Decretum; English rendering

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 the universal passage from a presheaf to a sheaf; it does not select which conflicting source deserves belief. The touchstones examined 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?

A map assembled from tiles must preserve the roads and boundaries its readers will follow across joins. A document assembled from contributions may instead preserve a disagreement by recording who said what. Both operations combine material, but they promise different results. The sheaf condition gives one exact account of assembly¹: a specified family is reproduced by a single section through its restriction maps.

Remark(Intuition: A Document Merge)

Suppose a hypothetical editor promises a document whose restriction to each submitted passage reproduces that passage exactly. Two contributors supply opposed sentences at the same designated location. A record containing both versions remains possible, as does a revised document. Neither is the promised exact reproduction of both at that one location under the stipulated restrictions.

If the representation is a sheaf and the submitted sections match exactly on a cover, the corresponding amalgamation exists uniquely. Ordinary editing software does not acquire those hypotheses merely by comparing text. Its handling of conflict is part of its own declared behavior.

Locality: No Hidden Globals

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

Locality

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.

Two global sections with the same restrictions on the cover must be equal. The axiom makes those views sufficient to distinguish the sections the model admits. It does not establish that the model records every relevant fact about the world.

Example

Suppose two project records differ in an integration setting that none of the module views includes. If both restrict to exactly the same module records, those views fail locality for the chosen project-record presheaf: the global difference is invisible to the cover. A build server reporting success while a module reports failure is a different problem—its proposed global answer conflicts with a local record. Neither problem is cured by merely calling the module views a cover.

Locality concerns distinguishability. Existence requires another condition.

Gluing: Matching Locals Produce Unique Globals

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

Matching Family

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.

Gluing

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.

In a sheaf, exact agreement establishes existence and uniqueness of the global section. A procedure that computes it requires an effective construction. In an arbitrary presheaf, matching alone does not establish existence.

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 the declared restrictions produce unequal values, the family fails matching. If the comparison depends on an equivalence that has not been established, the check is incomplete. The system retains the local claims without certifying their amalgamation; it must not report missing evidence as a verified disagreement.

This gluing supports a global section that reproduces the specified local family. Other global conclusions may rest on independent evidence or a different construction; their grounds must be established separately.

The Sheaf Condition

A13

Sheaf (A13)

A presheaf F : C^op → Set on site (C, J) is a sheaf iff for every cover $\{U_i \to U\}$ ²:

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³ 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.

A13 identifies the sections of this specified sheaf with its exactly matching local families. Whether those sections adequately represent the evidence is a separate obligation of the model.

Remark(Scope: Set-valued presheaves)

The definition uses Set-valued presheaves and exact equality on overlaps. A set can contain real numbers, probability distributions or time-indexed records; those subjects do not by themselves require approximate equality. The unsettled step is replacing equality with tolerance or graded agreement while retaining a gluing guarantee. Overlapping confidence intervals, for example, do not establish a unique shared value. Appendix L, §L.8, Problem 8 leaves the required enriched theory open. The exact results below cannot certify that extension.

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

Consider the candidate local tuple ("navy", "dark blue", "navy"). The two parallel arrows compare the restrictions of its entries. If the declared maps produce unequal values on A∧B, this tuple is not matching and cannot be the restriction of a global section. Restrictions of an actual global section necessarily match by functoriality. A new comparison map or coarser representation changes the proposed construction; it does not retroactively make the original values equal.

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: Distinct global sections have identical local restrictions. The chosen views do not distinguish a difference retained by the global record.

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 failure of the sheaf property for the specified cover and presheaf, not necessarily a failure of coverage or an unavailable algorithm.

These failures concern the specified sections and cover. They need not indicate misconduct or an unusable system. They identify which local-to-global guarantee this representation cannot supply.

Obstruction Witness

When a check establishes unequal restrictions, the proposed interface returns an obstruction witness for that failure. For cover $\{U_i \to U\}$ , it records:

The family $\{s_i\}$ of local sections
The overlaps $U_i \wedge U_j$ where unequal restrictions were established
Provenance for each conflicting claim
Proposed remediation and its new obligations: revise the comparison, supply evidence, change the representation or retain separate claims

A matching family with no amalgamation has no unequal pair to report. Failure to establish existence, an undecidable comparison and an exhausted checking budget likewise need their own status. A useful failure record tells the recipient which obligation failed or remains open.

For a finite cover with effective restriction maps and decidable equality, the disagreeing pairs can be computed and recorded: “contexts $U_i$ and $U_j$ disagree on this overlap, with these values.” Appendix K.7 states and proves the obstruction-localization result. Its disagreement set identifies exactly those unequal pairs. Separation supplies at most one amalgamation; the sheaf hypothesis also supplies existence. These are additional properties of the representation, not discoveries made by finding the disagreement set empty.

That difference governs what a completed check can report. If equality cannot be decided or the comparison stops before covering the required pairs, an empty list of discovered conflicts is not a certificate that the family matches. If all pairs have been checked and match, the recipient still needs the appropriate sheaf hypothesis to invoke the existence and uniqueness guarantee. The ObstructionWitness records a demonstrated disagreement; it cannot stand in for every reason a gluing has not been established.

Touchstones Transformed

The touchstones reveal different prerequisites for this exact comparison.

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. No global section can restrict to both members of this nonmatching family. This does not exclude a separately supported conclusion about P(x). The system records the obstruction: the views, the overlap, the conflicting claims, the remediation options.

In T1, the sheaf condition is doing its job, blocking incoherent gluing.

T2 (Reference) requires evidence before a matching problem is settled. Different names do not imply different referents. A witnessed identification can supply a proposed common representation for the observations. Only then can the declared restrictions be checked. Missing identity evidence is not itself a verified unequal pair.

T7 (Contextual Equivalence) requires the comparison to preserve meaning. In the hypothetical location example, one source uses a term for a district and another for the encompassing city. A representation can retain both descriptions. Treating them as one boundary requires evidence the example does not supply; a common spelling cannot discharge it.

CAP and the Operational Burden

The CAP result concerns the compatibility of atomic consistency and availability under its network-partition model⁴. It is not derived from the sheaf axiom, and its consistency requirement is not merely equality of arbitrary local semantic descriptions.

There is a practical connection to this chapter's concern. A system may lack the communication needed to establish a promised global condition when a request arrives. The implementation must specify which operations wait, fail or proceed under a weaker contract. More money or a larger declared checking budget does not by itself restore the missing communication.

Consensus protocols such as Paxos⁵ and Raft⁶ address their own agreement and replication problems under stated assumptions. A correct implementation of one does not establish that two source vocabularies mean the same thing. The site, the data and their restrictions still need to be supplied.

Sheafification

For a presheaf $F$ , sheafification supplies a sheaf $aF$ and a map $F \to aF$ through which every map from $F$ to a sheaf factors uniquely⁷. This is its meaning as a best approximation. It is not a rule for deciding which merchant to believe.

The usual plus construction takes matching families modulo agreement after refinement. Applying it twice yields the sheafification. It can add amalgamations and identify sections that are locally indistinguishable. Simply collecting compatible rows or deleting a disagreeing branch is a different operation.

Example

If merchants A and C report navy while B reports royal blue, a receiving catalog might retain the separate reports, seek better evidence, narrow the comparison or adopt a documented reconciliation. Those choices have different consequences for B's report. The sheafification theorem does not select one of them.

There need not be a unique largest consistent sub-presheaf: different choices can preserve incompatible branches. Calling one choice “the coherent core” would hide the selection it made. What the mathematics supplies is a universal construction relative to a declared site and presheaf. Whether that construction is an adequate representation of the records is a further question the engineer must answer.

The Exact Case of A5

A5 (Chapter 5) asked for local definability, overlap agreement and invariant preservation. A12 and A12b (Chapter 10) supplied the site structure. A13 now gives the exact case: every matching family has a unique amalgamation when the specified presheaf is a sheaf.

The invariants must belong to the construction whose sheaf property is established. Filtering an existing sheaf afterward can destroy that property. A matching family may then have no invariant-satisfying amalgamation, although every overlap comparison succeeded. Calling the result “coherent” cannot repair the missing existence proof.

Theorem: Gluing Correctness

The following theorem, drawn from standard sheaf theory⁸, 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 restricts to all the members of that family. The failure is localized to the specific overlap(s) where disagreement occurs, producing an obstruction witness per the definition above.

∎

The proof identifies the work the recipient can inherit: existence and uniqueness follow from the established sheaf structure once this family has been shown to match. It does not furnish an algorithm for arbitrary data or establish that the chosen sections represent the evidence adequately. An implementation must supply its restriction maps and checking method; the representation must carry the invariants whose preservation is claimed.

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? A presheaf already assigns potentially different sets of sections to different contexts. The next chapter makes type dependence and reindexing themselves explicit through a fibration. That variation is not an edge case; it is the common case for any predicate involving preference, value, or evaluation.

Explore Res Agentica

Reading

The Sheaf Condition

The Promise of Gluing

Locality: No Hidden Globals

Gluing: Matching Locals Produce Unique Globals

The Sheaf Condition

Failure Modes

Touchstones Transformed

CAP and the Operational Burden

Sheafification

The Exact Case of A5

Theorem: Gluing Correctness

Search the book

In this chapter