CorollaryStatement: 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 field finitely generated as a k-algebra is a finite extension of k

Statement

Let $k \subseteq K$ be a field extension. If $K$ is finitely generated as a $k$ -algebra, then $K$ is a finite field extension of $k$ .

Facts & Assumptions

Given: A field extension $k \subseteq K$ with $K$ finitely generated as a $k$ -algebra.

[L1]

A finitely generated field over $k$ is integral over a localization of a polynomial ring on any transcendence basis (A finite-type field reduces to a localization over a transcendence basis).

[L2]

A localization $k [t_{1}, \dots, t_{r}] [1 / s]$ with $r > 0$ is not a field (A finitely localized polynomial ring in positive dimension is not a field).

[L3]

A field generated by finitely many algebraic elements over $k$ is a finite extension of $k$ (An extension generated by finitely many algebraic elements is finite).

Proof

technique · contradiction

1.1

Let $t_{1}, \dots, t_{r}$ be a transcendence basis of $K$ over $k$ . By [L1] there exists a nonzero $s \in k [t_{1}, \dots, t_{r}]$ such that $K$ is integral over $R : = k [t_{1}, \dots, t_{r}] [1 / s]$ .

L1givenchoose

2.1

Assume $r > 0$ . Because $K$ is a field and integral over $R$ , every nonzero element $a \in R$ is a unit of $R$ : the inverse $a^{- 1} \in K$ satisfies a monic equation over $R$ , and multiplying by a large power of $a$ rewrites that equation as $a^{- 1} = - (c_{n - 1} + c_{n - 2} a + \dots + c_{0} a^{n - 1}) \in R .$ Thus $R$ would be a field, contradicting [L2].

L2step 1.1assume-contracontradiction

3.1

Therefore $r = 0$ , so the transcendence basis is empty and $K / k$ is algebraic. Since $K$ is finitely generated as a $k$ -algebra, choose algebra generators $a_{1}, \dots, a_{m}$ ; they are algebraic over $k$ , and [L3] makes $K = k (a_{1}, \dots, a_{m})$ finite over $k$ .

L3step 2.1discharge-contradiction∎

Depends on

Used by

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, Theorem 13.1 (standard reference, not scraped)
Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, 13th ed., Theorem (15.4) (standard reference, not scraped)