ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedaudited 2026-09-27

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 finite algebra is its own Zariski Main factor

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $R \to S$ be a ring map such that $S$ is a finite $R$ -algebra, that is module-finite over $R$ (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras). Then:

The integral closure $S^{'} = {Int}_{R} (S)$ of the image of $R$ in $S$ (Integral elements subalgebra of an arbitrary ring map) is all of $S$ .
In the local form of Zariski's main theorem (Algebraic Zariski Main localization at a quasi-finite prime) the element $g : = 1$ witnesses the conclusion at every prime: $1 \notin q$ for every $q \in Spec (S)$ and $S_{1}^{'} = S_{1} = S = S_{1} .$
In the finite factorization theorem (A quasi-finite algebra factors openly through a finite algebra) one may take $T : = S$ : this is a finite $R$ -subalgebra of $S^{'}$ that equals $S^{'}$ , the contraction map $Spec (S) \to Spec (T)$ is the identity of $Spec (S)$ , its image $Spec (S)$ is open, and the cover of the theorem may be the single principal open $D_{T} (1) = Spec (T)$ (Distinguished-subset identities).

Thus for a module-finite algebra the local element, the finite factor and the open piece are the trivial ones: the relative integral closure is the whole algebra, nothing needs to be inverted, and the factorization is the identity. The Axiom of Choice is inherited from the two general theorems cited in parts 2 and 3; the direct verification below uses the finite-module criterion for integrality and requires no choice.

Facts & Assumptions

Given: A ring map $R \to S$ such that $S$ is module-finite over $R$ , i.e. a finite $R$ -algebra, with $A = Im (R) \subseteq S$ the image of the structure map, and the Axiom of Choice.

[L1]

An $R$ -algebra $A$ is module-finite over $R$ when it is finitely generated as an $R$ -module (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras).

[L2]

An element $b$ of a commutative ring $B$ is integral over a subring $A \subseteq B$ when it is a root of a monic polynomial in $A [X]$ (Integral elements over a commutative ring and algebraic integers).

[L3]

The Axiom of Choice (AC) is the statement that every family of nonempty sets has a choice function (The Axiom of Choice).

[L4]

Let $A \subseteq B$ be commutative rings with $A \neq 0$ and $b \in B$ . Then $b$ is integral over $A$ if and only if there exists a faithful $A [b]$ -module that is finitely generated over $A$ , faithfulness meaning that $r M = 0$ implies $r = 0$ for $r \in A [b]$ (Integrality and finite-module characterizations for one element).

[L5]

For a unital ring map $R \to S$ the relative integral closure ${Int}_{R} (S)$ is the subring of $S$ of elements integral over the map; it contains the image of $R$ and is exactly the integral closure of that image in $S$ (Integral elements subalgebra of an arbitrary ring map).

[L6]

A proper ideal $P ⊊ R$ is prime when $a b \in P$ implies $a \in P$ or $b \in P$ (Prime ideals and maximal ideals in a commutative ring).

[L7]

For $f \in R$ the principal localisation is $R_{f} = S_{f}^{- 1} R$ with $S_{f} = {1, f, f^{2}, \dots}$ ; in particular $R_{1}$ is canonically isomorphic to $R$ (Principal localisation $R_{f} = {1, f, f^{2}, \dots}^{- 1} R$ ).

[L8]

For every ring homomorphism $φ : R \to A$ contraction defines a continuous map $Spec (A) \to Spec (R)$ , and $Spec$ is a contravariant functor, so the identity ring map induces the identity on spectra (The prime-spectrum construction is a contravariant functor to topological spaces).

[L9]

The subsets $V (I)$ of $Spec (R)$ contain $Spec (R)$ and $\emptyset$ and define a topology on $Spec (R)$ (The vanishing sets define the Zariski topology on the prime spectrum).

[L10]

For $f \in R$ one has $D (0) = \emptyset$ and $D (1) = Spec (R)$ , and $D (f g) = D (f) \cap D (g)$ (Distinguished-subset identities).

[L11]

