LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-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 finite-type field reduces to a localization over a transcendence basis

Statement

Let $k \subseteq K$ be a field extension, and assume that $K$ is finitely generated as a $k$ -algebra. Let $t_{1}, \dots, t_{r} \in K$ be a transcendence basis of $K$ over $k$ . Then there exists a nonzero polynomial $s \in k [t_{1}, \dots, t_{r}]$ such that $K$ is integral over the localization

k [t_{1}, \dots, t_{r}] [\frac{1}{s}] .

Facts & Assumptions

Given: A field extension $k \subseteq K$ , a finite $k$ -algebra generating set for $K$ , and a transcendence basis $t_{1}, \dots, t_{r}$ of $K$ over $k$ .

[L1]

The notation $k (t_{1}, \dots, t_{r})$ denotes the generated subfield (Finitely generated field extensions $F (a_{1}, \dots, a_{r})$ ).

[L2]

A transcendence basis makes the ambient field algebraic over the generated field (A maximal algebraically independent set is a transcendence basis).

[A1]

Clearing finitely many leading coefficients is enough to make finitely many algebraic elements integral over one localization.

Proof

technique · direct

1.1

Choose generators $a_{1}, \dots, a_{m} \in K$ of $K$ as a $k$ -algebra. Since $t_{1}, \dots, t_{r}$ is a transcendence basis, [L2] shows that each $a_{i}$ is algebraic over $F : = k (t_{1}, \dots, t_{r})$ .

L1L2givenchoose

2.1

For each $i$ , choose a nonzero polynomial $c_{i, d_{i}} X^{d_{i}} + \dots + c_{i, 0} \in k [t_{1}, \dots, t_{r}] [X]$ with $c_{i, d_{i}} \neq 0$ and value zero at $a_{i}$ . Let $s$ be the product of all leading coefficients $c_{i, d_{i}}$ . After localizing at $s$ , each $c_{i, d_{i}}$ becomes invertible, so each $a_{i}$ satisfies a monic polynomial over $k [t_{1}, \dots, t_{r}] [1 / s]$ . Hence every $a_{i}$ is integral over that localization.

step 1.1choosealgebra

3.1

The field $K$ is generated over $k [t_{1}, \dots, t_{r}] [1 / s]$ by the integral elements $a_{1}, \dots, a_{m}$ . Therefore every element of $k [t_{1}, \dots, t_{r}] [1 / s] [a_{1}, \dots, a_{m}] = K$ is integral over $k [t_{1}, \dots, t_{r}] [1 / s]$ .

step 2.1algebra

4.1

Thus $K$ is integral over $k [t_{1}, \dots, t_{r}] [1 / s]$ .

step 3.1∎

Depends on

Used by

A field finitely generated as a k-algebra is a finite extension of k Corollary

Dependency tree · two levels

11 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

J. S. Milne, A Primer of Commutative Algebra, v4.03, Corollary 13.3 (standard reference, not scraped)