Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedverified 2026-09-26 (gpt-6-sol)
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 f:X→S and affine source and target covers.

Proof

technique · direct
1.1given

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.

2.1step 1.1givenalgebra

Conversely, let V=Spec⁡R be an affine target and U=Spec⁡A⊆f−1(V) an affine source open. Around each point of U, choose an affine chart W=Spec⁡C from the given finite-type source cover. First choose a principal open in U contained in W, then a smaller principal open in W contained in the first one. The latter is principal in U as well: its defining function on the first open belongs to a localization of A, so clearing a power of the first defining function gives one element of A. Quasi-compactness of U now supplies a finite cover U=⋃i=1nDU(ai) by such common principal opens. Each Aai is a localization of a finite-type R-algebra C, hence is finite type over R.

3.1step 2.1constructalgebra

Here is the needed finite-localization descent, rather than just an appeal to it. Choose hi∈A with ∑ihiai=1. For every i, choose finitely many R-algebra generators of Aai and write each as yij/aikij with yij∈A. Let B⊆A be the R-subalgebra generated by all ai,hi,yij. Then Bai=Aai for every i, and the ai generate the unit ideal already in B. For any x∈A/B, localization gives aiNix=0 for some Ni for each i. The powers aiNi also generate the unit ideal in B, so x=0. Thus A=B is finitely generated over R. This is the finite-type part of Stacks Project, Tag 00EP.

4.1step 1.1step 2.1step 3.1algebra∎

On an affine target V, refine any target cover to a finite cover by opens DV(rj) that are principal also in the chosen affine target charts, using the common-principal construction of step 2.1. Base change to each DV(rj) preserves finite type of the source charts. For an affine U⊆f−1(V), the inverse images are the principal opens DU(f#rj); steps 2.1 and 3.1 make their coordinate rings finite type over OS(DV(rj)), hence over OS(V). Applying step 3.1 again gives finite type on U. Finally, quasi-compactness of f 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

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