Assume the Axiom of Choice. For a finite type map $R \to S$ quasi-finite at $q \in Spec (S)$ there is $g \in S^{'} ∖ q$ with $S^{'} \to S$ inducing an isomorphism $S_{g}^{'} ≅ S_{g}$ (Algebraic Zariski Main localization at a quasi-finite prime).

[L12]

Assume the Axiom of Choice. For a finite type map $R \to S$ quasi-finite at every prime, with $S^{'}$ the integral closure of the image of $R$ in $S$ , there are a finite $R$ -subalgebra $T \subseteq S^{'}$ and finitely many $g_{1}, \dots, g_{n} \in T$ with the contraction map $Spec (S) \to Spec (T)$ a homeomorphism onto the open set $U = D_{T} (g_{1}) \cup \dots \cup D_{T} (g_{n})$ , $T_{g_{i}} ≅ S_{g_{i}}$ , and $T_{g} ≅ S_{g}$ whenever $D_{T} (g) \subseteq U$ (A quasi-finite algebra factors openly through a finite algebra).

Proof

technique · direct

1.1

We assume the Axiom of Choice as recorded in [L3]. By hypothesis $S$ is finitely generated as an $R$ -module by [L1], and $A = Im (R) \subseteq S$ is the image of the structure map. If $A = 0$ then $1_{S} = φ (1_{R}) = 0$ , so $S = 0$ and every element of $S$ is trivially integral over $R$ ; assume from now on that $A \neq 0$ .

givenL1L3

2.1

Fix $b \in S$ . Then $S$ is an $A [b]$ -module through the subalgebra $A [b] \subseteq S$ , and it is finitely generated over $A$ because it is finitely generated over $R$ and $A$ is a quotient of $R$ : the same finite generating set works. Moreover $S$ is a faithful $A [b]$ -module, because $r S = 0$ for $r \in A [b]$ forces $r = r \cdot 1_{S} = 0$ . By [L4] applied to $A \subseteq S$ and the element $b$ , the element $b$ is integral over $A$ in the sense of [L2]. As $b \in S$ was arbitrary, every element of $S$ is integral over the map $R \to S$ , and since $S^{'} = {Int}_{R} (S)$ consists exactly of those elements by [L5], we get $S^{'} = S$ . This is part 1.

givenstep 1.1L1L2L4L5

3.1

For part 2 let $q \in Spec (S)$ . Since $q$ is a proper ideal by [L6] we have $1 \notin q$ ; and $S^{'} = S$ by step 2.1, so $S_{1}^{'} = S_{1} = S = S_{1}$ by [L7]. Hence the triple $(S^{'}, g) = (S, 1)$ satisfies the conclusion of [L11] at every prime $q$ : the localisation $S^{'} \to S$ at the element $1$ is an isomorphism.

givenstep 2.1L6L7L11

3.2

For part 3 put $T : = S$ . Then $T$ is module-finite over $R$ by [L1], that is a finite $R$ -algebra, and $T = S = S^{'}$ is a finite $R$ -subalgebra of $S^{'}$ by step 2.1. The contraction map $Spec (S) \to Spec (T)$ induced by the identity ring map $S \to T = S$ is the identity of $Spec (S)$ by [L8], its image $Spec (S)$ is open in itself by [L9], and the single principal open $D_{T} (1)$ equals $Spec (T)$ by [L10]. Finally $T_{1} = T = S = S_{1}$ by [L7], so the data $T = S$ , $n = 1$ , $g_{1} = 1$ , $U = Spec (T)$ satisfy all the assertions (1) and (2) of [L12].

givenstep 2.1L1L7L8L9L10L12

4.1

The Axiom of Choice was used only through the two general theorems cited in steps 3.1 and 3.2, namely [L11] and [L12]; the direct verification of parts 1 to 3 above (the finite-module criterion of [L4], the element $1$ , the algebra $T = S$ , and the identities $S_{1}^{'} = S_{1} = S$ , $D_{T} (1) = Spec (T)$ ) manipulates finitely many explicit objects and selects nothing. This proves all three parts. ∎

givenstep 2.1step 3.1step 3.2L3L11L12

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

54 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, Commutative Algebra, Section 10.123, Theorem 10.123.12 and Lemma 10.123.14 in the case of a finite algebra (standard reference, not scraped)
J. S. Milne, A Primer of Commutative Algebra, version 4.03, Corollary 17.12 (standard reference, not scraped)