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.

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

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources