LemmaStatement: Literature-sourcedProof: 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 sheaf with no stalks off a closed subset is a pushforward

Statement

Let $i : Z ↪ X$ be the inclusion of a closed subset $Z \subseteq X$ carrying the subspace topology (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace), and let $G$ be a sheaf of abelian groups on $X$ (A sheaf on a topological space, Sheaves of abelian groups, and likewise sheaves of modules on a ringed space, form abelian categories) whose stalks vanish off $Z$ , that is $G_{x} = 0$ for every $x \in X ∖ Z$ (The stalk of a presheaf at a point). Then the unit $η : G ⟶ i_{*} i^{- 1} G$ of the adjunction (Inverse image is left adjoint to direct image on sheaves) between inverse image and direct image (Direct image of a sheaf along a continuous map, Direct image preserves sheaves and objectwise algebraic structure) is an isomorphism of sheaves of abelian groups; equivalently $G ≅ i_{*} (G ∣_{Z})$ under the identification $G ∣_{Z} = i^{- 1} G$ (Restriction of a sheaf to an open subspace).

Facts & Assumptions

[F1]

Direct image is $(f_{*} F) (V) = F (f^{- 1} (V))$ on open $V \subseteq Y$ (Direct image of a sheaf along a continuous map), and it sends sheaves to sheaves (Direct image preserves sheaves and objectwise algebraic structure).

[F2]

The stalk of a presheaf at $x$ is the filtered colimit of its section groups over the open neighbourhoods of $x$ (The stalk of a presheaf at a point).

[F3]

For a sheaf $F$ of sets, $F (\emptyset)$ is a singleton (A set-valued sheaf has a unique section over the empty open set).

[F4]

Open subsets of the subspace $S \subseteq X$ are exactly the traces $U \cap S$ of open subsets of $X$ (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).

[F5]

Inverse image is left adjoint to direct image, ${Hom}_{X} (f^{- 1} G, F) ≅ {Hom}_{Y} (G, f_{*} F)$ , with unit the adjunct of the identity of $f^{- 1} G$ (Inverse image is left adjoint to direct image on sheaves).

[F6]

The stalk of an inverse image is the stalk at the image point, $(f^{- 1} G)_{x} ≅ G_{f (x)}$ (The stalk of an inverse image sheaf is the stalk over the image point).

[F7]

A morphism of sheaves of sets is an isomorphism if and only if all its stalk maps are bijections (A morphism of sheaves is an isomorphism exactly when it is an isomorphism on every stalk).

Proof

Given: A closed subset $Z \subseteq X$ with inclusion $i$ , a sheaf of abelian groups $G$ on $X$ with $G_{x} = 0$ for all $x \in X ∖ Z$ , and the unit $η : G \to i_{*} i^{- 1} G$ of the adjunction of [F5].

1.1

Let $H : = i_{*} i^{- 1} G$ , a sheaf of abelian groups on $X$ by [F1]. For $z \in Z$ the traces $V \cap Z$ of the open neighbourhoods $V$ of $z$ in $X$ are cofinally the open neighbourhoods of $z$ in $Z$ [F4], so [F1] and [F2] give $H_{z} ≅ (i^{- 1} G)_{z}$ , and $(i^{- 1} G)_{z} ≅ G_{z}$ by [F6]. For $x \notin Z$ the open set $X ∖ Z$ contains $x$ and meets $Z$ in the empty set, so the colimit of [F2] is computed by the subdiagram of neighbourhoods $V$ with $V \cap Z = \emptyset$ , on which $H$ has the constant value $(i^{- 1} G) (\emptyset)$ , a singleton by [F3] and hence the zero group; thus $H_{x} = 0$ for every $x \notin Z$ .

F1F2F3F4F6

2.1

Let $z \in Z$ . Composing the stalk map $η_{z} : G_{z} \to H_{z}$ with the identifications of [step 1.1] gives a map $G_{z} \to (i^{- 1} G)_{z} ≅ G_{z}$ , and this composite is the identity: the unit is the adjunct of the identity of $i^{- 1} G$ under the adjunction [F5], a section $s \in G (V)$ over an open $V ∋ z$ is sent to the class of $s$ in the colimit defining $(i^{- 1} G) (V \cap Z)$ because $V$ is one of the open sets tested in that colimit, and the identification $(i^{- 1} G)_{z} ≅ G_{z}$ of [F6] sends that class to the germ of $s$ . Hence $η_{z}$ is an isomorphism for every $z \in Z$ .

F5F6step 1.1

2.2

Let $x \notin Z$ . By hypothesis $G_{x} = 0$ and by [step 1.1] also $H_{x} = 0$ , so the stalk map $η_{x}$ is a map $0 \to 0$ , hence a bijection.

step 1.1

3.1

Every point of $X$ lies in $Z$ or in $X ∖ Z$ , so [step 2.1] and [step 2.2] show that all stalk maps of $η$ are bijections; by [F7] the morphism $η$ is an isomorphism of sheaves of sets, and since $G$ and $H$ are sheaves of abelian groups whose structure is determined by the underlying sheaves of sets with their addition, $η$ is an isomorphism of sheaves of abelian groups. ∎

F7step 2.1step 2.2

Depends on

Used by

Grothendieck vanishing on a Noetherian space Theorem

Dependency tree · two levels

30 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, Sheaves on Spaces (standard reference, not scraped)