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.
Local-section formula for derived direct image
Statement
Assume the Axiom of Choice and the Axiom of Dependent Choice. Let be a morphism of schemes (Morphisms of schemes) and let be an -module (Modules on a ringed space). Then for every the higher direct image sheaf (Higher direct image of a sheaf) is the sheafification (Sheafification of a presheaf) of the presheaf of -modules on the open subsets , where is sheaf cohomology (Sheaf cohomology as right derived global sections). The identification respects restriction maps and the -module structure: the sheafified presheaf is an -module isomorphic to , and for both sides are zero.
Facts & Assumptions
Given: The Axiom of Choice and the Axiom of Dependent Choice, a morphism of schemes and an -module .
Fix the supplied functorial injective resolution datum on of Enough injective sheaves of modules; it gives one specific injective resolution with deleted complex , and is the -th cohomology object of this complex of -modules, with for . (Higher direct image of a sheaf, Injective resolutions in an abelian category)
For open , extension by zero gives an -linear monomorphism : on a stalk in it is the identity on , and on every other stalk its source is zero. Step 1.4 of Enough injective sheaves of modules identifies naturally with for every open . (Flasque sheaf, A sequence of abelian sheaves is exact exactly when it is exact on every stalk)
Under AC every flasque sheaf of abelian groups on a space has for every open and every ; equivalently every restriction is -acyclic. (Flasque abelian sheaves are Γ-acyclic, Gamma-acyclic abelian sheaf)
Under DC the acyclic resolution theorem holds: if is an -acyclic resolution of relative to a supplied injective resolution datum and the syzygies remain in the domain of the datum, then canonically. (The acyclic-resolution theorem for right derived functors)
Under AC the groups are defined as right derived objects of the global-sections functor of relative to the supplied functorial injective resolution datum on abelian sheaves over , and they vanish for . (Sheaf cohomology as right derived global sections, Enough injective abelian sheaves)
A complex of sheaves of -modules has cohomology objects with , ; the image subsheaf of a morphism is the sheafification of its presheaf image. (Cohomology object of a cochain complex, The image sheaf is the sheafification of the presheaf image)
Sheafification is a left adjoint of the inclusion of sheaves: every presheaf morphism into a sheaf factors uniquely through the unit, and sheafification induces bijections on stalks. (Sheafification of a presheaf, Sheafification is left adjoint to the inclusion of sheaves into presheaves, Sheafification preserves stalks)
A sequence of sheaves is exact if and only if it is exact on every stalk; a sequence of -modules is exact if and only if its underlying sequence of abelian sheaves is exact. (Exact sequences of sheaves, A sequence of abelian sheaves is exact exactly when it is exact on every stalk)
For an open subset the sections of the direct image presheaf are . (Direct image of a sheaf along a continuous map)
The global-sections functor on abelian sheaves over a space is additive and left exact. (Global sections are left exact but need not preserve epimorphisms)
Proof
Let be the resolution supplied by the datum of [F1]. Fix open . The map of [F2] is a monomorphism of -modules. Since is injective in , every morphism extends across this monomorphism to . Under the natural identifications of [F2], this is precisely surjectivity of the restriction . Thus every is flasque as an underlying sheaf of abelian groups.
For every open the restricted sheaf is flasque: for open the restriction is the restriction of the flasque sheaf , which is surjective.
For every open the restricted complex is exact at every positive term with as its degree-zero cohomology sheaf: exactness of is checked on stalks [F8], and a point has the same stalks in as in . Hence is a resolution by flasque sheaves.
By [F3] each restricted term is -acyclic, so the resolution of step 3.1 is an acyclic resolution of ; the functorial injective resolution datum on abelian sheaves over the space is defined on the whole category [F5], so every syzygy of that resolution lies in its domain, and the left exactness of the global-sections functor [F10] lets [F4] apply to , giving canonical isomorphisms for every , the right-hand side being the cohomology of the complex of sections.
Let be the complex of -modules with for open [F9]. Its cohomology presheaf is , and the cohomology sheaf of [F6] is the sheafification of this presheaf: indeed has because kernels of sheaf morphisms are computed on opens, is the sheafification of the presheaf by [F6], and passing to the quotient and to stalks, which commute, shows that the sheafified presheaf cohomology and have the same stalk at every point; a morphism of sheaves with bijective stalks is an isomorphism, so the two agree.
Combining steps 4.1 and 4.2, the sheaf is canonically isomorphic to the sheafification of the presheaf . The isomorphism is natural in because every map used above is induced by restriction of sections along inclusions of opens, and for both sides are zero by [F1] and [F5].
Finally the presheaf is a presheaf of -modules: for restriction along is additive and compatible with the ring maps, and the action of is induced by the action of its image in . The action maps are morphisms of presheaves into the sheaf , so by the universal property of sheafification [F7] they descend uniquely to an -module structure on the sheafification, and the isomorphism of step 5.1 is -linear. This proves the statement, and AC and DC are used exactly through the injective resolution datum [F1], the acyclicity [F3] and the acyclic resolution theorem [F4].
Depends on
- Direct image of a sheaf along a continuous map
- Higher direct image of a sheaf
- Right derived objects relative to supplied injective resolution data
- Injective resolutions in an abelian category
- Enough injective sheaves of modules
- Flasque sheaf
- Flasque abelian sheaves are Γ-acyclic
- Gamma-acyclic abelian sheaf
- The acyclic-resolution theorem for right derived functors
- Sheaf cohomology as right derived global sections
- Cohomology object of a cochain complex
- Exact sequences of sheaves
- A sequence of abelian sheaves is exact exactly when it is exact on every stalk
- Sheafification of a presheaf
- Sheafification is left adjoint to the inclusion of sheaves into presheaves
- Sheafification preserves stalks
- The image sheaf is the sheafification of the presheaf image
- Modules on a ringed space
- Global sections are left exact but need not preserve epimorphisms
- Enough injective abelian sheaves
- The Axiom of Choice
- The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain
Used by
Dependency tree · two levels
85 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, Cohomology of Schemes, Chapter 30, §§30.2–30.22 (standard reference, not scraped)
- Ravi Vakil, The Rising Sea (29 August 2022), §§19.1, 19.6, 19.9, 28.1–28.2 (standard reference, not scraped)