TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-30

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.

Generic flatness for finite type morphisms over Noetherian integral bases

Statement

Assume the Axiom of Choice (AC). Let $f : X \to S$ be a morphism of finite type (Locally finite type and finite type morphisms) whose base $S$ is a Noetherian integral scheme (Locally Noetherian and Noetherian schemes, Integral schemes). Then there exists a dense open subscheme $U \subseteq S$ such that the restriction $f^{- 1} (U) \to U$ is flat.

The open set produced is a finite union of nonempty principal opens and may meet parts of $S$ over which the fibre of $f$ is empty; no nonemptiness of fibres is used.

Facts & Assumptions

Given: The data and hypotheses displayed in the Statement, with the conventions fixed there.

[F1]

Assume AC. If $A$ is a Noetherian domain, $B$ a finitely generated $A$ -algebra and $M$ a finitely generated $B$ -module, then there is a nonzero $a \in A$ with $M_{a}$ free over $A_{a}$ (Generic freeness over a Noetherian domain).

[F2]

An integral scheme is nonempty and every nonempty affine open of it is the spectrum of a domain (Integral schemes).

[F3]

A morphism is of finite type when it is locally of finite type and quasi-compact; equivalently it is affine-locally given by finite-type ring maps, and inverse images of affine opens are quasi-compact (Locally finite type and finite type morphisms, Quasi-compact and quasi-separated morphisms).

[F4]

On affine charts $U = Spec B \subseteq X$ over $V = Spec A \subseteq S$ the morphism is flat at every point of $U$ if and only if $B$ is flat over $A$ (Affine-local flatness).

[F5]

For an affine chart $Spec B$ over $Spec A$ and $g \in A$ , the inverse image of $D (g)$ is $Spec (B \otimes_{A} A_{g}) = Spec B_{g}$ : fibre products of affine schemes are computed by tensor products (Affine fibre products are spectra of tensor products).

[F6]

Free modules are flat (Under the stated choice boundary, free modules are projective and hence flat).

Proof

technique · direct

1.1F2F3

Since $S$ is integral and Noetherian, affine opens form a basis and $S$ is quasi-compact; choose finitely many affine opens $Spec A_{1}, \dots, Spec A_{r}$ covering $S$ , so that each $A_{i}$ is a Noetherian domain by [F2].

1.2F3

For each $i$ the open $f^{- 1} (Spec A_{i})$ is quasi-compact by [F3]; choose a finite affine open cover $Spec B_{i 1}, \dots, Spec B_{i s_{i}}$ of it, so the induced ring maps $A_{i} \to B_{i j}$ are of finite type.

1.3F1F6

Apply [F1] to the Noetherian domain $A_{i}$ , the finitely generated $A_{i}$ -algebra $B_{i j}$ and the finitely generated $B_{i j}$ -module $M = B_{i j}$ : there is $0 \neq g_{i j} \in A_{i}$ with $(B_{i j})_{g_{i j}}$ free, hence flat, over $(A_{i})_{g_{i j}}$ .

2.1F2step 1.3

For each $i$ put $g_{i} = \prod_{j = 1}^{s_{i}} g_{i j} \in A_{i}$ , with the empty product $g_{i} = 1$ when $s_{i} = 0$ , and set $U_{i} = D (g_{i}) \subseteq Spec A_{i}$ . Since $A_{i}$ is a domain and every $g_{i j}$ is nonzero, $g_{i} \neq 0$ , so $U_{i}$ is a nonempty principal open. Put $U = U_{1} \cup \dots \cup U_{r} \subseteq S$ . Each $U_{i}$ is a nonempty open subset of the irreducible space $S$ , hence is dense in $S$ ; therefore $U$ is a dense open subset of $S$ and is a finite union of nonempty principal opens.

2.2F4F5F6step 1.3algebra

Fix $i$ and $j$ . The inverse image of $U_{i} = D (g_{i})$ inside the source chart $Spec B_{i j}$ is $Spec (B_{i j})_{g_{i}}$ by [F5]. Since $g_{i}$ is a multiple of $g_{i j}$ , this is the base change $(B_{i j})_{g_{i j}} \otimes_{(A_{i})_{g_{i j}}} (A_{i})_{g_{i}}$ ; the free $(A_{i})_{g_{i j}}$ -basis from step 1.3 remains a free basis after this base change. Thus $(B_{i j})_{g_{i}}$ is free, hence flat by [F6], over $(A_{i})_{g_{i}} = Γ (U_{i}, O_{S})$ . By [F4], $f$ is flat on this restricted source chart.

3.1F4step 1.2step 2.1step 2.2

For each $i$ , the source charts $Spec B_{i j}$ from step 1.2 cover the whole inverse image $f^{- 1} (Spec A_{i})$ , so their restrictions $Spec (B_{i j})_{g_{i}}$ cover the whole inverse image $f^{- 1} (U_{i})$ . If $s_{i} = 0$ , that inverse image is empty and flatness there is vacuous. Step 2.2 makes every nonempty restricted chart flat over $U_{i}$ . As the $U_{i}$ cover $U$ , flatness is local on source and target by [F4], and $f^{- 1} (U) \to U$ is flat.

4.1

The construction uses only the algebra maps $A_{i} \to B_{i j}$ ; no fibre of $f$ is assumed nonempty, and where $B_{i j}$ is the zero ring the lemma [F1] still supplies a nonzero $g_{i j}$ with $(B_{i j})_{g_{i j}} = 0$ free over $(A_{i})_{g_{i j}}$ , so charts with empty fibres are included in $U$ without harm. The Axiom of Choice is used exactly through [F1], as the Statement declares. [F1, step 1.3] $□$

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

39 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, Section 29.26 (flat morphisms, descent) (standard reference, not scraped)
The Stacks Project, Commutative Algebra, Section 10.40 (faithfully flat descent) (standard reference, not scraped)
The Stacks Project, Commutative Algebra, Section 10.108 (generic flatness) (standard reference, not scraped)