Central characters are constant on dot orbits

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. The centre Z(U(L)) acts on every highest weight module of weight λ through the central character χ_λ = TauCeti.vermaCentralCharacter b λ. This file proves that χ_λ depends only on the orbit of λ under the dot action w · λ = w(λ + ρ) - ρ of the Weyl group:

χ_{w · λ} = χ_λ (TauCeti.vermaCentralCharacter_dotAction).

Read through the Harish-Chandra projection TauCeti.hcProjection b : Z(U(L)) →ₐ[K] S(H), whose value at λ is χ_λ (TauCeti.lift_hcProjection), this says that the projection takes values in the dot-invariants S(H)^{W·} (TauCeti.hcProjection_mem_dotInvariants), the polynomial functions p on H* with p(w · λ) = p(λ) for all w and λ (TauCeti.dotInvariants). This is the inclusion half of the Harish-Chandra isomorphism Z(U(L)) ≃ S(H)^{W·}, and the easy direction of the theorem that χ_λ = χ_μ exactly when μ ∈ W · λ.

The argument

The Weyl group is generated by the simple reflections, so it suffices to treat one simple reflection sᵢ, which acts by sᵢ · λ = λ - (⟨λ, αᵢ^∨⟩ + 1) αᵢ.

• Integral weights: a singular vector. If ⟨λ, αᵢ^∨⟩ = n is a natural number, then for a nonzero lowering vector fᵢ of αᵢ the vector fᵢ^{n+1} · v_λ of the Verma module M(λ) is nonzero (TauCeti.pow_toEnd_vermaGenerator_ne_zero, from Poincaré--Birkhoff--Witt) and is a highest weight vector of weight sᵢ · λ (TauCeti.isHighestWeightVector_pow_toEnd_vermaGenerator, from the integrability relation). The centre acts on it by χ_{sᵢ · λ}, and also by χ_λ, since it acts on all of M(λ) by χ_λ; so the two characters agree.
• All weights: density. For a central z, both λ ↦ χ_λ(z) and λ ↦ χ_{sᵢ · λ}(z) are polynomial functions of λ (TauCeti.lift_hcProjection), so along the line λ + t αᵢ they are polynomials in t (SymmetricAlgebra.exists_polynomial_eval_eq_lift_add_smul), using sᵢ · (λ + t αᵢ) = sᵢ · λ - t αᵢ. Since ⟨λ + t αᵢ, αᵢ^∨⟩ = ⟨λ, αᵢ^∨⟩ + 2t, the integral case makes the two polynomials agree at the infinitely many t for which this is a natural number, hence everywhere, and in particular at t = 0.

Main definitions

• TauCeti.dotInvariants b: the dot-invariants S(H)^{W·}, the subalgebra of S(H) of elements p with p(w · λ) = p(λ) for every Weyl group element w and weight λ.

Main results

• TauCeti.isHighestWeightVector_pow_toEnd_vermaGenerator: for a simple root αᵢ with ⟨λ, αᵢ^∨⟩ = n ∈ ℕ, fᵢ^{n+1} · v_λ is a highest weight vector of M(λ) of weight λ - (n + 1) αᵢ.
• TauCeti.vermaCentralCharacter_dotAction: central characters are constant on dot orbits.
• TauCeti.hcProjection_mem_dotInvariants: the Harish-Chandra projection takes values in the dot-invariants.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §23.2 and §23.3.
• J. E. Humphreys, Representations of Semisimple Lie Algebras in the BGG Category O, Chapter 1, "Harish-Chandra's theorem".

The singular vector of an integral simple root

theorem TauCeti.isHighestWeightVector_pow_toEnd_vermaGenerator {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} {i : ↥LieSubalgebra.root} (hi : i ∈ b.support) {n : ℕ} (hn : lam ((LieAlgebra.IsKilling.rootSystem H).coroot i) = ↑n) {f : L} (hf : f ∈ LieAlgebra.rootSpace H ⇑(-↑i)) (hf0 : f ≠ 0) : IsHighestWeightVector b (lam - (n + 1) • (LieAlgebra.IsKilling.rootSystem H).root i) (((LieModule.toEnd K L (VermaModule b lam)) f ^ (n + 1)) (vermaGenerator b lam))

The singular vector of M(lam) along an integral simple root. If αᵢ is a simple root with lam (αᵢ^∨) = n a natural number and f is a nonzero lowering vector of αᵢ, then f^{n+1} · v_lam is a highest weight vector of the Verma module M(lam), of weight lam - (n + 1) αᵢ, the dot reflection of lam in αᵢ.

Invariance under a simple reflection

Invariance under the Weyl group

@[simp]

theorem TauCeti.vermaCentralCharacter_dotAction {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) (w : ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup) (lam : Module.Dual K ↥H) : vermaCentralCharacter b (dotAction (LieAlgebra.IsKilling.rootSystem H) b w lam) = vermaCentralCharacter b lam

Central characters are constant on dot orbits: χ_{w · lam} = χ_lam for every element w of the Weyl group, where w · lam = w (lam + ρ) - ρ is the dot action.

The dot-invariants

noncomputable def TauCeti.dotInvariants {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) : Subalgebra K (SymmetricAlgebra K ↥H)

The dot-invariants S(H)^{W·}: the elements p of the symmetric algebra S(H), read as polynomial functions on the weights H*, with p(w · lam) = p(lam) for every Weyl group element w and every weight lam, where w · lam is the dot action.

Equations

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

@[simp]

theorem TauCeti.mem_dotInvariants_iff {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} {p : SymmetricAlgebra K ↥H} : p ∈ dotInvariants b ↔ ∀ (w : ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup) (lam : Module.Dual K ↥H), (SymmetricAlgebra.lift (dotAction (LieAlgebra.IsKilling.rootSystem H) b w lam)) p = (SymmetricAlgebra.lift lam) p

Membership in the dot-invariants: p(w · lam) = p(lam) for every Weyl group element w and every weight lam.

theorem TauCeti.hcProjection_mem_dotInvariants {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} (z : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L))) : (hcProjection b) z ∈ dotInvariants b

The Harish-Chandra projection takes values in the dot-invariants: its value at a weight is the central character, which is constant on dot orbits.