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.
Long exact global sheaf Ext sequence in the first variable
Statement
Assume the Axiom of Choice. Let be a ringed space whose structure sheaf is commutative, let be a short exact sequence of -modules and let be an -module. Then the injective-resolution global Ext of Sheaf Ext of coherent modules fits into a natural long exact sequence beginning in degree zero with The sequence is natural in the short exact sequence and in ; it is made from one fixed -injective resolution of , and the resulting connecting maps do not depend on that choice. No claim is made here about a long exact sequence in the second variable, about vanishing of for , or about splitting.
Facts & Assumptions
Given: a ringed space with commutative structure sheaf, a short exact sequence of -modules, and an -module .
An object of an abelian category is injective when for every monomorphism and every morphism there is a morphism with . (Injective object)
A short exact sequence of cochain complexes in an abelian category yields a natural long exact sequence in cohomology, with connecting maps . (The long exact sequence in cohomology)
For supplied injective-resolution data the complex has th term and differential , and its cohomology is . (Ext via an injective resolution of the second variable)
For an -module and a supplied injective resolution one sets ; the coaugmentation identifies , and comparison maps and homotopies make all of this independent of the supplied resolution. (Sheaf Ext of coherent modules)
Any two coaugmentation-preserving maps between injective resolutions extending the same object morphism are cochain-homotopic. (Injective comparison maps are unique up to cochain homotopy)
The declared Axiom of Choice implies the Dependent Choice hypothesis of the published injective-comparison existence and uniqueness theorems. (The Axiom of Choice, AC implies DC implies countable choice, Injective comparison maps exist)
Proof
Using AC and the in-run theorem lem-ringed-space-module-sheaves-enough-injectives of the cohomology-of-quasi-coherent-sheaves pair, which supplies an -injective resolution for every -module, fix one such resolution ; by [F3] applied in the abelian category of -modules the complex has th term and differential , and by [F4] its th cohomology is .
For every the module is injective, so by [F1] every morphism defined on a subobject of extends to ; applying this to the subobject gives exactness of : surjectivity of the last map is the extension property applied to , injectivity of the first is immediate from the epimorphism , and exactness in the middle follows because a morphism killing factors through the quotient .
The three complexes , and are concentrated in degrees , their differentials are post-composition with the differential of , so the degreewise exact sequence of step 1.2 commutes with those differentials; hence is a short exact sequence of cochain complexes.
By [F2] the sequence of step 2.1 has a natural long exact sequence , and substituting the identification of [F4] turns its terms into , and .
Since the complexes are concentrated in degrees , the terms in the long exact sequence of step 3.1 vanish, so the sequence begins ; by the degree-zero clause of [F4] the first three terms are , and , which is the displayed beginning of the statement.
Naturality in and resolution independence hold as follows: a morphism with injective resolutions , admits a coaugmentation-preserving comparison map extending by [F6], and post-composition with it is a cochain map inducing maps on cohomology that intertwine the connecting maps of [F2]; two choices of comparison map are cochain-homotopic by [F5], whose Dependent Choice hypothesis is licensed by [F6], so the induced maps on cohomology agree and the sequence depends on and not on the resolution.
Naturality in the short exact sequence holds because a morphism of short exact sequences of -modules induces a morphism of the degreewise exact sequences of complexes built in step 2.1, and [F2] provides the induced morphism of long exact sequences; the connecting maps are then those supplied by [F2] composed with the identifications of [F4]. The statement claims the long exact sequence and its naturality, and no splitting or vanishing beyond degree zero, so nothing further is asserted.
Depends on
Sheaf Ext of coherent modules
Ext via an injective resolution of the second variable
Injective object
The long exact sequence in cohomology
Injective comparison maps exist
Injective comparison maps are unique up to cochain homotopy
Enough injective sheaves of modules
The Axiom of Choice
AC implies DC implies countable choice