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.
Finite type and finitely presented module sheaves
Definition
Let be a scheme and let be a quasi-coherent -module (Quasi-coherent module on a scheme). For write for the sheaf with componentwise restriction, a sheaf of -modules (Modules on a ringed space); it is the free -module of rank , and .
Finite type. is of finite type if every point has an affine open neighbourhood together with an -module and an isomorphism such that is finitely generated (Finitely presented modules and finitely presented algebras).
Finitely presented. is finitely presented if every point has an affine open neighbourhood together with an -module and an isomorphism such that is finitely presented.
The equivalent local form under AC. Assume the Axiom of Choice (The Axiom of Choice), inherited from the associated-sheaf existence theorem in the equivalence argument below. Because of the local nature of the conditions, is of finite type if and only if can be covered by affine opens on which there is a finite family of sections generating , meaning that the induced morphism of -modules is an epimorphism, equivalently that is an exact sequence of sheaves (Exact sequences of sheaves). Likewise is finitely presented if and only if can be covered by affine opens admitting an exact sequence with finite.
Why the two forms agree under AC. Let be affine and let for an -module . First , since the two sheaves have the same sections on every distinguished open and sheaves on the basis are determined by those sections (The associated module sheaf exists). Every morphism of -modules is induced by its component on global sections, an -linear map : a morphism is determined by its components on distinguished opens (The associated module sheaf exists), a general -linear map induces compatible maps on distinguished opens, and these two constructions are inverse by the functoriality of the localisations recorded in Module sheaf on an affine scheme. If is generated by the images of the standard basis under , then localisation is exact (Localisation of modules is exact), so each component is surjective, and a morphism whose components on a basis are surjective is an epimorphism: a germ of at a point is represented on some distinguished open and can be lifted there. Conversely, let correspond to an epimorphism and put ; the components of the composite are , because localisation is right exact, so this composite is the zero morphism on every distinguished open and hence is zero; it is also a composite of epimorphisms, so its target has all stalks zero, and then by the identification of global sections (The associated module sheaf exists). Thus is surjective, so is generated by elements and exhibits the finite family of global sections . Applying the same translation to the kernel of a surjection gives the finitely presented form. The elementwise criterion for equality and vanishing in a localisation (Localisation of a module at a multiplicative subset) is what turns the componentwise statements into statements about .
Immediate consequences. The conditions are local on and invariant under isomorphism of -modules; a finitely presented quasi-coherent module is of finite type, since a finitely presented module is generated by the images of the standard basis; restrictions to open subschemes again satisfy the corresponding condition; and the zero module is finitely presented (take ), hence of finite type, on every chart. No Noetherian, separatedness or finiteness hypothesis on is built into the definition, and the definition says nothing about existence of local frames, which is the stronger condition treated separately on this page.
Depends on
- The Axiom of Choice
- Quasi-coherent module on a scheme
- Finitely presented modules and finitely presented algebras
- Module sheaf on an affine scheme
- The associated module sheaf exists
- Localisation of a module at a multiplicative subset
- Localisation of modules is exact
- Exact sequences of sheaves
- Modules on a ringed space
Used by
- Euler characteristic in a proper flat family is locally constant Corollary
- Global functions on geometrically connected and geometrically reduced proper schemes Corollary
- Upper semicontinuity of fibre cohomology dimensions Corollary
- Finite type need not be locally free Counterexample
- Proper cohomology need not be finite for noncoherent sheaves Counterexample
- Coherent module sheaves Definition
- Fitting ideal sheaves Definition
- Internal Hom of module sheaves Definition
- A coherent closed-point skyscraper Example
- All twists on the projective line Example
- An upper jump of h0 in a flat projective family Example
- Fitting ideals of a diagonal two-by-two presentation Example
- Closed immersion preserves cohomology and coherent pushforward Lemma
- Finite projective complex for proper flat coherent cohomology Lemma
- Finite-stage descent of finitely presented quasi-coherent sheaves Lemma
- Finite-stage descent of relative flatness for a finitely presented sheaf Lemma
- Flat field extension commutes with coherent cohomology Lemma
- Geometric Nakayama for finite-type sheaves Lemma
- Internal Hom from a finitely presented sheaf is quasi-coherent Lemma
- Noetherian approximation of proper flat finitely presented sheaf data Lemma
- Noetherian devissage for coherent proper pushforward Lemma
- Projective coherent finiteness and large twist vanishing Lemma
- Regular hyperplane step for coherent support induction Lemma
- Support dimension under field extension Lemma
- Universal finite projective cohomology complex over any base Lemma
- Coherence is essential for proper finiteness Remark
- Coherent higher direct images under proper morphisms Theorem
- Coherent sheaves on a locally Noetherian scheme Theorem
- Cohomology and base change for proper flat coherent families Theorem
- Finite coherent cohomology for proper schemes Theorem
- Fitting ideals control fibre generator loci Theorem
- High powers of an ample line bundle embed a proper scheme Theorem
- Openness of the finite free locus Theorem
- Serre global-generation criterion for ampleness Theorem
- Support of a finite-type quasi-coherent sheaf is closed Theorem
Dependency tree · two levels
34 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, Schemes, §§26.5, 26.7, 26.24 (standard reference, not scraped)
- Ravi Vakil, The Rising Sea, 29 August 2022, Chapters 6, 14, 17 (standard reference, not scraped)
- The Stacks Project, Cohomology of Schemes §30.9 (standard reference, not scraped)
- The Stacks Project, Properties of Schemes, §§28.20, 28.26 (standard reference, not scraped)