LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Local finiteness conditions under base change

Statement

Every arbitrary base change of a locally finite-type morphism is locally of finite type. Every arbitrary base change of a locally finitely presented morphism is locally of finite presentation. There is no Noetherian or flatness hypothesis on the base.

Facts & Assumptions

Given: The objects, hypotheses and conventions in the statement above.

[F1]

A morphism $f : X \to S$ is locally of finite type if every point of $X$ has an affine open neighbourhood $U$ and $f (U)$ lies in an affine open $V = Spec A$ of $S$ such that $U = Spec B$ and $A \to B$ is of finite type. It is of finite type if it is locally of finite type and quasi-compact. (Locally finite type and finite type morphisms)

[F2]

A morphism $f : X \to S$ is locally of finite presentation if it admits affine charts as in the locally finite-type definition for which $A \to B$ is a finitely presented $A$ -algebra. This is stronger than locally finite type over a non-Noetherian base. (Locally finite presentation morphisms)

[F3]

Let $A \to C$ be a unital ring map. For any set of variables $(t_{i})$ and any ideal $I \subseteq A [t_{i}]$ , $(A [t_{i}] / I) \otimes_{A} C ≅ C [t_{i}] / I C [t_{i}] .$ Here the extended ideal is generated by the coefficient images of all elements of $I$ . For a multiplicative subset $M \subseteq A$ , $(M^{- 1} A) \otimes_{A} C ≅ {\overline{M}}^{- 1} C .$ These are ring isomorphisms; no flatness, finite-generation or nonzero-ring hypothesis is required. (Presentations and localization under base extension)

[F4]

Every diagram $X \to S \leftarrow Y$ of schemes has a fibre product. Given an affine cover $S = ⋃_{i} Spec A_{i}$ and affine covers $f^{- 1} (Spec A_{i}) = ⋃_{j} Spec B_{i j}$ and $g^{- 1} (Spec A_{i}) = ⋃_{k} Spec C_{i k}$ , the product has open affine cover $Spec (B_{i j} \otimes_{A_{i}} C_{i k}) .$ (Existence of all scheme fibre products)

Proof

1.1

At a point of the pullback, choose witnessing affine neighbourhoods $Spec B \to Spec A$ of its original source and target as in F1 or F2. Choose an affine neighbourhood $Spec C$ of its new-base image mapping into $Spec A$ . F4 gives the open product chart with ring $B \otimes_{A} C$ containing the point.

givenF1F2F4

2.1

For finite type, write $B = A [t_{1}, \dots, t_{n}] / I$ . By F3 the new ring is $C [t_{1}, \dots, t_{n}] / I C [t_{1}, \dots, t_{n}]$ , still generated by the images of the same finite list. This supplies the local witness required by F1.

F1F3step 1.1

3.1

For finite presentation, choose in addition $I = (r_{1}, \dots, r_{m})$ . Its extended ideal is generated by the same $m$ coefficient images, supplying the witness required by F2. Empty lists of generators or relations are allowed. If a chart becomes zero it is empty and contributes no point to check. These are presentations of rings themselves, including nilpotents. Localizing a finitely presented $A$ -algebra $B$ at $b$ adjoins one generator $z$ and the relation $z b - 1$ , so it remains finitely presented. This permits shrinking a witnessing source chart to principal opens inside any prescribed source open. To shrink its target to an open neighbourhood, first choose a principal target open inside it; coefficient localization gives a finite presentation over that target ring, and then perform the source shrink. Thus restrictions to opens retain the local property. Finally, composition of finite presentations $A \to B \to C$ is finite presentation: choose a finite polynomial presentation of $B$ , lift the finitely many coefficients in a finite presentation of $C$ to that polynomial ring, and use the union of the two finite variable and relation lists. To apply this to local morphisms, shrink a witnessing chart of the first map into a witnessing chart of the second by the just-proved restriction argument.

F2F3step 1.1∎

Depends on

Used by

Finite type under base change and products over a field Corollary

Dependency tree · two levels

12 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

Vakil 10.4.B(e,g); Stacks 29.15.4 and 29.22.4 (standard reference, not scraped)