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

For a finite group of ring automorphisms the orbit polynomial is monic over the invariant subring, so the ring is integral over its invariants

Statement

Let $G$ be a finite group acting by ring automorphisms on a nonzero commutative ring $C$ , and let $C^{G}$ be the invariant subring (A group acting on a ring by automorphisms and its invariant subring). Extend the action to the polynomial ring $C [T]$ coefficientwise, fixing $T$ . For $x \in C$ put

$P_{x} (T) : = \prod_{g \in G} (T - g \cdot x) \in C [T] .$

Then $P_{x}$ is monic of degree $∣ G ∣$ , every coefficient of $P_{x}$ lies in $C^{G}$ , and $P_{x} (x) = 0$ . Consequently every element of $C$ is integral over $C^{G}$ (Integral elements over a commutative ring and algebraic integers).

Finiteness of $G$ is a hypothesis, not a convenience: the product is over the index set $G$ and is a polynomial only because that set is finite. The hypothesis $C \neq 0$ is what makes $1_{C} \neq 0_{C}$ , so that a monic polynomial exists at all.

Facts & Assumptions

Given: A finite group $G$ acting by ring automorphisms on a nonzero commutative ring $C$ , an element $x \in C$ , and the polynomial ring $C [T]$ .

[L1]

For an action of a group $G$ on a commutative ring $C$ by ring automorphisms, $C^{G} = {c \in C : g \cdot c = c$ for every $g \in G}$ is a subring of $C$ , and each $g$ acts as a ring automorphism, so $g \cdot 1_{C} = 1_{C}$ (A group acting on a ring by automorphisms and its invariant subring).

[L2]

In a group every element $h$ has a two-sided inverse $h^{- 1}$ , and multiplication is associative (Group and abelian group).

[L3]

A left action satisfies $e \cdot c = c$ and $(g h) \cdot c = g \cdot (h \cdot c)$ for all $g, h \in G$ and $c \in C$ (Left group actions, transitive actions, and faithful actions).

[L4]

$C [T]$ is the set of finitely supported functions $N \to C$ with $(a + b)_{i} = a_{i} + b_{i}$ and $(a b)_{i} = \sum_{j + k = i} a_{j} b_{k}$ ; the constant $c$ is supported at $0$ and $T$ has coefficient $1_{C}$ at index $1$ (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution).

[L5]

For $0 \neq f \in C [T]$ the degree is the largest index carrying a nonzero coefficient, the leading coefficient is the coefficient there, and $f$ is monic when that coefficient is $1_{C}$ (Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).

[L6]

For nonzero $f, g \in C [T]$ : the coefficient of $T^{\deg f + \deg g}$ in $f g$ is $lc (f) lc (g)$ , and if $f g \neq 0$ then $\deg (f g) \leq \deg f + \deg g$ (Degree inequalities for sums and products over a commutative ring).

[L7]

For commutative rings $C, S$ , a unital ring homomorphism $φ ⁣ : C \to S$ and $s \in S$ , there is a unique unital ring homomorphism $C [T] \to S$ extending $φ$ on constants and sending $T$ to $s$ (Universal property of $R [x]$ : a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism).

[L8]

The value of $f = \sum_{i} a_{i} T^{i}$ at $s$ along $φ$ is $f_{φ} (s) = \sum_{i} φ (a_{i}) s^{i}$ , and $s$ is a root of $f$ when that value is $0$ (Evaluation and roots of a polynomial in a commutative target ring).

[L9]

For a homomorphism of commutative rings $A \to B$ , an element $b \in B$ is integral over $A$ when it is a root of a monic polynomial in $A [X]$ (Integral elements over a commutative ring and algebraic integers).

[L10]

For a commutative ring $C$ , the polynomial ring $C [T]$ is a commutative ring (Polynomial convolution makes $R [x]$ a commutative ring containing $R$ as its constant subring).

Proof

technique · direct

1.1L1L2L3L4given

