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.
Depends on
Used by
- Frobenius linear systems have nonreduced general members Counterexample
- The equation must define the intended scheme Counterexample
- Affine n-space over an arbitrary base Example
- A transverse hyperplane slice is smooth at the chosen point Lemma
- Affine finite-type source immerses into relative projective space Lemma
- An S-rational map defined after a faithfully flat smooth base change is defined Lemma
- Closed gluing of two projective three-spaces is proper Lemma
- Eventual generation of coherent projective twists Lemma
- Fpqc descent of properness components Lemma
- Projective space is of finite type over its base Lemma
- Properness is local on the target Lemma
- Properness survives composition Lemma
- Rational maps from a smooth curve to a proper scheme are morphisms Lemma
- Support dimension under field extension Lemma
- High powers of an ample line bundle embed a proper scheme Theorem
- Immersions are monomorphisms locally of finite type Theorem
- Purely inseparable field algebras separate regularity from smoothness Theorem
Dependency tree · two levels
18 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, Morphisms of Schemes, Lemma 15.2 (standard reference, not scraped)
- The Stacks Project, Algebra, Lemma 10.23.3 (standard reference, not scraped)