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.

Universal finite projective cohomology complex over any base

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 N-indexed chain), inherited from the Noetherian approximation and the Noetherian-stage construction cited below. Let A be a commutative ring, let f:X→Spec⁡A be a proper morphism of finite presentation (Proper morphisms, Locally finite presentation morphisms), and let F be a finitely presented OX-module (Finite type and finitely presented module sheaves) that is flat over A, meaning that for every x∈X the stalk Fx is a flat module over the local ring Af(x)=OSpec⁡A,f(x) (Flat and faithfully flat modules and ring homomorphisms).

Then there are an integer r≥0 and a bounded complex K∙ of finite projective A-modules, concentrated in degrees 0,…,r and finite free in all positive degrees, such that for every A-algebra A′ and every q∈Z there is a canonical isomorphism Hq(K∙⊗AA′)  ≅  Hq(XA′,FA′), where XA′:=X×Spec⁡ASpec⁡A′ with projection p:XA′→X (Base change of objects, morphisms and properties) and FA′:=p∗F (Pullback of a module along a morphism of ringed spaces). The isomorphisms are natural in the A-algebra A′ and compatible with composition of A-algebra maps.

Locally on Spec⁡A the complex can be made finite free: there is an open cover of Spec⁡A by affine opens V such that K∙⊗AO(V) is a bounded complex of finite free O(V)-modules.

The empty source X=∅, the zero sheaf F=0, the one-member case r=0, the zero ring A=0, the base change A′=0, the degrees q<0 and q>r, and the case where A is already finitely generated over Z are included.

Facts & Assumptions

Given: The Axiom of Choice and the Axiom of Dependent Choice, a commutative ring A, a proper morphism of finite presentation f:X→Spec⁡A, a finitely presented OX-module F with Fx flat over Af(x) for every x∈X, and, for the base change statements, an A-algebra A′.

[F1]

Noetherian approximation: if A is any commutative ring, f:X→Spec⁡A is proper of finite presentation and F is a finitely presented OX-module that is flat over A in the sense that each stalk Fx is a flat A-module through A→OX,x, then there are a finitely generated Z-subalgebra Ai⊆A, a proper morphism of finite presentation fi:Xi→Spec⁡Ai, a finitely presented OXi-module Fi flat over Ai, and identifications X≅Xi×Spec⁡AiSpec⁡A and F≅q∗Fi over A, where q:X→Xi is the projection; if A is finitely generated over Z the descent is trivial, and the empty source and the zero sheaf are included. (Noetherian approximation of proper flat finitely presented sheaf data, Proper morphisms, Locally finite presentation morphisms, Finite type and finitely presented module sheaves, Flat and faithfully flat modules and ring homomorphisms)

[F2]

A finitely generated algebra over the Noetherian ring Z is Noetherian. (Every algebra of finite type over a Noetherian ring is a Noetherian ring, Noetherian commutative rings and modules)

[F3]

Noetherian-stage perfect complex: for a Noetherian commutative ring B, a proper morphism g:Y→Spec⁡B and a coherent OY-module G flat over Spec⁡B (each stalk flat over the corresponding base local ring), there are an integer r≥0 and a bounded complex K∙ of finite projective B-modules, concentrated in degrees 0,…,r and finite free in positive degrees, with canonical isomorphisms Hq(K∙⊗BB′)≅Hq(YB′,GB′) for every B-algebra B′, natural in B′ and compatible with composition of ring maps; and after restricting to a suitable Zariski open cover of Spec⁡B the complex becomes a bounded complex of finite free modules. (Finite projective complex for proper flat coherent cohomology)

[F4]

Flatness of localisations, transitivity and base change: for a multiplicative set the localisation R→S−1R is a flat ring map; if R→S is a flat ring map and N is a flat S-module, then N is flat as an R-module; and extension of scalars along any ring map carries flat modules to flat modules. (Every localization is flat, and localizing a flat module preserves flatness, Flatness is transitive under a flat change of rings, Extension of scalars carries flat modules to flat modules)

[F5]

Flatness is local and localisation is tensor: an R-module M is flat if and only if every localisation Mp is flat over Rp; for a multiplicative set S there is a natural isomorphism S−1M≅S−1R⊗RM; tensor products of modules may be regrouped; and for an S-module N the unit map S⊗SN→N is an isomorphism. (A module is flat if and only if all prime localizations are flat, equivalently all maximal localizations are flat, Localisation of modules is extension of scalars, Associativity of tensor products for compatible bimodules, The regular module is a tensor unit: R⊗RN≅N and M⊗RR≅M)

[F6]

Stalk structure: for x∈X the local ring OX,x has for units exactly the elements outside its maximal ideal, and the structure map A→OX,x carries every a∈A∖f(x) to a unit, so it factors through the localisation A→Af(x). (The stalk of the affine structure sheaf at a prime is A_p, A local ring is a nonzero commutative ring with a unique maximal ideal)

[F7]

