LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 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.

Finite-type maps from Jacobson rings induce finite residue-field extensions at maximal ideals

Statement

Let $R$ be a Jacobson ring, let $A$ be a finite-type $R$ -algebra, and let $m$ be a maximal ideal of $A$ . Put $p = m \cap R$ . Then the residue field $κ (m) = A_{m} / m A_{m}$ is a finite field extension of

κ (p) = R_{p} / p R_{p} .

Facts & Assumptions

Given: A Jacobson ring $R$ , a finite-type $R$ -algebra $A$ , and a maximal ideal $m \subseteq A$ with contraction $p = m \cap R$ .

[L1]

Finite type means generated by finitely many algebra elements (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras).

[L2]

Localizing at a prime uses the denominator set outside that prime (Localisation at a prime ideal: $R_{p} = (R ∖ p)^{- 1} R$ ).

[L3]

The localization at a prime is a local ring with the extended prime as its maximal ideal ( $R_{p}$ is local with unique maximal ideal $p R_{p}$ ).

[L4]

The residue field at a prime is the fraction field of the quotient by that prime ( $R_{p} / p R_{p} ≅ Frac (R / p)$ is the residue field at $p$ ).

[L5]

A field finitely generated as an algebra over a field is a finite extension (A field finitely generated as a k-algebra is a finite extension of k).

Proof

technique · direct

1.1

By [L1], choose generators $a_{1}, \dots, a_{n}$ of $A$ over $R$ . Localizing at $p$ gives $A_{p} ≅ R_{p} [a_{1} / 1, \dots, a_{n} / 1],$ so $A_{p}$ is a finite-type $R_{p}$ -algebra.

L1L2givenchoose

2.1

The maximal ideal $m$ extends to a maximal ideal $m A_{p}$ of $A_{p}$ , and localizing further at that maximal ideal yields the local ring $A_{m}$ with residue field $κ (m)$ . By [L4], the base residue field is $κ (p) = Frac (R / p)$ .

L3L4step 1.1

3.1

Passing to residue fields sends the finite-type algebra $A_{p}$ over $R_{p}$ to the finite-type $κ (p)$ -algebra $κ (p) \otimes_{R_{p}} A_{p} ↠ κ (m) .$ Because $κ (m)$ is a field, [L5] implies that it is a finite extension of $κ (p)$ .

L4L5step 2.1

4.1

Hence $κ (m) / κ (p)$ is finite.

step 3.1∎

Depends on

Used by

In a finite-type algebra over a field, radical ideals are intersections of maximal ideals Corollary

Dependency tree · two levels

21 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

Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, 13th ed., Theorem (15.26) (standard reference, not scraped)