LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 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.

Eventual generation of coherent projective twists

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $A$ be a Noetherian commutative ring (Noetherian commutative rings and modules) and let $X$ be a scheme projective over $A$ in the finite-dimensional H-projective convention (Projective morphisms before Proj): the structure morphism $X \to Spec A$ (The underlying space of an affine spectrum) factors over $Spec A$ as a closed immersion $X ↪ P_{A}^{n}$ (Relative projective space from standard charts) followed by the projection, for some $n \geq 0$ . Let $L$ be an ample invertible $O_{X}$ -module (Absolute ampleness by affine section opens, Invertible sheaves) and let $F$ be a coherent $O_{X}$ -module (Coherent module sheaves). Then there is an integer $m_{0}$ such that $F \otimes_{O_{X}} L^{\otimes m}$ is globally generated (Global generation by the evaluation map) for every $m \geq m_{0}$ ; the bound may depend on $F$ . The empty scheme $X$ , the zero module $F = 0$ and the cases $n = 0$ and $Spec A = \emptyset$ are included, and no effectivity of $m_{0}$ is claimed.

Facts & Assumptions

Given: The Axiom of Choice, a Noetherian commutative ring $A$ , a scheme $X$ projective over $A$ , an ample invertible $O_{X}$ -module $L$ and a coherent $O_{X}$ -module $F$ .

[F1]

$f : X \to S$ is projective in the H-projective convention when for some $n \geq 0$ it factors over $S$ as a closed immersion $X ↪ P_{S}^{n}$ followed by the projection of relative projective space; $n = 0$ is allowed with $P_{S}^{0} ≅ S$ , and for $S = Spec A$ the standard charts of $P_{A}^{n}$ are the affine schemes $Spec A [x_{ℓ}^{(i)}]$ . (Projective morphisms before Proj, Relative projective space from standard charts, The underlying space of an affine spectrum)

[F2]

Assume AC. Every projective morphism is proper; a morphism is proper exactly when it is separated, of finite type and universally closed. (Projective morphisms are proper, Proper morphisms)

[F3]

A morphism is of finite type when it is locally of finite type and quasi-compact; a morphism is quasi-compact when the inverse image of every quasi-compact open is quasi-compact; being locally of finite type is affine-local on source and target, so over an affine target it is tested on affine source charts, and a quasi-compact morphism locally of finite type is of finite type. (Locally finite type and finite type morphisms, Quasi-compact and quasi-separated morphisms, Finite type is affine-local on source and target)

[F4]

Every commutative algebra of finite type over a Noetherian commutative ring is a Noetherian ring; a scheme is locally Noetherian when it has an affine open cover by spectra of Noetherian rings and Noetherian when it is in addition quasi-compact. (Every algebra of finite type over a Noetherian ring is a Noetherian ring, Locally Noetherian and Noetherian schemes, Every affine scheme is quasi-compact)

[F5]

Serre criterion for ampleness: for a Noetherian scheme $X$ and an invertible $O_{X}$ -module $L$ , the sheaf $L$ is ample if and only if for every coherent $O_{X}$ -module $G$ the twist $G \otimes_{O_{X}} L^{\otimes n}$ is globally generated for all sufficiently large integers $n$ , the bound depending on $G$ . (Serre global-generation criterion for ampleness)

[F6]

Conventions: $L$ invertible means locally free of rank one, with tensor powers $L^{\otimes m}$ , $m \geq 0$ , and $L^{\otimes 0} = O_{X}$ ; ampleness is the covering-by-nonvanishing-loci condition of the cited definition; a sheaf is globally generated when its evaluation map $Γ (X, H) \otimes_{Z} O_{X} \to H$ is surjective; coherence is the finite-type-and-kernel condition of the cited definition. (Invertible sheaves, Absolute ampleness by affine section opens, Global generation by the evaluation map, Coherent module sheaves)

[F7]

The Axiom of Choice states that every family of nonempty sets has a choice function. (The Axiom of Choice)

Proof

technique · direct: a projective morphism is proper, so $X$ has affine charts of finite type over the Noetherian ring $A$ and is quasi-compact; hence $X$ is Noetherian, and the forward direction of the Serre criterion yields the eventual global generation

1.1F1

By [F1] the structure morphism $p : X \to Spec A$ is projective: there are $n \geq 0$ and a closed immersion $i : X ↪ P_{A}^{n}$ with $p = π \circ i$ , where $π$ is the projection of the relative projective space.

1.2F2F3

By [F2] the morphism $p$ is proper, hence of finite type and (being of finite type) quasi-compact by [F3].

2.1F3F4step 1.2

Let $x \in X$ . Since $p$ is locally of finite type and the target $Spec A$ is affine, [F3] provides an affine open $U = Spec B \subseteq X$ containing $x$ with $p (U) \subseteq Spec A$ and $A \to B$ of finite type. As $A$ is Noetherian, [F4] makes $B$ a Noetherian ring. The point $x$ was arbitrary, so $X$ has an affine open cover by spectra of Noetherian rings and is locally Noetherian by [F4].

3.1F3F4step 1.2step 2.1

The scheme $Spec A$ is quasi-compact, so the inverse image $X = p^{- 1} (Spec A)$ is quasi-compact because $p$ is quasi-compact by 1.2; with 2.1, [F4] makes $X$ a Noetherian scheme.

4.1F5step 3.1

Apply the forward direction of the Serre criterion [F5] to the Noetherian scheme $X$ , the ample invertible sheaf $L$ and the coherent sheaf $F$ : there is an integer $m_{0}$ , depending on $F$ , such that $F \otimes_{O_{X}} L^{\otimes m}$ is globally generated for every $m \geq m_{0}$ , which is the asserted conclusion.

5.1F1F2F5F6F7step 2.1step 4.1∎

Boundaries and choice accounting. If $X = \emptyset$ then the empty morphism to $Spec A$ is projective (take $n = 0$ and the empty closed subscheme of $P_{A}^{0} = Spec A$ ), the only coherent module on $X$ is $F = 0$ by [F6], and $0 \otimes_{O_{X}} L^{\otimes m} = 0$ is globally generated for every $m$ , so any $m_{0}$ works; the same argument covers $F = 0$ over any $X$ . If $Spec A = \emptyset$ then also $X = \emptyset$ , since a projective morphism has empty source over an empty target. If $n = 0$ then $X$ is isomorphic to a closed subscheme $Spec (A / I)$ of $Spec A$ and is affine Noetherian, and 4.1 still applies. The bound $m_{0}$ is obtained from [F5] without effectivity, and it is unique only up to enlarging. The Axiom of Choice [F7] is consumed through [F2] and [F5] and through the selection, in 2.1, of one affine Noetherian chart for each point of $X$ ; all statements remain those of the cited suppliers.

Depends on

Used by

Dependency tree · two levels

65 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, Properties of Schemes, Proposition 28.27.13 (Tag 01Q3) (standard reference, not scraped)
The Stacks Project, Morphisms of Schemes, Lemma 29.44.5 (Tag 01WC) (standard reference, not scraped)
Ravi Vakil, The Rising Sea (29 August 2022), Sections 17.4, 17.6 (standard reference, not scraped)