LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Invariants of a finite-dimensional module are finitely generated

Statement

Assume the Axiom of Choice inherited from the named suppliers. Let $V$ be a finite-dimensional rational module over a complex reductive affine algebraic group $G$ (Complete reducibility and the Reynolds operator for a complex reductive group). Then $C [V]^{G}$ is a finitely generated $C$ -algebra.

Facts & Assumptions

Given: AC; a complex reductive affine algebraic group $G$ ; a finite-dimensional rational $G$ -module $V$ ; the polynomial ring $A = C [V]$ with the action $(g f) (v) = f (g^{- 1} v)$ , and the Reynolds operator $R_{V} : A \to A^{G}$ of the bridge theorem.

[F1]

A rational algebra with a grading. The coordinate ring $A = C [V]$ is a rational $G$ -module on which $G$ acts by algebra automorphisms preserving the unit (The coordinate ring of an affine algebraic action is a locally finite rational module, Classical complex affine algebraic actions and rational modules); as a polynomial ring in the coordinates of $V$ it carries the positive total-degree grading $A = ⨁_{n \geq 0} A_{n}$ with $A_{0} = C$ and each $A_{n}$ finite-dimensional (Nonnegatively graded rings and modules, homogeneous elements, and twists).

[F2]

Polynomial rings are Noetherian. For every field $K$ and finite $d$ , $K [x_{1}, \dots, x_{d}]$ is Noetherian (Finite-variable polynomial algebras over fields are Noetherian by finite generators).

[F3]

Invariants of a Noetherian algebra. With the notation of the Reynolds lemma, for every ideal $I \subseteq A^{G}$ one has $R_{X} (I A) = I$ , and $A^{G}$ is Noetherian whenever $A$ is Noetherian (The Reynolds operator and the ideal theory of the invariant subring).

[F4]

Positively graded Noetherian algebras. A positively graded commutative ring $S = ⨁_{n \geq 0} S_{n}$ with $S_{0}$ a field and $S$ Noetherian is a finitely generated $S_{0}$ -algebra (A positively graded Noetherian algebra is finitely generated over its degree-zero part).

Proof

technique · direct

1.1F1

Since $G$ acts linearly on $V$ , substitution by $g^{- 1}$ preserves the total degree of homogeneous polynomials, so it preserves the grading of $A = C [V]$ : each graded piece $A_{n}$ is $G$ -stable and $A_{0} = C$ consists of constants; hence $A^{G} = ⨁_{n \geq 0} A_{n}^{G}$ is a positively graded $C$ -subalgebra with degree-zero part $C$ .

1.2F2

The polynomial algebra $A = C [V]$ is Noetherian, because $V$ is finite-dimensional with, say, $d$ coordinates and $C [x_{1}, \dots, x_{d}]$ is Noetherian.

2.1F3step 1.2

By the Reynolds ideal theory, applied with $X = V$ , the invariant subalgebra $A^{G}$ is Noetherian.

3.1F4step 1.1step 2.1∎

Finally $A^{G}$ is a positively graded Noetherian $C$ -algebra whose degree-zero part is the field $C$ , so the graded finite-generation lemma makes $A^{G}$ a finitely generated $C$ -algebra. This is the statement.

Remarks

This is Brion's proof of Theorem 1.24(i) in the case $X = V$ : finite generation is reduced to Noetherianity of the invariants by the Reynolds operator and then to the graded Nakayama argument; it is also Popov–Vinberg's Theorem 3.6.
No choice is used beyond the named suppliers: the Reynolds lemma inherits AC from the bridge theorem and the coordinate-ring rationality theorem, and the polynomial Noetherianity and graded finite generation are choice-free.

Depends on

Used by

Dependency tree · two levels

52 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

Michel Brion, Introduction to actions of algebraic groups, Les cours du CIRM 1 (2010), no. 1, 1-22 (standard reference, not scraped)
V. L. Popov and E. B. Vinberg, Invariant Theory, in Algebraic Geometry IV, Encyclopaedia of Mathematical Sciences 55, Springer 1994 (standard reference, not scraped)