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 -indexed chain), inherited from the Noetherian approximation and the Noetherian-stage construction cited below. Let be a commutative ring, let be a proper morphism of finite presentation (Proper morphisms, Locally finite presentation morphisms), and let be a finitely presented -module (Finite type and finitely presented module sheaves) that is flat over , meaning that for every the stalk is a flat module over the local ring (Flat and faithfully flat modules and ring homomorphisms).
Then there are an integer and a bounded complex of finite projective -modules, concentrated in degrees and finite free in all positive degrees, such that for every -algebra and every there is a canonical isomorphism where with projection (Base change of objects, morphisms and properties) and (Pullback of a module along a morphism of ringed spaces). The isomorphisms are natural in the -algebra and compatible with composition of -algebra maps.
Locally on the complex can be made finite free: there is an open cover of by affine opens such that is a bounded complex of finite free -modules.
The empty source , the zero sheaf , the one-member case , the zero ring , the base change , the degrees and , and the case where is already finitely generated over are included.
Facts & Assumptions
Given: The Axiom of Choice and the Axiom of Dependent Choice, a commutative ring , a proper morphism of finite presentation , a finitely presented -module with flat over for every , and, for the base change statements, an -algebra .
Noetherian approximation: if is any commutative ring, is proper of finite presentation and is a finitely presented -module that is flat over in the sense that each stalk is a flat -module through , then there are a finitely generated -subalgebra , a proper morphism of finite presentation , a finitely presented -module flat over , and identifications and over , where is the projection; if is finitely generated over 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)
A finitely generated algebra over the Noetherian ring is Noetherian. (Every algebra of finite type over a Noetherian ring is a Noetherian ring, Noetherian commutative rings and modules)
Noetherian-stage perfect complex: for a Noetherian commutative ring , a proper morphism and a coherent -module flat over (each stalk flat over the corresponding base local ring), there are an integer and a bounded complex of finite projective -modules, concentrated in degrees and finite free in positive degrees, with canonical isomorphisms for every -algebra , natural in and compatible with composition of ring maps; and after restricting to a suitable Zariski open cover of the complex becomes a bounded complex of finite free modules. (Finite projective complex for proper flat coherent cohomology)
Flatness of localisations, transitivity and base change: for a multiplicative set the localisation is a flat ring map; if is a flat ring map and is a flat -module, then is flat as an -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)
Flatness is local and localisation is tensor: an -module is flat if and only if every localisation is flat over ; for a multiplicative set there is a natural isomorphism ; tensor products of modules may be regrouped; and for an -module the unit map 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: and )
Stalk structure: for the local ring has for units exactly the elements outside its maximal ideal, and the structure map carries every to a unit, so it factors through the localisation . (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)
Finite free covers and splittings: a finitely generated -module with generators is a quotient of by ; 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 -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)
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 tensored with is the corresponding finite direct sum of copies of once the unit isomorphism is applied. (Tensoring is right exact, Module homomorphisms induce tensor-product homomorphisms functorially, Tensor products commute with arbitrary direct sums)
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)
Change of rings: for a ring map , a right -module and a left -module there is a natural isomorphism ; restriction of scalars leaves the underlying groups and maps unchanged. (Change of rings: , Restriction of scalars and extension of scalars along a ring homomorphism )
Iterated base change and affine preimages: for and an -scheme there is a canonical isomorphism compatible with the projections; for an open its preimage in a base change represents ; and for affine opens the fibre product is 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)
Pullback of modules along a composition: the pullback is contravariantly functorial, and the composite of pullbacks is canonically identified with the pullback along the composite, , by associativity of the sheaf tensor products defining pullback; on generators the identification is the identity. (Pullback of a module along a morphism of ringed spaces)
Complexes: tensoring a complex of -modules with the ring placed in degree gives the complex with terms , and 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)
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
Hypothesis transfer. Let and put . By [F6] the structure map factors through the localisation , so is an -module whose restriction to is its given -module structure; since is flat and is flat over by hypothesis, [F4] makes flat over as well.
The Noetherian stage. By 1.1 the hypotheses of [F1] hold for and , so there are a finitely generated -subalgebra , Noetherian by [F2], a proper morphism of finite presentation , a finitely presented -module flat over in the sense of [F1], and identifications and over , where is the projection.
The stage is flat over its base local rings. Let and put ; the -module has its -action factoring through and is flat over by 1.2. For every prime , corresponding to a prime of , the change-of-rings isomorphism [F10] together with the identifications of [F5] gives , the localisation of the -module at , and this is flat over by [F4] and [F5]; hence is flat over by the local flatness criterion [F5].
The Noetherian-stage complex. By 1.3 and [F3] applied to and there are 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 and every , natural in and compatible with composition; moreover becomes a bounded complex of finite free modules on some open cover of .
Base change of finite projective modules. If is a finitely generated projective -module, then is a finitely generated projective -module: choosing finitely many generators gives a surjection [F7], projectivity of splits it so that is a direct summand of [F7], tensoring with is right exact and carries the splitting section to a splitting section [F8], the identification follows from the unit isomorphism and compatibility with finite direct sums [F5, F8], so is both a quotient and a direct summand of the free -module ; hence it is finitely generated and projective over by [F9].
The complex and its coefficient change. Put , a bounded complex of finite projective -modules concentrated in degrees and finite free in positive degrees by 1.5 and [F13]; for every -algebra the associativity and unit isomorphisms of [F5] applied to the -module and the ring give canonical isomorphisms because , natural in and compatible with composition, hence an isomorphism of complexes .
The base-changed geometry. Under the identification of 1.2, iterated base change [F11] with gives, for every -algebra , a canonical isomorphism that is compatible with the projections to .
The base-changed sheaf. The identification of 1.2 and the composition rule for pullbacks [F12] give canonical identifications , while for the projection ; since by 1.7, the isomorphism identifies these two pullbacks canonically, so naturally in and compatibly with composition of -algebra maps.
The comparison isomorphism. For every -algebra and every compose the isomorphism of 1.6 with the isomorphism of 1.4 applied to the -algebra , and with the identification induced by 1.7 and 1.8; each constituent is canonical, natural in and compatible with composition of -algebra maps, so the composite is as well.
Local finite freeness. By 1.4 there is an open cover of by affine opens such that is a bounded complex of finite free -modules; by [F11] the preimages are affine opens with and they cover . For each the associativity and unit identifications of [F5] give , a bounded complex that is finite free over because extension of scalars of a free module is free [F8]; hence is finite free locally on .
Boundaries and choice accounting. If the stage of 1.2 may be taken with , the stage complex is the zero complex with by 1.4, and for every the scheme is empty with vanishing cohomology, so both sides of 1.9 vanish; if the same argument applies with ; if then and , and if then and ; the one-member case is covered because 1.4 and 1.5 leave concentrated in degree ; for both sides of 1.9 vanish, and for the complex is concentrated in degrees by 1.6 while by 1.4; if is finitely generated over the stage 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
- Change of rings: $N\otimes_RM\cong N\otimes_S(S\otimes_RM)$
- Every algebra of finite type over a Noetherian ring is a Noetherian ring
- Affine open subschemes
- The underlying space of an affine spectrum
- The Axiom of Choice
- Base change of objects, morphisms and properties
- Cohomology object of a cochain complex
- The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain
- Finite type and finitely presented module sheaves
- Flat and faithfully flat modules and ring homomorphisms
- Generated submodule, cyclic and finitely generated modules, module basis and free module
- Locally finite presentation morphisms
- A local ring is a nonzero commutative ring with a unique maximal ideal
- Noetherian commutative rings and modules
- Projective modules and the lifting property
- Proper morphisms
- Pullback of a module along a morphism of ringed spaces
- Restriction of scalars and extension of scalars $S\otimes_RM$ along a ring homomorphism $R\to S$
- The tensor product of a right and a left chain complex is totalized by direct sums with the Koszul differential
- Iterated base change
- Restricting fibre products to open subschemes
- The submodule generated by a subset consists of the finite $R$-linear combinations of that subset
- Noetherian approximation of proper flat finitely presented sheaf data
- Finite projective complex for proper flat coherent cohomology
- Extension of scalars carries flat modules to flat modules
- Module homomorphisms induce tensor-product homomorphisms functorially
- Flatness is transitive under a flat change of rings
- Affine fibre products are spectra of tensor products
- 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
- Localisation of modules is extension of scalars
- Every localization is flat, and localizing a flat module preserves flatness
- Equivalent characterizations of projective modules
- Tensoring is right exact
- The splitting lemma for short exact sequences of modules
- The stalk of the affine structure sheaf at a prime is A_p
- Tensor products commute with arbitrary direct sums
- The regular module is a tensor unit: $R\otimes_RN\cong N$ and $M\otimes_RR\cong M$
- Universal property of a direct sum of modules
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
- The Stacks Project, Derived Categories of Schemes, Section 36.30 (perfect complexes and base change) (standard reference, not scraped)
- The Stacks Project, Cohomology of Schemes, Lemma 30.22.1 (Tag 07VK) (standard reference, not scraped)
- The Stacks Project, Limits of Schemes, Sections 32.8-32.13, especially Lemma 32.13.1 (standard reference, not scraped)
- Ravi Vakil, The Rising Sea (29 August 2022), Sections 28.1-28.2 (standard reference, not scraped)