Basic invariants as a regular sequence

A homogeneous polynomial presentation of an invariant algebra gives a regular sequence in the ambient symmetric algebra whenever that algebra is flat over its invariants. In particular, the basic invariants of a finite pseudoreflection group of invertible order form a regular sequence in the polynomial functions on its representation.

Regularity includes properness of the generated ideal: positive-degree invariants lie in the irrelevant ideal. It is not just the assertion that multiplication is injective on successive quotients. This is the regular-sequence input for computing the graded coinvariant algebra from homogeneous basic invariants.

The argument transports the regular sequence of polynomial coordinates to the invariant algebra, then uses Mathlib's regular-sequence flat-base-change theorem. The required flatness for pseudoreflection groups is supplied by the divided-difference and Tor argument, not assumed as a consequence of polynomiality.

References

• R. Kane, Reflection Groups and Invariant Theory, Springer (2001), §§ 17–18.
• J. E. Humphreys, Reflection Groups and Coxeter Groups, Cambridge University Press (1990), Chapter 3.

theorem Representation.isRegular_symmetricAlgebraInvariants_of_flat {K : Type u_1} {G : Type u_2} {M : Type u_3} [CommRing K] [Nontrivial K] [Monoid G] [AddCommMonoid M] [Module K M] (ρ : Representation K G M) [Module.Flat (↥ρ.symmetricAlgebraInvariants) (SymmetricAlgebra K M)] {n : ℕ} (f : Fin n → ↥ρ.symmetricAlgebraInvariants) (hf : ∀ (i : Fin n), ∃ (d : ℕ), 0 < d ∧ ↑(f i) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule K M d) (hbij : Function.Bijective ⇑(MvPolynomial.aeval f)) : RingTheory.Sequence.IsRegular (SymmetricAlgebra K M) (List.ofFn fun (i : Fin n) => ↑(f i))

If the symmetric algebra is flat over its invariants, any homogeneous polynomial presentation by positive-degree invariants gives a regular sequence in the symmetric algebra. The statement includes the empty sequence.

theorem Representation.isRegular_symmetricAlgebraInvariants_dual_of_pseudoreflectionSubgroup_eq_top {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] [Fintype G] [Invertible ↑(Fintype.card G)] (ρ : Representation K G V) (hG : ρ.pseudoreflectionSubgroup = ⊤) {n : ℕ} (f : Fin n → ↥ρ.dual.symmetricAlgebraInvariants) (hf : ∀ (i : Fin n), ∃ (d : ℕ), 0 < d ∧ ↑(f i) ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule K (Module.Dual K V) d) (hbij : Function.Bijective ⇑(MvPolynomial.aeval f)) : RingTheory.Sequence.IsRegular (SymmetricAlgebra K (Module.Dual K V)) (List.ofFn fun (i : Fin n) => ↑(f i))

Homogeneous basic invariants of a finite group generated by pseudoreflections form a regular sequence in the polynomial functions Sym(V*), provided the group order is invertible in the field. No faithfulness or algebraic closedness is required.