The Casimir element of a universal enveloping algebra

Let L be a finite-dimensional Lie algebra over a field K whose Killing form κ is nondegenerate. Choosing a basis x₁, …, xₙ of L and the basis y₁, …, yₙ dual to it under κ, the Casimir element is

Ω = ∑ᵢ xᵢ yᵢ ∈ U(L),

a distinguished element of the universal enveloping algebra. In the classical setting of a split semisimple Lie algebra in characteristic zero it is the source of Weyl's complete reducibility theorem: it is central, so it acts on any module by a module endomorphism, and on a highest weight module by a scalar that separates the trivial module from the others. Those extra hypotheses are needed only for that application; centrality, the statement proved here, needs nothing beyond a nondegenerate Killing form.

Two facts make Ω an invariant of L rather than of the chosen basis. They are developed in Ado.Algebra.Lie.Killing.DualBasis and applied here.

• Ω does not depend on the basis. The mechanism is Ado.sum_apply_killingDualBasis_eq: for every K-bilinear map f out of L × L, the value ∑ᵢ f xᵢ yᵢ is the same for all bases, because expanding one basis in the other exchanges the two dual bases. The Casimir element is the instance f x y = x * y in U(L), so Ado.casimirElement_eq_sum computes it from any basis at all, and the chosen basis in the definition is immaterial.
• Ω is central (Ado.casimirElement_mem_center). The same bilinear mechanism gives Ado.sum_apply_lie_killingDualBasis_add_eq_zero, the statement that the element ∑ᵢ xᵢ ⊗ yᵢ is annihilated by the adjoint action of L; this is exactly the invariance κ ⁅z, x⁆ y = -κ x ⁅z, y⁆ of the Killing form, summed. Feeding it the commutator identity ι z * ι x - ι x * ι z = ι ⁅z, x⁆ turns it into ι z * Ω = Ω * ι z, and the canonical Lie generators generate U(L) (Ado.UniversalEnvelopingAlgebra.adjoin_range_ι), so Ω commutes with everything.

Only nondegeneracy, symmetry and invariance of the Killing form are used, so the argument below would go through for any invariant nondegenerate symmetric form once the definitions and lemmas are parameterised by such a form; as written they are stated for the Killing form, which is the canonical choice this development needs and the one the roadmap pins.

Main definitions

• Ado.casimirElement: the Casimir element of U(L).

Main results

• Ado.sum_killingForm_killingDualBasis_eq_trace: the sum ∑ᵢ κ (p xᵢ) yᵢ is the trace of the endomorphism p.
• Ado.sum_apply_killingDualBasis_of_isAdjointPair: a pair of endomorphisms adjoint for the Killing form may be moved from the first slot of f to the second.
• Ado.casimirElement_eq_sum: the Casimir element is ∑ᵢ xᵢ yᵢ for any basis x of L and its Killing-dual basis y, so the basis chosen in the definition does not matter.
• Ado.representation_casimirElement_apply_eq_zero_of_isTrivial: the Casimir element acts by zero on a module with trivial Lie action.
• Ado.ι_mul_casimirElement: the Casimir element commutes with every canonical Lie generator.
• Ado.representation_casimirElement_lie: the Casimir operator of a module commutes with the Lie action.
• Ado.map_representation_casimirElement: a homomorphism of Lie modules intertwines the Casimir operators.
• Ado.casimirElement_mem_center: the Casimir element is central in U(L).

