Chevalley's restriction theorem: injectivity and the coreflections

Let L be a finite-dimensional Lie algebra over a field K of characteristic zero whose Killing form is nondegenerate, and H a splitting Cartan subalgebra. Restricting polynomial functions from L to H is, through the Killing identifications, the algebra map TauCeti.lieCartanRestriction H : S(L) →ₐ[K] S(H). This file proves that it is injective on the invariants S(L)^L, and that the restriction of an invariant is fixed by the coreflection of every root.

On the side of polynomial functions the argument is the classical one. An invariant polynomial function p ∈ S(L*)^L is invariant under the group Int(L) of inner automorphisms (TauCeti.SymmetricAlgebra.lift_eval_smul_of_mem_intLieAlgebra). If it vanishes on H it therefore vanishes on every conjugate g h, g ∈ Int(L), h ∈ H, and these conjugates are Zariski dense in L (LieSubalgebra.polynomial_eq_zero_of_invariant_of_cartan), so p = 0. The two statements are joined by reading p as a polynomial in the coordinates of a basis of L (Module.Basis.lift_eval_apply_eq_eval_equivMvPolynomial_dualBasis). The Killing equivalence S(L) ≃ S(L*) identifies the invariants on both sides (TauCeti.killingSymmetricEquiv_mem_lieInvariants_iff) and turns restriction to H into lieCartanRestriction (TauCeti.map_dualMap_killingSymmetricEquiv).

For a nonzero root α with sl₂ triple (α^∨, e, f), the inner automorphism σ = exp(ad e) exp(-ad f) exp(ad e) (TauCeti.weylAut) acts on H by the coreflection h ↦ h - α(h) • α^∨, and it preserves the Killing form, so it commutes with the Killing-orthogonal projection L → H defining the restriction. An invariant is fixed by σ, so its restriction is fixed by the coreflection.

Main results

• TauCeti.eq_zero_of_mem_lieInvariants_of_lift_eval_eq_zero: an invariant polynomial function on L vanishing on H is zero.
• LieSubalgebra.lieCartanRestriction_injOn_lieInvariants: lieCartanRestriction H is injective on S(L)^L.
• TauCeti.map_coreflection_lieCartanRestriction: the coreflection of a root fixes the restriction of an invariant.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §23.1.
• J. Dixmier, Enveloping Algebras, §7.3.

theorem TauCeti.eq_zero_of_mem_lieInvariants_of_lift_eval_eq_zero {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {p : SymmetricAlgebra K (Module.Dual K L)} (hp : p ∈ SymmetricAlgebra.lieInvariants K L (Module.Dual K L)) (hH : ∀ h ∈ H, (SymmetricAlgebra.lift ((Module.Dual.eval K L) h)) p = 0) : p = 0

An invariant polynomial function vanishing on a Cartan subalgebra is zero. If an element p of the algebra S(L*) of polynomial functions on L is killed by the coadjoint action of L and vanishes at every point of the splitting Cartan subalgebra H, then p = 0.

theorem TauCeti.map_coreflection_lieCartanRestriction {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (i : ↥LieSubalgebra.root) {p : SymmetricAlgebra K L} (hp : p ∈ SymmetricAlgebra.lieInvariants K L L) : (SymmetricAlgebra.map K ↑((LieAlgebra.IsKilling.rootSystem H).coreflection i)) ((lieCartanRestriction H) p) = (lieCartanRestriction H) p

The coreflections fix the restriction of an invariant. For a root α, the coreflection h ↦ h - α(h) • α^∨ of H fixes the restriction TauCeti.lieCartanRestriction H p of every invariant p ∈ S(L)^L. On H it is the inner automorphism exp(ad e) exp(-ad f) exp(ad e) of an sl₂ triple of α, which fixes p.

theorem LieSubalgebra.lieCartanRestriction_injOn_lieInvariants {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (H : LieSubalgebra K L) [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] : Set.InjOn ⇑(TauCeti.lieCartanRestriction H) ↑(TauCeti.SymmetricAlgebra.lieInvariants K L L)

Chevalley's restriction theorem, injectivity. Restriction of polynomial functions from L to the splitting Cartan subalgebra H, read on S(L) as TauCeti.lieCartanRestriction H, is injective on the invariants S(L)^L.