Root exponentials and the density of the conjugates of a Cartan subalgebra

Let L be a finite-dimensional Lie algebra over a field K of characteristic zero whose Killing form is nondegenerate, and let H be a splitting Cartan subalgebra. Choose a nonzero vector e_α in each root space and list the roots in some order α₁, …, α_m. The root-exponential map

φ(t, h) = exp(t₁ ad e_{α₁}) ⋯ exp(t_m ad e_{α_m}) h, t ∈ K^m, h ∈ H,

takes values in the conjugates Int(L) · H of H under the group Int(L) of inner automorphisms (TauCeti.intLieAlgebra). Each ad e_α is nilpotent, so each exponential is a finite sum and the coordinates of φ in a basis of L are polynomials in t and in the coordinates of h.

At a point (0, h₀) the differential of φ sends (τ, η) to η + ∑ τ_α ⁅e_α, h₀⁆, and ⁅e_α, h₀⁆ = -α(h₀) e_α. If no root vanishes at h₀ (such an h₀ exists because K is infinite) the image of the differential contains H and every root space, so by the root space decomposition it is all of L. A polynomial map whose differential is surjective at one point is dominant (TauCeti.eq_zero_of_forall_eval_eq_zero_of_mulVec_surjective_jacobiMatrixAt), so:

a polynomial function on L that vanishes on Int(L) · H is zero.

This is the density statement on which the injectivity half of Chevalley's restriction theorem rests: an Int(L)-invariant polynomial function vanishing on H vanishes on Int(L) · H, hence everywhere.

The differential is computed by evaluating the coordinate polynomials at a dual-number point (TauCeti.jacobiMatrixAt_mulVec_apply_eq_snd_aeval): every exponential becomes 1 + ε τ_α ad e_α, and the product of these is 1 + ε ∑ τ_α ad e_α because ε² = 0.

Main results

• LieSubalgebra.exists_rootExponentialPolynomialParametrization: a polynomial family, in the coordinates of a basis of L, whose values all lie in Int(L) · H and whose Jacobian matrix is surjective at some point.
• LieSubalgebra.polynomial_eq_zero_of_intCartan: a polynomial in the coordinates of a basis of L that vanishes on Int(L) · H is zero.
• LieSubalgebra.polynomial_eq_zero_of_invariant_of_cartan: an Int(L)-invariant polynomial that vanishes on H is zero.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §23.1, where the injectivity of the Chevalley restriction map is proved by the density of Int(L) · H.

theorem LieSubalgebra.exists_rootExponentialPolynomialParametrization {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] (H : LieSubalgebra K L) [CharZero K] [LieAlgebra ℚ L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {ι : Type u_3} {κ : Type u_4} [Finite ι] [Fintype κ] (b : Module.Basis ι K L) (bH : Module.Basis κ K ↥H) : ∃ (p : ι → MvPolynomial (↥root ⊕ κ) K), (∃ (v : ↥root ⊕ κ → K), Function.Surjective (TauCeti.jacobiMatrixAt p v).mulVec) ∧ ∀ (x : ↥root ⊕ κ → K), ∃ g ∈ TauCeti.intLieAlgebra K L, ∃ h ∈ H, b.equivFun (g • h) = fun (i : ι) => (MvPolynomial.eval x) (p i)

The root-exponential parametrization of the conjugates of a Cartan subalgebra. Given a basis b of L and a basis bH of the splitting Cartan subalgebra H, there is a family of polynomials in one variable for each root and one for each basis vector of H, with these two properties: its values, read in the coordinates of b, are all of the form g h with g in Int(L) and h ∈ H, and its Jacobian matrix is surjective at some point. The polynomials are the coordinates of (t, h) ↦ ∏_α exp(t_α ad e_α) h for chosen root vectors e_α.

theorem LieSubalgebra.polynomial_eq_zero_of_intCartan {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] (H : LieSubalgebra K L) [CharZero K] [LieAlgebra ℚ L] [LieAlgebra.IsKilling K L] [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {ι : Type u_3} [Finite ι] (b : Module.Basis ι K L) {q : MvPolynomial ι K} (hq : ∀ g ∈ TauCeti.intLieAlgebra K L, ∀ h ∈ H, (MvPolynomial.eval (b.equivFun (g • h))) q = 0) : q = 0

A polynomial vanishing on the conjugates of a Cartan subalgebra is zero. In the coordinates of a basis b of L, a polynomial that vanishes at g h for every inner automorphism g ∈ Int(L) and every h in the splitting Cartan subalgebra H is the zero polynomial.

theorem LieSubalgebra.polynomial_eq_zero_of_invariant_of_cartan {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] (H : LieSubalgebra K L) [CharZero K] [LieAlgebra ℚ L] [LieAlgebra.IsKilling K L] [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {ι : Type u_3} [Finite ι] (b : Module.Basis ι K L) {q : MvPolynomial ι K} (hinv : ∀ g ∈ TauCeti.intLieAlgebra K L, ∀ (x : L), (MvPolynomial.eval (b.equivFun (g • x))) q = (MvPolynomial.eval (b.equivFun x)) q) (hH : ∀ h ∈ H, (MvPolynomial.eval (b.equivFun h)) q = 0) : q = 0

Chevalley injectivity on polynomials. In the coordinates of a basis b of L, a polynomial invariant under the inner automorphisms Int(L) that vanishes on the splitting Cartan subalgebra H is the zero polynomial.