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.
Coherent module sheaves
Definition
Let be a scheme and let be a quasi-coherent -module (Quasi-coherent module on a scheme) that is of finite type (Finite type and finitely presented module sheaves). Then is coherent if for every open and every morphism the kernel sheaf is of finite type (Kernel sheaves are objectwise, while cokernels and images are sheafified).
Under the Axiom of Choice (The Axiom of Choice), inherited from the associated-sheaf existence theorem at the sheaf-kernel identification below, the following affine test is equivalent to the definition. Since the conditions are local, it suffices to test affine opens on which for a finitely generated -module : then a morphism is given by an -linear map (Finite type and finitely presented module sheaves) and, as localisation is exact (Localisation of modules is exact), the kernel sheaf has , so it is the associated sheaf of the finitely generated module precisely when that kernel is finitely generated (The associated module sheaf exists).
Finite presentation does not imply coherence under the same AC assumption. Over a general base the kernel condition is a genuine additional hypothesis. Let be a field and let the classes of form a -basis of , so as a -module, and multiplication by , viewed as an -linear map , has kernel , which is not finitely generated as an -module. The module is finitely presented, even free of rank one, but the associated sheaf on receives the morphism corresponding to (Finite type and finitely presented module sheaves, The associated module sheaf exists) whose kernel is the associated sheaf of and is not of finite type. Hence is not coherent on this ; finite presentation, and even local freeness of finite rank, do not by themselves imply coherence over an arbitrary base. The identification of coherent with finite type is a theorem about locally Noetherian schemes, proved on this page; over a locally Noetherian scheme finite locally free sheaves are therefore coherent.
Immediate consequences. Coherence is local on and invariant under isomorphism; a coherent module is of finite type by definition; restrictions of coherent modules to open subschemes are coherent; and the zero module is coherent. On a locally Noetherian scheme the kernel condition is automatic for finite-type quasi-coherent modules, and the theorem on this page proves the converse direction: there, finite type and coherent coincide (Locally Noetherian and Noetherian schemes). Over a non-Noetherian ring the two notions differ, as the example above shows, and the relation-kernel condition must be checked; the remark on this page records that warning.