For $g \in G$ let $g$ act on $C [T]$ by $g \cdot \sum_{i} a_{i} T^{i} : = \sum_{i} (g \cdot a_{i}) T^{i}$ . This is additive because addition of polynomials is coefficientwise, multiplicative because $g \cdot \sum_{j + k = i} a_{j} b_{k} = \sum_{j + k = i} (g \cdot a_{j}) (g \cdot b_{k})$ by the ring-homomorphism property of $g$ on $C$ , and it sends $1$ to $1$ and $T$ to $T$ ; the action axioms are inherited coefficientwise, so this is again an action of $G$ by ring automorphisms, restricting to the given one on constants.

2.1L4L5L6step 1.1

$P_{x} = \prod_{g \in G} (T - g \cdot x)$ is monic of degree $∣ G ∣$ . Each factor $T - g \cdot x$ is nonzero of degree $1$ with leading coefficient $1_{C} \neq 0_{C}$ , because $C \neq 0$ . Multiplying the factors one at a time: if $f$ is monic of degree $d$ then the coefficient of $T^{d + 1}$ in $f \cdot (T - g \cdot x)$ is $1_{C} \cdot 1_{C} = 1_{C} \neq 0_{C}$ , so that product is nonzero, its degree is at most $d + 1$ , and the nonvanishing coefficient at $T^{d + 1}$ forces the degree to be exactly $d + 1$ with leading coefficient $1_{C}$ . Since $G$ is finite and nonempty, the product over all of $G$ is monic of degree $∣ G ∣$ .

2.2L1L2L3L10step 1.1

$P_{x}$ is fixed by the action. For $h \in G$ , applying $h$ coefficientwise to a product is applying it to each factor, so $h \cdot P_{x} = \prod_{g \in G} (T - (h g) \cdot x)$ ; the map $g \mapsto h g$ is a bijection of $G$ onto itself, with inverse $g \mapsto h^{- 1} g$ , so it merely permutes the factors of a product in the commutative ring $C [T]$ and $h \cdot P_{x} = P_{x}$ . Since the action on $C [T]$ is coefficientwise, every coefficient of $P_{x}$ is fixed by every $h \in G$ , that is, lies in $C^{G}$ .

3.1L3L7L8step 2.1

$P_{x} (x) = 0$ . Evaluation at $x$ along the identity of $C$ is the unique unital ring homomorphism $C [T] \to C$ fixing constants and sending $T$ to $x$ , so it carries the product $\prod_{g} (T - g \cdot x)$ to $\prod_{g} (x - g \cdot x)$ . The factor indexed by the identity $e$ of $G$ is $x - e \cdot x = x - x = 0$ , and a product in a commutative ring with a zero factor is zero.

4.1L1L5L9step 2.1step 2.2step 3.1∎

By step 2.2 all coefficients of $P_{x}$ lie in the subring $C^{G}$ , so $P_{x}$ is a polynomial in $C^{G} [T]$ ; its leading coefficient is $1_{C} = 1_{C^{G}}$ , so it is monic there as well, and by step 3.1 the element $x$ is a root of it. Hence $x$ is integral over $C^{G}$ , and since $x \in C$ was arbitrary, $C$ is integral over $C^{G}$ .

Remarks

The product is over the whole group, not over the orbit. Repeated factors are tolerated and are what keeps the degree equal to $∣ G ∣$ independently of the stabiliser of $x$ ; taking the product over the orbit would give a polynomial of varying degree and would need the orbit to be a set of distinct elements.
Nothing is said about $C^{G}$ being large. For a faithful action with many invariants the polynomial $P_{x}$ is informative; for the trivial group it is $(T - x)^{1}$ and the statement is the tautology that every element of $C$ is integral over $C$ .
Infinite $G$ gives nothing here. The construction produces no polynomial at all, since an infinite product of linear factors is not an element of $C [T]$ , and the conclusion can fail.

Depends on

Used by

Dependency tree · two levels

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