The Hilbert ideal of a linear group action

Let a group G act linearly on a module M over a commutative ring R, and so on the symmetric algebra S = Sym M, with invariant subalgebra A = Sym(M)^G. The Hilbert ideal is the ideal A₊ · S of S generated by the invariants with zero constant term; equivalently, by the homogeneous invariants of positive degree. The quotient S ⧸ A₊ · S is the coinvariant algebra of the action. For M = V* with the contragredient action, the zero set of the Hilbert ideal is the null cone of the action on V, and the results below show that for a finite group it is the origin.

For a finite group G, every element p of the irrelevant ideal S₊ (the elements with zero constant term) satisfies p ^ #G ∈ A₊ · S: the lower coefficients of the orbit polynomial ∏ g, (X - g • p) are invariants with zero constant term (Ideal.pow_card_mem_map_under). Hence the radical of the Hilbert ideal is the radical of S₊, which is S₊ itself over a reduced base. In particular the positive-degree elements of the coinvariant algebra are nilpotent, and when M is finitely generated the coinvariant algebra is a finite R-module. None of these results needs #G to be invertible in R.

Main definitions

• Representation.symmetricAlgebraHilbertIdeal: the Hilbert ideal A₊ · S.
• Representation.coinvariantAlgebra: the representation of G on the coinvariant algebra S ⧸ A₊ · S.

Main results

• Representation.symmetricAlgebraHilbertIdeal_le_iff: an ideal contains the Hilbert ideal exactly when it contains every invariant with zero constant term.
• Representation.symmetricAlgebraHilbertIdeal_eq_span: the Hilbert ideal is generated by the homogeneous invariants of positive degree.
• Representation.isHomogeneous_symmetricAlgebraHilbertIdeal: it is a homogeneous ideal.
• Representation.under_irrelevant_eq_span: the ideal A₊ of invariants with zero constant term is generated in A by the homogeneous invariants of positive degree.
• Representation.symmetricAlgebraHilbertIdeal_le_comap: the Hilbert ideal is stable under the induced action.
• Representation.sub_algebraMap_algebraMapInv_mem_symmetricAlgebraHilbertIdeal: an invariant is congruent to its constant term modulo the Hilbert ideal.
• Representation.pow_card_mem_symmetricAlgebraHilbertIdeal: for a finite group, p ^ #G lies in the Hilbert ideal for every p with zero constant term.
• Representation.radical_symmetricAlgebraHilbertIdeal_of_isReduced: over a reduced base, the radical of the Hilbert ideal is the irrelevant ideal.
• Representation.moduleFinite_quotient_symmetricAlgebraHilbertIdeal: for a finite group and a finitely generated module, the coinvariant algebra is a finite R-module.

References

• H. Derksen, G. Kemper, Computational Invariant Theory, Springer (2002), Chapter 2.
• L. Smith, Polynomial Invariants of Finite Groups, A K Peters (1995), Chapter 2.
• R. Kane, Reflection Groups and Invariant Theory, CMS Books in Mathematics, Springer (2001), § 17.

