ExampleConstruction: AI-generatedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

Identifying the coefficient algebra in a concrete Artin–Tate tower

Example

Let $k$ be a field and take the tower

$A = k \subseteq B = k [t^{2}, t^{3}] \subseteq C = k [t]$

inside the polynomial ring $k [t]$ . Here $C$ is of finite type over $A$ , generated by $t$ , and $C$ is module-finite over $B$ with module generators $y_{1} = 1$ and $y_{2} = t$ .

Running The Artin–Tate coefficient subalgebra is a Noetherian algebra of finite type on this tower collects the coefficients

$t = 0 \cdot y_{1} + 1 \cdot y_{2}, y_{1} y_{1} = 1 \cdot y_{1} + 0 \cdot y_{2}, y_{1} y_{2} = y_{2} y_{1} = 0 \cdot y_{1} + 1 \cdot y_{2}, y_{2} y_{2} = t^{2} \cdot y_{1} + 0 \cdot y_{2},$

so the coefficients are $0$ , $1$ and $t^{2}$ and the coefficient subalgebra is $A^{'} = k [t^{2}]$ . It is of finite type over $k$ and Noetherian, and $B$ is a finite $A^{'}$ -module, generated by $1$ and $t^{3}$ . The Artin–Tate lemma (Artin–Tate lemma: an intermediate ring over which a finite-type algebra is module-finite is itself of finite type) therefore returns that $B$ is of finite type over $k$ , which is directly visible here: $B = k [t^{2}, t^{3}]$ .

Facts & Assumptions

Given: A field $k$ , the polynomial ring $C = k [t]$ , the subalgebra $B = k [t^{2}, t^{3}]$ of $C$ , and $A = k$ .

[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 such a subring for a finite list, and module-finite when it is finitely generated as an $R$ -module (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras).

[L2]

A subset $S$ of a ring is a subring when $1 \in S$ and $S$ is closed under addition, additive inverses and multiplication (Subring: a subset containing $1_{R}$ and closed under addition, additive inverses and multiplication).

[L3]

$R [x]$ is the set of finitely supported functions $N \to R$ , with coefficientwise addition and the convolution product (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution).

[L4]

In the Artin–Tate setup, with $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).

[L5]

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

[L6]

Every field is a Noetherian ring (Fields and $Z$ are Noetherian, and so are their polynomial rings in finitely many variables).

[L7]

For 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$ , the ring $B$ is of finite type over $A$ (Artin–Tate lemma: an intermediate ring over which a finite-type algebra is module-finite is itself of finite type).

Verification

technique · direct

1.1

$B = k + t^{2} k [t]$ . The set $k + t^{2} k [t]$ is a subring of $k [t]$ : it contains $1$ , is closed under addition and additive inverses, and $(c + t^{2} f) (c^{'} + t^{2} f^{'}) = c c^{'} + t^{2} (c f^{'} + c^{'} f + t^{2} f f^{'})$ ; it contains $t^{2}$ and $t^{3}$ , so it contains $B$ . Conversely $t^{a} \in B$ for every $a \geq 2$ , being $(t^{2})^{m}$ when $a = 2 m$ and $t^{3} (t^{2})^{m}$ when $a = 2 m + 3$ , and $k \subseteq B$ , so $k + t^{2} k [t] \subseteq B$ . Hence $k \subseteq B \subseteq C$ with each a subring of the next, and $C = k [t]$ is of finite type over $k$ .

L1L2L3given

2.1

$C = B \cdot 1 + B \cdot t$ , so $C$ is module-finite over $B$ with generators $y_{1} = 1$ and $y_{2} = t$ . Indeed any $g \in k [t]$ splits as $g = g_{0} + g_{1} t + t^{2} h$ with $g_{0}, g_{1} \in k$ and $h \in k [t]$ , and then $g = (g_{0} + t^{2} h) \cdot 1 + g_{1} \cdot t$ with both coefficients in $B$ by step 1.1. Note also $t \notin B$ : an element of $k + t^{2} k [t]$ has coefficient $0$ at $t^{1}$ , whereas $t$ has coefficient $1$ there.

L1L2L3step 1.1

3.1

With $r = 1$ , $t_{1} = t$ , $n = 2$ , $y_{1} = 1$ and $y_{2} = t$ , the required relations hold with the coefficients displayed in the Example: $t = 0 \cdot 1 + 1 \cdot t$ ; $y_{1} y_{1} = 1$ ; $y_{1} y_{2} = y_{2} y_{1} = t$ ; and $y_{2} y_{2} = t^{2} = t^{2} \cdot 1 + 0 \cdot t$ , where $t^{2} \in B$ . The collected coefficients are therefore $0$ , $1$ and $t^{2}$ , and the $k$ -subalgebra of $B$ they generate is $A^{'} = k [t^{2}]$ , since $0$ and $1$ already lie in $k$ .

L1L4step 2.1

4.1

$A^{'} = k [t^{2}]$ is of finite type over the Noetherian ring $k$ and is Noetherian, and $B$ is module-finite over $A^{'}$ with generators $1$ and $t^{3}$ . For the last point, $A^{'}$ is the $k$ -span of the powers $t^{2 m}$ , so $A^{'} \cdot 1$ is the $k$ -span of the even powers of $t$ and $A^{'} \cdot t^{3}$ is the $k$ -span of the odd powers $t^{2 m + 3}$ . By step 1.1 the ring $B$ is the $k$ -span of $1$ and of all $t^{a}$ with $a \geq 2$ , so every basis monomial of $B$ lies in one of these two $A^{'}$ -submodules; hence every element of $B$ lies in their sum, and $B = A^{'} \cdot 1 + A^{'} \cdot t^{3}$ .

L4L5L6step 3.1

5.1

The tower now satisfies every hypothesis of the Artin–Tate lemma: $k$ is Noetherian, $C$ is of finite type over $k$ , and $C$ is module-finite over $B$ . The lemma returns that $B$ is of finite type over $k$ ; assembling its generating list from the collected coefficients and the $A^{'}$ -module generators of $B$ gives $k [t^{2}, 1, 0, t^{3}] = k [t^{2}, t^{3}]$ , which is $B$ as presented.

L1L6L7step 4.1∎

Remarks

The coefficient subalgebra is smaller than $B$ here. $A^{'} = k [t^{2}]$ is a polynomial ring in one variable and $B = k [t^{2}, t^{3}]$ is not; the lemma does not claim $A^{'} = B$ , only that $A^{'}$ is Noetherian and that $B$ is a finite $A^{'}$ -module.
The coefficients depend on the chosen module generators. Replacing $y_{2} = t$ by $y_{2} = t + t^{2}$ , which also works since $t = y_{2} - t^{2} \cdot 1$ , changes the structure constants and can change $A^{'}$ ; only the conclusion is independent of the choice.
Nothing here uses the characteristic of $k$ . Every computation above is an identity between polynomials with coefficients $0$ and $1$ , so the example runs unchanged over $F_{2}$ and over $Q$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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