The centre of U(L) on isotypic components

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)) of the universal enveloping algebra acts on every highest weight module of weight lam through the central character chi_lam = TauCeti.vermaCentralCharacter b lam. This file reads that statement on the isotypic components of an arbitrary module, and then, for a finite-dimensional module over an algebraically closed field, as a decomposition of the module under the centre.

• The centre acts on the L(lam)-isotypic component by chi_lam (TauCeti.isotypicComponent_irreducibleQuotient_le_centerEigenspace): every Lie submodule equivalent to L(lam) is a highest weight module of weight lam, so it lies in the centre eigenspace M_{chi_lam} (TauCeti.UniversalEnvelopingAlgebra.centerEigenspace), and so does their sum. No finite-dimensionality is needed. Consequently isotypic components whose central characters differ are disjoint (TauCeti.disjoint_isotypicComponent_irreducibleQuotient_of_vermaCentralCharacter_ne).
• The centre acts semisimply on a finite-dimensional module (TauCeti.isInternal_centerEigenspace): by Weyl's theorem such a module is a direct sum of irreducible submodules, each a copy of some L(lam) with lam dominant integral, so it is the sum of the centre eigenspaces M_{chi_lam} over dominant integral lam (TauCeti.iSup_centerEigenspace_vermaCentralCharacter_eq_top). Centre eigenspaces for distinct eigenvalue functions are independent, so the module is the internal direct sum of its centre eigenspaces, and the only eigenvalue functions occurring are the central characters of dominant integral weights (TauCeti.exists_isDominantIntegral_eq_vermaCentralCharacter).

This is the eigenspace-of-the-centre refinement of the isotypic decomposition M ≅ ⨁ L(lam)^{m lam} (TauCeti.nonempty_lieModuleEquiv_directSum_irreducibleQuotient): it groups the isotypic components by central character. That distinct dominant integral weights have distinct central characters, which would make the two decompositions coincide, is the Harish-Chandra orbit theorem and is not proved here.

Main results

• TauCeti.IsHighestWeightVector.lieSpan_le_centerEigenspace: the submodule generated by a highest weight vector of weight lam lies in the centre eigenspace of chi_lam.
• TauCeti.centerEigenspace_irreducibleQuotient_eq_top: the centre acts on L(lam) by chi_lam.
• TauCeti.isotypicComponent_irreducibleQuotient_le_centerEigenspace: the centre acts on the L(lam)-isotypic component of any module by chi_lam.
• TauCeti.iSup_centerEigenspace_vermaCentralCharacter_eq_top: a finite-dimensional module is spanned by the centre eigenspaces of the central characters of dominant integral weights.
• TauCeti.isInternal_centerEigenspace: a finite-dimensional module is the internal direct sum of its centre eigenspaces.
• TauCeti.exists_isDominantIntegral_eq_vermaCentralCharacter: every eigenvalue function with a nonzero centre eigenspace in a finite-dimensional module is the central character of a dominant integral weight.

References

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

theorem TauCeti.IsHighestWeightVector.lieSpan_le_centerEigenspace {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] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.IsTriangularizable K (↥H) L] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} (hv : IsHighestWeightVector b lam v) : LieSubmodule.lieSpan K L {v} ≤ UniversalEnvelopingAlgebra.centerEigenspace K L M ⇑(vermaCentralCharacter b lam)

The submodule generated by a highest weight vector of weight lam lies in the centre eigenspace of the central character chi_lam.

@[simp]

theorem TauCeti.centerEigenspace_irreducibleQuotient_eq_top {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) : UniversalEnvelopingAlgebra.centerEigenspace K L (irreducibleQuotient b lam) ⇑(vermaCentralCharacter b lam) = ⊤

The centre of U(L) acts on L(lam) by the central character chi_lam.

theorem TauCeti.le_centerEigenspace_of_nonempty_lieModuleEquiv {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] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.IsTriangularizable K (↥H) L] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {P : LieSubmodule K L M} (e : Nonempty (↥P ≃ₗ⁅K,L⁆ irreducibleQuotient b lam)) : P ≤ UniversalEnvelopingAlgebra.centerEigenspace K L M ⇑(vermaCentralCharacter b lam)

A Lie submodule equivalent to L(lam) lies in the centre eigenspace of chi_lam.

theorem TauCeti.isotypicComponent_irreducibleQuotient_le_centerEigenspace {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] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.IsTriangularizable K (↥H) L] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} : LieModule.isotypicComponent K L M (irreducibleQuotient b lam) ≤ UniversalEnvelopingAlgebra.centerEigenspace K L M ⇑(vermaCentralCharacter b lam)

The centre of U(L) acts on the L(lam)-isotypic component of any module by the central character chi_lam: the isotypic component lies in the centre eigenspace of chi_lam.

theorem TauCeti.disjoint_isotypicComponent_irreducibleQuotient_of_vermaCentralCharacter_ne {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] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [LieModule.IsTriangularizable K (↥H) L] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam mu : Module.Dual K ↥H} (h : vermaCentralCharacter b lam ≠ vermaCentralCharacter b mu) : Disjoint (LieModule.isotypicComponent K L M (irreducibleQuotient b lam)) (LieModule.isotypicComponent K L M (irreducibleQuotient b mu))

Isotypic components with distinct central characters are disjoint.

theorem TauCeti.iSup_centerEigenspace_vermaCentralCharacter_eq_top {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] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [IsAlgClosed K] [FiniteDimensional K M] (b : (LieAlgebra.IsKilling.rootSystem H).Base) : ⨆ (lam : { l : Module.Dual K ↥H // IsDominantIntegral b l }), UniversalEnvelopingAlgebra.centerEigenspace K L M ⇑(vermaCentralCharacter b ↑lam) = ⊤

A finite-dimensional module is spanned by the centre eigenspaces of the central characters of dominant integral weights. By Weyl's theorem the module is a sum of irreducible submodules, each a copy of some L(lam) with lam dominant integral, on which the centre acts by chi_lam.

theorem TauCeti.isInternal_centerEigenspace {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (M : Type w) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [IsAlgClosed K] [FiniteDimensional K M] : DirectSum.IsInternal fun (χ : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L)) → K) => ↑(UniversalEnvelopingAlgebra.centerEigenspace K L M χ)

The centre of U(L) acts semisimply on a finite-dimensional module: the module is the internal direct sum of its centre eigenspaces.

theorem TauCeti.exists_isDominantIntegral_eq_vermaCentralCharacter {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] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [IsAlgClosed K] [FiniteDimensional K M] (b : (LieAlgebra.IsKilling.rootSystem H).Base) {χ : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L)) → K} (h : UniversalEnvelopingAlgebra.centerEigenspace K L M χ ≠ ⊥) : ∃ (lam : Module.Dual K ↥H), IsDominantIntegral b lam ∧ χ = ⇑(vermaCentralCharacter b lam)

The only eigenvalue functions of the centre on a finite-dimensional module are the central characters of dominant integral weights: a nonzero centre eigenspace belongs to chi_lam for a dominant integral weight lam.