Finite free covers and splittings: a finitely generated R-module with generators m1,…,mn is a quotient of Rn by ej↦mj; projectivity is the lifting property against surjections; and a short exact sequence whose epimorphism has a section splits, exhibiting its target as a direct summand of its middle term. (The submodule generated by a subset consists of the finite R-linear combinations of that subset, Generated submodule, cyclic and finitely generated modules, module basis and free module, Universal property of a direct sum of modules, Projective modules and the lifting property, The splitting lemma for short exact sequences of modules)

[F8]

Tensor exactness, functoriality and direct sums: tensoring is right exact and functorial in both variables, and it commutes with arbitrary direct sums, so a finite direct sum of copies of R tensored with R′ is the corresponding finite direct sum of copies of R′ once the unit isomorphism is applied. (Tensoring is right exact, Module homomorphisms induce tensor-product homomorphisms functorially, Tensor products commute with arbitrary direct sums)

[F9]

Projectivity characterisation: under the Axiom of Choice a module is projective if and only if it is a direct summand of a free module. (Equivalent characterizations of projective modules, The Axiom of Choice)

[F10]

Change of rings: for a ring map R→S, a right S-module N and a left R-module M there is a natural isomorphism N⊗RM≅N⊗S(S⊗RM); restriction of scalars leaves the underlying groups and maps unchanged. (Change of rings: N⊗RM≅N⊗S(S⊗RM), Restriction of scalars and extension of scalars S⊗RM along a ring homomorphism R→S)

[F11]

Iterated base change and affine preimages: for S′′→S′→S and an S-scheme X there is a canonical isomorphism (X×SS′)×S′S′′≅X×SS′′ compatible with the projections; for an open U⊆X its preimage in a base change represents U×SS′; and for affine opens the fibre product is Spec⁡ of the tensor product of the section rings. (Iterated base change, Base change of objects, morphisms and properties, Restricting fibre products to open subschemes, Affine fibre products are spectra of tensor products, Affine open subschemes, The underlying space of an affine spectrum)

[F12]

Pullback of modules along a composition: the pullback f∗G=OX⊗f−1OYf−1G is contravariantly functorial, and the composite of pullbacks is canonically identified with the pullback along the composite, f∗g∗≅(g∘f)∗, by associativity of the sheaf tensor products defining pullback; on generators 1⊗1⊗s the identification is the identity. (Pullback of a module along a morphism of ringed spaces)

[F13]

Complexes: tensoring a complex of A-modules with the ring A′ placed in degree 0 gives the complex with terms Kj⊗AA′, and Hq denotes the cohomology object of a cochain complex. (The tensor product of a right and a left chain complex is totalized by direct sums with the Koszul differential, Cohomology object of a cochain complex)

[F14]

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 N-indexed chain)

Proof

technique · direct: transfer the flatness hypothesis to the form required by the Noetherian approximation, descend to a Noetherian stage, apply the Noetherian-stage perfect complex there, base change the finite projective complex along the stage map, and compare coefficient change, base-changed geometry and pullbacks of the sheaf along the canonical identifications, with finite freeness pulled back from the stage
1.1F4F6

Hypothesis transfer. Let x∈X and put p=f(x). By [F6] the structure map A→OX,x factors through the localisation A→Ap, so Fx is an Ap-module whose restriction to A is its given A-module structure; since A→Ap is flat and Fx is flat over Ap by hypothesis, [F4] makes Fx flat over A as well.

1.2F1F2

The Noetherian stage. By 1.1 the hypotheses of [F1] hold for f and F, so there are a finitely generated Z-subalgebra Ai⊆A, Noetherian by [F2], a proper morphism of finite presentation fi:Xi→Spec⁡Ai, a finitely presented OXi-module Fi flat over Ai in the sense of [F1], and identifications X≅Xi×Spec⁡AiSpec⁡A and F≅q∗Fi over A, where q:X→Xi is the projection.

1.3F4F5F10

The stage is flat over its base local rings. Let x∈Xi and put pi=fi(x); the OXi,x-module (Fi)x has its Ai-action factoring through Ai→(Ai)pi and is flat over Ai by 1.2. For every prime q⊆(Ai)pi, corresponding to a prime pi′⊆pi of Ai, the change-of-rings isomorphism [F10] together with the identifications of [F5] gives (Fi)x⊗(Ai)pi(Ai)pi′≅(Fi)x⊗Ai(Ai)pi′, the localisation of the Ai-module (Fi)x at pi′, and this is flat over (Ai)pi′=((Ai)pi)q by [F4] and [F5]; hence (Fi)x is flat over (Ai)pi by the local flatness criterion [F5].

1.4F3

The Noetherian-stage complex. By 1.3 and [F3] applied to fi and Fi there are an integer r≥0 and a bounded complex Ki∙ of finite projective Ai-modules, concentrated in degrees 0,…,r and finite free in all positive degrees, with canonical isomorphisms Hq(Ki∙⊗AiAi′)≅Hq((Xi)Ai′,(Fi)Ai′) for every Ai-algebra Ai′ and every q, natural in Ai′ and compatible with composition; moreover Ki∙ becomes a bounded complex of finite free modules on some open cover of Spec⁡Ai.

