CorollaryStatement: Literature-sourcedProof: 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.

Quasi-finite algebras are source locally localizations of finite algebras

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $R \to S$ be a ring map of finite type (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras) that is quasi-finite at every prime of $S$ (Quasi-finiteness at a prime of a finite-type algebra), and let $S^{'} \subseteq S$ be the integral closure of the image of $R$ in $S$ (Integral elements subalgebra of an arbitrary ring map). Then for every prime $q \in Spec (S)$ there are a finite $R$ -subalgebra $T \subseteq S^{'}$ , module-finite over $R$ , and an element $g \in T$ with $g \notin q$ such that the inclusion $T \to S$ induces an isomorphism $T_{g} \overset{≅}{\to} S_{g}$ of principal localisations (Principal localisation $R_{f} = {1, f, f^{2}, \dots}^{- 1} R$ ).

In other words, on the source every point of a quasi-finite finite-type algebra has an open neighbourhood, the principal open $D_{S} (g)$ , on which the algebra is a principal localisation of a finite algebra, and this already happens inside the relative integral closure. The element $g$ lies in the finite intermediate algebra $T$ and need not be the image of an element of $R$ : the corollary is a statement about the source, and it makes no base-principal or globally finite claim. The Axiom of Choice is inherited from the factorization theorem A quasi-finite algebra factors openly through a finite algebra used in the proof, whose finite cover it reuses.

Facts & Assumptions

Given: A ring map $R \to S$ of finite type that is quasi-finite at every prime of $S$ , the relative integral closure $S^{'} = {Int}_{R} (S) \subseteq S$ of the image of $R$ in $S$ , a prime $q \in Spec (S)$ , and the Axiom of Choice.

[L1]

The map $R \to S$ is quasi-finite when it is of finite type and quasi-finite at every prime of $S$ , where quasi-finiteness at $q$ is finiteness of $S_{q} / p S_{q}$ over $κ (p)$ (Quasi-finiteness at a prime of a finite-type algebra).

[L2]

An $R$ -algebra $A$ is of finite type over $R$ when $A = R [a_{1}, \dots, a_{n}]$ for finitely many elements, and 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).

[L3]

For a unital ring map $R \to S$ the relative integral closure ${Int}_{R} (S)$ is an $R$ -subalgebra of $S$ containing the image of $R$ , namely the set of elements integral over the map (Integral elements subalgebra of an arbitrary ring map).

[L4]

Assume the Axiom of Choice. If $R \to S$ is of finite type and quasi-finite at every prime of $S$ and $S^{'}$ is the integral closure of the image of $R$ in $S$ , then there are a finite $R$ -subalgebra $T \subseteq S^{'}$ , module-finite over $R$ , and finitely many elements $g_{1}, \dots, g_{n} \in T$ such that $U = D_{T} (g_{1}) \cup \dots \cup D_{T} (g_{n})$ is open in $Spec (T)$ , the contraction map $Spec (S) \to Spec (T)$ is a homeomorphism onto $U$ , $T_{g_{i}} ≅ S_{g_{i}}$ for every $i$ , and for every $g \in T$ with $D_{T} (g) \subseteq U$ the inclusion induces an isomorphism $T_{g} \to S_{g}$ (A quasi-finite algebra factors openly through a finite algebra).

[L5]

For $f$ in a commutative ring $R$ the principal localisation is $R_{f} = S_{f}^{- 1} R$ with $S_{f} = {1, f, f^{2}, \dots}$ , and its elements may be written $r / f^{n}$ (Principal localisation $R_{f} = {1, f, f^{2}, \dots}^{- 1} R$ ).

[L6]

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

Proof

technique · direct

1.1

We assume the Axiom of Choice as recorded in [L6]. The hypothesis on $R \to S$ together with [L2] says that $S$ is a finitely generated $R$ -algebra and that the quasi-finiteness condition of [L1] holds at every prime of $S$ , so the factorization theorem [L4] applies; the relative integral closure $S^{'}$ is an $R$ -subalgebra of $S$ by [L3].

givenL1L2L3L4L6

2.1

Fix $q \in Spec (S)$ . By step 1.1 and [L4] there are a finite $R$ -subalgebra $T \subseteq S^{'}$ , module-finite over $R$ , and finitely many elements $g_{1}, \dots, g_{n} \in T$ such that $U = D_{T} (g_{1}) \cup \dots \cup D_{T} (g_{n})$ is an open subset of $Spec (T)$ onto which the contraction map $Spec (S) \to Spec (T)$ is a homeomorphism, and $T_{g_{i}} ≅ S_{g_{i}}$ for every $i$ .

givenstep 1.1L4

3.1

The image $p : = q \cap T$ of $q$ under the contraction map lies in the image of that homeomorphism, namely $U$ ; hence $p \in D_{T} (g_{i})$ for some index $i$ , that is $g_{i} \notin p = q \cap T$ . Since $g_{i} \in T \subseteq S$ , this means $g_{i} \notin q$ .

givenstep 2.1L4

4.1

For this index $i$ the inclusion $T \subseteq S$ induces an isomorphism $T_{g_{i}} \to S_{g_{i}}$ . Indeed $D_{T} (g_{i}) \subseteq U$ because $U$ is the union of the $D_{T} (g_{j})$ , and $T_{g_{i}} ≅ S_{g_{i}}$ is also one of the conclusions of step 2.1; either form of the factorization theorem gives the isomorphism, the first by its local form and the second by its cover statement.

givenstep 2.1step 3.1L4

5.1

Taking $g : = g_{i} \in T$ we have produced a finite $R$ -subalgebra $T \subseteq S^{'}$ that is module-finite over $R$ and an element $g \in T$ with $g \notin q$ such that $T_{g} ≅ S_{g}$ ; by [L5] these are principal localisations, so the source principal open $D_{S} (g)$ has algebra $S_{g} ≅ T_{g}$ over $R$ . No step uses that $g$ lies in the image of $R$ , and none asserts finiteness of $S$ or of $T_{g}$ over $R$ beyond the module-finiteness of $T$ , so no base-principal or globally finite statement is claimed.

givenstep 1.1step 3.1step 4.1L5

6.1

The Axiom of Choice was used only in step 2.1, through the factorization theorem [L4]; the only other selections are the single index $i$ of step 3.1 and the single element $g$ of step 5.1. This proves the corollary. ∎

givenstep 2.1step 5.1L4L6

Depends on

Used by

Quasi-finite does not imply finite Counterexample

Dependency tree · two levels

36 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, Lemma 10.123.14 (1) and (2) (standard reference, not scraped)
J. S. Milne, A Primer of Commutative Algebra, version 4.03, Corollary 17.12 (standard reference, not scraped)