LemmaStatement: 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.

Scheme Zariski Main factorization for separated quasi-finite morphisms

Statement

Assume the Axiom of Choice. If $f : X \to S$ is separated and quasi-finite and $S$ is quasi-compact and quasi-separated, then there is a factorization $X \overset{j}{\to} \overline{X} \overset{g}{\to} S$ with $j$ an open immersion and $g$ finite. For arbitrary $S$ , such a factorization exists Zariski locally on $S$ : each point of $S$ has an affine open neighbourhood on which the restricted morphism factors in this way. The local factorizations are not asserted to glue without the qcqs hypothesis.

This is the scheme-level factorization. The affine algebra factorization A quasi-finite algebra factors openly through a finite algebra alone does not prove it for a nonaffine source. The proof below reduces the qcqs claim to the finite-stage relative-normalization conclusion of Relative normalization and its finite-stage reduction, whose étale local descent and finite-stage construction are proved locally.

Facts & Assumptions

Given: AC and the separated quasi-finite morphism of the Statement.

[F1]

For a separated quasi-finite morphism over a qcqs base, the relative normalization construction has an open $X$ -image in a finite relative spectrum stage. Its recorded proof uses locally proved qcqs finite-subalgebra extension, standard étale local structure, and descent of the local open immersion (Relative normalization and its finite-stage reduction).

[F2]

A finite morphism is affine and has module-finite coordinate algebras over every affine base open (Finite morphisms of schemes, Finite is affine and local on its target). Affine quasi-finite algebras have an open finite-algebra model; this handles an affine chart but has no gluing claim (A quasi-finite algebra factors openly through a finite algebra).

[F3]

Fibre products commute with restriction to open subschemes (Restricting fibre products to open subschemes). Quasi-finite means finite type with finite fibres (Quasi-finite morphisms of schemes).

[F4]

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

Proof

Proof technique: apply the finite-stage relative-normalization lemma, then restrict to affine base opens.

1.1F1F2

Suppose first that $S$ is qcqs. By [F1] there is a finite quasi-coherent $O_{S}$ -algebra $C_{0}$ and an open immersion $j : X ↪ \overline{X} : = {Spec}_{S} C_{0}$ whose composite with the relative-spectrum projection is $f$ . On every affine base open $V = Spec A$ , the inverse image in $\overline{X}$ is $Spec C_{0} (V)$ and $C_{0} (V)$ is a finite $A$ -module by [F1], so $g : \overline{X} \to S$ is finite by [F2]. This is exactly the claimed factorization.

2.1F1F2F3step 1.1

Let $S$ be arbitrary and let $s \in S$ . Choose an affine open $V \subseteq S$ containing $s$ . The base change $f_{V} : X_{V} \to V$ is again separated and quasi-finite by restriction to an open base, using [F3]; the affine scheme $V$ is qcqs. Step 1.1 applied to $f_{V}$ gives an open immersion $X_{V} \to {\overline{X}}_{V}$ followed by a finite morphism ${\overline{X}}_{V} \to V$ . This proves the Zariski-local assertion, with no claim that the finite models on different affine opens agree.

3.1F1F2F3F4step 1.1step 2.1∎

The empty source factors through the empty finite scheme ${Spec}_{S} 0$ . No Noetherian or reducedness assumption is used; nonreduced finite fibres are allowed. The converse direction is not part of the claim. AC is inherited from [F1] and [F2], and the finite-stage and open-immersion inputs are proved in [F1].

Depends on

Used by

A proper quasi-finite morphism is finite Theorem

Dependency tree · two levels

52 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, More on Morphisms, Section 37.43 (Zariski Main Theorem) (standard reference, not scraped)