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.

In the Artin–Tate setup the intermediate ring is module-finite over the coefficient subalgebra

Statement

Keep the data and the notation of The Artin–Tate coefficient subalgebra is a Noetherian algebra of finite type: commutative rings $A \subseteq B \subseteq C$ , each a subring of the next, with $A$ Noetherian, $C = A [t_{1}, \dots, t_{r}]$ , a $B$ -module generating list $y_{1}, \dots, y_{n}$ of $C$ with $y_{1} = 1_{C}$ , coefficients $z_{i j}, z_{i j k} \in B$ as displayed there, and $A^{'}$ the $A$ -subalgebra of $B$ they generate.

Then $C$ is generated as an $A^{'}$ -module by $y_{1}, \dots, y_{n}$ , so $C$ is module-finite over $A^{'}$ ; and $B$ is module-finite over $A^{'}$ as well (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras).

Facts & Assumptions

Given: The data of The Artin–Tate coefficient subalgebra is a Noetherian algebra of finite type, and the set $M : = \sum_{j = 1}^{n} A^{'} y_{j} = {\sum_{j = 1}^{n} a_{j} y_{j} : a_{j} \in A^{'}} \subseteq C$ .

[L1]

In that setup $A \subseteq A^{'} \subseteq B$ , the algebra $A^{'}$ is of finite type over $A$ , and $A^{'}$ is a Noetherian ring (The Artin–Tate coefficient subalgebra is a Noetherian algebra of finite type).

[L2]

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

[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]

Let $A$ be a Noetherian commutative ring and $B$ a commutative $A$ -algebra module-finite over $A$ with $A$ a subring of $B$ ; then every ring $C$ with $A \subseteq C \subseteq B$ is module-finite over $A$ and is a Noetherian ring (A module-finite algebra over a Noetherian ring is a Noetherian ring, and so is every ring between the two).

[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.1

The set $M = \sum_{j = 1}^{n} A^{'} y_{j}$ is the $A^{'}$ -submodule of $C$ generated by $y_{1}, \dots, y_{n}$ , by the finite-sum description of a generated submodule; it is in particular an additive subgroup of $C$ closed under multiplication by elements of $A^{'}$ . Since $y_{1} = 1_{C}$ we have $A^{'} = A^{'} y_{1} \subseteq M$ , and therefore $A \subseteq M$ and $1_{C} \in M$ .

L1L3L5given

2.1

$M$ is closed under multiplication, hence is a subring of $C$ . It suffices to multiply two generators with coefficients: for $a, a^{'} \in A^{'}$ , $(a y_{i}) (a^{'} y_{j}) = a a^{'} (y_{i} y_{j}) = a a^{'} \sum_{k = 1}^{n} z_{i j k} y_{k} = \sum_{k = 1}^{n} (a a^{'} z_{i j k}) y_{k}$ , and each $a a^{'} z_{i j k}$ lies in $A^{'}$ because $A^{'}$ is a subring of $B$ containing every $z_{i j k}$ . A product of two elements of $M$ expands by distributivity into a finite sum of such terms, so it lies in $M$ ; with the additive subgroup property and $1_{C} \in M$ from step 1.1, $M$ is a subring of $C$ .

L1L3L5step 1.1

3.1

$M$ contains each $t_{i}$ , since $t_{i} = \sum_{j = 1}^{n} z_{i j} y_{j}$ and every $z_{i j}$ lies in $A^{'}$ . So $M$ is a subring of $C$ containing $A$ and $t_{1}, \dots, t_{r}$ . But $C = A [t_{1}, \dots, t_{r}]$ is the smallest such subring, so $C \subseteq M$ ; and $M \subseteq C$ by construction. Hence $C = M$ , and $y_{1}, \dots, y_{n}$ generate $C$ as an $A^{'}$ -module, so $C$ is module-finite over $A^{'}$ .

L2L3step 1.1step 2.1

4.1

Now $A^{'}$ is a Noetherian commutative ring, $A^{'}$ is a subring of $C$ , and $C$ is module-finite over $A^{'}$ ; the intermediate-ring clause applied to $A^{'} \subseteq B \subseteq C$ gives that $B$ is module-finite over $A^{'}$ .

L1L4step 3.1∎

Remarks

No induction on total degree is needed. Showing directly that $\sum_{j} A^{'} y_{j}$ is a subring containing $A$ and the algebra generators, and then invoking minimality of $A [t_{1}, \dots, t_{r}]$ , replaces the degreewise reduction of a polynomial expression; the multiplication table $y_{i} y_{j} = \sum_{k} z_{i j k} y_{k}$ is exactly what makes the closure argument work in one line.
$y_{1} = 1_{C}$ is used, and used here. It is what puts $A^{'}$ itself inside $M$ , without which $M$ need not contain $A$ and the minimality argument would not apply.
Only $A^{'}$ is known to be Noetherian. The final step is applied with $A^{'}$ as the Noetherian base, never with $B$ , which is exactly the point of the Artin–Tate argument.

Depends on

Used by

Dependency tree · two levels

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