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.
Closed immersion preserves cohomology and coherent pushforward
Statement
Assume the Axiom of Choice (The Axiom of Choice). Let be a closed immersion of schemes (Closed immersions of schemes) and let be a quasi-coherent -module (Quasi-coherent module on a scheme), with direct image (Direct image of a sheaf along a continuous map, Direct image preserves sheaves and objectwise algebraic structure). Then for every there is a canonical isomorphism where denotes sheaf cohomology (Sheaf cohomology as right derived global sections).
If in addition is locally Noetherian (Locally Noetherian and Noetherian schemes) and is coherent (Coherent module sheaves), then is a coherent -module. The empty scheme, the zero module and the case affine are included.
Facts & Assumptions
Given: The Axiom of Choice, a closed immersion and a quasi-coherent -module .
A closed immersion is affine: for every affine open there is an ideal with , in particular is affine. (Closed immersions are affine quotients and survive base change, Affine morphisms, Principal distinguished subsets of the prime spectrum)
Affine morphisms and cohomology: if is affine, then the map is an isomorphism for every and every quasi-coherent -module (Affine pushforward is compatible with sheaf cohomology).
Affine equivalence: for an affine scheme the quasi-coherent modules are, up to canonical isomorphism, exactly the associated sheaves of -modules (Affine quasi-coherent sheaves are modules, Module sheaf on an affine scheme); a quasi-coherent module is of finite type if and only if some/every presenting module is finitely generated (Finite type and finitely presented module sheaves); for one has with restrictions the localisation maps (Sections of the associated sheaf on basic opens). On a locally Noetherian scheme coherence is local on the scheme, and a finite-type quasi-coherent module whose presenting modules are finitely generated over Noetherian rings is coherent (Coherent module sheaves, Locally Noetherian and Noetherian schemes).
Proof
The closed immersion is an affine morphism: by [F1] the inverse image of every affine open subscheme of is affine.
Apply [F2] to and : the edge map is an isomorphism for every , which is the asserted canonical isomorphism (in degree it is the identity of under the canonical identification of with ).
Now assume locally Noetherian and coherent. Coherence of is local on , so fix an affine open ; then is Noetherian, and by [F1] there is an ideal with , . By [F3] the coherent module is the associated sheaf of a finitely generated -module , and , being a quotient of the Noetherian ring , is Noetherian.
The restriction is the associated sheaf of viewed as an -module through : indeed for with image one has by [F1] and [F3], and these isomorphisms are compatible with the restriction maps, which on both sides are the canonical localisations; sheaves are determined by their sections on the basis of principal opens.
The -module is finitely generated, because it is finitely generated over the quotient ring by 1.3; hence is a coherent -module by [F3], since is Noetherian. As was an arbitrary affine open of the locally Noetherian scheme , coherence of follows.
Boundary and choice accounting. If then , and both sides of the isomorphism are the zero group in every degree; if then also ; if the isomorphism is . Affine is the case in which the local verification of 1.3-1.5 is already global. The Axiom of Choice is a hypothesis, consumed through the affine edge-map theorem [F2] and the affine equivalence [F3]; the localisation identifications of 1.4 make no further choice.
Depends on
The Axiom of Choice
Affine morphisms
Closed immersions of schemes
Closed immersions are affine quotients and survive base change
Affine pushforward is compatible with sheaf cohomology
Direct image of a sheaf along a continuous map
Direct image preserves sheaves and objectwise algebraic structure
Quasi-coherent module on a scheme
Coherent module sheaves
Locally Noetherian and Noetherian schemes
Affine quasi-coherent sheaves are modules
Module sheaf on an affine scheme
Sections of the associated sheaf on basic opens
Finite type and finitely presented module sheaves
Principal distinguished subsets of the prime spectrum
Sheaf cohomology as right derived global sections