Root vectors normalised against the coroots #
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. Each root α has a
one-dimensional root space Lα, so a root vector is determined by a scalar, and Mathlib's
LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero produces one root vector at a time:
for a single root α there are e ∈ Lα and f ∈ L₍₋α₎ with ⁅e, f⁆ = α^∨.
Chevalley's construction needs those choices made simultaneously and compatibly, for all roots
at once: a family x : Weight K H L → L with x α ∈ Lα and
⁅x α, x (-α)⁆ = α^∨ for every root α.
This file defines that condition as TauCeti.IsSl2System — the name records what it says, that
(α^∨, x α, x (-α)) is an sl₂ triple for every root — and proves that such a family exists.
Choosing the root vectors one root at a time does not give a system: the vector chosen for -α and
the partner of the vector chosen for α are two elements of the same line, and they need not agree.
The construction below therefore chooses one root out of each pair {α, -α} and reads off the
vector at the other root from the triple already chosen, which is possible because α ↦ -α is a
fixed-point-free involution on the roots. That selection is
TauCeti.exists_rootPairRepresentatives, stated separately because every later rescaling of a
normalised family has to make the same choice. The resulting family satisfies the normalisation
on the nose, in both directions, because an sl₂ triple stays one when e and f are exchanged
and h is negated, and (-α)^∨ = -α^∨.
Beyond the definition and the existence theorem, the file records what a system gives: the sl₂
triple at each root, the resulting nonvanishing and the identification of each root space as the
line it spans, the Cartan relation ⁅β^∨, x α⁆ = α(β^∨) • x α, the grading ⁅x α, x β⁆ ∈ L₍α+β₎
with its vanishing when α + β is not a root, that the root vectors together with H span L,
the Killing pairing of opposite normalized root vectors, and that two systems differ by scalars
c α subject to c α * c (-α) = 1.
What this is not #
An IsSl2System is not yet a Chevalley basis, and this file does not claim it is. A Chevalley basis
asks in addition that the structure constants c α β in ⁅x α, x β⁆ = c α β • x (α + β) be the
integers ±(p + 1), p the root-string parameter, and Bourbaki's Chevalley system asks moreover
that the family be exchanged with its negatives by the Chevalley involution. Neither condition is
imposed here: the normalisation ⁅x α, x (-α)⁆ = α^∨ alone is what pins the Cartan part of the
would-be integral form, and it is a prerequisite of both, since the structure constants are only
defined once the root vectors are.
Main definitions #
TauCeti.IsSl2System: a family of root vectors, one for each weight, normalised so that⁅x α, x (-α)⁆ = α^∨at every root and carrying no data at a zero weight.
Main results #
TauCeti.Weight.ne_neg_of_isNonZero: negation fixes no root.TauCeti.exists_rootPairRepresentatives: a set of weights containing exactly one ofαand-αfor every rootα.TauCeti.exists_isSl2System: such a family exists.TauCeti.IsSl2System.isSl2Triple:(α^∨, x α, x (-α))is ansl₂triple.TauCeti.IsSl2System.toSubmodule_rootSpace_eq_span:x αspans the root space ofα.TauCeti.IsSl2System.killingForm_root_neg_eq: the Killing pairing of opposite normalized root vectors is2 / α((cartanEquivDual H)⁻¹ α).TauCeti.IsSl2System.lie_coroot: the Cartan relation.TauCeti.IsSl2System.isNilpotent_ad_rootVector: every member of the family acts nilpotently in the adjoint representation.TauCeti.IsSl2System.lie_mem_rootSpace_addandTauCeti.IsSl2System.lie_eq_zero_of_rootSpace_add_eq_bot: the root grading of the bracket.TauCeti.IsSl2System.exists_lie_eq_smul_of_coe_eq_add: the structure constants exist.TauCeti.IsSl2System.span_range_sup_toSubmodule_eq_top: the root vectors andHspanL.TauCeti.IsSl2System.eq_of_forall_isNonZero: a system is determined by its root vectors.TauCeti.IsSl2System.mul_eq_one_of_eq_smul: two systems differ by scalarscwithc α * c (-α) = 1.TauCeti.IsSl2System.smul: rescaling by scalars inverse on opposite roots preserves a normalised system.
References #
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §25.2.
- N. Bourbaki, Lie Groups and Lie Algebras, Chapter VIII, §2, no. 4.
A family of root vectors normalised against the coroots: x α lies in the root space of α,
and ⁅x α, x (-α)⁆ is the coroot α^∨ for every root α. Equivalently, (α^∨, x α, x (-α)) is
an sl₂ triple for every root α, whence the name.
Only the roots carry data: the value at a zero weight is pinned to 0, so that a system is
determined by its root vectors, as TauCeti.IsSl2System.eq_of_forall_isNonZero records.
Each member of the family is a root vector for its own root.
- lie_neg (α : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) : ⁅x α, x (-α)⁆ = ↑(LieAlgebra.IsKilling.coroot α)
The members at
αand-αare normalised so that their bracket is the coroot ofα. The family carries no data at a zero weight.
Instances For
The Cartan relation: a coroot acts on a root vector by the corresponding Cartan number.
The sl₂ triple attached to a root by a normalised family of root vectors.
A root vector of a normalised family is nonzero, being the e of an sl₂ triple.
Every member of a normalised root-vector system acts nilpotently in the adjoint
representation. At a root this is the nilpotency of ad on a root space; at a zero weight the
member is 0. This is the nilpotency hypothesis for divided-power exponentials; lattice stability
supplies their integrality separately.
The Killing pairing of opposite vectors in a normalised root-vector system is
2 / α((cartanEquivDual H)⁻¹ α).
A root vector of a normalised family spans its root space.
The root grading: the bracket of two root vectors lies in the root space of the sum.
Two root vectors bracket to zero when the sum of their roots is not itself a root.
The structure constants of a normalised family: when the sum of two roots is again a root, the
bracket of the two root vectors is a multiple of the root vector at the sum. The normalisation says
nothing about the constants themselves; pinning them to the integers ±(p + 1) is exactly what
upgrades a normalised family to a Chevalley basis.
The root vectors of a normalised family span L over the Cartan subalgebra: together with H
they span the whole Lie algebra.
A normalised family is determined by its root vectors: two systems agreeing at every root agree everywhere, since both vanish at a zero weight.
Two normalised families differ by a scalar at each root, since the root spaces are lines.
The scalars relating two normalised families are inverse to one another at α and -α: this
is the one constraint the normalisation ⁅x α, x (-α)⁆ = α^∨ imposes on those scalars.
Rescaling a normalised family by scalars inverse on opposite roots preserves its normalisation.
A root is not its own negative. Evaluating at the coroot separates the two: a root takes
the value 2 there, and its negative the value -2.
One root out of each opposite pair. There is a set of weights containing, for every root
α, exactly one of α and -α.
Negation is a fixed-point-free involution on the roots by
TauCeti.Weight.ne_neg_of_isNonZero, so a set of representatives for the equivalence relation it
generates is such a set. The choice is what a
construction has to make whenever it treats α and -α asymmetrically, as the normalisation
⁅x α, x (-α)⁆ = α^∨ and the rescalings preserving it both force it to.
Existence of a normalised family of root vectors. Root vectors can be chosen for all roots
at once so that ⁅x α, x (-α)⁆ = α^∨ holds at every root, and not merely one root at a time.
The construction picks one root from each pair {α, -α}, takes the sl₂ triple Mathlib attaches
to it, assigns e to the chosen root and f to its negative, and 0 to a zero weight.