Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedjudge 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.

Finite type and finitely presented module sheaves

Definition

Let X be a scheme and let F be a quasi-coherent OX-module (Quasi-coherent module on a scheme). For n≥0 write OXn for the sheaf U↦OX(U)n with componentwise restriction, a sheaf of OX-modules (Modules on a ringed space); it is the free OX-module of rank n, and OX0=0.

Finite type. F is of finite type if every point x∈X has an affine open neighbourhood U=Spec⁡A together with an A-module M and an isomorphism F∣U≅M~ such that M is finitely generated (Finitely presented modules and finitely presented algebras).

Finitely presented. F is finitely presented if every point x∈X has an affine open neighbourhood U=Spec⁡A together with an A-module M and an isomorphism F∣U≅M~ such that M 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, F is of finite type if and only if X can be covered by affine opens U=Spec⁡A on which there is a finite family of sections s1,…,sn∈F(U) generating F∣U, meaning that the induced morphism of OU-modules OUn→F∣U is an epimorphism, equivalently that OU n⟶F∣U⟶0 is an exact sequence of sheaves (Exact sequences of sheaves). Likewise F is finitely presented if and only if X can be covered by affine opens U admitting an exact sequence OU m⟶OU n⟶F∣U⟶0 with m,n finite.

Why the two forms agree under AC. Let U=Spec⁡A be affine and let F∣U≅M~ for an A-module M. First An~≅OUn, since the two sheaves have the same sections (Af)n on every distinguished open and sheaves on the basis are determined by those sections (The associated module sheaf exists). Every morphism An~→M~ of OU-modules is induced by its component on global sections, an A-linear map ψ:An→M: a morphism is determined by its components on distinguished opens (The associated module sheaf exists), a general A-linear map induces compatible maps Afn→Mf on distinguished opens, and these two constructions are inverse by the functoriality of the localisations recorded in Module sheaf on an affine scheme. If M is generated by the images of the standard basis under ψ, then localisation is exact (Localisation of modules is exact), so each component Afn→Mf is surjective, and a morphism whose components on a basis are surjective is an epimorphism: a germ of M~ at a point is represented on some distinguished open and can be lifted there. Conversely, let ψ:An→M correspond to an epimorphism φ and put N=M/ψ(An); the components of the composite An~→M~→N~ are Afn→Mf→Nf=0, 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 N=Γ(U,N~)=0 by the identification of global sections (The associated module sheaf exists). Thus ψ is surjective, so M is generated by n elements and φ exhibits the finite family of global sections ψ(e1),…,ψ(en). Applying the same translation to the kernel of a surjection An→M 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 M.

Immediate consequences. The conditions are local on X and invariant under isomorphism of OX-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 m=n=0), hence of finite type, on every chart. No Noetherian, separatedness or finiteness hypothesis on X 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

Used by

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