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

Artin–Tate lemma: an intermediate ring over which a finite-type algebra is module-finite is itself of finite type

Statement

Let $A \subseteq B \subseteq C$ be commutative rings, each a subring of the next (Subring: a subset containing $1_{R}$ and closed under addition, additive inverses and multiplication), with $A$ Noetherian. Suppose $C$ is of finite type over $A$ and module-finite over $B$ (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras). Then $B$ is of finite type over $A$ .

No Noetherian hypothesis is placed on $B$ ; that is what the argument has to do without, and it is why a Noetherian subring of $B$ is manufactured on the way.

Facts & Assumptions

Given: Commutative rings $A \subseteq B \subseteq C$ , each a subring of the next, with $A$ Noetherian, $C$ of finite type over $A$ and $C$ module-finite over $B$ .

[L1]

$R [a_{1}, \dots, a_{n}]$ is the smallest subring of $A$ containing the image of $R$ and $a_{1}, \dots, a_{n}$ ; an algebra is of finite type over $R$ when it equals $R [a_{1}, \dots, a_{n}]$ for some finite list, and module-finite over $R$ when it is finitely generated as an $R$ -module (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras).

[L2]

For a ring $R$ , a left $R$ -module $M$ and $S \subseteq M$ , the submodule $⟨ S ⟩_{R}$ is the set of finite sums $\sum_{i = 1}^{k} r_{i} s_{i}$ with $k \in N$ , $r_{i} \in R$ and $s_{i} \in S$ (The submodule generated by a subset consists of the finite $R$ -linear combinations of that subset).

[L3]

With $A \subseteq B \subseteq C$ as above, $C = A [t_{1}, \dots, t_{r}]$ , a $B$ -module generating list $y_{1}, \dots, y_{n}$ of $C$ with $y_{1} = 1_{C}$ and coefficients $z_{i j}, z_{i j k} \in B$ satisfying $t_{i} = \sum_{j} z_{i j} y_{j}$ and $y_{i} y_{j} = \sum_{k} z_{i j k} y_{k}$ : the $A$ -subalgebra $A^{'} \subseteq B$ generated by those coefficients satisfies $A \subseteq A^{'} \subseteq B$ , is of finite type over $A$ , and is a Noetherian ring (The Artin–Tate coefficient subalgebra is a Noetherian algebra of finite type).

[L4]

In that same setup $C$ is module-finite over $A^{'}$ , and $B$ is module-finite over $A^{'}$ (In the Artin–Tate setup the intermediate ring is module-finite over the coefficient subalgebra).

[L5]

A subring contains the identity of the ambient ring and is closed under sums, additive inverses and products (Subring: a subset containing $1_{R}$ and closed under addition, additive inverses and multiplication).

Proof

technique · direct

1.1L1L2given

Fix $r \in N$ and $t_{1}, \dots, t_{r} \in C$ with $C = A [t_{1}, \dots, t_{r}]$ , available because $C$ is of finite type over $A$ . Fix a finite list generating $C$ as a $B$ -module and adjoin $1_{C}$ to it; the result $y_{1}, \dots, y_{n}$ is still finite and still generates, and it may be indexed so that $n \geq 1$ and $y_{1} = 1_{C}$ .

2.1L2L3step 1.1

Each $t_{i}$ and each product $y_{i} y_{j}$ lies in $C$ , so each is a $B$ -linear combination of $y_{1}, \dots, y_{n}$ ; fix coefficients $z_{i j}, z_{i j k} \in B$ with $t_{i} = \sum_{j} z_{i j} y_{j}$ and $y_{i} y_{j} = \sum_{k} z_{i j k} y_{k}$ , and let $A^{'}$ be the $A$ -subalgebra of $B$ they generate. Then $A \subseteq A^{'} \subseteq B$ , $A^{'}$ is of finite type over $A$ , and $A^{'}$ is a Noetherian ring.

3.1L2L4step 2.1

In this setup $B$ is module-finite over $A^{'}$ : fix $s \in N$ and $w_{1}, \dots, w_{s} \in B$ generating $B$ as an $A^{'}$ -module, so that every element of $B$ is $\sum_{l = 1}^{s} a_{l} w_{l}$ with $a_{l} \in A^{'}$ .

4.1L1L2L5step 2.1step 3.1∎

Let $D$ be the smallest subring of $B$ containing $A$ , all the coefficients $z_{i j}$ and $z_{i j k}$ , and $w_{1}, \dots, w_{s}$ ; that is, $D$ is the $A$ -subalgebra of $B$ generated by that finite list. Then $D$ contains $A$ and the coefficients, hence contains the smallest subring of $B$ containing them, which is $A^{'}$ ; and $D$ contains each $w_{l}$ and is closed under products and sums, so $D$ contains every $\sum_{l} a_{l} w_{l}$ with $a_{l} \in A^{'}$ , that is all of $B$ . Since also $D \subseteq B$ , we get $B = D$ , so $B$ is generated as an $A$ -algebra by a finite list and is of finite type over $A$ .

Remarks

The Noetherian ring in play is $A^{'}$ , never $B$ . The hypothesis is that $A$ is Noetherian, and $A^{'}$ inherits that as a finite-type algebra over $A$ ; the conclusion about $B$ is then read off from $B$ being a finite $A^{'}$ -module.
The generating list of $B$ is explicit. It consists of the structure coefficients $z_{i j}$ and $z_{i j k}$ together with the $A^{'}$ -module generators $w_{l}$ of $B$ , all of which depend on the choices made in steps 1.1 to 3.1. No minimality is claimed.

Depends on

Used by

Dependency tree · two levels

19 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.21) (standard reference, not scraped)
M. Hochster, Introduction to Commutative Algebra, Math 614, Ch. 5 (standard reference, not scraped)