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, with nilradicals n⁻ and n⁺. The triangular decomposition TauCeti.UniversalEnvelopingAlgebra.triangularMulEquiv : U(n⁻) ⊗ U(H) ⊗ U(n⁺) ≃ U(L) writes every element of U(L) uniquely as a sum of ordered products f h e. Applying the augmentation ε to the two outer factors gives the Cartan projection

TauCeti.cartanProjection b : U(L) →ₗ[K] U(H), f h e ↦ ε(f) ε(e) h.

It is linear, and not multiplicative on all of U(L). Its value on a central element z computes the central character of every weight: since H is abelian, U(H) is the symmetric algebra S(H), the algebra of polynomial functions on the weights H*, and

χ_λ(z) = (cartanProjection b z)(λ)

(TauCeti.vermaCentralCharacter_eq_lift_cartanProjection). The reason is the Verma module: M(λ) is a free U(n⁻)-module on its generator v_λ, and f h e · v_λ = ε(e) λ(h) f · v_λ, so reading off the coefficient of v_λ in z · v_λ = χ_λ(z) v_λ returns ε(f) ε(e) λ(h) summed over the decomposition of z, which is the value of cartanProjection b z at λ.

Central characters are algebra homomorphisms, and a polynomial function over an infinite field is determined by its values, so the evaluation formula shows that the Cartan projection is multiplicative on the centre. This gives the Harish-Chandra projection

TauCeti.hcProjection b : Z(U(L)) →ₐ[K] S(H),

the restriction of the Cartan projection to the centre, read in S(H), with no ρ-shift. It is the homomorphism whose image is identified, in the Harish-Chandra isomorphism, with the polynomials invariant under the dot action of the Weyl group.

Main definitions #

TauCeti.cartanProjection: the projection U(L) →ₗ[K] U(H) along the triangular decomposition.
TauCeti.hcProjection: the Harish-Chandra projection Z(U(L)) →ₐ[K] S(H).

Main results #

TauCeti.cartanProjection_mul_mul: the projection of an ordered product f h e is ε(f) ε(e) h.
TauCeti.vermaCentralCharacter_eq_lift_cartanProjection: the central character of a weight λ is evaluation at λ of the Cartan projection.
TauCeti.lift_hcProjection: the same formula for hcProjection.

References #

J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §23.3.
J. E. Humphreys, Representations of Semisimple Lie Algebras in the BGG Category O, §1.7.

The Cartan projection #

source

noncomputable def TauCeti.cartanProjection {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) :

UniversalEnvelopingAlgebra K L →ₗ[K] UniversalEnvelopingAlgebra K ↥H

The Cartan projection U(L) → U(H): write an element of U(L) through the triangular decomposition U(n⁻) ⊗ U(H) ⊗ U(n⁺) ≃ U(L) and apply the augmentation to the two outer factors, so that an ordered product f h e goes to ε(f) ε(e) h (TauCeti.cartanProjection_mul_mul). It is linear but not multiplicative; on the centre of U(L) it is the Harish-Chandra projection TauCeti.hcProjection.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem TauCeti.cartanProjection_mul_mul {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) (f : UniversalEnvelopingAlgebra K ↥(negativeNilradical H b)) (h : UniversalEnvelopingAlgebra K ↥H) (e : UniversalEnvelopingAlgebra K ↥(positiveNilradical H b)) :

(cartanProjection b) ((UniversalEnvelopingAlgebra.map K (negativeNilradical H b).incl) f * (UniversalEnvelopingAlgebra.map K H.incl) h * (UniversalEnvelopingAlgebra.map K (positiveNilradical H b).incl) e) = (CoalgebraStruct.counit f * CoalgebraStruct.counit e) • h

The Cartan projection of an ordered product f h e, with f in U(n⁻), h in U(H) and e in U(n⁺), is ε(f) ε(e) h.

source

@[simp]

theorem TauCeti.cartanProjection_map_incl {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) (h : UniversalEnvelopingAlgebra K ↥H) :

(cartanProjection b) ((UniversalEnvelopingAlgebra.map K H.incl) h) = h

The Cartan projection restricts to the identity on U(H).

Evaluation at a weight #

The central character through the Cartan projection #

source

theorem TauCeti.vermaCentralCharacter_eq_lift_cartanProjection {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 : Module.Dual K ↥H) (z : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L))) :

(vermaCentralCharacter b lam) z = (SymmetricAlgebra.lift lam) ((UniversalEnvelopingAlgebra.symmetricAlgebraEquiv K ↥H).symm ((cartanProjection b) ↑z))

The central character of a weight is evaluation of the Cartan projection at that weight: for a central z in U(L), χ_lam(z) is the value at lam of cartanProjection b z, read as a polynomial function on the weights through U(H) ≃ S(H).