theorem Representation.symmetricAlgebra_mem_irrelevant {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (g : G) {p : SymmetricAlgebra R M} (hp : p ∈ HomogeneousIdeal.irrelevant (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M)) : (ρ.symmetricAlgebra g) p ∈ HomogeneousIdeal.irrelevant (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M)

The induced action preserves the irrelevant ideal: it does not change constant terms.

noncomputable def Representation.symmetricAlgebraHilbertIdeal {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) : Ideal (SymmetricAlgebra R M)

The Hilbert ideal A₊ · S of the induced action on S = Sym M: the ideal generated by the invariants with zero constant term, that is, the extension to S of the contraction of the irrelevant ideal S₊ to the invariant subalgebra A.

theorem Representation.symmetricAlgebraHilbertIdeal_le_iff {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) {J : Ideal (SymmetricAlgebra R M)} : ρ.symmetricAlgebraHilbertIdeal ≤ J ↔ ∀ p ∈ ρ.symmetricAlgebraInvariants, p ∈ HomogeneousIdeal.irrelevant (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M) → p ∈ J

An ideal contains the Hilbert ideal exactly when it contains every invariant with zero constant term.

theorem Representation.mem_symmetricAlgebraHilbertIdeal_of_mem {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) {p : SymmetricAlgebra R M} (hp : p ∈ ρ.symmetricAlgebraInvariants) (hp' : p ∈ HomogeneousIdeal.irrelevant (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M)) : p ∈ ρ.symmetricAlgebraHilbertIdeal

An invariant with zero constant term lies in the Hilbert ideal.

theorem Representation.symmetricAlgebraHilbertIdeal_eq_span_of_surjective {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) {ι : Type u_4} (f : ι → ↥ρ.symmetricAlgebraInvariants) (hf : ∀ (i : ι), ↑(f i) ∈ HomogeneousIdeal.irrelevant (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M)) (hsurj : Function.Surjective ⇑(MvPolynomial.aeval f)) : ρ.symmetricAlgebraHilbertIdeal = Ideal.span (Set.range fun (i : ι) => ↑(f i))

A generating family for the invariant algebra, all of whose members have zero constant term, generates the Hilbert ideal in the ambient symmetric algebra. Polynomial independence and finiteness of the family are not needed.

theorem Representation.symmetricAlgebraHilbertIdeal_le_irrelevant {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) : ρ.symmetricAlgebraHilbertIdeal ≤ (HomogeneousIdeal.irrelevant (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M)).toIdeal

The Hilbert ideal is contained in the irrelevant ideal.

theorem Representation.symmetricAlgebraHilbertIdeal_le_comap {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (g : G) : ρ.symmetricAlgebraHilbertIdeal ≤ Ideal.comap (SymmetricAlgebra.map R (ρ g)) ρ.symmetricAlgebraHilbertIdeal

The induced action of each g maps the Hilbert ideal into itself, since g fixes the invariants generating it.

theorem Representation.symmetricAlgebraHilbertIdeal_eq_span {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) : ρ.symmetricAlgebraHilbertIdeal = Ideal.span {p : SymmetricAlgebra R M | p ∈ ρ.symmetricAlgebraInvariants ∧ ∃ (n : ℕ), 0 < n ∧ p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n}

The Hilbert ideal is generated by the homogeneous invariants of positive degree.

theorem Representation.isHomogeneous_symmetricAlgebraHilbertIdeal {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) : Ideal.IsHomogeneous (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M) ρ.symmetricAlgebraHilbertIdeal

The Hilbert ideal is a homogeneous ideal, so the coinvariant algebra is graded.

theorem Representation.under_irrelevant_eq_span {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) : Ideal.under (↥ρ.symmetricAlgebraInvariants) (HomogeneousIdeal.irrelevant (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M)).toIdeal = Ideal.span {f : ↥ρ.symmetricAlgebraInvariants | ∃ (n : ℕ), 0 < n ∧ ↑f ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n}

The ideal A₊ of invariants with zero constant term is generated by the homogeneous invariants of positive degree.

theorem Representation.sub_algebraMap_algebraMapInv_mem_symmetricAlgebraHilbertIdeal {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) {p : SymmetricAlgebra R M} (hp : p ∈ ρ.symmetricAlgebraInvariants) : p - (algebraMap R (SymmetricAlgebra R M)) (SymmetricAlgebra.algebraMapInv p) ∈ ρ.symmetricAlgebraHilbertIdeal

An invariant is congruent to its constant term modulo the Hilbert ideal, the constant term being its image under the augmentation SymmetricAlgebra.algebraMapInv.

noncomputable def Representation.coinvariantAlgebra {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) : Representation R G (SymmetricAlgebra R M ⧸ ρ.symmetricAlgebraHilbertIdeal)

The representation of G on the coinvariant algebra Sym M ⧸ A₊ · Sym M induced by ρ: the Hilbert ideal is stable under the induced action, so each g descends to the quotient, where it acts by an algebra endomorphism (an automorphism when G is a group).

This is not Mathlib's Representation.Coinvariants, the largest quotient of a representation on which the group acts trivially.

@[simp]

theorem Representation.coinvariantAlgebra_mk {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (g : G) (p : SymmetricAlgebra R M) : (ρ.coinvariantAlgebra g) ((Ideal.Quotient.mk ρ.symmetricAlgebraHilbertIdeal) p) = (Ideal.Quotient.mk ρ.symmetricAlgebraHilbertIdeal) ((ρ.symmetricAlgebra g) p)

On the coinvariant algebra, g acts on the class of p through the induced action on p.

theorem Representation.pow_card_mem_symmetricAlgebraHilbertIdeal {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [Finite G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) {p : SymmetricAlgebra R M} (hp : p ∈ HomogeneousIdeal.irrelevant (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M)) : p ^ Nat.card G ∈ ρ.symmetricAlgebraHilbertIdeal

Elements with zero constant term are nilpotent modulo the Hilbert ideal. For a finite group G and p in the irrelevant ideal, p ^ #G lies in the Hilbert ideal.

theorem Representation.isNilpotent_mk_symmetricAlgebraHilbertIdeal {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [Finite G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) {p : SymmetricAlgebra R M} (hp : p ∈ HomogeneousIdeal.irrelevant (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M)) : IsNilpotent ((Ideal.Quotient.mk ρ.symmetricAlgebraHilbertIdeal) p)

The image in the coinvariant algebra of an element with zero constant term is nilpotent.

theorem Representation.radical_symmetricAlgebraHilbertIdeal {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [Finite G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) : ρ.symmetricAlgebraHilbertIdeal.radical = (HomogeneousIdeal.irrelevant (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M)).toIdeal.radical

For a finite group, the Hilbert ideal and the irrelevant ideal have the same radical.

theorem Representation.radical_symmetricAlgebraHilbertIdeal_of_isReduced {R : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing R] [Group G] [Finite G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) [IsReduced R] : ρ.symmetricAlgebraHilbertIdeal.radical = (HomogeneousIdeal.irrelevant (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M)).toIdeal

For a finite group over a reduced base, the radical of the Hilbert ideal is the irrelevant ideal.

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

Finiteness of the coinvariant algebra. For a finite group acting on a finitely generated module, the coinvariant algebra Sym M ⧸ A₊ · Sym M is a finite R-module: it is of finite type, and generated by nilpotent, hence integral, elements.