Finite generation of invariant algebras of finite groups

Let a finite group G act on a commutative R-algebra A by R-algebra automorphisms, and let A^G = FixedPoints.subalgebra R A G be the invariant subalgebra. This file proves that A^G is finitely generated whenever A is, in two forms.

Noether's finiteness theorem. If A is of finite type over R, it is integral over A^G (Mathlib's Algebra.IsInvariant.isIntegral, through the monic orbit polynomial), hence a finite A^G-module. If moreover R is Noetherian, the Artin–Tate lemma fg_of_fg_of_fg makes A^G of finite type over R. Nothing is assumed about the characteristic, so this includes the modular case, where the order of G is not invertible in R.

Noether's degree bound. If R is a ℚ-algebra and A is generated by a family x, finite or not, then A^G is generated by the orbit sums ∑_{g ∈ G} g • x^d of the monomials x^d of total degree at most |G|. For the polynomial functions A = Sym(V*), with G acting through a linear action on V* and x a basis of V*, these are homogeneous invariants of degree at most |G|; an arbitrary algebra automorphism of Sym(V*) need not preserve the grading. This bounds the degrees of some generating set; it is not the list of degrees of a system of basic invariants, which need not exist, and the bound says nothing about how many generators are needed. Here R need not be Noetherian. The bound also holds when only |G| is invertible in a field (Fleischmann, Fogarty), which is not proved here.

The proof of the degree bound is Noether's. Only the finitely many xᵢ occurring in d enter the orbit sum of x^d, so we may take the family finite. In the polynomial ring A[u₁, …, uₙ] put y_g = ∑ᵢ (g • xᵢ) uᵢ for g ∈ G. The coefficient of u^d in the power sum ∑_g y_g^k is multinomial(d) • ∑_g g • x^d when d has degree k, and zero otherwise. By Newton's identities for the |G| elements y_g, every power sum lies in the subalgebra generated over R by the first |G| power sums, and so has all its coefficients in the subalgebra generated by the orbit sums of monomials of degree at most |G|. Dividing by the multinomial coefficient, the orbit sum of every monomial lies there. Finally every invariant f is |G|⁻¹ ∑_g g • f, a linear combination of orbit sums of monomials.

Main results

• TauCeti.FixedPoints.moduleFinite_subalgebra: a finite-type R-algebra is a finite module over its invariants under a finite group.
• TauCeti.FixedPoints.finiteType_subalgebra: Noether's finiteness theorem: over a Noetherian base, the invariants of a finite group acting on a finite-type algebra form a finite-type algebra.
• TauCeti.sum_smul_prod_pow_mem_adjoin: over a ℚ-algebra, the orbit sum of every monomial in x is a polynomial in the orbit sums of the monomials of degree at most |G|.
• TauCeti.FixedPoints.subalgebra_eq_adjoin_sum_smul_prod_pow: Noether's degree bound: if x generates A over a ℚ-algebra R, the orbit sums of the monomials in x of degree at most |G| generate A^G.
• TauCeti.FixedPoints.finiteType_subalgebra_of_algebraRat: over any ℚ-algebra, Noetherian or not, the invariants of a finite group acting on a finite-type algebra form a finite-type algebra.

References

• E. Noether, Der Endlichkeitssatz der Invarianten endlicher Gruppen, Math. Ann. 77 (1916), 89–92.
• M. F. Atiyah and I. G. Macdonald, Introduction to Commutative Algebra, Proposition 7.8 (Artin–Tate) and Chapter 7, Exercise 5.
• P. Fleischmann, The Noether bound in invariant theory of finite groups, Adv. Math. 156 (2000), 23–32; J. Fogarty, On Noether's bound for polynomial invariants of a finite group, Electron. Res. Announc. Amer. Math. Soc. 7 (2001), 5–7.

instance TauCeti.FixedPoints.moduleFinite_subalgebra (R : Type u_1) (A : Type u_2) (G : Type u_3) [CommRing R] [CommRing A] [Algebra R A] [Group G] [MulSemiringAction G A] [SMulCommClass G R A] [Algebra.FiniteType R A] [Finite G] : Module.Finite (↥(FixedPoints.subalgebra R A G)) A

A finite-type R-algebra is a finite module over its invariants under a finite group.

instance TauCeti.FixedPoints.finiteType_subalgebra (R : Type u_1) (A : Type u_2) (G : Type u_3) [CommRing R] [CommRing A] [Algebra R A] [Group G] [MulSemiringAction G A] [SMulCommClass G R A] [IsNoetherianRing R] [Algebra.FiniteType R A] [Finite G] : Algebra.FiniteType R ↥(FixedPoints.subalgebra R A G)

Noether's finiteness theorem. Over a Noetherian base ring R, the invariants of a finite group acting on a finite-type R-algebra form a finite-type R-algebra.

theorem TauCeti.sum_smul_prod_pow_mem_adjoin {R : Type u_1} {A : Type u_2} {G : Type u_3} [CommRing R] [Algebra ℚ R] [CommRing A] [Algebra R A] [Fintype G] {ι : Type u_4} [Monoid G] [MulSemiringAction G A] (x : ι → A) (d : ι →₀ ℕ) : (∑ g : G, g • d.prod fun (i : ι) (n : ℕ) => x i ^ n) ∈ Algebra.adjoin R ((fun (e : ι →₀ ℕ) => ∑ g : G, g • e.prod fun (i : ι) (n : ℕ) => x i ^ n) '' {e : ι →₀ ℕ | Finsupp.degree e ≤ Fintype.card G})

Over a ℚ-algebra R, the orbit sum ∑_{g ∈ G} g • x^d of every monomial x^d in a family x, finite or not, is a polynomial over R in the orbit sums of the monomials of total degree at most |G|.

theorem TauCeti.FixedPoints.subalgebra_eq_adjoin_sum_smul_prod_pow {R : Type u_1} {A : Type u_2} {G : Type u_3} [CommRing R] [Algebra ℚ R] [CommRing A] [Algebra R A] [Fintype G] {ι : Type u_4} [Group G] [MulSemiringAction G A] [SMulCommClass G R A] (x : ι → A) (hx : Algebra.adjoin R (Set.range x) = ⊤) : FixedPoints.subalgebra R A G = Algebra.adjoin R ((fun (d : ι →₀ ℕ) => ∑ g : G, g • d.prod fun (i : ι) (n : ℕ) => x i ^ n) '' {d : ι →₀ ℕ | Finsupp.degree d ≤ Fintype.card G})

Noether's degree bound. If a family x, finite or not, generates a commutative algebra A over a ℚ-algebra R, then the invariants of a finite group G acting on A are generated by the orbit sums ∑_{g ∈ G} g • x^d of the monomials x^d of total degree at most |G|.

instance TauCeti.FixedPoints.finiteType_subalgebra_of_algebraRat (R : Type u_1) (A : Type u_2) (G : Type u_3) [CommRing R] [Algebra ℚ R] [CommRing A] [Algebra R A] [Group G] [MulSemiringAction G A] [SMulCommClass G R A] [Algebra.FiniteType R A] [Finite G] : Algebra.FiniteType R ↥(FixedPoints.subalgebra R A G)

Over a ℚ-algebra R, Noetherian or not, the invariants of a finite group acting on a finite-type R-algebra form a finite-type R-algebra. This follows from Noether's degree bound.