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.

A positively graded Noetherian algebra is finitely generated over its degree-zero part

Statement

Assume the Axiom of Choice inherited from the named suppliers. Let $A = ⨁_{n \geq 0} A_{n}$ be a graded commutative ring with $A_{0}$ a field, and suppose $A$ is Noetherian (Nonnegatively graded rings and modules, homogeneous elements, and twists, Left and right Noetherian rings). Then $A$ is a finitely generated $A_{0}$ -algebra (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras).

Facts & Assumptions

Given: AC; a nonnegatively graded commutative ring $A = ⨁_{n \geq 0} A_{n}$ with $A_{n} A_{m} \subseteq A_{n + m}$ , whose degree-zero part $A_{0}$ is a field, and which is Noetherian.

[F1]

Graded rings. A nonnegatively graded ring is a commutative ring $S = ⨁_{n \geq 0} S_{n}$ with $S_{n} S_{m} \subseteq S_{n + m}$ for all $m, n \geq 0$ ; an element of $S_{n}$ is homogeneous of degree $n$ (Nonnegatively graded rings and modules, homogeneous elements, and twists).

[F2]

Noetherian ideals are finitely generated. Every ideal of a Noetherian commutative ring is finitely generated (A commutative ring is Noetherian exactly when every ideal is finitely generated, exactly when its ideals satisfy the ascending chain condition, and exactly when every nonempty set of ideals has a maximal member).

[F3]

Finite generation over the base. A commutative $R$ -algebra $A$ is of finite type over $R$ , equivalently a finitely generated $R$ -algebra, when $A = R [a_{1}, \dots, a_{n}]$ for some $n \in N$ and some $a_{1}, \dots, a_{n} \in A$ ; for $n = 0$ this is the image of $R$ (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras).

Proof

technique · direct

1.1F1F2given

Put $A_{+} = ⨁_{n \geq 1} A_{n}$ . Then $A = A_{0} \oplus A_{+}$ as abelian groups, and $A_{+}$ is an ideal of $A$ : for $a \in A_{m}$ with $m \geq 1$ and $b \in A_{n}$ one has $a b \in A_{m + n}$ with $m + n \geq 1$ , and $A_{+}$ is closed under sums by the direct-sum decomposition. Since $A$ is Noetherian, the ideal $A_{+}$ is finitely generated.

2.1F1step 1.1

Fix a finite generating list $h_{1}, \dots, h_{r}$ of $A_{+}$ . Each $h_{j}$ is the finite sum of its homogeneous components, and because $h_{j}$ lies in $A_{+} = ⨁_{n \geq 1} A_{n}$ and this is a direct sum decomposition, the component of $h_{j}$ in $A_{d}$ vanishes for $d = 0$ and lies in $A_{d} \subseteq A_{+}$ for $d \geq 1$ ; each $h_{j}$ is therefore the sum of its homogeneous components of positive degree. Discarding zero components and relabelling, we obtain finitely many homogeneous elements $g_{1}, \dots, g_{m} \in A_{+}$ of positive degrees $e_{1}, \dots, e_{m} \geq 1$ that still generate $A_{+}$ : every $h_{j}$ is an $A$ -linear combination of the $g_{i}$ while each $g_{i}$ lies in $A_{+} = (h_{1}, \dots, h_{r})$ , so $(h_{1}, \dots, h_{r}) \subseteq (g_{1}, \dots, g_{m}) \subseteq A_{+}$ and the two lists generate the same ideal.

3.1F1step 2.1

Every homogeneous element $f \in A_{d}$ lies in the $A_{0}$ -subalgebra $A_{0} [g_{1}, \dots, g_{m}]$ . This is proved by induction on $d$ . For $d = 0$ one has $f \in A_{0} \subseteq A_{0} [g_{1}, \dots, g_{m}]$ . For $d \geq 1$ , step 2.1 gives $f \in A_{+} = (g_{1}, \dots, g_{m})$ , so $f = \sum_{i} r_{i} g_{i}$ with $r_{i} \in A$ ; taking the homogeneous component of degree $d$ of this identity, and using that $g_{i}$ is homogeneous of degree $e_{i}$ , we may assume each $r_{i}$ lies in $A_{d - e_{i}}$ , which is the zero group when $d - e_{i} < 0$ because the grading is nonnegative. In the nonzero cases $d - e_{i} < d$ , so the induction hypothesis gives $r_{i} \in A_{0} [g_{1}, \dots, g_{m}]$ and hence $f = \sum_{i} r_{i} g_{i} \in A_{0} [g_{1}, \dots, g_{m}]$ .

4.1F1F3step 3.1∎

Let $f \in A$ be arbitrary. Since $A$ is the direct sum of the graded pieces $A_{d}$ , the element $f$ is a finite sum $f = \sum_{d} f_{d}$ of homogeneous elements $f_{d} \in A_{d}$ ; by step 3.1 each $f_{d}$ lies in $A_{0} [g_{1}, \dots, g_{m}]$ , hence so does $f$ . Therefore $A = A_{0} [g_{1}, \dots, g_{m}]$ is generated as an $A_{0}$ -algebra by the finitely many elements $g_{1}, \dots, g_{m}$ , that is, $A$ is a finitely generated $A_{0}$ -algebra.

Remarks

The argument is the graded form of Nakayama: $A_{+}$ is a homogeneous ideal, so it can be generated by homogeneous elements, and the top-degree part of a relation lowers the degree. This is the argument used by Brion in the proof of his Theorem 1.24(i) and by Popov–Vinberg in Theorem 3.6.
No choice is used beyond the finite generation supplied by the Noetherian hypothesis; with an empty generating list the conclusion reads $A = A_{0} = A_{0} [\emptyset]$ .

Depends on

Used by

Dependency tree · two levels

20 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; Russian original in Itogi Nauki i Tekhniki 55 (1989), 137-309 (standard reference, not scraped)