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 is affine-local on source and target
Statement
Being locally of finite type is affine-local on both source and target. A quasi-compact morphism locally of finite type is of finite type; equivalently, over each affine target open it may be tested on a finite affine source cover.
Facts & Assumptions
Given: A morphism and affine source and target covers.
Proof
Restricting a finite-type ring map to distinguished affine opens localizes the map and retains a finite generating set, so the condition survives affine refinement.
Conversely, let be an affine target and an affine source open. Around each point of , choose an affine chart from the given finite-type source cover. First choose a principal open in contained in , then a smaller principal open in contained in the first one. The latter is principal in as well: its defining function on the first open belongs to a localization of , so clearing a power of the first defining function gives one element of . Quasi-compactness of now supplies a finite cover by such common principal opens. Each is a localization of a finite-type -algebra , hence is finite type over .
Here is the needed finite-localization descent, rather than just an appeal to it. Choose with . For every , choose finitely many -algebra generators of and write each as with . Let be the -subalgebra generated by all . Then for every , and the generate the unit ideal already in . For any , localization gives for some for each . The powers also generate the unit ideal in , so . Thus is finitely generated over . This is the finite-type part of Stacks Project, Tag 00EP.
On an affine target , refine any target cover to a finite cover by opens that are principal also in the chosen affine target charts, using the common-principal construction of step 2.1. Base change to each preserves finite type of the source charts. For an affine , the inverse images are the principal opens ; steps 2.1 and 3.1 make their coordinate rings finite type over , hence over . Applying step 3.1 again gives finite type on . Finally, quasi-compactness of supplies a finite affine source subcover over each affine target open, so locally finite type plus quasi-compactness is exactly finite type.