The four-term relation among root-vector structure constants #
Let x be a TauCeti.IsSl2System in a Lie algebra L with non-degenerate Killing form, so that
⁅x α, x β⁆ = N(α, β) x(α + β) whenever α + β is a root. This file proves the relation between
the structure constants of four roots summing to zero.
Write B for the Killing form. Pairing the brackets of root vectors in twos, rather than iterating
them, is what makes the Jacobi identity readable at the level of structure constants: if
α + β + γ + δ = 0 then ⁅x γ, x δ⁆ lies in the root space of -(α + β), so B ⁅x α, x β⁆ ⁅x γ, x δ⁆ is N(α, β) N(γ, δ) weighted by B (x μ) (x (-μ)) for μ = α + β, and it vanishes
outright when α + β is not a root. The cyclic identity
TauCeti.traceForm_lie_lie_cyclic_eq_zero therefore reads
N(α, β) N(γ, δ) B(x μ, x (-μ)) + N(β, γ) N(α, δ) B(x ν, x (-ν))
+ N(γ, α) N(β, δ) B(x ρ, x (-ρ)) = 0
for μ = α + β, ν = β + γ and ρ = γ + α. Since B (x μ) (x (-μ)) is 2 / ⟨μ, μ⟩ for the
invariant form TauCeti.invForm on weights, this is Carter's displayed relation
N(α, β) N(γ, δ) / ⟨γ + δ, γ + δ⟩ + N(β, γ) N(α, δ) / ⟨α + δ, α + δ⟩
+ N(γ, α) N(β, δ) / ⟨β + δ, β + δ⟩ = 0,
recorded here as TauCeti.IsSl2System.structureConstant_four_term_invForm, whose denominators
are those of μ, ν and ρ: they agree with Carter's because γ + δ = -(α + β) and the form is
even, and likewise in the other two summands.
A summand drops out when its pair of roots does not sum to a root, and the resulting shorter
relations are the ones Carter's recursion over extraspecial pairs actually runs on: with one
summand absent the other two are negatives of each other, and with two absent the remaining pair
cannot sum to a root at all, which
TauCeti.IsSl2System.rootSpace_add_eq_bot_of_rootSpace_add_eq_bot reads off as a statement about
the root system.
Nothing here normalises the structure constants: the relation holds for every normalised family,
and the choice of a family whose constants are the Chevalley integers ±(p + 1) is exactly what
it is an input to.
Main results #
TauCeti.IsSl2System.killingForm_lie_lie_eq_mul_mulandTauCeti.IsSl2System.killingForm_lie_lie_eq_zero_of_rootSpace_add_eq_bot: the evaluation of a paired Killing bracket, in the case where the first pair sums to a root and in the case where it does not.TauCeti.IsSl2System.structureConstant_four_term: the four-term relation.TauCeti.IsSl2System.structureConstant_four_term_of_rootSpace_add_eq_bot: its two-summand form when one of the three pairs does not sum to a root.TauCeti.IsSl2System.rootSpace_add_eq_bot_of_rootSpace_add_eq_bot: two absent summands force the third pair not to sum to a root either.TauCeti.IsSl2System.structureConstant_four_term_invForm: Carter's displayed form of the relation, with the root lengths of the invariant form as denominators.
References #
- R. W. Carter, Simple Groups of Lie Type, §4.1, Proposition 4.1.2.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §25.1.
Roadmap #
Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md builds the split reductive group scheme over
ℤ "via a Chevalley basis and the Kostant ℤ-form of the enveloping algebra", and
TauCeti.IsChevalleySystem is that Chevalley basis. Producing one reduces, by
TauCeti.IsSl2System.isChevalleyNormalized_iff_exists_isChevalleySystem, to normalising the
structure constants of some family to ±(p + 1), which Carter performs in §4.2 by a recursion over
the extraspecial pairs enumerated in TauCeti/LinearAlgebra/RootSystem/ExtraspecialPair.lean. The
relation proved here is the identity that recursion propagates. Milestone L0 of
TauCetiRoadmap/CFSGStatement/README.md is the downstream consumer of the assembled pinned group
scheme.
Evaluating a pair of brackets against the Killing form #
The Killing pairing of two brackets of root vectors, when the first pair sums to the root μ
and the second to its opposite. Both brackets are then multiples of opposite root vectors, so the
pairing is the product of the two structure constants weighted by the Killing pairing of that
opposite pair.
The Killing pairing of two brackets of root vectors vanishes when the first pair does not sum to a root, since the first bracket is then already zero.
The relation #
The four-term relation. Let α, β, γ, δ be weights whose sum is zero, and suppose
that μ = α + β, ν = β + γ and ρ = γ + α are roots, so that the six structure constants below
are defined. Then the three products, each weighted by the Killing pairing of the opposite pair of
root vectors it belongs to, sum to zero.
Requiring μ, ν and ρ to be roots already excludes the degenerate configurations in which two
of the four weights are opposite, since a Weight is a root exactly when it is non-zero.
The four-term relation when one of the three pairs does not sum to a root: the remaining two
summands are then negatives of one another. The pair left out is γ + α, which is the shape the
recursion of Carter's §4.2 uses, where one decomposition of a root is compared with another.
Two absent summands force the third pair not to sum to a root either. If four roots sum to
zero, if α + β is not itself zero, and if neither β + γ nor γ + α is a root, then α + β is
not a root.
This is a root-system statement, obtained from the relation because a structure constant of two
roots whose sum is a root is non-zero and the Killing pairing of an opposite pair of root vectors
is non-zero. The hypothesis α + β ≠ 0 cannot be dropped: for β = -α and δ = -γ the two
brackets are the coroots of α and γ, whose Killing pairing has no reason to vanish.
Carter's form, with the root lengths of the invariant form #
Carter's form of the four-term relation. The three products of structure constants, divided by the lengths of the roots their pairs sum to, add to zero.
This is TauCeti.IsSl2System.structureConstant_four_term after replacing each Killing pairing by
2 / ⟨μ, μ⟩ and cancelling the common factor 2. The lengths appearing here are those of
α + β, β + γ and γ + α; Carter writes the relation with the lengths of γ + δ, α + δ and
β + δ, which are the same because those weights are the negatives of these and the form is
even.