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 sequence of abelian sheaves is exact exactly when it is exact on every stalk
Statement
Let
be a sequence of sheaves of abelian groups on a topological space . Then the sequence is exact if and only if, for every point , the stalk sequence
is exact.
Facts & Assumptions
Given: A sequence of sheaves of abelian groups on .
Exactness of a sequence of sheaves means exactness in the abelian category of sheaves, so at each middle term the image sheaf equals the kernel sheaf (Exact sequences of sheaves).
Stalks are germs of neighbourhood sections (The stalk of a presheaf at a point).
Kernels are objectwise, while images and cokernels are obtained by sheafifying the corresponding presheaves (Kernel sheaves are objectwise, while cokernels and images are sheafified).
Sheafification preserves stalks (Sheafification preserves stalks).
A morphism of sheaves is an isomorphism exactly when it is so on every stalk (A morphism of sheaves is an isomorphism exactly when it is an isomorphism on every stalk).
Proof
Assume the sheaf sequence is exact. At each middle term , [F1] says that the canonical map is an isomorphism. Using [F2] for the stalk construction and then [L1] and [L2], its stalk at is the canonical map so the stalk sequence is exact at . Since was arbitrary, the whole stalk sequence is exact.
Conversely, assume every stalk sequence is exact. For each middle term, consider the canonical morphism . Using [F2] for the stalk construction and then [L1] and [L2], its stalk at is which is an isomorphism by the stalkwise exactness hypothesis. Therefore [L3] implies that is an isomorphism of sheaves.
By [F1], step 1.2 is exactly the assertion that the original sequence is exact. Together with step 1.1, this proves the equivalence.
Depends on
- Exact sequences of sheaves
- The stalk of a presheaf at a point
- Sheaves of abelian groups, and likewise sheaves of modules on a ringed space, form abelian categories
- A morphism of sheaves is an isomorphism exactly when it is an isomorphism on every stalk
- Kernel sheaves are objectwise, while cokernels and images are sheafified
- Sheafification preserves stalks
Used by
- Degree is additive on invertible sheaves over a proper curve Corollary
- Twisting the exact sequence of an effective Cartier divisor Corollary
- A global section of the quotient that does not lift, and its nonzero connecting class Counterexample
- Compactly supported global sections and their right derived functors Definition
- Principal parts of an invertible sheaf on a curve Definition
- A short exact sequence of abelian groups gives a short exact sequence of skyscraper sheaves Example
- Compact support and softness on a finite discrete space Example
- A surjective ring map induces a closed immersion of affine spectra Lemma
- Abelian sheaves form a Grothendieck category Lemma
- Analytic field sheaves have injective derived models Lemma
- Bounded fibrewise-soft resolutions from a uniform all-sheaf dimension bound Lemma
- Closed immersions are affine quotients and survive base change Lemma
- Cofinal Čech vanishing implies derived acyclicity Lemma
- Compact-support acyclicity of c-soft sheaves Lemma
- Compact-support calculus along open and closed embeddings Lemma
- Complex algebraic constructible complexes have finite conical cochain models Lemma
- Derived tensor product of abelian sheaves Lemma
- Derived tensor–Hom and inverse/direct image for field sheaves Lemma
- Effective Cartier divisors give a short exact sequence Lemma
- Enough injective sheaves of modules Lemma
- Extension by zero and the closed complement: a short exact sequence Lemma
- Extensions of line bundles on the projective line split after ordering Lemma
- Finite filtration of a generated subsheaf of the constant integer sheaf Lemma
- Finite simplicial constructible sheaves have an actual derived incidence model Lemma
- Finite twisted locally free resolutions on projective space Lemma
- Finite twisted resolutions over a regular local base Lemma
- Flasque kernel lifts quotient sections Lemma
- Flat resolutions of abelian sheaves and K-flatness of bounded-above flat complexes Lemma
- Flatness criteria and canonical epimorphisms from flat abelian sheaves Lemma
- Global sections on module sheaves have ordinary sheaf cohomology as derived functors Lemma
- H¹ of a line bundle on a curve as principal parts modulo meromorphic and regular sections Lemma
- High-degree section module is finite graded Lemma
- Hypersurface cohomology sequence Lemma
- Injective abelian sheaves are flasque Lemma
- Injective modules are flasque and Ext from the structure sheaf is cohomology Lemma
- Koszul sheaf Ext of a smooth regular immersion is concentrated in codimension Lemma
- Local-section formula for derived direct image Lemma
- Locally split Cech nerves give actual derived Cartesian sheaf descent Lemma
- Noetherian devissage for coherent proper pushforward Lemma
- Nonzero maps from an invertible sheaf to a locally free sheaf are injective Lemma
…and 26 more results.
Dependency tree · two levels
21 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, Lemma 17.3.2 (standard reference, not scraped)
- Ravi Vakil, The Rising Sea, Exercise 2.6.D (standard reference, not scraped)