The central character of a highest weight module

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field K of characteristic zero, let H be a splitting Cartan subalgebra and b a base of its root system. The centre Z(U(L)) = Subalgebra.center K (UniversalEnvelopingAlgebra K L) of the enveloping algebra acts on a highest weight module of weight lam by scalars, and this file builds the resulting K-algebra homomorphism

chi_lam : Z(U(L)) →ₐ[K] K,

the central character of lam.

Why the scalar exists

A central z commutes with the whole Lie action (TauCeti.UniversalEnvelopingAlgebra.representation_lie_of_mem_center), so it carries a highest weight vector v of weight lam into the lam-weight space: the Cartan subalgebra still acts on z · v through lam. On a highest weight module — one generated by v — that weight space is the line K ∙ v (TauCeti.genWeightSpace_eq_span_singleton_of_isHighestWeightVector_of_lieSpan_eq_top), so z · v = c • v for a unique c, and centrality propagates the identity from the generator to the whole module (TauCeti.UniversalEnvelopingAlgebra.representation_eq_smul_of_mem_center_of_lieSpan_eq_top). Nothing here needs v to generate an irreducible module, and nothing needs finite dimensionality: Schur's lemma is not the mechanism, the one-dimensionality of the top weight space is.

The character of a weight, not of a module

The construction above takes a highest weight module as input. It does not depend on it, so the character is attached to the weight alone: the Verma module M(lam) maps onto any module carrying a highest weight vector of weight lam, by its universal property (TauCeti.existsUnique_lieModuleHom_apply_vermaGenerator), and a homomorphism of Lie modules intertwines the two enveloping-algebra actions (TauCeti.UniversalEnvelopingAlgebra.map_representation), so the scalar is the one read off M(lam). That is TauCeti.IsHighestWeightVector.representation_eq_vermaCentralCharacter_smul, and it makes TauCeti.vermaCentralCharacter the central character of the weight lam. The vector is not assumed to generate its module there: any highest weight vector of weight lam, anywhere, is an eigenvector of the centre with eigenvalue chi_lam. In particular the irreducible quotient L(lam) has the central character of lam, being a highest weight module of that weight (TauCeti.isHighestWeightVector_irreducibleQuotientGenerator).

Main definitions

• TauCeti.vermaCentralCharacter: the central character chi_lam of the weight lam, a K-algebra homomorphism Z(U(L)) →ₐ[K] K.

Main results

• TauCeti.IsHighestWeightVector.representation_eq_vermaCentralCharacter_smul: the defining property, on any highest weight vector of weight lam in any module, and TauCeti.IsHighestWeightVector.representation_eq_vermaCentralCharacter_smul_of_lieSpan_eq_top, on the whole module when that vector generates it.
• TauCeti.IsHighestWeightVector.vermaCentralCharacter_eq_of_representation_eq_smul: the central character is the only scalar with that property, which is how its values are computed.
• TauCeti.vermaCentralCharacter_casimirElement: the central character sends the Casimir element to the Casimir scalar ⟨lam + rho, lam + rho⟩ - ⟨rho, rho⟩ of Layer 5.

References

This is the "central characters" half of the first item of Layer 7 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, whose target signature centralCharacter is pinned in the accompanying Suggested.lean and whose text fixes the route used here: the character is defined through the action of the centre on the one-dimensional top weight line of the Verma module, and is then shown to be the character of every highest weight module of that weight, the Casimir eigenvalue of Layer 5 being its value at the Casimir element. The name TauCeti.centralCharacter is already taken by the central character of a simple module over an arbitrary algebra (TauCeti/RingTheory/Semisimple/CentralCharacter.lean), obtained from Schur's lemma. That construction is not available here: it assumes [IsAlgClosed K], [IsSimpleModule A M] and [FiniteDimensional K M], none of which is assumed in this file, and M(lam) is not known to be simple — simplicity of M(lam) is equivalent to antidominance of lam (Humphreys, BGG Category O, §4.8).

• 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.

A central element acts on a highest weight vector by a scalar

The central character

The central character of a weight

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

The central character chi_lam of a weight, read off the Verma module M(lam): the scalar by which a central element of U(L) acts on the canonical generator. By TauCeti.IsHighestWeightVector.representation_eq_vermaCentralCharacter_smul it is the scalar by which the centre acts on any highest weight vector of weight lam.

Equations

• TauCeti.vermaCentralCharacter b lam = TauCeti.centralCharacterAux✝ ⋯ ⋯

theorem TauCeti.IsHighestWeightVector.representation_eq_vermaCentralCharacter_smul {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] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} (hv : IsHighestWeightVector b lam v) (u : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L))) : ((UniversalEnvelopingAlgebra.representation K L M) ↑u) v = (vermaCentralCharacter b lam) u • v

The defining property of the central character: a central element of U(L) acts on any highest weight vector of weight lam, in any module, by chi_lam. The vector is not assumed to generate its module: the universal property of M(lam) maps the canonical generator to it, and a homomorphism of Lie modules intertwines the two actions of U(L).

theorem TauCeti.IsHighestWeightVector.vermaCentralCharacter_eq_of_representation_eq_smul {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] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} (hv : IsHighestWeightVector b lam v) {u : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L))} {c : K} (h : ((UniversalEnvelopingAlgebra.representation K L M) ↑u) v = c • v) : (vermaCentralCharacter b lam) u = c

The central character is the only scalar with the defining property, a highest weight vector being nonzero. This is how the values of the character are computed.

theorem TauCeti.IsHighestWeightVector.representation_eq_vermaCentralCharacter_smul_of_lieSpan_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] {M : Type w} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M} (hv : IsHighestWeightVector b lam v) (hgen : LieSubmodule.lieSpan K L {v} = ⊤) (u : ↥(Subalgebra.center K (UniversalEnvelopingAlgebra K L))) (m : M) : ((UniversalEnvelopingAlgebra.representation K L M) ↑u) m = (vermaCentralCharacter b lam) u • m

A central element acts on a whole highest weight module by the central character of its weight. Centrality makes the locus where it acts by that scalar a Lie submodule, and it contains the generator.

The Casimir element

@[simp]

theorem TauCeti.vermaCentralCharacter_casimirElement {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) : (vermaCentralCharacter b lam) ⟨casimirElement K L, ⋯⟩ = casimirScalar b lam

The central character sends the Casimir element to the Casimir scalar ⟨lam + rho, lam + rho⟩ - ⟨rho, rho⟩, so the eigenvalue computed in TauCeti/Algebra/Lie/HighestWeight/Casimir.lean is a value of the central character.