The leading term of the Harish-Chandra projection

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field K of characteristic zero, H a splitting Cartan subalgebra and b a base of its root system, so that L = n⁻ ⊕ H ⊕ n⁺. This file shows that the Cartan projection TauCeti.cartanProjection b : U(L) → U(H) is compatible with the PBW filtrations, and computes its leading term.

• Filtration. If u has PBW degree at most n, so does its Cartan projection (TauCeti.cartanProjection_mem_pbwFiltration).
• Leading term. On a word ι x₁ ⋯ ι xₙ the Cartan projection is ι (π x₁) ⋯ ι (π xₙ) up to PBW degree strictly less than n, where π = TauCeti.killingCartanProjection H is the projection of L onto H along the root spaces (TauCeti.cartanProjection_prod_map_ι_sub_mem_pbwFiltrationPrevious).

Both rest on the three rules for multiplying by a generator from TauCeti.Algebra.Lie.HighestWeight.CentralCharacter.HarishChandra: a generator from n⁻ on the left or one from n⁺ on the right is killed by the projection, and a generator h of H on the left passes through it (TauCeti.cartanProjection_ι_coe_mul). A generator e of n⁺ on the left is moved to the right at the cost of the commutator ⁅ι e, u⁆, which has smaller PBW degree.

Read in S(H) through U(H) ≃ S(H), the PBW filtration of U(H) is the degree filtration of S(H). On the centre this gives the two facts about the Harish-Chandra projection TauCeti.hcProjection b that the degree induction proving the Harish-Chandra isomorphism needs: it preserves degrees (TauCeti.hcProjection_mem_wordFiltration), and on the symmetrization of a homogeneous Lie invariant p of degree n it agrees with the Chevalley restriction TauCeti.lieCartanRestriction H p up to degree strictly less than n (TauCeti.hcProjection_sub_lieCartanRestriction_mem_wordFiltrationPrevious).

Main results

• TauCeti.cartanProjection_mem_pbwFiltration: the Cartan projection preserves PBW degree.
• TauCeti.cartanProjection_prod_map_ι_sub_mem_pbwFiltrationPrevious: its leading term on words.
• TauCeti.cartanProjection_pbwHomogeneousSymmetrization_sub_mem_pbwFiltrationPrevious: its leading term on symmetrizations is the Chevalley restriction.
• TauCeti.hcProjection_mem_wordFiltration, TauCeti.hcProjection_mem_wordFiltrationPrevious and TauCeti.hcProjection_sub_lieCartanRestriction_mem_wordFiltrationPrevious: the same for the Harish-Chandra projection, in S(H).

References

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

The PBW filtration

theorem TauCeti.cartanProjection_mem_pbwFiltration {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) {n : ℕ} {u : UniversalEnvelopingAlgebra K L} (hu : u ∈ UniversalEnvelopingAlgebra.pbwFiltration K L n) : (cartanProjection b) u ∈ UniversalEnvelopingAlgebra.pbwFiltration K (↥H) n

The Cartan projection preserves PBW degree: if u is a combination of words of at most n generators in U(L), then cartanProjection b u is one in U(H).

theorem TauCeti.cartanProjection_mem_pbwFiltrationPrevious {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) {n : ℕ} {u : UniversalEnvelopingAlgebra K L} (hu : u ∈ UniversalEnvelopingAlgebra.pbwFiltrationPrevious K L n) : (cartanProjection b) u ∈ UniversalEnvelopingAlgebra.pbwFiltrationPrevious K (↥H) n

The Cartan projection preserves a strict PBW degree bound: the companion of TauCeti.cartanProjection_mem_pbwFiltration for the step preceding degree n.

theorem TauCeti.cartanProjection_prod_map_ι_sub_mem_pbwFiltrationPrevious {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) (l : List L) : (cartanProjection b) (List.map (⇑(UniversalEnvelopingAlgebra.ι K)) l).prod - (List.map (fun (x : L) => (UniversalEnvelopingAlgebra.ι K) ((killingCartanProjection H) x)) l).prod ∈ UniversalEnvelopingAlgebra.pbwFiltrationPrevious K (↥H) l.length

The leading term of the Cartan projection on a word: the Cartan projection of ι x₁ ⋯ ι xₙ is ι (π x₁) ⋯ ι (π xₙ) up to PBW degree strictly less than n, where π is the Killing-orthogonal projection TauCeti.killingCartanProjection H of L onto H.

theorem TauCeti.hcProjection_mem_wordFiltration {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) {n : ℕ} {z : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L))} (hz : ↑z ∈ UniversalEnvelopingAlgebra.pbwFiltration K L n) : (hcProjection b) z ∈ Algebra.wordFiltration (SymmetricAlgebra.ι K ↥H) n

The Harish-Chandra projection preserves degree: a central element of PBW degree at most n has Harish-Chandra projection of degree at most n in S(H).

theorem TauCeti.hcProjection_mem_wordFiltrationPrevious {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) {n : ℕ} {z : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L))} (hz : ↑z ∈ UniversalEnvelopingAlgebra.pbwFiltrationPrevious K L n) : (hcProjection b) z ∈ Algebra.wordFiltrationPrevious (SymmetricAlgebra.ι K ↥H) n

A central element of PBW degree below n has Harish-Chandra projection of degree below n in S(H).

Symmetrizations

theorem TauCeti.cartanProjection_pbwHomogeneousSymmetrization_sub_mem_pbwFiltrationPrevious {K : Type} {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) {n : ℕ} (hn : IsUnit ↑n.factorial) (p : ↥(SymmetricAlgebra.homogeneousSubmodule K L n)) : (cartanProjection b) ((UniversalEnvelopingAlgebra.pbwHomogeneousSymmetrization K L n hn) p) - (UniversalEnvelopingAlgebra.symmetricAlgebraEquiv K ↥H) ((lieCartanRestriction H) ↑p) ∈ UniversalEnvelopingAlgebra.pbwFiltrationPrevious K (↥H) n

The leading term of the Cartan projection on a symmetrization is the Chevalley restriction: for p homogeneous of degree n in S(L), the Cartan projection of its PBW symmetrization agrees with the restriction TauCeti.lieCartanRestriction H p, read in U(H) = S(H), up to PBW degree strictly less than n.

theorem TauCeti.hcProjection_sub_lieCartanRestriction_mem_wordFiltrationPrevious {K : Type} {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) {n : ℕ} (hn : IsUnit ↑n.factorial) (p : ↥(SymmetricAlgebra.homogeneousSubmodule K L n)) {z : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L))} (hz : ↑z = (UniversalEnvelopingAlgebra.pbwHomogeneousSymmetrization K L n hn) p) : (hcProjection b) z - (lieCartanRestriction H) ↑p ∈ Algebra.wordFiltrationPrevious (SymmetricAlgebra.ι K ↥H) n

The leading term of the Harish-Chandra projection is the Chevalley restriction: if the central element z is the PBW symmetrization of p, homogeneous of degree n (such a p is a Lie invariant, by TauCeti.UniversalEnvelopingAlgebra.pbwHomogeneousSymmetrization_mem_center_iff), then hcProjection b z agrees with the restriction TauCeti.lieCartanRestriction H p up to degree strictly less than n in S(H).