LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

The Artin–Tate coefficient subalgebra is a Noetherian algebra 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 = A [t_{1}, \dots, t_{r}]$ is of finite type over $A$ , with $r \in N$ and $t_{1}, \dots, t_{r} \in C$ (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras);
$y_{1}, \dots, y_{n} \in C$ generate $C$ as a $B$ -module, with $n \geq 1$ and $y_{1} = 1_{C}$ .

Choose elements $z_{i j} \in B$ for $1 \leq i \leq r$ and $1 \leq j \leq n$ , and $z_{i j k} \in B$ for $1 \leq i, j, k \leq n$ , such that

$t_{i} = \sum_{j = 1}^{n} z_{i j} y_{j}, y_{i} y_{j} = \sum_{k = 1}^{n} z_{i j k} y_{k} .$

Let $A^{'}$ be the $A$ -subalgebra of $B$ generated by all the $z_{i j}$ and all the $z_{i j k}$ . Then $A \subseteq A^{'} \subseteq B$ , the algebra $A^{'}$ is of finite type over $A$ , and $A^{'}$ is a Noetherian ring.

Such coefficients exist, because the $y_{j}$ generate $C$ as a $B$ -module and $t_{i}$ and $y_{i} y_{j}$ are elements of $C$ . They are chosen, not canonical: only their existence and their finite number are used, and a different choice gives a possibly different $A^{'}$ with the same properties.

Facts & Assumptions

Given: Commutative rings $A \subseteq B \subseteq C$ , each a subring of the next, with $A$ Noetherian; a finite list $t_{1}, \dots, t_{r}$ with $C = A [t_{1}, \dots, t_{r}]$ ; a list $y_{1}, \dots, y_{n}$ generating $C$ as a $B$ -module with $y_{1} = 1_{C}$ ; and coefficients $z_{i j}, z_{i j k} \in B$ as displayed.

[L1]

$R [a_{1}, \dots, a_{n}]$ is the image of the unital ring homomorphism $R [x_{1}, \dots, x_{n}] \to A$ agreeing with the structure map on constants and sending $x_{i}$ to $a_{i}$ , and it 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 (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras).

[L2]

Every commutative algebra of finite type over a Noetherian commutative ring is a Noetherian ring (Every algebra of finite type over a Noetherian ring is a Noetherian ring).

[L3]

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).

[L4]

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

Proof

technique · direct

1.1

The coefficients exist. Each $t_{i}$ and each product $y_{i} y_{j}$ is an element of $C$ , and $C$ is generated as a $B$ -module by $y_{1}, \dots, y_{n}$ , so by the finite-sum description each of them is a $B$ -linear combination of $y_{1}, \dots, y_{n}$ ; fix one such expression for each, which is a selection over a finite index set.

L3L4given

2.1

The elements $z_{i j}$ and $z_{i j k}$ form a finite list of elements of $B$ , indexed by the finitely many pairs $(i, j)$ with $i \leq r$ , $j \leq n$ and the finitely many triples $(i, j, k)$ with $i, j, k \leq n$ . Let $A^{'}$ be the $A$ -subalgebra of $B$ they generate, that is, the smallest subring of $B$ containing $A$ and all of them. Then $A \subseteq A^{'} \subseteq B$ , and $A^{'}$ is of finite type over $A$ by definition, being generated as an $A$ -algebra by a finite list.

L1L4step 1.1

3.1

The base ring $A$ is Noetherian and $A^{'}$ is a commutative $A$ -algebra of finite type, so $A^{'}$ is a Noetherian ring.

L2step 2.1∎

Remarks

Nothing here uses that $B$ is Noetherian, and nothing may. Whether $B$ is Noetherian is not among the hypotheses of the Artin–Tate lemma; the point of passing to $A^{'}$ is to obtain a Noetherian ring inside $B$ without assuming one.
The normalisation $y_{1} = 1_{C}$ costs nothing. A finite $B$ -module generating list of $C$ stays finite and generating when $1_{C}$ is adjoined to it, so it may always be arranged; it is used where the relations are read back, not here.

Depends on

Used by

Dependency tree · two levels

18 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)