The Harish-Chandra isomorphism

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over an algebraically closed field K of characteristic zero, H a 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) records the central characters, χ_λ(z) = (hcProjection b z)(λ), and lands in the dot-invariants S(H)^{W·}; its linear normalization TauCeti.hcProjectionLinear b, the translate by -ρ, lands in the Weyl invariants S(H)^W. Both are injective (TauCeti.hcProjection_injective) and onto (TauCeti.range_hcProjection and TauCeti.range_hcProjectionLinear). This file packages them as isomorphisms

Z(U(L)) ≃ₐ[K] S(H)^{W·} and Z(U(L)) ≃ₐ[K] S(H)^W

(TauCeti.harishChandraIso and TauCeti.harishChandraLinearIso), and derives the central-character orbit theorem: χ_λ = χ_μ exactly when μ lies in the dot orbit W · λ (TauCeti.vermaCentralCharacter_eq_iff). Given equal central characters, every dot-invariant p is hcProjection b z for a central z, so p takes the same value at λ and μ; since the dot-invariants separate dot orbits (TauCeti.forall_mem_dotInvariants_lift_eq_iff), μ ∈ W · λ.

Main definitions

• TauCeti.harishChandraLinearIso b: the linear Harish-Chandra isomorphism Z(U(L)) ≃ₐ[K] S(H)^W.
• TauCeti.harishChandraIso b: the Harish-Chandra isomorphism Z(U(L)) ≃ₐ[K] S(H)^{W·}.

Main results

• TauCeti.harishChandraLinearIso_symm_mem_pbwFiltration and TauCeti.harishChandraIso_symm_mem_pbwFiltration: the inverse isomorphisms send an invariant of degree at most n to a central element of PBW degree at most n.
• TauCeti.vermaCentralCharacter_eq_iff: two weights have the same central character exactly when they lie in one dot orbit.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §23.3.
• J. Dixmier, Enveloping Algebras, §7.4.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapter VIII, §8.

The isomorphisms

noncomputable def TauCeti.harishChandraLinearIso {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] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L)) ≃ₐ[K] ↥(linearInvariants H)

The linear Harish-Chandra isomorphism Z(U(L)) ≃ₐ[K] S(H)^W: the linear Harish-Chandra projection TauCeti.hcProjectionLinear b, with its values in the Weyl invariants.

@[simp]

theorem TauCeti.coe_harishChandraLinearIso_apply {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] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (z : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L))) : ↑((harishChandraLinearIso b) z) = (hcProjectionLinear b) z

The linear Harish-Chandra isomorphism is the linear Harish-Chandra projection.

@[simp]

theorem TauCeti.hcProjectionLinear_harishChandraLinearIso_symm_apply {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] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (q : ↥(linearInvariants H)) : (hcProjectionLinear b) ((harishChandraLinearIso b).symm q) = ↑q

The inverse of the linear Harish-Chandra isomorphism sends a Weyl invariant to the central element projecting to it.

noncomputable def TauCeti.harishChandraIso {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] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L)) ≃ₐ[K] ↥(dotInvariants b)

The Harish-Chandra isomorphism Z(U(L)) ≃ₐ[K] S(H)^{W·}: the Harish-Chandra projection TauCeti.hcProjection b, with its values in the dot-invariants.

@[simp]

theorem TauCeti.coe_harishChandraIso_apply {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] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (z : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L))) : ↑((harishChandraIso b) z) = (hcProjection b) z

The Harish-Chandra isomorphism is the Harish-Chandra projection.

@[simp]

theorem TauCeti.hcProjection_harishChandraIso_symm_apply {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] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (p : ↥(dotInvariants b)) : (hcProjection b) ((harishChandraIso b).symm p) = ↑p

The inverse of the Harish-Chandra isomorphism sends a dot-invariant to the central element projecting to it.

theorem TauCeti.harishChandraIso_trans_dotInvariantsEquivLinearInvariants {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] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) : (harishChandraIso b).trans (dotInvariantsEquivLinearInvariants b) = harishChandraLinearIso b

The two Harish-Chandra isomorphisms differ by the translation by -ρ from the dot-invariants to the Weyl invariants: the linear one is the Harish-Chandra isomorphism followed by TauCeti.dotInvariantsEquivLinearInvariants b.

Inverse filtration

@[simp]

theorem TauCeti.harishChandraLinearIso_symm_mem_pbwFiltration {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] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) {n : ℕ} (q : ↥(linearInvariants H)) : ↑((harishChandraLinearIso b).symm q) ∈ UniversalEnvelopingAlgebra.pbwFiltration K L n ↔ ↑q ∈ Algebra.wordFiltration (SymmetricAlgebra.ι K ↥H) n

The inverse linear Harish-Chandra isomorphism preserves degrees: a Weyl invariant has degree at most n exactly when the corresponding central element has PBW degree at most n.

@[simp]

theorem TauCeti.harishChandraIso_symm_mem_pbwFiltration {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] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) {n : ℕ} (p : ↥(dotInvariants b)) : ↑((harishChandraIso b).symm p) ∈ UniversalEnvelopingAlgebra.pbwFiltration K L n ↔ ↑p ∈ Algebra.wordFiltration (SymmetricAlgebra.ι K ↥H) n

The inverse Harish-Chandra isomorphism preserves degrees: a dot-invariant has degree at most n exactly when the corresponding central element has PBW degree at most n.

Central characters and dot orbits

theorem TauCeti.vermaCentralCharacter_eq_iff {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] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) {lam mu : Module.Dual K ↥H} : vermaCentralCharacter b lam = vermaCentralCharacter b mu ↔ ∃ (w : ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup), dotAction (LieAlgebra.IsKilling.rootSystem H) b w lam = mu

Harish-Chandra's theorem on central characters: two weights lam and mu have the same central character, χ_lam = χ_mu, exactly when mu lies in the dot orbit of lam, that is mu = w · lam = w (lam + ρ) - ρ for an element w of the Weyl group.