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.
Cohomology and base change for proper flat coherent families
Statement
Assume the Axiom of Choice and the Axiom of Dependent Choice (The Axiom of Choice, The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain), inherited from the Noetherian approximation and the finite-free criterion cited below. Let be a proper morphism of finite presentation (Proper morphisms, Locally finite presentation morphisms) with an arbitrary scheme, and let be a coherent -module (Coherent module sheaves) that is flat over (Flat and faithfully flat modules and ring homomorphisms); by [F1] is then finitely presented.
Fix and an integer , write for the residue field (The residue field at a point of an affine scheme), put with projection and (Pullback of a module along a morphism of ringed spaces), and let be the cohomology and base-change map at (Cohomology and base-change map, Higher direct image of a sheaf).
(a) If is surjective, then there is an affine open neighbourhood of such that for every morphism , with and projection (Base change of objects, morphisms and properties), the base-change map of Cohomology and base-change map is an isomorphism of -modules.
(b) Assume moreover that is surjective. Then is locally free of finite rank in a neighbourhood of (Locally free sheaves of finite rank) if and only if is surjective; for the condition on is automatic, so is then finite locally free near .
(c) Under the hypothesis of (a), itself is an isomorphism.
The empty source , the zero sheaf , the degrees and with , and an arbitrary (not necessarily Noetherian) base are included. No flatness or finite-presentation hypothesis is imposed on beyond the stated ones, and no projectivity, Noetherianness or Krull-dimension hypothesis is imposed on .
Facts & Assumptions
Given: The Axiom of Choice and the Axiom of Dependent Choice, a proper morphism of finite presentation , a coherent -module flat over , a point and an integer .
Coherence unpacked and finite presentation: a coherent -module is quasi-coherent of finite type, and for every open and every morphism with finite its kernel is of finite type; consequently, on an affine open with and finitely generated, a surjection has finitely generated kernel, so is finitely presented and is finitely presented; restrictions of coherent modules to open subschemes are coherent. (Coherent module sheaves, Finite type and finitely presented module sheaves, Quasi-coherent module on a scheme, Kernel sheaves are objectwise, while cokernels and images are sheafified, Affine quasi-coherent sheaves are modules, Finitely presented modules and finitely presented algebras)
Flatness and localisation: is flat over meaning that each stalk is flat over the local ring ; flatness is preserved by restriction to open subschemes and by base change, a localisation is a flat ring map, and flatness of a module is local on the base ring. (Flat and faithfully flat modules and ring homomorphisms, Every localization is flat, and localizing a flat module preserves flatness, Flatness is transitive under a flat change of rings, A module is flat if and only if all prime localizations are flat, equivalently all maximal localizations are flat, Extension of scalars carries flat modules to flat modules)
Properness, affine bases and fibres: a proper morphism is separated, of finite type and universally closed, and a morphism of finite type is quasi-compact; affine opens form a basis of every scheme, so there is an affine open containing , with corresponding prime ; the restriction is proper and of finite presentation, and is quasi-compact and separated; the canonical morphism factors through , so the fibre is canonically identified with , and is the residue field of the local ring . (Proper morphisms, Locally finite presentation morphisms, Locally finite type and finite type morphisms, Quasi-compact and quasi-separated morphisms, Schemes, Affine open subschemes, The underlying space of an affine spectrum, The residue field at a point of an affine scheme, Base change of objects, morphisms and properties, Iterated base change, Properness survives arbitrary base change, Localisation at a prime ideal: )
The perfect complex over an affine base: for the ring , the proper morphism of finite presentation and the coherent, hence finitely presented [F1], module flat over by [F2], the cited lemma provides an integer and a bounded complex of finite projective -modules, concentrated in degrees and finite free in all positive degrees, with canonical isomorphisms for every -algebra , natural in and compatible with composition of -algebra maps, where and is the pullback of ; moreover becomes a bounded complex of finite free modules after restricting to the members of an open cover of by affine opens. (Universal finite projective cohomology complex over any base, The Axiom of Choice, The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain)
Naturality of the comparison with base-change maps: the naturality clause of [F4] says that for -algebras the square with the maps and commutes, where the algebraic horizontal arrow is induced by tensoring representatives of cohomology classes, and the geometric horizontal arrow is the extension of scalars of the pullback of cohomology classes along composed with the canonical map , that is, the map on global sections induced by the base-change map of the cohomology-and-base-change definition for the Cartesian square over ; the pullback of classes is the map supplied by the contravariance of sheaf cohomology in the space. (Universal finite projective cohomology complex over any base, Cohomology and base-change map, Variance of sheaf cohomology, Associativity of tensor products for compatible bimodules, The regular module is a tensor unit: and )
The finite-free criterion: for a ring with maximal ideal and residue field and a bounded complex of finite free -modules with differentials , the map induced by tensoring representatives satisfies: (1) it is surjective if and only if there is such that over there are bases of and in which is ; (2) if so, then is a finitely generated -module and the natural map is an isomorphism for every -algebra ; (3) given (1), is a finite projective -module for some if and only if, after shrinking further, the analogous map is also surjective, and if this surjectivity is automatic. The Axiom of Choice enters only through the Nakayama lemma and its corollary. (Finite-free local criterion for cohomology and base change, Assuming the Axiom of Choice, Nakayama's lemma, Assuming the Axiom of Choice, generators modulo an ideal in the Jacobson radical lift to generators, Cohomology object of a cochain complex, The Axiom of Choice)
Higher direct images and the fibre map: for quasi-compact and separated and quasi-coherent, each is quasi-coherent, for , and for an affine open there is a canonical isomorphism with the associated sheaf of the -module ; hence , the fibre at is for every affine open , and the fibre map of the cohomology-and-base-change definition is the extension of scalars of the pullback-of-classes map , its colimit description being independent of the chosen affine neighbourhood of . (Higher direct image of a sheaf, Higher direct images localize over an affine base, Cohomology and base-change map, Fibre of a module sheaf at a point, Module sheaf on an affine scheme, The stalk of an associated sheaf is the localisation, Pullback of a module along a morphism of ringed spaces)
Finite locally free modules on affine schemes: for a ring and a finitely presented -module , the associated sheaf is locally free of finite rank near if and only if is free over ; the locus of primes at which a finitely presented module is free of a fixed rank is open, and the module is free of that rank on an open neighbourhood of any such prime. (Locally free sheaves of finite rank, Openness of the finite free locus, Affine quasi-coherent sheaves are modules, Module sheaf on an affine scheme, The stalk of an associated sheaf is the localisation)
Finitely generated projective modules: a finitely generated module is a quotient of a finite free module; a surjection onto a projective module splits, exhibiting the projective module as a direct summand of a free module under the Axiom of Choice; over a local ring a finitely generated module generated by elements whose classes generate is generated by them; passing to the residue field is right exact; and a direct summand of a finitely generated free module is finitely generated, while a finitely presented module has finitely generated syzygies. (Generated submodule, cyclic and finitely generated modules, module basis and free module, The splitting lemma for short exact sequences of modules, Equivalent characterizations of projective modules, Projective modules and the lifting property, Assuming the Axiom of Choice, Nakayama's lemma, Assuming the Axiom of Choice, generators modulo an ideal in the Jacobson radical lift to generators, The Jacobson radical of a ring, A local ring is a nonzero commutative ring with a unique maximal ideal, Tensoring is right exact, Universal property of a direct sum of modules, Finitely presented modules and finitely presented algebras, The Axiom of Choice)
The Axiom of Choice and the Axiom of Dependent Choice are the choice principles named in the statement. (The Axiom of Choice, The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain)
Proof
Affine setup. By [F3] fix an affine open containing , with prime and residue field . By [F4], is finite free on an affine neighbourhood of ; shrink to a principal open with and . The ideal is prime, and is the local ring at with maximal ideal and residue field . The ring is the coordinate ring of an actual affine open of ; the local ring is used only for the finite-free criterion.
Put , a bounded finite-free complex by 1.1, and . By [F1] the coherent module is finitely presented and by [F2] it is flat over , so [F4] applies to and every -algebra. Apply [F6] to over the local ring , whose residue field is : its maps and are defined. Flat localisation gives , so these fibre maps agree with the corresponding tensoring-representatives maps for at .
The comparison of [F4] identifies with , and identifies with . By [F5], the natural tensoring-representatives map becomes the geometric fibre map on the affine neighbourhood of [F7]. The localisation identities in step 1.2 identify that algebraic map with over , and likewise in degree . Thus is surjective exactly when is, and the same holds in degree .
Part (a). If is surjective, then so is by step 2.1. By F6, has a split matrix in bases of and over . The finitely many entries of the bases, their inverses, and the matrix identities descend from to some with ; hence has that split form in bases of . Writing in this form, is finitely presented, and right exactness of tensor gives for every -algebra , exactly the split-matrix calculation in F6. Put , an affine open containing . For any and any affine chart , the comparison and naturality in [F4,F5] identify the section map of with this algebraic isomorphism. Such charts cover , so the sheaf morphism is an isomorphism by A morphism of sheaves is an isomorphism exactly when it is an isomorphism on every stalk.
Part (c). Apply (a) with . On global sections the isomorphism is , which is the fibre map computed on the affine neighbourhood by [F7]. Thus is an isomorphism.
Part (b), first direction. Assume and are surjective. By step 2.1 both maps for are surjective, so F6 makes finite projective over the local ring , hence finite free by [F9]. By step 3.1, after a principal shrinking the module is finitely presented, and its localisation at is . The openness of the finite-free locus [F8] therefore supplies a further principal neighbourhood of on which is finite locally free. Comparison [F4] and the affine direct-image formula [F7] identify this sheaf with there.
Part (b), second direction. Assume is surjective and is finite locally free near . By step 3.1 shrink to where the split differential makes finitely presented, and then shrink so [F7] identifies this module with the sections of a free sheaf. Its localisation at is finite free over . By F6, is surjective; step 2.1 transports this to surjectivity of . For , because [F4] concentrates the model in nonnegative degrees, so is automatically surjective by F6; the first direction then gives finite local freeness of near .
Boundaries and choice. If or , all cohomology modules are zero, all fibre and base-change maps are isomorphisms, and is finite locally free. If , the fibre map evaluates local sections on the fibre as in Cohomology and base-change map, and the automatic condition is covered in step 5.1. If or , then , so is surjective and parts (a)–(c) apply without any separate neighbourhood-vanishing claim. If there is no point and the statement is vacuous. The two directions of (b) are steps 4.2–5.1 and (c) is step 4.1. AC and DC enter through the cited perfect-complex and finite-free suppliers [F4,F6,F9,F10]; only finitely many bases, matrix entries and affine neighbourhoods are selected locally.
Depends on
Assuming the Axiom of Choice, generators modulo an ideal in the Jacobson radical lift to generators
is the residue field at
Affine open subschemes
The underlying space of an affine spectrum
Module sheaf on an affine scheme
The Axiom of Choice
Cohomology and base-change map
Base change of objects, morphisms and properties
Coherent module sheaves
Cohomology object of a cochain complex
The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain
Fibre of a module sheaf at a point
Finite type and finitely presented module sheaves
Finitely presented modules and finitely presented algebras
Flat and faithfully flat modules and ring homomorphisms
Generated submodule, cyclic and finitely generated modules, module basis and free module
Higher direct image of a sheaf
The Jacobson radical of a ring
Kernel sheaves are objectwise, while cokernels and images are sheafified
Locally finite presentation morphisms
Locally finite type and finite type morphisms
Locally free sheaves of finite rank
A local ring is a nonzero commutative ring with a unique maximal ideal
Localisation at a prime ideal:
Multiplicative subsets and the localisation as equivalence classes of fractions
Projective modules and the lifting property
Proper morphisms
Pullback of a module along a morphism of ringed spaces
Quasi-coherent module on a scheme
Quasi-compact and quasi-separated morphisms
The residue field at a point of an affine scheme
Schemes
The stalk of an associated sheaf is the localisation
Iterated base change
Finite-free local criterion for cohomology and base change
Variance of sheaf cohomology
Restricting fibre products to open subschemes
Higher direct images localize over an affine base
Universal finite projective cohomology complex over any base
Properness survives arbitrary base change
Extension of scalars carries flat modules to flat modules
Flatness is transitive under a flat change of rings
Affine fibre products are spectra of tensor products
Affine quasi-coherent sheaves are modules
Associativity of tensor products for compatible bimodules
A module is flat if and only if all prime localizations are flat, equivalently all maximal localizations are flat
Every localization is flat, and localizing a flat module preserves flatness
Openness of the finite free locus
A morphism of sheaves is an isomorphism exactly when it is an isomorphism on every stalk
Assuming the Axiom of Choice, Nakayama's lemma
Equivalent characterizations of projective modules
Tensoring is right exact
The splitting lemma for short exact sequences of modules
The regular module is a tensor unit: and
Universal property of a direct sum of modules