Noether finiteness for the invariants of a finite linear group

Let a finite group G act linearly on a finitely generated module M over a commutative ring R, and so on the symmetric algebra S = Sym M, with invariant subalgebra A = Sym(M)^G. Then S is a finite A-module, and over a Noetherian base A is a finitely generated R-algebra (Noether's finiteness theorem). Both facts are the general results for fixed subalgebras of finite groups, transported along Representation.symmetricAlgebraInvariants_eq_fixedPoints.

Over a commutative rational algebra, the invariants are generated by homogeneous elements of positive degree at most the group order. The action need not be faithful and the module need not be free or finite. For a finite module, a finite set of such generators exists even if the coefficient algebra is not Noetherian. For polynomial functions apply this to the contragredient representation on the dual space.

The degree bound concerns algebra generators, not a basic-invariant degree list or polynomiality. The proof specializes TauCeti.FixedPoints.subalgebra_eq_adjoin_sum_smul_prod_pow: linearity makes the orbit sums homogeneous, and degree-zero orbit sums are scalars that can be omitted.

Main results

• Representation.moduleFinite_symmetricAlgebraInvariants: Sym M is a finite module over the invariant subalgebra.
• Representation.finiteType_symmetricAlgebraInvariants: over a Noetherian base, the invariant subalgebra is of finite type.
• Representation.symmetricAlgebraInvariants_eq_adjoin_homogeneous: over a rational algebra, homogeneous invariants of degrees between one and the group order generate the invariants.
• Representation.exists_finset_adjoin_eq_symmetricAlgebraInvariants: for a finite module over a rational algebra, there is a finite set of such homogeneous generators.

References

• E. Noether, Der Endlichkeitssatz der Invarianten endlicher Gruppen, Math. Ann. 77 (1916), 89–92.
• L. Smith, Polynomial Invariants of Finite Groups, A K Peters (1995), Chapter 2.
• H. Derksen, G. Kemper, Computational Invariant Theory, Springer (2002), Chapter 2.

instance Representation.moduleFinite_symmetricAlgebraInvariants {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) [Finite G] [Module.Finite R M] : Module.Finite (↥ρ.symmetricAlgebraInvariants) (SymmetricAlgebra R M)

For a finite group acting on a finitely generated module M, the symmetric algebra Sym M is a finite module over the invariant subalgebra.

instance Representation.finiteType_symmetricAlgebraInvariants {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) [Finite G] [IsNoetherianRing R] [Module.Finite R M] : Algebra.FiniteType R ↥ρ.symmetricAlgebraInvariants

Noether's finiteness theorem for the invariants of a finite group acting on a finitely generated module over a Noetherian ring: the invariant subalgebra is of finite type.

theorem Representation.symmetricAlgebraInvariants_eq_adjoin_homogeneous {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) [Fintype G] [Algebra ℚ R] : ρ.symmetricAlgebraInvariants = Algebra.adjoin R {p : SymmetricAlgebra R M | p ∈ ρ.symmetricAlgebraInvariants ∧ ∃ (n : ℕ), 0 < n ∧ n ≤ Fintype.card G ∧ p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n}

The homogeneous Noether bound. The invariants of a finite linear group over a rational algebra are generated by homogeneous invariants of positive degree at most the group order. This holds without finite generation or freeness of the underlying module.

theorem Representation.exists_finset_adjoin_eq_symmetricAlgebraInvariants {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) [Fintype G] [Algebra ℚ R] [Module.Finite R M] : ∃ (s : Finset (SymmetricAlgebra R M)), (∀ p ∈ s, p ∈ ρ.symmetricAlgebraInvariants ∧ ∃ (n : ℕ), 0 < n ∧ n ≤ Fintype.card G ∧ p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n) ∧ Algebra.adjoin R ↑s = ρ.symmetricAlgebraInvariants

Finite homogeneous Noether generators. If the module is finite, its polynomial invariants admit a finite generating set of homogeneous elements with degrees between one and the group order. No Noetherian hypothesis on the rational coefficient algebra is needed.