CorollaryStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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.

Every algebra of finite type over a Noetherian ring is a Noetherian ring

Statement

Let $R$ be a Noetherian commutative ring and let $A$ be a commutative $R$ -algebra of finite type (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras). Then $A$ is a Noetherian ring.

Facts & Assumptions

Given: A Noetherian commutative ring $R$ and a commutative $R$ -algebra $A$ of finite type, with structure map $η_{A} ⁣ : R \to A$ .

[L1]

An $R$ -algebra $A$ is of finite type over $R$ when $A = R [a_{1}, \dots, a_{n}]$ for some $n \in N$ and $a_{1}, \dots, a_{n} \in A$ , where $R [a_{1}, \dots, a_{n}]$ is the image of the unital ring homomorphism $R [x_{1}, \dots, x_{n}] \to A$ agreeing with $η_{A}$ on constants and sending $x_{i}$ to $a_{i}$ (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras).

[L2]

For a ring homomorphism $f ⁣ : R \to S$ there is a ring isomorphism $R / \ker f ≅ im f$ (First isomorphism theorem for rings: $R / \ker f ≅ im f$ ).

[L3]

If $R$ is a Noetherian commutative ring then $R [x_{1}, \dots, x_{n}]$ is Noetherian for every $n \in N$ (If $R$ is Noetherian then $R [x_{1}, \dots, x_{n}]$ is Noetherian for every $n \in N$ ).

[L4]

Every quotient $R / I$ of a Noetherian commutative ring by an ideal is Noetherian (Every quotient and every localisation of a Noetherian ring is Noetherian).

Proof

technique · direct

1.1L1given

By the finite-type hypothesis there are $n \in N$ and $a_{1}, \dots, a_{n} \in A$ with $A = R [a_{1}, \dots, a_{n}]$ , so the evaluation homomorphism $ev ⁣ : R [x_{1}, \dots, x_{n}] \to A$ sending $x_{i}$ to $a_{i}$ has image all of $A$ and is therefore surjective.

2.1L2step 1.1

The first isomorphism theorem applied to $ev$ gives a ring isomorphism $R [x_{1}, \dots, x_{n}] / \ker ev ≅ A$ .

3.1L3L4step 2.1algebra∎

The ring $R [x_{1}, \dots, x_{n}]$ is Noetherian because $R$ is, so its quotient by the ideal $\ker ev$ is Noetherian; a ring isomorphism carries ideals to ideals and finite generating lists to finite generating lists, so $A$ is Noetherian.

Remarks

This is the form of the Hilbert basis theorem later pages use. A ring presented by finitely many generators and any relations at all is Noetherian, with no hypothesis on the relations; the number of generators is what matters, not their independence.
The converse is false and is not claimed. A Noetherian ring need not be of finite type over a Noetherian subring: a field extension generated by infinitely many algebraic elements is a field, hence Noetherian, and is not of finite type over the base field as an algebra.

Depends on

Used by

A plane intersection with no common component is nonempty and zero-dimensional Corollary
Degree is additive on invertible sheaves over a proper curve Corollary
Euler characteristic in a proper flat family is locally constant Corollary
Every algebra of finite type over a principal ideal domain is a Noetherian ring Corollary
Global functions on geometrically connected and geometrically reduced proper schemes Corollary
The degree of a divisor descends to the Picard group of a normal proper curve Corollary
The dimension of a complete linear system Corollary
A normal singular surface: the quadric cone Counterexample
A Weil divisor that is not Cartier at the vertex of the quadric cone Counterexample
The intersection product needs Cartier or complementary-dimension hypotheses Counterexample
Base points and base-point-free linear systems Definition
Canonical bundle and canonical divisors Definition
Complete linear system Definition
Degree of an invertible sheaf on a proper one-dimensional scheme Definition
Delta invariant of a curve singularity Definition
Divisors on a smooth proper curve Definition
Genus and arithmetic genus of a curve Definition
Principal parts of an invertible sheaf on a curve Definition
Ramification points, branch points and unramifiedness Definition
The Riemann-Roch dimension l(D) Definition
A nondegenerate projective quadric Example
Affine space is normal Example
k[x,y]/(xy) and ℤ[x]/(x²-2) are Noetherian without classifying their ideals Example
Pulling a divisor back along the cusp normalization Example
The family xy=t Example
The subalgebra k[x,xy,xy²,…] of k[x,y] is not Noetherian Example
A nonconstant rational function defines a finite map to the projective line Lemma
A transverse hyperplane slice is smooth at the chosen point Lemma
An S-rational map defined after a faithfully flat smooth base change is defined Lemma
Chow lemma for proper Noetherian schemes Lemma
Dense relative-dimension strata in flat finitely presented fibres Lemma
Euler characteristic and normalization defect under a point blowup Lemma
Eventual generation of coherent projective twists Lemma
Every normal subgroup of an affine group is a representation kernel Lemma
Every subgroup scheme of an affine group is a line stabilizer Lemma
Fibre degree of the finite locally free map to the projective line Lemma
Finite morphisms over a projective variety over any field Lemma
Finite relative integral-closure charts for classical quasi-finite morphisms Lemma
Finite schemes over projective schemes are projective over a Noetherian affine base Lemma
Finite-dimensionality of the Riemann-Roch space Lemma

…and 41 more results.

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

A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., (16.12) (standard reference, not scraped)
J. S. Milne, A Primer of Commutative Algebra, v4.03, §3 Theorem 3.7 (standard reference, not scraped)
M. Hochster, Introduction to Commutative Algebra, Math 614, Corollary 5.7 (standard reference, not scraped)