Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30
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 f:X→S be a morphism of schemes (Morphisms of schemes) and let F be an OX-module (Modules on a ringed space). Then for every q≥0 the higher direct image sheaf Rqf∗F (Higher direct image of a sheaf) is the sheafification (Sheafification of a presheaf) of the presheaf of OS-modules V⟼Hq(f−1V,F∣f−1V) on the open subsets V⊆S, where Hq is sheaf cohomology (Sheaf cohomology as right derived global sections). The identification respects restriction maps and the OS-module structure: the sheafified presheaf is an OS-module isomorphic to Rqf∗F, and for q<0 both sides are zero.

Facts & Assumptions

Given: The Axiom of Choice and the Axiom of Dependent Choice, a morphism of schemes f:X→S and an OX-module F.

[F1]

Fix the supplied functorial injective resolution datum I on Mod(OX) of Enough injective sheaves of modules; it gives one specific injective resolution 0→F→I0→I1→⋯ with deleted complex Idel, and Rqf∗F=Hq(f∗Idel) is the q-th cohomology object of this complex of OS-modules, with Rqf∗F=0 for q<0. (Higher direct image of a sheaf, Injective resolutions in an abelian category)

[F2]

For open U⊆V⊆X, extension by zero gives an OX-linear monomorphism jU!OU→jV!OV: on a stalk in U it is the identity on OX,x, and on every other stalk its source is zero. Step 1.4 of Enough injective sheaves of modules identifies Hom⁡OX(jW!OW,I) naturally with I(W) for every open W. (Flasque sheaf, A sequence of abelian sheaves is exact exactly when it is exact on every stalk)

[F3]

Under AC every flasque sheaf of abelian groups G on a space X has Hq(U,G∣U)=0 for every open U⊆X and every q>0; equivalently every restriction G∣U is Γ-acyclic. (Flasque abelian sheaves are Γ-acyclic, Gamma-acyclic abelian sheaf)

[F4]

Under DC the acyclic resolution theorem holds: if 0→A→J0→J1→⋯ is an F-acyclic resolution of A relative to a supplied injective resolution datum and the syzygies remain in the domain of the datum, then RnF(A)≅Hn(F(Jdel∙)) canonically. (The acyclic-resolution theorem for right derived functors)

[F5]

Under AC the groups Hq(U,G) are defined as right derived objects of the global-sections functor of U relative to the supplied functorial injective resolution datum on abelian sheaves over U, and they vanish for q<0. (Sheaf cohomology as right derived global sections, Enough injective abelian sheaves)

[F6]

A complex of sheaves of OS-modules has cohomology objects Hq(C∙)=coker⁡(Bq→Zq) with Zq=ker⁡(dq), Bq=im⁡(dq−1); 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)

[F7]

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)

[F8]

A sequence of sheaves is exact if and only if it is exact on every stalk; a sequence of OX-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)

[F9]

For an open subset U⊆X the sections of the direct image presheaf are (f∗G)(V)=G(f−1V). (Direct image of a sheaf along a continuous map)

[F10]

The global-sections functor Γ(W,−) on abelian sheaves over a space W is additive and left exact. (Global sections are left exact but need not preserve epimorphisms)

Proof

technique · direct: an injective resolution in $\mathrm{Mod}(\mathcal O_X)$ is a flasque resolution, hence an acyclic resolution on every $f^{-1}V$; the cohomology sheaf of the resulting complex of sections is the sheafification of its presheaf cohomology
1.1F1F2

Let 0→F→I0→I1→⋯ be the resolution supplied by the datum I of [F1]. Fix open U⊆V⊆X. The map jU!OU→jV!OV of [F2] is a monomorphism of OX-modules. Since Ip is injective in Mod(OX), every morphism jU!OU→Ip extends across this monomorphism to jV!OV. Under the natural identifications of [F2], this is precisely surjectivity of the restriction Ip(V)→Ip(U). Thus every Ip is flasque as an underlying sheaf of abelian groups.

2.1F2step 1.1construct

For every open U⊆X the restricted sheaf Ip∣U is flasque: for open W⊆V⊆U the restriction (Ip∣U)(V)→(Ip∣U)(W) is the restriction Ip(V)→Ip(W) of the flasque sheaf Ip, which is surjective.

3.1F8step 2.1construct

For every open V⊆S the restricted complex I∙∣f−1V is exact at every positive term with F∣f−1V as its degree-zero cohomology sheaf: exactness of 0→F→I0→I1→⋯ is checked on stalks [F8], and a point x∈f−1V has the same stalks in f−1V as in X. Hence 0→F∣f−1V→I0∣f−1V→I1∣f−1V→⋯ is a resolution by flasque sheaves.

4.1F3F4F5F10step 3.1

By [F3] each restricted term Ip∣f−1V is Γ-acyclic, so the resolution of step 3.1 is an acyclic resolution of F∣f−1V; the functorial injective resolution datum on abelian sheaves over the space f−1V 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 Γ(f−1V,−), giving canonical isomorphisms Hq(f−1V,F∣f−1V)≅Hq(Γ(f−1V,I∙)) for every q≥0, the right-hand side being the cohomology of the complex of sections.

4.2F6F7F8F9step 3.1

Let C∙=f∗I∙ be the complex of OS-modules with Cp(V)=Γ(f−1V,Ip) for open V⊆S [F9]. Its cohomology presheaf is V↦Hq(C∙(V))=Hq(Γ(f−1V,I∙)), and the cohomology sheaf Hq(C∙) of [F6] is the sheafification of this presheaf: indeed Zq=ker⁡dq has Zq(V)=ker⁡(dq ⁣:Cq(V)→Cq+1(V)) because kernels of sheaf morphisms are computed on opens, Bq is the sheafification of the presheaf V↦im⁡(dq−1 ⁣:Cq−1(V)→Cq(V)) by [F6], and passing to the quotient and to stalks, which commute, shows that the sheafified presheaf cohomology and coker⁡(Bq→Zq) have the same stalk at every point; a morphism of sheaves with bijective stalks is an isomorphism, so the two agree.

5.1F1F5step 4.1step 4.2

Combining steps 4.1 and 4.2, the sheaf Rqf∗F=Hq(f∗I∙) is canonically isomorphic to the sheafification of the presheaf V↦Hq(f−1V,F∣f−1V). The isomorphism is natural in V because every map used above is induced by restriction of sections along inclusions of opens, and for q<0 both sides are zero by [F1] and [F5].

6.1F1F3F4F7step 5.1given∎

Finally the presheaf V↦Hq(f−1V,F∣f−1V) is a presheaf of OS-modules: for V′⊆V restriction along f−1V′⊆f−1V is additive and compatible with the ring maps, and the action of a∈OS(V) is induced by the action of its image in OX(f−1V). The action maps are morphisms of presheaves into the sheaf Rqf∗F, so by the universal property of sheafification [F7] they descend uniquely to an OS-module structure on the sheafification, and the isomorphism of step 5.1 is OS-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

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