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.
Sheafification preserves stalks
Statement
Let be a presheaf on a topological space . For every , the sheafification map induces a bijection
Facts & Assumptions
Given: A presheaf on and a point .
Sheafification is with unit (Sheafification of a presheaf).
For any presheaf, the first plus construction preserves stalks (The first plus construction is separated and preserves stalks).
Equality in a filtered-colimit stalk is eventual on a smaller neighbourhood (Two representatives in a filtered colimit of sets are equal exactly when they become equal at one common later stage).
Proof
Apply [L1] to the presheaf . This gives a bijection
Apply [L1] again, now to the presheaf . Since [L1] holds for every presheaf, it yields a bijection The reference to [F2] is the same eventual-equality argument used inside [L1] to prove injectivity on stalks.
Composing the bijections of steps 1.1 and 2.1 gives the required isomorphism By [F1], this composite is exactly the map induced by .
Depends on
Used by
- A global section of the quotient that does not lift, and its nonzero connecting class Counterexample
- Sheaf total quotient rings Definition
- A meromorphic unit has locally finite nonzero order support Lemma
- Abelian sheaves form a Grothendieck category Lemma
- Associator, symmetry and unitors of the abelian sheaf tensor product Lemma
- Cartier divisor local equation equivalence 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
- Filtered colimits of sheaves and sections over compact opens Lemma
- Finite filtration of a generated subsheaf of the constant integer sheaf Lemma
- Geometric Gauss-Manin Hodge variations and integral lattices Lemma
- Higher direct images localize over an affine base Lemma
- Local-section formula for derived direct image Lemma
- Locally contractible metric spaces have singular constant sheaf cohomology Lemma
- Sections on a compact set extend to a neighbourhood Lemma
- Stalks, coproducts and right exactness of the abelian sheaf tensor product Lemma
- The constant sheaf is the sheaf of locally constant functions Lemma
- The exact sequence for adding one point to a divisor Lemma
- The stalk of a tensor product sheaf is the tensor product of the stalks Lemma
- The stalk of an inverse image sheaf is the stalk over the image point Lemma
- A sequence of abelian sheaves is exact exactly when it is exact on every stalk Theorem
- Higher direct images of quasi-coherent modules vanish along affine morphisms Theorem
- Sheaves of abelian groups, and likewise sheaves of modules on a ringed space, form abelian categories Theorem
Dependency tree · two levels
9 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, Section 17 (standard reference, not scraped)
- Ravi Vakil, Foundations of Algebraic Geometry, Class 3, Section 4.8 (standard reference, not scraped)