Invariant polynomials of a finite linear group separate orbits

Let a finite group G act linearly on a vector space V over a field K through a representation ρ, and so on the polynomial functions Sym(V*) through the contragredient representation ρ.dual. A vector v : V defines the evaluation SymmetricAlgebra.lift (Module.Dual.eval K V v) : Sym(V*) →ₐ[K] K, which sends a linear form φ to φ v. Translating a polynomial by g corresponds to evaluating at ρ g⁻¹ v.

The invariant polynomials Sym(V*)^G separate the orbits of G on V: two vectors have the same value on every invariant exactly when they lie in the same orbit, and vectors in distinct orbits are separated by an invariant with values 0 and 1. This is the specialization of FixedPoints.forall_mem_subalgebra_eq_iff to evaluations at vectors; it needs neither finite-dimensionality nor any hypothesis on the characteristic of K.

Since the orbit of 0 is {0}, the only vector at which every homogeneous invariant of positive degree vanishes is 0. Geometrically, the fibre of the quotient map V → V/G over the vertex, the point cut out by the invariants of positive degree, consists of the origin alone. Over an algebraically closed field the Nullstellensatz turns this into the equality of the radical of the Hilbert ideal Sym(V*)^G₊ · Sym(V*) with the ideal of positive-degree elements, which is how the dimension of the invariant ring at its vertex is compared with that of Sym(V*).

Main results

• Representation.lift_eval_symmetricAlgebra_dual: evaluating a translate at v is evaluating at ρ g⁻¹ v.
• Representation.exists_mem_symmetricAlgebraInvariants_lift_eval_eq_zero_and_eq_one: vectors in distinct orbits are separated by an invariant with values 0 and 1.
• Representation.forall_mem_symmetricAlgebraInvariants_lift_eval_eq_iff: two vectors agree on every invariant exactly when they lie in the same orbit.
• Representation.forall_homogeneous_mem_symmetricAlgebraInvariants_lift_eval_eq_zero_iff: every homogeneous invariant of positive degree vanishes at v exactly when v = 0.

References

• H. Derksen, G. Kemper, Computational Invariant Theory, Springer (2002), Chapter 2.

theorem Representation.lift_eval_symmetricAlgebra_dual {K : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring K] [Group G] [AddCommMonoid V] [Module K V] (ρ : Representation K G V) (g : G) (v : V) (p : SymmetricAlgebra K (Module.Dual K V)) : (SymmetricAlgebra.lift ((Module.Dual.eval K V) v)) ((ρ.dual.symmetricAlgebra g) p) = (SymmetricAlgebra.lift ((Module.Dual.eval K V) ((ρ g⁻¹) v))) p

Evaluating the translate by g of a polynomial function at v is evaluating the polynomial function at ρ g⁻¹ v.

theorem Representation.exists_mem_symmetricAlgebraInvariants_lift_eval_eq_zero_and_eq_one {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [Finite G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) {v w : V} (h : ∀ (g : G), (ρ g) v ≠ w) : ∃ p ∈ ρ.dual.symmetricAlgebraInvariants, (SymmetricAlgebra.lift ((Module.Dual.eval K V) v)) p = 0 ∧ (SymmetricAlgebra.lift ((Module.Dual.eval K V) w)) p = 1

Invariant polynomials separate orbits. If w is not in the orbit of v, then some invariant polynomial function takes the value 0 at v and 1 at w.

theorem Representation.forall_mem_symmetricAlgebraInvariants_lift_eval_eq_iff {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [Finite G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) {v w : V} : (∀ p ∈ ρ.dual.symmetricAlgebraInvariants, (SymmetricAlgebra.lift ((Module.Dual.eval K V) v)) p = (SymmetricAlgebra.lift ((Module.Dual.eval K V) w)) p) ↔ ∃ (g : G), (ρ g) v = w

Invariant polynomials detect orbits. Two vectors have the same value on every invariant polynomial function exactly when they lie in the same orbit.

theorem Representation.forall_homogeneous_mem_symmetricAlgebraInvariants_lift_eval_eq_zero_iff {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [Finite G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) {v : V} : (∀ (n : ℕ), 0 < n → ∀ p ∈ ρ.dual.symmetricAlgebraInvariants, p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule K (Module.Dual K V) n → (SymmetricAlgebra.lift ((Module.Dual.eval K V) v)) p = 0) ↔ v = 0

The fibre over the vertex is the origin. Every homogeneous invariant polynomial function of positive degree vanishes at v exactly when v = 0.