Invariants of a finite group separate orbits of rational points

Let a finite group G act on a commutative algebra S over a field K by K-algebra automorphisms. The K-points of S, the K-algebra homomorphisms χ : S →ₐ[K] K, are permuted by G through precomposition: g sends χ to χ ∘ (g • ·). Two points in the same orbit agree on every invariant. Conversely, two points in distinct orbits are separated by an invariant taking the values 0 and 1 on them.

To construct it, interpolate on the finitely many points of the two orbits (AlgHom.surjective_pi_of_injective): some q : S vanishes on the first orbit and equals 1 on the second. The product ∏ g, g • q of the translates of q is invariant and still takes the values 0 and 1 on the two points. No hypothesis on the characteristic of K is needed, since the separating invariant is a product of translates rather than an average.

For the action of a finite linear group on polynomial functions, this is the statement that the invariant polynomials separate the orbits of points, which identifies the fibres of the quotient map by the invariant ring.

Main results

• FixedPoints.exists_mem_subalgebra_eq_zero_and_eq_one: points in distinct orbits are separated by an invariant with values 0 and 1.
• FixedPoints.forall_mem_subalgebra_eq_iff: two points agree on every invariant exactly when they lie in the same orbit.

The construction is the one used for dot orbits of weights in TauCeti.exists_mem_dotInvariants_lift_eq_zero_one, stated here for an arbitrary finite action.

References

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

theorem FixedPoints.exists_mem_subalgebra_eq_zero_and_eq_one {K : Type u_1} {S : Type u_2} {G : Type u_3} [Field K] [CommSemiring S] [Algebra K S] [Group G] [Finite G] [MulSemiringAction G S] [SMulCommClass G K S] {χ ψ : S →ₐ[K] K} (h : ∀ (g : G), χ.comp (MulSemiringAction.toAlgHom K S g) ≠ ψ) : ∃ p ∈ subalgebra K S G, χ p = 0 ∧ ψ p = 1

Invariants separate orbits of points. If no translate χ ∘ (g • ·) of the point χ is the point ψ, then some invariant takes the value 0 at χ and 1 at ψ.

theorem FixedPoints.forall_mem_subalgebra_eq_iff {K : Type u_1} {S : Type u_2} {G : Type u_3} [Field K] [CommSemiring S] [Algebra K S] [Group G] [Finite G] [MulSemiringAction G S] [SMulCommClass G K S] {χ ψ : S →ₐ[K] K} : (∀ p ∈ subalgebra K S G, χ p = ψ p) ↔ ∃ (g : G), χ.comp (MulSemiringAction.toAlgHom K S g) = ψ

Invariants detect orbits of points. Two points of S agree on every invariant exactly when one is a translate of the other.