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

Noether's finiteness theorem: the invariants of a finite group acting on a finite-type algebra over a Noetherian ring form an algebra of finite type

Statement

Let $A$ be a Noetherian commutative ring, let $C$ be a commutative $A$ -algebra of finite type (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras) with $A$ a subring of $C$ (Subring: a subset containing $1_{R}$ and closed under addition, additive inverses and multiplication), and let $G$ be a finite group acting on $C$ by $A$ -algebra automorphisms (A group acting on a ring by automorphisms and its invariant subring). Then the invariant subring $C^{G}$ is of finite type over $A$ .

Facts & Assumptions

Given: A Noetherian commutative ring $A$ , a commutative $A$ -algebra $C$ of finite type with $A$ a subring of $C$ , and a finite group $G$ acting on $C$ by $A$ -algebra automorphisms.

[L1]

For an action by ring automorphisms, $C^{G} = {c \in C : g \cdot c = c$ for every $g \in G}$ is a subring of $C$ ; when the action is by $A$ -algebra automorphisms and $A$ is a subring of $C$ , one has $A \subseteq C^{G} \subseteq C$ (A group acting on a ring by automorphisms and its invariant subring).

[L2]

For a finite group acting by ring automorphisms on a nonzero commutative ring $C$ , every element of $C$ is integral over $C^{G}$ (For a finite group of ring automorphisms the orbit polynomial is monic over the invariant subring, so the ring is integral over its invariants).

[L3]

For commutative rings $A \subseteq B \subseteq C$ , each a subring of the next, with $A$ Noetherian, $C$ of finite type over $A$ and every element of $C$ integral over $B$ , the ring $B$ is of finite type over $A$ (The Artin–Tate lemma with integrality in place of module finiteness).

[L4]

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

[L5]

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

Proof

technique · direct

1.1

Dispose of the zero ring. If $C = 0$ then $1_{C} = 0_{C}$ , and since $A$ is a subring of $C$ it has the same zero and identity, so $A = 0$ ; also $C^{G} = 0$ , which is the image of $A$ in $C^{G}$ and hence equals $A []$ , an algebra of finite type over $A$ . For the rest of the argument assume $C \neq 0$ .

L1L4L5given

1.2

The invariant subring sits between the two: $C^{G}$ is a subring of $C$ , and every $g \in G$ fixes $A$ pointwise because the action is by $A$ -algebra automorphisms and $A$ is a subring of $C$ , so $A \subseteq C^{G} \subseteq C$ , each a subring of the next.

L1L5given

2.1

Since $G$ is finite and $C$ is nonzero, every element of $C$ is integral over $C^{G}$ .

L2step 1.1

3.1

The three rings $A \subseteq C^{G} \subseteq C$ satisfy the hypotheses of the integral form of the Artin–Tate lemma: $A$ is Noetherian, $C$ is of finite type over $A$ , and every element of $C$ is integral over $C^{G}$ . Therefore $C^{G}$ is of finite type over $A$ .

L3L4step 1.2step 2.1∎

Remarks

The theorem says finite type, and no more. It produces finitely many algebra generators of $C^{G}$ over $A$ and identifies none of them; for the symmetric group acting on a polynomial ring the companion examples page compares this with the classical description by elementary symmetric polynomials, which is strictly more information.
Finiteness of $G$ is used only through For a finite group of ring automorphisms the orbit polynomial is monic over the invariant subring, so the ring is integral over its invariants, and there it is essential: it is what makes the orbit polynomial a polynomial.
No hypothesis on the characteristic, and no invertibility of $∣ G ∣$ . The route through integrality and the Artin–Tate lemma avoids averaging entirely, which is why nothing here breaks when the order of $G$ is not invertible in $C$ .

Depends on

Used by

Dependency tree · two levels

26 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, Theorem 5.8 (standard reference, not scraped)
A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., (16.22) (standard reference, not scraped)