TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 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.

A proper quasi-finite morphism is finite

Statement

Assume the Axiom of Choice. Every proper quasi-finite morphism of schemes $f : X \to S$ is finite (Proper morphisms, Quasi-finite morphisms of schemes, Finite morphisms of schemes). No Noetherian or nonemptiness hypothesis is imposed, and the assertion is local on the base.

This proof depends on the scheme-level Zariski Main factorization Scheme Zariski Main factorization for separated quasi-finite morphisms. Its relative-normalization and finite-stage inputs are proved locally; the reduction from that factorization to finiteness is completed below.

Facts & Assumptions

Given: AC and a proper quasi-finite morphism $f : X \to S$ .

[F1]

A quasi-finite separated morphism factors Zariski locally on the base as an open immersion $j : X ↪ \overline{X}$ followed by a finite morphism $g : \overline{X} \to S$ ; the supplier proves the étale descent and finite-stage construction (Scheme Zariski Main factorization for separated quasi-finite morphisms).

[F2]

A finite morphism is affine (Finite is affine and local on its target) and an affine morphism is separated (Affine morphisms are separated).

[F3]

If $X \to S$ is proper and $Y \to S$ separated, every $S$ -morphism $X \to Y$ is proper (Morphisms from a proper scheme to a separated one are proper). A proper morphism is closed (Proper morphisms are closed).

[F4]

On an affine target $Spec B$ , a closed immersion has source $Spec (B / I)$ for an ideal $I$ , compatibly with base change (Closed immersions are affine quotients and survive base change). A quotient of a module-finite $A$ -algebra is module-finite over $A$ .

[F5]

A morphism is finite exactly when it is affine with finite module algebras over affine target opens (Finite morphisms of schemes). It is proper when separated, of finite type and universally closed; in particular properness supplies separatedness (Proper morphisms).

[F6]

AC is the choice-function axiom (The Axiom of Choice).

Proof

technique · factor through a finite scheme, then make the open immersion closed using properness

1.1F1F2F3F5

Finiteness is local on the base by [F5], so replace $S$ by an affine open in a cover on which [F1] supplies $f = g \circ j$ with $j : X ↪ \overline{X}$ open and $g : \overline{X} \to S$ finite. Since $f$ is proper it is separated, as required by [F1]. By [F2] the finite morphism $g$ is separated, so [F3] applied to the $S$ -map $j$ makes $j$ proper.

2.1F3F4step 1.1

The image $j (X)$ is open in $\overline{X}$ because $j$ is an open immersion, and closed because $j$ is proper and hence a closed map by [F3]. Thus it is open and closed. An open immersion identifies $X$ with the open subscheme $j (X)$ ; because its complement is also open, the same inclusion is a closed immersion. On any affine open $Spec B$ of $\overline{X}$ , [F4] therefore writes the corresponding part of $X$ as $Spec (B / I)$ .

3.1F4F5step 1.1step 2.1

For an affine open $Spec A \subseteq S$ , finiteness of $g$ gives $g^{- 1} (Spec A) = Spec B$ with $B$ finite as an $A$ -module. By step 2.1 the inverse image under $f$ is $Spec (B / I)$ for an ideal $I$ , and $B / I$ is a quotient of the finite $A$ -module $B$ . Hence $f$ is finite over this affine base by [F5]. The base-local conclusions glue to give finiteness over all of $S$ .

4.1F1F4F5F6step 3.1∎

If $X = \emptyset$ , the coordinate algebra is the zero ring, finite as an $A$ -module, and the argument still applies. No reducedness or Noetherian hypothesis is used. AC enters only through the invoked suppliers in [F1] and [F4]; the scheme-level factorization is supplied by [F1].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

65 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.44 (finite morphisms) (standard reference, not scraped)