Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-27
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.

Variance of sheaf cohomology

Statement

Assume the Axiom of Choice, let X be a topological space with supplied functorial injective resolution datum IX and sheaf cohomology Hq(X,−) as in Sheaf cohomology as right derived global sections.

  1. (Covariance in the sheaf.) Every morphism φ:F→G of abelian sheaves on X induces additive maps Hq(X,φ):Hq(X,F)→Hq(X,G), and F↦Hq(X,F) is a covariant additive functor.
  2. (Contravariance in the space.) Let f:X→Y be a continuous map, let G be an abelian sheaf on Y, let F be an abelian sheaf on X, and let φ:f−1G→F be a morphism of abelian sheaves. Then there are maps Hq(Y,G)⟶Hq(X,F)(q≥0) depending only on φ, natural in G and F, and in degree 0 the map is the composite Γ(Y,G)→Γ(X,f−1G)→ Γ(X,φ) Γ(X,F) of section pullback with φ; for composable data g:Y→Z, ψ:g−1H→G, φ:f−1G→F the map of the composite pair φ∘f−1ψ:(gf)−1H→F is the composite of the two maps (compatibility with compositions).

Facts & Assumptions

[F1]

Hq(X,F)=RIXqΓ(X,F) is computed from the supplied functorial datum, and Hq(X,φ)=RIXqΓ(φ) (Sheaf cohomology as right derived global sections).

[F2]

In degree 0 the cohomology is global sections, with the identification given by the kernel description (Degree-zero sheaf cohomology is global sections).

[F3]

Inverse and direct image are adjoint: Hom⁡X(f−1G,F)≅Hom⁡Y(G,f∗F), naturally in both variables (Inverse image is left adjoint to direct image on sheaves).

[F4]

The stalk of an inverse image is the stalk at the image point: (f−1G)x≅Gf(x) (The stalk of an inverse image sheaf is the stalk over the image point).

[F5]

Exactness of a sequence of abelian sheaves is checked stalkwise (A sequence of abelian sheaves is exact exactly when it is exact on every stalk).

[F6]

A morphism of sheaves of sets is an isomorphism if and only if all its stalk maps are bijections (A morphism of sheaves is an isomorphism exactly when it is an isomorphism on every stalk).

[F7]

A natural transformation α:F⇒G of additive functors on the domain of a supplied injective resolution datum induces natural maps RIn(α):RInF⇒RInG on the derived objects (A natural transformation induces natural transformations of right derived functors).

[F8]

Cochain-homotopic cochain maps induce the same map on homology (Chain-homotopic maps induce the same map on homology).

[F9]

The derived objects RInF form an additive functor in A for a fixed additive F (Right derived functors relative to supplied data are additive functors).

[F10]
[F11]

Under DC a morphism from the coaugmentation of an exact coaugmented complex into the coaugmentation of a complex of injective objects extends to a coaugmentation-preserving cochain map, and any two such lifts are cochain-homotopic (Lifting a morphism from an exact complex into an injective resolution).

[F12]

Γ(X,−) is an additive left exact functor (Global sections of an abelian sheaf).

[F13]

The direct image sheaf satisfies (f∗F)(V)=F(f−1(V)), so over Y it is Γ(Y,f∗F)=Γ(X,F) (Direct image of a sheaf along a continuous map).

Proof

Given: The Axiom of Choice, the continuous map f:X→Y, the abelian sheaves G on Y and F on X, and the morphism φ:f−1G→F.

1.1

By [F10] AC gives DC, which is the hypothesis of the comparison item [F11]; by [F12] the global-sections functors are additive and left exact, and applying Enough injective abelian sheaves to X and to Y supplies functorial injective resolution data IX and IY. Hence Hq(X,−) and Hq(Y,−) are defined by [F1], and the inverse image f−1 is additive because it is a left adjoint [F3].

F3F10F12given
1.2

For a morphism φ:F→G in Ab(X), put Hq(X,φ):=RIXqΓ(φ); this is additive in φ and preserves identities and composites because RIXqΓ is an additive functor on the domain of IX by [F9]. Thus F↦Hq(X,F) is a covariant additive functor, which is assertion 1.

F1F9
1.3

For a sheaf H on Y, applying [F3] to the identity of f−1H produces the unit ηH:H→f∗f−1H; taking sections over Y and using (f∗f−1H)(Y)=(f−1H)(X) [F13] gives the section-pullback map Γ(Y,H)→Γ(X,f−1H), natural in H.

F3F13
1.4

The functor f−1 is exact: by [F4] the stalk at x of the inverse image of a sequence of sheaves on Y is the stalk of that sequence at f(x), so by [F5] every exact sequence on Y pulls back to a sequence exact at each x∈X; hence f−1 is exact and preserves kernels and cokernels.

F4F5
2.1

For continuous maps f:X→Y and g:Y→Z the functors (gf)−1 and f−1g−1 agree on stalks by [F4], both giving Hg(f(x)) at x, so the canonical comparison (gf)−1H→f−1g−1H is an isomorphism by [F6]; the identification is compatible with the units of step 1.3, the unit of a composite adjunction being the composite of the units.

F4F6
2.2

By [F7] the natural transformation α:Γ(Y,−)⇒Γ(X,f−1(−)) of step 1.3 induces, for every q, a natural map RIYqΓ(Y,H)→RIYq(Γ(X,f−1(−)))(H); by [F1] the target is Hq(Γ(X,f−1IY(H)∙)), the cohomology of the complex obtained by applying Γ(X,−) to the deleted resolution f−1IY(H)del∙. Hence there is a natural map Hq(Y,H)→Hq(Γ(X,f−1IY(H)∙)). [F1, F7, step 1.3]

F1F7
2.3

Let G be a sheaf on Y and φ:f−1G→F. By step 1.4 the complex f−1IY(G)∙ is an exact coaugmented complex resolving f−1G, and IX(F)∙ is a complex of injectives, so by [F11] the morphism φ extends to a coaugmentation-preserving cochain map ψ∙:f−1IY(G)∙→IX(F)∙, unique up to cochain homotopy. [F11, step 1.4, construct]

F11construct
3.1

Define the space map as the composite Hq(Y,G)→Hq(Γ(X,f−1IY(G)∙))→ Hq(Γ(ψ∙)) Hq(Γ(X,IX(F)∙))=Hq(X,F), the first arrow from step 2.2 and the last identification from [F1]. By [F11] any two lifts ψ∙ are cochain-homotopic, hence by [F8] they induce the same map on cohomology, so the composite depends only on φ; it is natural in G and F by step 2.2 and by naturality of Hq(X,−) [F1]. [F1, F8, F11, step 2.2, step 2.3]

F1F8F11
4.1

For composable data as in the statement the map of the composite pair agrees with the composite of the two maps: step 2.1 identifies (gf)−1H with f−1g−1H, the unit of the composite adjunction is the composite of the units by step 1.3, and the two comparison maps involved differ by a cochain homotopy by [F11], hence induce the same map on cohomology by [F8]. In degree 0, step 3.1 is the composite Γ(Y,G)→Γ(X,f−1G)→Γ(X,F) of section pullback with Γ(X,φ), by [F2] and step 1.3. [F2, F8, F11, step 2.1, step 3.1] ∎

F2F8F11∎

Depends on

Used by

Dependency tree · two levels

66 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