Opposite structure constants multiply to -(p + 1)²

Let x be an IsSl2System in a finite-dimensional Lie algebra with non-degenerate Killing form over a field of characteristic zero, so that ⁅x α, x (-α)⁆ = α∨, and let γ = α + β be a root. Writing

⁅x α, x β⁆ = N(α, β) x γ,

this file proves the identity

N(α, β) * N(-α, -β) = -(p + 1)²,      p = chainBotCoeff α β.

Nothing beyond the normalisation ⁅x α, x (-α)⁆ = α∨ is assumed: no Chevalley involution, and no integrality of the constants. The proof combines the root-string product formula, the cyclic Killing-form symmetry applied to the triple (γ, -α, β), and the invariant root-length ratio.

The identity is exactly the rescaling invariant of a normalised system. Replacing x by c α • x α with c α * c (-α) = 1 multiplies N(α, β) by c α * c β / c γ and N(-α, -β) by its inverse, so the product is the same for every normalised system, and the two constants determine each other. The consequence recorded here is that the Chevalley-involution symmetry N(-α, -β) = -N(α, β) holds precisely when N(α, β) is one of the Chevalley integers ±(p + 1). That equivalence turns the compatibility with a Chevalley involution, which is data, into a property of the structure constants alone.

Main results

• TauCeti.IsSl2System.structureConstant_mul_structureConstant_neg_neg: the product identity.
• TauCeti.IsSl2System.structureConstant_neg_neg_eq_neg_iff: the Chevalley-involution symmetry holds exactly when the constant is ±(p + 1).

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §25.2.
• R. W. Carter, Simple Groups of Lie Type, §4.1.

This advances the Chevalley-basis input to the explicit Chevalley--Demazure construction in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, consumed by milestone L0 of the CFSGStatement roadmap.

theorem TauCeti.IsSl2System.structureConstant_mul_structureConstant_neg_neg {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) (α β γ : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) (hβ : β.IsNonZero) (hγ : γ.IsNonZero) (hαβ : ⇑γ = ⇑α + ⇑β) : hx.structureConstant α β γ hγ hαβ * hx.structureConstant (-α) (-β) (-γ) ⋯ ⋯ = -↑(LieModule.chainBotCoeff (⇑α) β + 1) ^ 2

Opposite structure constants multiply to -(p + 1)². For a normalised root-vector system and a root γ = α + β,

N(α, β) * N(-α, -β) = -(p + 1)²,

where p = chainBotCoeff α β. No compatibility with a Chevalley involution is assumed: the identity holds for every normalised system, and is invariant under the rescalings that relate two of them.

The proof multiplies the root-string product formula N(α, β) N(-α, γ) = q (p + 1) by the cyclic Killing-form symmetry of the triple (γ, -α, β), which rewrites N(-α, γ) in terms of N(-α, -β), and then cancels q against the invariant root-length ratio q B(x β, x (-β)) = (p + 1) B(x γ, x (-γ)).

theorem TauCeti.IsSl2System.structureConstant_neg_neg_eq_neg_iff {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) (α β γ : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) (hβ : β.IsNonZero) (hγ : γ.IsNonZero) (hαβ : ⇑γ = ⇑α + ⇑β) : hx.structureConstant (-α) (-β) (-γ) ⋯ ⋯ = -hx.structureConstant α β γ hγ hαβ ↔ hx.structureConstant α β γ hγ hαβ = ↑(LieModule.chainBotCoeff (⇑α) β + 1) ∨ hx.structureConstant α β γ hγ hαβ = -↑(LieModule.chainBotCoeff (⇑α) β + 1)

The Chevalley-involution symmetry is integrality. For a normalised root-vector system and a root γ = α + β, the structure constants at (α, β) and (-α, -β) are negatives of each other exactly when the constant at (α, β) is one of the Chevalley integers ±(p + 1).

The forward direction is the reason a Chevalley system has integral structure constants; the reverse direction is what lets a Chevalley involution be built from an integrally normalised system rather than assumed alongside it.