Dot-invariant polynomials separate dot orbits

For two weights in distinct dot orbits, finite interpolation produces a polynomial taking values zero and one on the respective orbits. Its product over Weyl pullbacks remains zero and one on those orbits and is dot-invariant. Consequently two weights have identical values on every dot-invariant polynomial exactly when they lie in one dot orbit.

This is the invariant-theoretic step of the Harish-Chandra central-character orbit theorem. It is independent of surjectivity of the Harish-Chandra projection.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapter VIII, §8, central characters.

theorem TauCeti.exists_mem_dotInvariants_lift_eq_zero_one {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam mu : Module.Dual K ↥H} (h : ¬∃ (w : ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup), dotAction (LieAlgebra.IsKilling.rootSystem H) b w lam = mu) : ∃ p ∈ dotInvariants b, (SymmetricAlgebra.lift lam) p = 0 ∧ (SymmetricAlgebra.lift mu) p = 1

Two distinct dot orbits are separated by a dot-invariant polynomial with values zero and one. The weights need not be integral or dominant.

theorem TauCeti.forall_mem_dotInvariants_lift_eq_iff {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam mu : Module.Dual K ↥H} : (∀ p ∈ dotInvariants b, (SymmetricAlgebra.lift lam) p = (SymmetricAlgebra.lift mu) p) ↔ ∃ (w : ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup), dotAction (LieAlgebra.IsKilling.rootSystem H) b w lam = mu

Equality of all dot-invariant polynomial values characterizes a dot orbit.