lin-0027
0.10 Presheaves, sheaves, and local-to-global reasoning
Many LINCS applications distribute information across overlapping contexts. A presheaf records what is known locally and how it restricts to smaller contexts.
Let \(\mathcal U\) be a category of contexts and inclusions. A presheaf on \(\mathcal U\) with values in \(\mathcal C\) is a contravariant functor
For an inclusion \(V\subseteq U\), it supplies a restriction map \(\rho ^U_V:X(U)\to X(V)\). Functoriality says that restricting in stages agrees with restricting directly.
For the ordinary sheaf condition, take \(\mathcal C=\mathbf{Set}\) and equip \(\mathcal U\) with a specified coverage or Grothendieck topology. Suppose \(U\) is covered by contexts \(U_i\). A family \(x_i\in X(U_i)\) is compatible when its restrictions agree on every overlap:
A sheaf requires every compatible family to arise from a unique global section \(x\in X(U)\). Compatibility is local agreement; effectivity is the existence of the global realization.
The paired arrows compare restrictions to overlaps. In familiar set-valued cases, global sections form an equalizer of those arrows.
A crossword makes the local-to-global structure visible without any categorical machinery. Let \(U_i\) be an across or down slot and let \(X(U_i)\) be the set of candidate words licensed by its clue and length. If slots \(U_i\) and \(U_j\) meet at a square \(c\), restriction extracts the letter occupying that square:
where \(\Sigma \) is the alphabet. The local answers are compatible exactly when the two extracted letters agree.
For example, an across candidate cat restricted at its second square and a down candidate are restricted at its first square both produce a. Replacing the down candidate by ore produces o; the failure is localized to that crossing. A family of answers that agrees at every crossing glues to a unique completed grid relative to those local answers.
The same puzzle can be read as a sketch. Word slots, crossing cells, letters, and clue-licensed answer sets are typed objects; letter extraction supplies the arrows. The declaration says that the two routes into every crossing must agree, while a designated limit identifies a completed grid with the compatible family of its word-level restrictions. The sketch states the rules of the puzzle; the sheaf organizes its local solutions and their gluing. A wrong crossing is therefore a small, typed obstruction rather than a scalar score saying only that the grid is bad.
Each foundry maintains a local predictive state on its own context. Two foundries may agree on every audited pairwise overlap without their family belonging to the admitted class of global predictive models. SID therefore separates compatibility from effectivity and reports which part of the descent declaration fails.
A source passage may support a ground locally, a warrant may connect that ground to a claim, and a qualifier may restrict the claim’s scope. Agreement of isolated text spans is not enough. Their typed roles, source bindings, and restrictions must glue to a coherent argument. A failed warrant or incompatible qualifier is localized to a different part of the sheaf diagram and licenses a different repair.
For an ordinary set-valued sheaf, compatibility on all pairwise overlaps is precisely the gluing hypothesis and already entails coherence on triple overlaps. Apparent higher-order obstructions arise when not all overlaps are observed, when the assignment is only a presheaf, when the admitted global model class is smaller than the sheaf semantics, or in enriched, derived, or higher-categorical versions where genuine cocycle data remain.