The invariant form on the weights of a Killing Lie algebra #
Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field K of
characteristic zero and let H be a splitting Cartan subalgebra. The Killing form restricts to a
non-degenerate form on H, which Mathlib packages as the linear equivalence
LieAlgebra.IsKilling.cartanEquivDual : H ≃ₗ[K] Module.Dual K H. Transporting the form along that
equivalence puts a symmetric non-degenerate bilinear form ⟨·,·⟩ on the space of weights
Module.Dual K H. This file builds that form as Ado.invForm and proves the two facts that
make it the right object: it is invariant under the reflections of the root system
(Ado.rootInvariantForm), and it is normalised against the coroots by
⟨λ, α^∨⟩ ⟨α, α⟩ = 2 ⟨λ, α⟩,
that is, α^∨ is the weight 2α / ⟨α, α⟩ (Ado.invForm_coroot).
That normalisation is what makes the form usable. The Cartan integers of
LieAlgebra.IsKilling.rootSystem are the numbers λ(α^∨), whereas the Casimir scalar and the Weyl
character and dimension formulas are written with ⟨·,·⟩; the identity above is the dictionary
between the two, and it is what makes an expression such as ⟨λ + ρ, λ + ρ⟩ - ⟨ρ, ρ⟩ agree with
the coroot pairings. So the form has to be pinned, with this normalisation proved, before any of
that can be stated.
Main definitions #
Ado.invForm: the symmetric bilinear form⟨·,·⟩onModule.Dual K Hinduced by the Killing form throughLieAlgebra.IsKilling.cartanEquivDual.Ado.rootInvariantForm:invFormpackaged as an invariant form on the root systemLieAlgebra.IsKilling.rootSystem H, which makes Mathlib'sRootPairing.InvariantFormAPI available for it.Ado.killingExtend: a weight, extended to a linear form onLby pairing with the vector that represents it under the Killing form.
Main results #
Ado.invForm_isSymmandAdo.invForm_nondegenerate: the form is symmetric and non-degenerate.Ado.invForm_apply_apply_eq_traceForm: the form is the transport of the Killing form.Ado.invForm_self_sub_invForm_self:⟨a, a⟩ - ⟨b, b⟩ = ⟨a + b, a - b⟩.Ado.invForm_cartanEquivDual_rightandAdo.invForm_cartanEquivDual_left: pairing a weight against one of the shapecartanEquivDual H xevaluates the other weight atx.Ado.cartanEquivDual_coroot: the corootα^∨is the weight2α / ⟨α, α⟩, read throughcartanEquivDual.Ado.invForm_corootandAdo.invForm_coroot_weight: the normalisation⟨λ, α^∨⟩ ⟨α, α⟩ = 2 ⟨λ, α⟩.Ado.traceForm_coroot_self_mul_invForm_self_eq_four:⟨α^∨, α^∨⟩ ⟨α, α⟩ = 4, so a long root has a short coroot.Ado.killingExtend_apply_cartanandAdo.killingExtend_apply_eq_zero: the extension of a weight is the weight itself onHand vanishes on every root space of a nonzero weight, so it sees the zero-weight component of a vector and nothing else.
The compatibility with LieAlgebra.IsKilling.rootSystem_pairing_apply — that a Cartan integer is
2 ⟨α, β⟩ / ⟨β, β⟩ — and the orthogonality criterion and reflection invariance of the form are not
restated here: Ado.rootInvariantForm makes them
RootPairing.InvariantForm.two_mul_apply_root_root,
RootPairing.InvariantForm.apply_root_root_zero_iff and
RootPairing.InvariantForm.apply_reflection_reflection.
Implementation notes #
invForm is bundled as a LinearMap.BilinForm, so that invForm a b still reads as the value of
the form at a pair of weights while the bilinearity is available as data; the latter is what
RootPairing.InvariantForm asks for.
The definition is Mathlib's transport combinator LinearMap.BilinForm.congr applied to
cartanEquivDual, and Ado.invForm_apply_apply_eq_traceForm is the resulting bridge back to
the restricted Killing form. The unfolding lemma Ado.invForm_apply_apply reads the form as a
dual pairing instead, because Mathlib's LieAlgebra.IsKilling.coroot is defined that way: keeping
the two on the same side of the equivalence is what makes Ado.cartanEquivDual_coroot, and
with it the normalisation, a computation rather than a transport argument.
The simp-normal form keeps invForm folded: Ado.invForm_apply_apply is not a simp lemma,
and it is the eliminators Ado.invForm_cartanEquivDual_left and
Ado.invForm_cartanEquivDual_right that carry @[simp]. That way simp normalises towards
the form rather than away from it, and the RootPairing.InvariantForm lemmas that
Ado.rootInvariantForm buys can still fire.
Only from Ado.invForm_self_ne_zero on do the results need the root-theory instances
CharZero K and IsTriangularizable K H L, so the general theory of the form is stated first
without them. The split is by typeclass, not by root-ness: Ado.invForm_coroot_weight still
takes an arbitrary weight.
References #
This file builds the invariant form on weights of Layer 5 of
TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md ("the induced symmetric bilinear
form on Module.Dual K H, transported from the Killing form on H via cartanEquivDual", with
"its normalization against coroots, ⟨λ, α^∨⟩ ⟨α, α⟩ = 2 ⟨λ, α⟩" and "its compatibility with
rootSystem_pairing_apply and IsKilling.coroot"), the prerequisite that roadmap asks for before
the Casimir element. The material is J. E. Humphreys, Introduction to Lie Algebras and
Representation Theory, GTM 9, §8.2-8.5.
The form #
The symmetric bilinear form ⟨·,·⟩ on the space of weights Module.Dual K H induced by the
Killing form of L through LieAlgebra.IsKilling.cartanEquivDual.
This is the form in which the Casimir scalar and the Weyl character and dimension formulas are
written; Ado.invForm_coroot is its normalisation against the coroots.
Equations
Instances For
The form is the transport of the restricted Killing form along cartanEquivDual.
The form read as a dual pairing: cartanEquivDual is the Killing form, so the transport of
that form pairs a with the vector representing b.
Pairing a weight against one of the shape cartanEquivDual H x is evaluation at x. This is
the shape of the transport used most often, because it mentions no inverse equivalence.
The form is symmetric, inheriting the symmetry of the Killing form.
A difference of squared lengths factors as ⟨a, a⟩ - ⟨b, b⟩ = ⟨a + b, a - b⟩, by the
symmetry of the form.
Pairing a weight of the shape cartanEquivDual H x on the left evaluates the other weight at
x; the left-hand companion of Ado.invForm_cartanEquivDual_right.
The form is non-degenerate, inheriting the non-degeneracy of the Killing form on H.
The coroot as a weight: α^∨ = 2α / ⟨α, α⟩, read through cartanEquivDual. This says that
LieAlgebra.IsKilling.coroot is the coroot of the invariant form, and every compatibility below
is a consequence of it.
No hypothesis on α is needed: at a zero weight both sides vanish.
A weight, extended to the Lie algebra #
A weight, extended to a linear form on L by pairing with the vector that represents it
under the Killing form. It agrees with the weight on H
(Ado.killingExtend_apply_cartan) and vanishes on every root space of a nonzero weight
(Ado.killingExtend_apply_eq_zero), so it sees the zero-weight component of a vector and
nothing else.
Equations
- Ado.killingExtend lam = (killingForm K L) ↑((LieAlgebra.IsKilling.cartanEquivDual H).symm lam)
Instances For
The defining formula of the extension: pairing with the vector that represents the weight.
On the Cartan subalgebra the extension is the weight itself.
The extension of a weight vanishes on the root space of a nonzero weight, the Cartan subalgebra being the zero root space.
Roots and coroots #
A root has non-zero length for the form.
The normalisation of the invariant form against the coroots: ⟨λ, α^∨⟩ ⟨α, α⟩ = 2 ⟨λ, α⟩,
that is, α^∨ is the weight 2α / ⟨α, α⟩.
Like Ado.cartanEquivDual_coroot, this needs no hypothesis on α: at a zero weight both
sides vanish.
The normalisation of the invariant form against the coroots, indexed by the roots of
LieAlgebra.IsKilling.rootSystem: ⟨λ, α^∨⟩ ⟨α, α⟩ = 2 ⟨λ, α⟩.
The invariant form of the root system #
Ado.invForm as an invariant form on LieAlgebra.IsKilling.rootSystem H.
Equations
- Ado.rootInvariantForm = { form := Ado.invForm, symm := ⋯, ne_zero := ⋯, isOrthogonal_reflection := ⋯ }
Instances For
The length of a coroot: ⟨α^∨, α^∨⟩ ⟨α, α⟩ = 4, so a long root has a short coroot.
The length ⟨α^∨, α^∨⟩ of the coroot is spelled as the Killing form of α^∨ with itself rather
than as invForm (cartanEquivDual H (coroot α)) (cartanEquivDual H (coroot α)): the eliminator
Ado.invForm_cartanEquivDual_right is a simp lemma, so the latter shape does not survive a
simp call.