ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6-sol)audited 2026-09-27

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.

A skyscraper sheaf is flasque and acyclic

Example

Assume the Axiom of Choice (The Axiom of Choice). Let $X$ be a topological space, let $x \in X$ and let $A$ be an abelian group, with skyscraper sheaf $i_{x, *} A$ at $x$ with value $A$ (A skyscraper sheaf of abelian groups at a point) and flasqueness as in Flasque sheaf. Then $i_{x, *} A$ is flasque, and for every open subspace $U \subseteq X$ and every integer $q > 0$ the sheaf cohomology of the restriction vanishes, $H^{q} (U, i_{x, *} A ∣_{U}) = 0.$ In particular $H^{q} (X, i_{x, *} A) = 0$ for every $q > 0$ . If $X = \emptyset$ no point $x \in X$ exists and the statement is vacuous.

Facts & Assumptions

[F1]

The skyscraper sheaf at $x$ with value $A$ has $(i_{x, *} A) (V) = A$ when $x \in V$ and $(i_{x, *} A) (V) = 0$ when $x \notin V$ ; for $V^{'} \subseteq V$ with $x$ in both the restriction is the identity on $A$ , and if $x \notin V^{'}$ the restriction to $0$ is the unique zero homomorphism (A skyscraper sheaf of abelian groups at a point).

[F2]

A sheaf of abelian groups $F$ is flasque when all of its restriction maps $ρ_{U}^{V} : F (V) \to F (U)$ , $U \subseteq V$ open, are surjective (Flasque sheaf).

[F3]

Assume AC; if $F$ is a flasque sheaf of abelian groups on $X$ , then $H^{q} (U, F ∣_{U}) = 0$ for every open subspace $U \subseteq X$ and every $q > 0$ (Flasque abelian sheaves are Γ-acyclic).

[F4]

The Axiom of Choice is the statement that every family of nonempty sets has a choice function (The Axiom of Choice).

[F5]

In ZF the Axiom of Choice implies the Axiom of Dependent Choice (AC implies DC implies countable choice).

Verification

Given: The Axiom of Choice, a topological space $X$ , a point $x \in X$ , an abelian group $A$ and the skyscraper sheaf $i_{x, *} A$ at $x$ with value $A$ .

Proof technique: direct.

1.1

Let $U \subseteq V \subseteq X$ be open and consider the restriction map $ρ_{U}^{V}$ of $i_{x, *} A$ . If $x \in U$ then $x \in V$ , so by [F1] both groups are $A$ and $ρ_{U}^{V}$ is the identity of $A$ , which is surjective. If $x \notin U$ then by [F1] the group $(i_{x, *} A) (U)$ is the zero group $0$ , and any map into the zero group is surjective, indeed the only such map is the zero homomorphism; no hypothesis on $V$ is needed for this case. Since $x \in U$ or $x \notin U$ , these two cases exhaust all pairs $U \subseteq V$ of open subsets, so every restriction map of $i_{x, *} A$ is surjective; by [F2] the sheaf $i_{x, *} A$ is flasque.

F1F2

2.1

By [step 1.1] the sheaf $i_{x, *} A$ on $X$ is flasque, so the vanishing theorem [F3] applies to it: for every open subspace $U \subseteq X$ and every integer $q > 0$ the cohomology of the restriction vanishes, $H^{q} (U, i_{x, *} A ∣_{U}) = 0.$ Taking $U = X$ , where the restriction of $i_{x, *} A$ to $X$ is $i_{x, *} A$ itself, gives $H^{q} (X, i_{x, *} A) = 0$ for every $q > 0$ .

F3step 1.1

3.1

The two conclusions are the flasqueness of $i_{x, *} A$ from [step 1.1] and the vanishing $H^{q} (U, i_{x, *} A ∣_{U}) = 0$ for all open $U \subseteq X$ and all $q > 0$ from [step 2.1], in particular $H^{q} (X, i_{x, *} A) = 0$ for $q > 0$ ; note that the flasqueness gives no information in degree zero, where $H^{0} (X, i_{x, *} A) = Γ (X, i_{x, *} A) = (i_{x, *} A) (X) = A$ because $x \in X$ . The Axiom of Choice of [F4] enters exactly once, in [step 2.1]: the vanishing theorem [F3] is proved by applying a supplied functorial injective resolution datum, whose availability is obtained from the Axiom of Choice through the implication to Dependent Choice recorded in [F5]. No further choice is made in this example — the point $x$ is part of the given data, not selected — and the computations of [step 1.1] are case distinctions on whether $x \in U$ . ∎

F4F5step 2.1step 1.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

The Stacks Project, Cohomology of Sheaves (standard reference, not scraped)