Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 1 result · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Constructible Incidence And Cochain Models Examples

1 · Prerequisites

2 · Summary

Objective. This companion page works the smallest non-trivial incidence computation of its A page. The closed interval is stratified by its two endpoints and its open edge, and a finite constructible sheaf is recorded by three vector spaces $V_{0}, V_{1}, V_{e}$ with generization maps $u_{0} : V_{0} \to V_{e}$ and $u_{1} : V_{1} \to V_{e}$ . The incidence cochains of the face poset reduce, after an invertible change of coordinates that strips off a contractible summand, to the two-term complex $[V_{0} \oplus V_{1} \overset{u_{0} - u_{1}}{\to} V_{e}]$ in degrees zero and one, so the actual derived global sections are not merely modelled but computed. The two boundary computations are then read off: the constant sheaf has cohomology $k$ in degree zero and nothing above, while the extension by zero of $k$ on the open edge has one copy of $k$ in degree one and vanishes in degree zero. The example depends only on the incidence lemma of constructible-incidence-and-cochain-models and finite linear algebra.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

Incidence cochains of a closed interval

Example

Assume AC (The Axiom of Choice). Stratify the closed interval by its endpoints and open edge. A finite constructible sheaf has vector spaces $V_{0}, V_{1}, V_{e}$ with generization maps $u_{0} : V_{0} \to V_{e}$ and $u_{1} : V_{1} \to V_{e}$ . Its actual derived global sections are computed by $[V_{0} \oplus V_{1} \overset{u_{0} - u_{1}}{\to} V_{e}],$ in degrees zero and one. Thus a constant sheaf $k$ has cohomology $k$ in degree zero and zero otherwise. Extension by zero of $k$ on the open edge has one copy of $k$ in degree one and zero otherwise.

Facts & Assumptions

Given: The Axiom of Choice The Axiom of Choice, a field $k$ , the full $1$ -simplex $K$ with nonempty faces $v_{0}, v_{1}, e$ with $D = \emptyset$ and realization the closed interval $X = ∣ K ∣$ (The geometric realization of an abstract simplicial complex), and a sheaf $F$ on $X$ which is finite-rank locally constant on every open simplex, so that by the incidence model it corresponds to the finite-dimensional diagram with $V_{0} : = F_{v_{0}}$ , $V_{1} : = F_{v_{1}}$ , $V_{e} : = F_{b_{e}}$ , where $b_{e}$ is the midpoint of the open edge and generization maps $u_{0} : V_{0} \to V_{e}$ , $u_{1} : V_{1} \to V_{e}$ . Cohomology is derived global sections (Sheaf cohomology as right derived global sections) and the constant sheaf is the sheaf of locally constant functions (The constant sheaf is the sheaf of locally constant functions); extension by zero is that of Extension by zero for abelian sheaves on an open subspace.

[F1]

Actual derived incidence model (Finite simplicial constructible sheaves have an actual derived incidence model): the exact realization of finite-dimensional diagrams realizes $F$ as $q^{- 1} V$ , and ordinary cohomology of $q^{- 1} V$ has a bounded finite cochain model computed from the diagram, agreeing with the derived global sections; the model is the finite incidence cochain complex of the diagram on the face poset.

[F2]

Constant sheaf (The constant sheaf is the sheaf of locally constant functions): the constant sheaf $k_{X}$ has sections the locally constant $k$ -valued functions, its stalks are $k$ , and its restriction to every open simplex is constant with value $k$ and identity generization maps.

[F3]

Extension by zero (Extension by zero for abelian sheaves on an open subspace): for the open edge inclusion $j : (0, 1) ↪ X$ , the sheaf $j_{!} k_{(0, 1)}$ has stalk $k$ at points of the open edge and stalk $0$ at the two endpoints, and it is constant on each open simplex; hence its diagram has $V_{0} = V_{1} = 0$ , $V_{e} = k$ and zero generization maps.

[F4]

Choice (The Axiom of Choice): AC is assumed; the computation below is finite linear algebra and uses no further selection.

Verification

1.1F1F4givenconstruct

The face poset is $P = {v_{0}, v_{1}, e}$ with $v_{0} \leq e$ and $v_{1} \leq e$ , and every strict chain has length at most one. The incidence cochain model for the derived inverse limit of the diagram $(V_{0}, V_{1}, V_{e}, u_{0}, u_{1})$ is the two-term complex with $C^{0} = V_{0} \oplus V_{1} \oplus V_{e}$ , $C^{1} = V_{e} \oplus V_{e}$ and differential $d (v_{0}, v_{1}, w) = (w - u_{0} v_{0}, w - u_{1} v_{1})$ ; by [F1] the cohomology of this complex is the actual derived global sections of $F$ , so $R^{i} Γ (X, F)$ vanishes outside degrees $0$ and $1$ .

2.1step 1.1algebra

Change coordinates invertibly in the source by $t : = w - u_{1} v_{1}$ and in the target by $(u, v) : = (first output - second output, second output)$ . In the new coordinates the differential is $d (t, v_{0}, v_{1}) = (u_{1} v_{1} - u_{0} v_{0}, t)$ , which is the direct sum of the identity map $V_{e} \overset{i d}{\to} V_{e}$ and the two-term complex $[V_{0} \oplus V_{1} \overset{u_{0} - u_{1}}{\to} V_{e}]$ after multiplying the first target coordinate by $- 1$ . The identity summand is contractible, so $R^{i} Γ (X, F) ≅ H^{i} [V_{0} \oplus V_{1} \overset{u_{0} - u_{1}}{\to} V_{e}]$ in degrees $0$ and $1$ and is zero in all other degrees.

3.1step 2.1F2F3algebra∎

For the constant sheaf $F = k_{X}$ we have $V_{0} = V_{1} = V_{e} = k$ with both generization maps the identity by [F2], so the difference map $k \oplus k \to k$ is surjective with kernel the diagonal copy of $k$ ; hence $H^{0} = k$ and $H^{1} = 0$ , and all higher cohomology vanishes by step 2.1. For $F = j_{!} k_{(0, 1)}$ the diagram is $V_{0} = V_{1} = 0$ , $V_{e} = k$ with zero maps by [F3], so the two-term complex reduces to a single copy of $k$ in degree $1$ ; hence $H^{1} = k$ , $H^{0} = 0$ and all other cohomology vanishes. This proves both stated computations, and no step selects from a family, so no choice beyond the inherited AC is used by the computation.

Sources

Mark Goresky, Lecture Notes on Sheaves and Perverse Sheaves, version of June 26, 2026