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.
High-degree section module is finite graded
Statement
Assume the Axiom of Choice as inherited from the cited suppliers (The Axiom of Choice). Let be a Noetherian commutative ring with (Noetherian commutative rings and modules), let , write for the polynomial ring in the total-degree grading (The polynomial ring as finitely supported coefficient families on monomials), let with twisting sheaves (Relative projective space from standard charts, Projective space is Proj of a polynomial ring), and let be a coherent -module (Coherent module sheaves). For every put (Twists of a quasi-coherent sheaf), so that is a graded -module with the multiplication induced by the maps of the twisting sheaves (Twisting sheaf on Proj, Invertible twists for degree-one generated rings).
Then there is an integer such that the truncated graded module is a finitely generated -module (Generated submodule, cyclic and finitely generated modules, module basis and free module).
Moreover, if is a closed subscheme and a coherent -module, then the extension by zero is a coherent -module and the same conclusion holds for it; that is, for a suitable the graded module is finitely generated over . The zero module, the zero ring , the empty projective space and the case are included.
Facts & Assumptions
Given: The Axiom of Choice as inherited, a Noetherian commutative ring , an integer , the graded polynomial ring , the projective space , and a coherent module on .
The twisting sheaves satisfy (Twisting sheaf on Proj), each is invertible with and (Invertible twists for degree-one generated rings, Twists of a quasi-coherent sheaf); on a standard chart the twist is trivial, so a twist of a finite type or quasi-coherent module is again of the same kind. Tensoring a short exact sequence of -modules by an invertible sheaf preserves exactness: on stalks the invertible sheaf is free of rank one over the local ring, tensoring with a free module is exact, and exactness is stalkwise. (Tensor product of sheaves of modules, The stalk of a tensor product sheaf is the tensor product of the stalks, Under the stated choice boundary, free modules are projective and hence flat, A sequence of abelian sheaves is exact exactly when it is exact on every stalk, Invertible sheaves)
is ample on in the absolute sense: the identity is a quasi-compact closed immersion over pulling back to , so is closed H-very ample relative to the affine base and hence ample. (Relative very ampleness in the finite projective-space convention, Relative very ampleness implies relative ampleness, Absolute ampleness by affine section opens)
Since is projective over the Noetherian ring in the H-projective convention (the identity is a closed immersion over ) and is ample, there is such that is globally generated for every . (Eventual generation of coherent projective twists, Global generation by the evaluation map)
A globally generated quasi-coherent module of finite type on a quasi-compact scheme is a quotient of for some finite : for every point there are finitely many global sections generating the stalk at , the locus where a fixed finite family of global sections generates is the complement of the support of the cokernel of , which is closed because that cokernel is quasi-coherent of finite type, and a finite subcover of the quasi-compact space is extracted from these loci. (Global generation by the evaluation map, Support of a finite-type quasi-coherent sheaf is closed, Quasi-compact and quasi-separated schemes)
On the locally Noetherian scheme the kernel of a morphism of coherent modules is coherent, and the same holds for twists of coherent modules. (Coherent sheaves on a locally Noetherian scheme, Locally Noetherian and Noetherian schemes, Coherent module sheaves)
For a coherent module on with Noetherian there is such that for every and every . Indeed Projective coherent finiteness and large twist vanishing gives a bound for each ; take the maximum of these finitely many bounds and . For all twists vanish by Projective n-space has quasi-coherent cohomological dimension at most n, so this maximum works for every , also for .
For the canonical map is an isomorphism, and these identifications are compatible with the multiplication maps, so that is the graded ring ; consequently for each fixed and all large , is identified with . (Cohomology of O(d) on projective space, Twisting sheaf on Proj)
For a fixed integer and , the shifted graded -module is generated in degree by the finitely many monomials of polynomial degree , so it is finitely generated; the ring is Noetherian, and a quotient of a finitely generated graded module over is finitely generated. (If is Noetherian then is Noetherian for every , Hilbert basis theorem: if is Noetherian then is Noetherian, Generated submodule, cyclic and finitely generated modules, module basis and free module)
For a closed immersion into the locally Noetherian scheme and a coherent -module , the pushforward is coherent (Closed immersion preserves cohomology and coherent pushforward), and on an affine chart with the identity holds, because both sides are, on the basic opens of the chart, the localisations of the same -module; hence . (Closed immersions are affine quotients and survive base change, Direct image of a sheaf along a continuous map, Tensor product of sheaves of modules)
Proof
Ampleness and eventual global generation. By [F2] the twisting sheaf is ample on ; the identity exhibits as closed H-projective over the Noetherian ring , so [F3] produces with globally generated for all .
A finite surjection from a finite sum of twists. Since is globally generated and of finite type on the quasi-compact scheme , [F4] gives a surjection for some finite . Twisting by and using [F1] and its inverse, this yields a surjection where is a finite direct sum of twists of .
The kernel is coherent. Let . Since is Noetherian, is locally Noetherian, and is coherent by [F5]; by [F1] every twist is coherent as well.
Serre vanishing for the kernel. Apply [F6] to the coherent module : there is such that for every and every ; in particular for those .
The section maps are surjective. For tensoring by the invertible sheaf keeps the sequence exact by [F1]. The long exact cohomology sequence of the underlying abelian sheaves (Long exact sequence of sheaf cohomology) contains ; hence the degree- component is surjective for every . These maps are compatible with the -module structure because they are induced by the morphism and the multiplication maps of the twisting sheaves.
The tail of is finitely generated. For the module is the direct sum of copies of , and by [F7] its sections are identified with the direct sum of copies of ; here by step 4.1. The resulting tail is therefore a finite direct sum of shifted tails of , each finitely generated by [F8].
The tail of is finitely generated. By [step 5.1] the -module homomorphism of tails is surjective, and the source is finitely generated by [step 6.1]; the quotient is finitely generated over the Noetherian ring by [F8]. This proves the first assertion with .
Extension by zero from a closed subscheme. Let be a closed subscheme with locally Noetherian and coherent on . By [F9] the pushforward is coherent on , so [step 7.1] applied to gives with finitely generated, and by the identification of [F9] this graded module is ; this proves the second assertion.
Boundary and choice accounting. If then every and the tail is the zero module, which is finitely generated (by the empty family). If then and , all coherent modules are zero and the tail is zero; the Noetherian hypotheses hold for the zero ring and is Noetherian by [F8]. If then is affine, is the associated sheaf of a finitely generated -module and one checks directly that the tail of is generated by a finite generating set of in degree , since the twisting by is an isomorphism on the single chart; this agrees with the general argument, which also applies because is ample by [F2]. The Axiom of Choice is consumed through the global-generation theorem [F3], the coherence theorem [F5] and the finiteness theorem [F6]; no chart, resolution or generating family is chosen here beyond the finitely many sections of [step 2.1].
Depends on
If is Noetherian then is Noetherian for every
Under the stated choice boundary, free modules are projective and hence flat
Absolute ampleness by affine section opens
The Axiom of Choice
Coherent module sheaves
Commutative ring
Direct image of a sheaf along a continuous map
Generated submodule, cyclic and finitely generated modules, module basis and free module
Global generation by the evaluation map
Invertible sheaves
Locally Noetherian and Noetherian schemes
Noetherian commutative rings and modules
The polynomial ring as finitely supported coefficient families on monomials
Quasi-coherent module on a scheme
Quasi-compact and quasi-separated schemes
Relative projective space from standard charts
Tensor product of sheaves of modules
Twists of a quasi-coherent sheaf
Twisting sheaf on Proj
Relative very ampleness in the finite projective-space convention
Closed immersions are affine quotients and survive base change
Closed immersion preserves cohomology and coherent pushforward
Eventual generation of coherent projective twists
Projective coherent finiteness and large twist vanishing
The stalk of a tensor product sheaf is the tensor product of the stalks
Relative very ampleness implies relative ampleness
Coherent sheaves on a locally Noetherian scheme
Projective n-space has quasi-coherent cohomological dimension at most n
Cohomology of O(d) on projective space
A sequence of abelian sheaves is exact exactly when it is exact on every stalk
Hilbert basis theorem: if is Noetherian then is Noetherian
Long exact sequence of sheaf cohomology
Projective space is Proj of a polynomial ring
Support of a finite-type quasi-coherent sheaf is closed
Invertible twists for degree-one generated rings