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.
The stalk of an inverse image sheaf is the stalk over the image point
Statement
Let be a continuous map, let be a sheaf on , and let . Then there is a canonical isomorphism
Facts & Assumptions
Given: A continuous map , a sheaf on , and a point .
The inverse image sheaf is the sheafification of the presheaf (Inverse image presheaf and inverse image sheaf).
A stalk is the colimit of sections over neighbourhoods of the point (The stalk of a presheaf at a point).
Sheafification preserves stalks (Sheafification preserves stalks).
Proof
By [F1] and [L1], it is enough to identify the stalk .
If with , then and defines a class . Sending the germ to the germ of at gives a map If two representatives agree on a smaller neighbourhood of , then their induced sections agree on the inverse image of that smaller neighbourhood, so is well defined.
Conversely, represent a germ in by a section with and . Since , the section has a germ . This depends only on the original germ at , because equality of germs in means equality after restricting to some smaller neighbourhood of , hence after restricting and to some common neighbourhood of . Thus there is a map
The maps and are inverse on representatives, so . Step 1.1 then gives .
Depends on
Used by
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, Lemma 6.21.5 (standard reference, not scraped)
- Ravi Vakil, The Rising Sea, Exercise 2.7.C (standard reference, not scraped)