Surjectivity of the Harish-Chandra projection

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over an algebraically closed field K of characteristic zero, H a splitting Cartan subalgebra and b a base of its root system, with Weyl vector ρ. The Harish-Chandra projection TauCeti.hcProjection b : Z(U(L)) →ₐ[K] S(H) takes values in the dot-invariants S(H)^{W·}, and its linear normalization TauCeti.hcProjectionLinear b, the projection followed by translation by -ρ, takes values in the Weyl invariants S(H)^W. This file proves that both are onto:

(hcProjectionLinear b).range = S(H)^W and (hcProjection b).range = S(H)^{W·}.

The proof is the degree induction of Harish-Chandra's theorem, with a degree bound on the preimage: a Weyl invariant q of degree at most n is the image of a central element of PBW degree at most n (TauCeti.exists_mem_pbwFiltration_hcProjectionLinear_eq). Its homogeneous component q_n of degree n is again a Weyl invariant, so by Chevalley's restriction theorem it is the restriction to H of a homogeneous invariant p ∈ S(L)^L of degree n. The PBW symmetrization z of p is central, and the leading term of the Harish-Chandra projection is the Chevalley restriction (TauCeti.hcProjection_sub_lieCartanRestriction_mem_wordFiltrationPrevious), while translation by -ρ only changes lower-degree terms. So hcProjectionLinear b z - q_n, and with it q - hcProjectionLinear b z, is a Weyl invariant of degree strictly less than n, to which the induction hypothesis applies.

Injectivity (TauCeti.hcProjection_injective) needs in addition that the PBW symbol of a central element is a Lie invariant; the resulting Harish-Chandra isomorphism Z(U(L)) ≃ S(H)^W is TauCeti.harishChandraLinearIso in TauCeti.Algebra.Lie.HighestWeight.CentralCharacter.Isomorphism.

Main results

• TauCeti.exists_mem_pbwFiltration_hcProjectionLinear_eq: a Weyl invariant of degree at most n is the linear Harish-Chandra projection of a central element of PBW degree at most n.
• TauCeti.range_hcProjectionLinear: the linear Harish-Chandra projection is onto the Weyl invariants.
• TauCeti.exists_mem_pbwFiltration_hcProjection_eq and TauCeti.range_hcProjection: the same for the Harish-Chandra projection and the dot-invariants.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §23.3.

theorem TauCeti.exists_mem_pbwFiltration_hcProjectionLinear_eq {K : Type} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (b : (LieAlgebra.IsKilling.rootSystem H).Base) {n : ℕ} {q : SymmetricAlgebra K ↥H} (hq : q ∈ linearInvariants H) (hqn : q ∈ Algebra.wordFiltration (SymmetricAlgebra.ι K ↥H) n) : ∃ (z : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L))), ↑z ∈ UniversalEnvelopingAlgebra.pbwFiltration K L n ∧ (hcProjectionLinear b) z = q

Harish-Chandra surjectivity with a degree bound. A Weyl invariant q ∈ S(H)^W of degree at most n is the linear Harish-Chandra projection of a central element of U(L) of PBW degree at most n.

theorem TauCeti.range_hcProjectionLinear {K : Type} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (b : (LieAlgebra.IsKilling.rootSystem H).Base) : (hcProjectionLinear b).range = linearInvariants H

The linear Harish-Chandra projection is onto the Weyl invariants: its range is S(H)^W.

theorem TauCeti.exists_mem_pbwFiltration_hcProjection_eq {K : Type} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (b : (LieAlgebra.IsKilling.rootSystem H).Base) {n : ℕ} {q : SymmetricAlgebra K ↥H} (hq : q ∈ dotInvariants b) (hqn : q ∈ Algebra.wordFiltration (SymmetricAlgebra.ι K ↥H) n) : ∃ (z : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L))), ↑z ∈ UniversalEnvelopingAlgebra.pbwFiltration K L n ∧ (hcProjection b) z = q

Harish-Chandra surjectivity with a degree bound, dot form. A dot-invariant q ∈ S(H)^{W·} of degree at most n is the Harish-Chandra projection of a central element of U(L) of PBW degree at most n.

theorem TauCeti.range_hcProjection {K : Type} {L : Type v} [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (b : (LieAlgebra.IsKilling.rootSystem H).Base) : (hcProjection b).range = dotInvariants b

The Harish-Chandra projection is onto the dot-invariants: its range is S(H)^{W·}.