1.5F5F7F8F9

Base change of finite projective modules. If P is a finitely generated projective Ai-module, then P⊗AiA is a finitely generated projective A-module: choosing finitely many generators gives a surjection Ain→P [F7], projectivity of P splits it so that P is a direct summand of Ain [F7], tensoring with A is right exact and carries the splitting section to a splitting section [F8], the identification Ain⊗AiA≅An follows from the unit isomorphism Ai⊗AiA≅A and compatibility with finite direct sums [F5, F8], so P⊗AiA is both a quotient and a direct summand of the free A-module An; hence it is finitely generated and projective over A by [F9].

1.6F5F13

The complex and its coefficient change. Put K∙:=Ki∙⊗AiA, a bounded complex of finite projective A-modules concentrated in degrees 0,…,r and finite free in positive degrees by 1.5 and [F13]; for every A-algebra A′ the associativity and unit isomorphisms of [F5] applied to the Ai-module Kij and the ring A give canonical isomorphisms Kij⊗AiA′≅(Kij⊗AiA)⊗A(A⊗AA′)≅Kj⊗AA′ because A⊗AA′≅A′, natural in A′ and compatible with composition, hence an isomorphism of complexes Ki∙⊗AiA′≅K∙⊗AA′.

1.7F11

The base-changed geometry. Under the identification X≅Xi×Spec⁡AiSpec⁡A of 1.2, iterated base change [F11] with Spec⁡A′→Spec⁡A→Spec⁡Ai gives, for every A-algebra A′, a canonical isomorphism ψ:XA′=(Xi×Spec⁡AiSpec⁡A)×Spec⁡ASpec⁡A′≅Xi×Spec⁡AiSpec⁡A′=(Xi)A′ that is compatible with the projections to Xi.

1.8F12

The base-changed sheaf. The identification F≅q∗Fi of 1.2 and the composition rule for pullbacks [F12] give canonical identifications FA′=p∗F≅p∗q∗Fi≅(q∘p)∗Fi, while (Fi)A′=(q′)∗Fi for the projection q′:(Xi)A′→Xi; since q′∘ψ=q∘p by 1.7, the isomorphism ψ identifies these two pullbacks canonically, so FA′≅(Fi)A′ naturally in A′ and compatibly with composition of A-algebra maps.

1.9algebra

The comparison isomorphism. For every A-algebra A′ and every q∈Z compose the isomorphism Hq(K∙⊗AA′)≅Hq(Ki∙⊗AiA′) of 1.6 with the isomorphism Hq(Ki∙⊗AiA′)≅Hq((Xi)A′,(Fi)A′) of 1.4 applied to the Ai-algebra A′, and with the identification Hq((Xi)A′,(Fi)A′)≅Hq(XA′,FA′) induced by 1.7 and 1.8; each constituent is canonical, natural in A′ and compatible with composition of A-algebra maps, so the composite Hq(K∙⊗AA′)≅Hq(XA′,FA′) is as well.

1.10F5F8F11

Local finite freeness. By 1.4 there is an open cover of Spec⁡Ai by affine opens Vj such that Ki∙⊗AiO(Vj) is a bounded complex of finite free O(Vj)-modules; by [F11] the preimages Vj′⊆Spec⁡A are affine opens with O(Vj′)≅A⊗AiO(Vj) and they cover Spec⁡A. For each j the associativity and unit identifications of [F5] give K∙⊗AO(Vj′)≅(Ki∙⊗AiO(Vj))⊗O(Vj)O(Vj′), a bounded complex that is finite free over O(Vj′) because extension of scalars of a free module is free [F8]; hence K∙ is finite free locally on Spec⁡A.

2.1F1F3F9F14∎

Boundaries and choice accounting. If X=∅ the stage of 1.2 may be taken with Xi=∅, the stage complex is the zero complex with r=0 by 1.4, and for every A′ the scheme XA′ is empty with vanishing cohomology, so both sides of 1.9 vanish; if F=0 the same argument applies with Fi=0; if A=0 then Spec⁡A=∅ and X=∅, and if A′=0 then XA′=∅ and K∙⊗AA′=0; the one-member case r=0 is covered because 1.4 and 1.5 leave K∙ concentrated in degree 0; for q<0 both sides of 1.9 vanish, and for q>r the complex K∙⊗AA′ is concentrated in degrees 0,…,r by 1.6 while Hq((Xi)A′,(Fi)A′)=0 by 1.4; if A is finitely generated over Z the stage Ai=A of [F1] is trivial, 1.2 and 1.3 are identities, and 1.9 reduces to [F3]. The Axiom of Choice is used through [F1] in 1.2 and through the projectivity characterisation [F9] in 1.5; the Axiom of Dependent Choice is consumed by [F3] in 1.4; no other selection is made.

Depends on

Used by

Dependency tree · two levels

161 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