The Casimir operator of an sl₂ triple #
For an sl₂ triple t : IsSl2Triple h e f in a Lie algebra L over a field K in which 2 is
nonzero, and an L-module M, the Casimir operator is the second-order operator
Ω = e f + f e + h² / 2
built from the action of the three elements of the triple on M. It is not the image of an element
of L; it is a quadratic expression in the action, and its point is that it commutes with the
whole action. The commutation is a short calculation from the relations ⁅e, f⁆ = h,
⁅h, e⁆ = 2e, ⁅h, f⁆ = -2f alone, so — unlike the Casimir element of a general semisimple Lie
algebra — it needs neither the universal enveloping algebra nor the Killing form, and is available
at this, the bottom, layer of the theory.
On a primitive vector of weight n the operator acts by the scalar n (n + 2) / 2
(TauCeti.sl2Casimir_apply_of_hasPrimitiveVectorWith), which vanishes exactly when n = 0, that is
exactly on the trivial module V(0). That dichotomy is the whole content of the operator:
TauCeti.sl2Casimir_injective turns it into the statement that on an irreducible module on which
L acts at all, the Casimir operator is injective.
Main definitions #
TauCeti.sl2Casimir: the Casimir operatore f + f e + h² / 2of a triple, as an endomorphism of a module.TauCeti.sl2CasimirHom: the Casimir operator as a morphism ofL-modules, available once the triple generatesL, so that its kernel is a Lie submodule.
Main results #
TauCeti.lie_sl2Casimir: the Casimir operator commutes with the action of every element of the subalgebra generated by the triple.TauCeti.sl2Casimir_apply_of_hasPrimitiveVectorWith: the Casimir operator acts on a primitive vector of weightnby the scalarn (n + 2) / 2.TauCeti.sl2Casimir_injective: the Casimir operator of a nontrivial irreducible module is injective.
Implementation notes #
Neither definition is exposed: TauCeti.sl2Casimir_apply and TauCeti.sl2CasimirHom_apply
characterise both completely, so nothing downstream needs to unfold further. Those two equations
are proved by the parenthesised (rfl), which elaborates against the definitions themselves; a
bare rfl in an exported theorem would demand that they be @[expose]d.
References #
This is Layer 0 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.
The operator #
The Casimir operator e f + f e + h² / 2 of a triple (h, e, f), acting on an L-module
M through the action of the three elements of the triple.
The formula makes sense over any field. The operator is worth naming only for an sl₂ triple,
where TauCeti.lie_sl2Casimir says it commutes with the action of the subalgebra the triple
generates; its coefficient 1 / 2 on h² is forced by that commutation, which is why the
commutation results — and not this definition — ask that 2 be nonzero.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Casimir operator is unchanged by the symmetry (h, e, f) ↦ (-h, f, e) of an sl₂ triple,
which merely exchanges the two off-diagonal terms and squares the sign on h.
The Casimir operator of a Lie submodule is the restriction of the Casimir operator of the ambient module: both are built from the same brackets.
Commutation with the action #
The Casimir operator commutes with the action of the Cartan element h. Each of the three
terms is separately preserved: h raises the weight by 2 on passing e and lowers it by 2 on
passing f, and each term of e f + f e + h²/2 pairs a raising with a lowering step.
The Casimir operator commutes with the action of the raising element e. This is the
calculation that fixes the coefficient 1 / 2 on h²: moving e past e f + f e produces
⁅e, ⁅h, m⁆⁆ + ⁅h, ⁅e, m⁆⁆, and moving it past h² / 2 produces exactly the negative of that.
The Casimir operator commutes with the action of the lowering element f, by the symmetry
TauCeti.sl2Casimir_neg_swap of the operator under (h, e, f) ↦ (-h, f, e).
The Casimir operator commutes with the action. Every element of the subalgebra generated by the triple commutes with the Casimir operator, since the three generators do and the statement is linear in the element.
The Casimir operator as a morphism of modules #
The Casimir operator as a morphism of L-modules, for a Lie algebra L generated by the
triple. Bundling it this way makes its kernel a Lie submodule, which is what lets
TauCeti.sl2Casimir_injective play irreducibility against it. Over an ambient L that the triple
does not generate the operator is still t.toLieSubalgebra K-equivariant, by
TauCeti.lie_sl2Casimir, but no more.
Equations
- TauCeti.sl2CasimirHom t htop M = { toLinearMap := TauCeti.sl2Casimir K h e f M, map_lie' := ⋯ }
Instances For
The Casimir scalar of a highest weight vector #
The Casimir scalar of a highest weight vector. A primitive vector of weight n is an
eigenvector of the Casimir operator with eigenvalue n (n + 2) / 2: the raising operator kills it,
so f e contributes nothing, e f contributes ⁅h, m⁆ = n m, and h² contributes n² m.
The Casimir scalar n (n + 2) / 2 determines the natural number n: the scalar is
((n + 1)² - 1)/2 and n + 1 is positive.
Injectivity on a nontrivial irreducible #
A highest weight vector of weight zero of an irreducible module is invariant, so the module
is trivial. The weight string of such a vector stops at once, so all three generators of L kill
it; its invariants are therefore a nonzero Lie submodule, hence everything.
The Casimir operator of a nontrivial irreducible module is injective. An irreducible module
has a primitive vector of some weight n : ℕ, on which the Casimir operator acts by
n (n + 2) / 2. If n = 0 the module is trivial, which is excluded; otherwise that scalar is
nonzero, so the kernel of the Casimir operator is a proper Lie submodule, hence zero.