The remaining statement about casimirElement, that it acts on a highest weight module of weight λ by the scalar ⟨λ + ρ, λ + ρ⟩ - ⟨ρ, ρ⟩, is not proved here but in TauCeti/Algebra/Lie/HighestWeight/Casimir.lean, which is where the highest weight vectors and the invariant form on weights that it is phrased in are available.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 1--3, Chapter I, §3, no. 7 ("Casimir element"), Proposition 11: given an invariant bilinear form whose restriction to an ideal a is nondegenerate, the element c = Σᵢ eᵢ eᵢ' built from a basis of a and the dual basis of a is independent of that basis and commutes with the whole Lie algebra. Taking a to be all of L and the form to be the Killing form gives the two statements proved here; Bourbaki is strictly more general, since the form may be degenerate on L and the sum then runs over a basis of the proper ideal a, which is beyond the generality noted above.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §6.2, which builds the Casimir element of the trace form of a faithful representation of a semisimple Lie algebra; the Killing form is the case of the adjoint representation.
• Highest weight roadmap, Layer 5, "The Casimir element".

The Casimir element

noncomputable def Ado.casimirElement (K : Type u) (L : Type v) [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] : UniversalEnvelopingAlgebra K L

The Casimir element Ω = ∑ᵢ xᵢ yᵢ ∈ U(L) of a Lie algebra with nondegenerate Killing form, built from a basis x of L and the basis y dual to it under the Killing form.

The definition names a particular basis, but the element does not depend on it: Ado.casimirElement_eq_sum evaluates Ω against an arbitrary basis.

Equations

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

theorem Ado.casimirElement_eq_sum {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {ι' : Type u_1} [DecidableEq ι'] [Fintype ι'] (b : Module.Basis ι' K L) : casimirElement K L = ∑ i : ι', (UniversalEnvelopingAlgebra.ι K) (b i) * (UniversalEnvelopingAlgebra.ι K) ((killingDualBasis b) i)

The Casimir element is ∑ᵢ xᵢ yᵢ for every basis x of L and its Killing-dual basis y, so the basis chosen in the definition is immaterial.

@[simp]

theorem Ado.representation_casimirElement_apply_eq_zero_of_isTrivial {K : Type u} {L : Type v} [Field 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] [LieModule.IsTrivial L M] (m : M) : ((UniversalEnvelopingAlgebra.representation K L M) (casimirElement K L)) m = 0

The Casimir element acts by zero on a module with trivial action. Every summand xᵢ yᵢ of Ω acts by a double bracket, and brackets vanish.

theorem Ado.ι_mul_casimirElement {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] (z : L) : (UniversalEnvelopingAlgebra.ι K) z * casimirElement K L = casimirElement K L * (UniversalEnvelopingAlgebra.ι K) z

The Casimir element commutes with every canonical Lie generator. Expanding the commutator of ι z with each summand xᵢ yᵢ by the Leibniz rule replaces the bracket by the adjoint action on ∑ᵢ xᵢ ⊗ yᵢ, which vanishes.

theorem Ado.casimirElement_mem_center (K : Type u) (L : Type v) [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] : casimirElement K L ∈ Subalgebra.center K (UniversalEnvelopingAlgebra K L)

The Casimir element is central in U(L). It commutes with the canonical Lie generators, which generate U(L) as an algebra.

@[simp]

theorem Ado.representation_casimirElement_lie {K : Type u} {L : Type v} [Field 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] (x : L) (m : M) : ((UniversalEnvelopingAlgebra.representation K L M) (casimirElement K L)) ⁅x, m⁆ = ⁅x, ((UniversalEnvelopingAlgebra.representation K L M) (casimirElement K L)) m⁆

The Casimir element commutes with the Lie action. This is the centrality of the Casimir element, read on a module: the Casimir operator of a module is a homomorphism of Lie modules.

theorem Ado.map_representation_casimirElement {K : Type u} {L : Type v} [Field 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] {N : Type u_1} [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] (f : M →ₗ⁅K,L⁆ N) (m : M) : f (((UniversalEnvelopingAlgebra.representation K L M) (casimirElement K L)) m) = ((UniversalEnvelopingAlgebra.representation K L N) (casimirElement K L)) (f m)

The Casimir operator is natural in the module. A homomorphism of Lie modules intertwines the two Casimir operators, being equivariant for the whole enveloping algebra. This is Ado.UniversalEnvelopingAlgebra.map_representation, which carries the simp attribute, at the Casimir element.