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 a tensor product sheaf is the tensor product of the stalks
Statement
Let be a ringed space, let be -modules, and let . Then there is a canonical isomorphism of -modules
Facts & Assumptions
Given: A ringed space , two -modules , and a point .
The sheaf tensor product is the sheafification of the presheaf (Tensor product of sheaves of modules).
Stalks are germs 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 of the tensor-product presheaf
For every neighbourhood of , the germ maps , , and induce an -balanced pairing into . Hence there is a homomorphism and these maps are compatible with restriction. Therefore they induce a map
Conversely, if and are represented by sections and on the same neighbourhood of , define If the representatives are changed on a smaller neighbourhood, the represented germ of is unchanged there, so is well defined on simple tensors and extends linearly to a homomorphism
On a simple tensor represented on one neighbourhood, and plainly undo each other. Since both sides are generated by simple tensors, they are inverse isomorphisms. Combining this with step 1.1 gives the stated isomorphism for the sheaf tensor product.
Depends on
Used by
Dependency tree · two levels
10 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.16.1 (standard reference, not scraped)
- Ravi Vakil, The Rising Sea, Exercise 2.6.J(b) (standard reference, not scraped)