Finite generation of graded subalgebras with ideal contraction

Let S be a Noetherian ℕ-graded k-algebra whose degree-zero part consists of scalars, and let B be a k-subalgebra of S. Suppose B contains the homogeneous components of its elements, and that every ideal J of B is recovered from its extension: J S ∩ B = J. Then B is a finitely generated k-algebra.

This is Hilbert's argument for the finite generation of rings of invariants. The ideal of S generated by the positive-degree homogeneous elements of B is generated by finitely many of them, f₁, …, fᵣ. A homogeneous element of B of positive degree d lies in this ideal, so by ideal contraction it is a combination ∑ bᵢ fᵢ with bᵢ ∈ B; keeping only the degree-d components, the coefficients become homogeneous elements of B of degree smaller than d, and induction on the degree shows that B is generated by f₁, …, fᵣ.

For the invariants of a linearly reductive group acting on a polynomial ring, ideal contraction is supplied by exactness of invariants, in place of the Reynolds operator of the classical argument.

The file also compares finite generation over the coefficients R with finite generation over the degree-zero part 𝒜 0, the form in which finiteness hypotheses enter the projective spectrum.

Main results

• Subalgebra.fg_of_decompose_mem_of_comap_map_le: a subalgebra closed under homogeneous components and with ideal contraction is finitely generated.
• TauCeti.GradedAlgebra.exists_finset_adjoin_eq_top_and_mem_grade_ne_zero: a finite-type semiring graded algebra is generated over its degree-zero part by finitely many homogeneous elements of nonzero degree.
• TauCeti.GradedAlgebra.finiteType_gradeZero_left: a graded algebra of finite type over R is of finite type over its degree-zero part.
• TauCeti.GradedAlgebra.finiteType_gradeZero: the degree-zero part of a graded algebra of finite type over R is of finite type over R.

References

• D. Hilbert, Über die Theorie der algebraischen Formen, Math. Ann. 36 (1890).
• S. Mukai, An Introduction to Invariants and Moduli, Cambridge University Press (2003), Theorem 4.51.

theorem Subalgebra.fg_of_decompose_mem_of_comap_map_le {k : Type u_1} {S : Type u_2} [CommSemiring k] [CommSemiring S] [Algebra k S] [IsNoetherianRing S] (𝒜 : ℕ → Submodule k S) [GradedAlgebra 𝒜] (h𝒜 : ∀ x ∈ 𝒜 0, x ∈ ⊥) (B : Subalgebra k S) (hBdecompose : ∀ x ∈ B, ∀ (n : ℕ), ↑(((DirectSum.decompose 𝒜) x) n) ∈ B) (hBideal : ∀ (J : Ideal ↥B), Ideal.comap (algebraMap (↥B) S) (Ideal.map (algebraMap (↥B) S) J) ≤ J) : B.FG

Hilbert's finiteness argument. In a Noetherian ℕ-graded algebra whose degree-zero part consists of scalars, a subalgebra containing the homogeneous components of its elements, and recovering each of its ideals from the ideal it generates, is finitely generated.

theorem TauCeti.GradedAlgebra.exists_finset_adjoin_eq_top_and_mem_grade_ne_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [Algebra.FiniteType (↥(𝒜 0)) A] : ∃ (s : Finset A), Algebra.adjoin ↥(𝒜 0) ↑s = ⊤ ∧ ∀ x ∈ s, ∃ (n : ℕ), n ≠ 0 ∧ x ∈ 𝒜 n

A graded algebra of finite type over 𝒜 0 is generated over 𝒜 0 by finitely many homogeneous elements of positive degree. This is the semiring version of Mathlib's GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero, which is stated for rings.

instance TauCeti.GradedAlgebra.finiteType_gradeZero_left {R : Type u_1} {A : Type u_2} {ι : Type u_3} [DecidableEq ι] [CommSemiring R] [CommSemiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [AddMonoid ι] [GradedAlgebra 𝒜] [Algebra.FiniteType R A] : Algebra.FiniteType (↥(𝒜 0)) A

A graded algebra of finite type over R is of finite type over its degree-zero part.

instance TauCeti.GradedAlgebra.finiteType_gradeZero {R : Type u_1} {A : Type u_2} {ι : Type u_3} [DecidableEq ι] [CommSemiring R] [CommSemiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [GradedAlgebra 𝒜] [Algebra.FiniteType R A] : Algebra.FiniteType R ↥(𝒜 0)

The degree-zero part of a graded algebra of finite type over R is of finite type over R: it is the image of the algebra under the projection a ↦ a₀, which is an R-algebra homomorphism because the scalars have degree zero.