TheoremStatement: 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.

A module-finite algebra over a Noetherian ring is a Noetherian ring, and so is every ring between the two

Statement

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

$B$ is a Noetherian ring;
if in addition the $A$ -algebra structure map is the inclusion of $A$ as a subring of $B$ (Subring: a subset containing $1_{R}$ and closed under addition, additive inverses and multiplication), then every subring $C$ of $B$ with $A \subseteq C \subseteq B$ is module-finite over $A$ and is a Noetherian ring;
every finitely generated $B$ -module is finitely generated as an $A$ -module, and hence is a Noetherian $A$ -module.

Facts & Assumptions

Given: A Noetherian commutative ring $A$ , a commutative $A$ -algebra $B$ with structure map $η_{B} ⁣ : A \to B$ that is module-finite over $A$ , and, for the second clause, the additional hypotheses that $η_{B}$ is the inclusion of $A$ as a subring of $B$ and that $C$ is a subring of $B$ with $A \subseteq C \subseteq B$ (Subring: a subset containing $1_{R}$ and closed under addition, additive inverses and multiplication).

[L1]

$B$ is module-finite over $A$ when it is finitely generated as an $A$ -module (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras).

[L2]

An $A$ -algebra is a unital ring $B$ with a unital ring homomorphism $η_{B} ⁣ : A \to B$ of central image, and the induced scalar action $a b : = η_{B} (a) b$ makes $B$ an $A$ -module (Algebras over a commutative ring, central structure maps, and algebra homomorphisms).

[L3]

Every finitely generated left module over a left Noetherian ring is Noetherian (Finitely generated modules over a left Noetherian ring are Noetherian).

[L4]

In a commutative ring, $(S)$ consists of finite sums $\sum r_{i} s_{i}$ , and $(a) = R a$ (In a commutative ring, $(S)$ consists of finite sums $\sum r_{i} s_{i}$ , and $(a) = R a$ ).

[L5]

A left $R$ -module is Noetherian when every submodule of it is finitely generated (Noetherian modules: every submodule is finitely generated).

[L6]

For a commutative ring, being Noetherian is equivalent to every ideal being finitely generated (A commutative ring is Noetherian exactly when every ideal is finitely generated, exactly when its ideals satisfy the ascending chain condition, and exactly when every nonempty set of ideals has a maximal member).

[L7]

A subset $N \subseteq M$ of a left $R$ -module is a submodule when it is a subgroup of the additive group of $M$ and is closed under scalars (Submodule of a module).

[L8]

If $B$ is generated as an $A$ -module by $b_{1}, \dots, b_{m}$ and a $B$ -module $M$ is generated as a $B$ -module by $u_{1}, \dots, u_{n}$ , then the $m n$ products $b_{i} u_{j}$ generate $M$ as an $A$ -module (Module finiteness is transitive along a tower of algebras).

Proof

technique · direct

1.1L1L2L3L5given

Let $B^{'}$ be any commutative $A$ -algebra that is module-finite over $A$ . Then $B^{'}$ is a finitely generated module over the Noetherian ring $A$ , hence a Noetherian $A$ -module: every $A$ -submodule of $B^{'}$ is finitely generated over $A$ . This applies in particular to $B^{'} = B$ .

2.1L4L5L6L7step 1.1

First clause. Let $b$ be an ideal of $B^{'}$ . It is an additive subgroup of $B^{'}$ closed under the $A$ -action, since $a \cdot x = η_{B^{'}} (a) x \in b$ for $x \in b$ , so it is an $A$ -submodule and therefore generated over $A$ by finitely many $x_{1}, \dots, x_{k} \in b$ . Every element of $b$ is then $\sum_{i} η_{B^{'}} (a_{i}) x_{i}$ , which lies in the ideal $(x_{1}, \dots, x_{k})$ of $B^{'}$ ; and that ideal is contained in $b$ because each $x_{i}$ lies in $b$ . So $b = (x_{1}, \dots, x_{k})$ is finitely generated as an ideal, and $B^{'}$ is a Noetherian ring. Taking $B^{'} = B$ gives the first clause.

2.2L5L7step 1.1given

Second clause, first half. Suppose the $A$ -algebra structure map is the inclusion $A \subseteq B$ and $C$ is a subring of $B$ with $A \subseteq C \subseteq B$ . Then $C$ is an additive subgroup of $B$ closed under the $A$ -action, because $a \cdot x = a x$ is a product of two elements of $C$ ; so $C$ is an $A$ -submodule of the Noetherian $A$ -module $B$ and is therefore finitely generated as an $A$ -module, that is, module-finite over $A$ .

2.3L1L3L8step 1.1

Third clause. Let $M$ be a finitely generated $B$ -module, say generated over $B$ by $u_{1}, \dots, u_{n}$ , and let $b_{1}, \dots, b_{m}$ generate $B$ over $A$ . The $m n$ products $b_{i} u_{j}$ generate $M$ as an $A$ -module, so $M$ is a finitely generated $A$ -module and hence a Noetherian $A$ -module.

3.1step 2.1step 2.2step 2.3∎

Step 2.2 makes $C$ a commutative $A$ -algebra, through the inclusion $A \subseteq C$ , that is module-finite over $A$ ; steps 1.1 and 2.1 were proved for an arbitrary such algebra, so applying them with $B^{'} = C$ makes $C$ a Noetherian ring. With steps 2.1 and 2.3 this establishes all three clauses.

Remarks

The intermediate-ring clause is the one that gets used. It says nothing about $C$ being of finite type over $A$ as an algebra, only that it is module-finite, which is stronger; the Artin–Tate lemma is what handles the situation where only $C$ sits between $A$ and a finite-type algebra without $B$ being module-finite over $A$ .
Module-finite is strictly stronger than finite type here. A finite-type algebra over a Noetherian ring is Noetherian as well, but its ideals need not be finitely generated over the base ring, and the argument of step 2.1 would not run.
The hypothesis that $A$ is a subring is used only in the second clause. Clauses 1 and 3 need no injectivity of $η_{B}$ .

Depends on

Used by

Dependency tree · two levels

31 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

M. Hochster, Introduction to Commutative Algebra, Math 614, Lemma 5.4 (standard reference, not scraped)
A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., (16.19) and (16.21) (standard reference, not scraped)
J. S. Milne, A Primer of Commutative Algebra, v4.03, §3 (standard reference, not scraped)