Structure constants of a normalised root-vector system

Let x be an IsSl2System in a finite-dimensional Lie algebra with non-degenerate Killing form. Thus x α is a root vector of α, and opposite root vectors are normalised by

⁅x α, x (-α)⁆ = α∨.

When γ = α + β is a non-zero root, the root space of γ is the line spanned by x γ. Consequently there is a unique scalar N such that

⁅x α, x β⁆ = N • x γ.

This file packages that scalar as TauCeti.IsSl2System.structureConstant. Its characteristic equation and uniqueness theorem keep downstream arguments independent of its choice-based implementation. The constants are non-zero when all three weights are roots, are skew-symmetric in α and β, transform by the expected ratio when a normalised system is rescaled, and satisfy the root-string product formula proved in TauCeti/Algebra/Lie/Weights/Root/String.lean.

These are the scalar identities needed before a coherent choice of signs can upgrade an IsSl2System to a Chevalley basis with constants ±(p + 1). This advances the explicit Chevalley--Demazure construction in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md; it does not assert that an arbitrary normalised system already has integral structure constants.

Main definitions and results

• TauCeti.IsSl2System.structureConstant: the coefficient of x γ in ⁅x α, x β⁆ when γ = α + β.
• TauCeti.IsSl2System.lie_eq_structureConstant_smul and TauCeti.IsSl2System.eq_structureConstant_iff: the characteristic equation and uniqueness.
• TauCeti.IsSl2System.structureConstant_ne_zero: nonvanishing when α, β, and γ are roots.
• TauCeti.IsSl2System.structureConstant_skew: skew-symmetry in the first two roots.
• TauCeti.IsSl2System.mul_structureConstant_eq_of_eq_smul: transformation under a rescaling of the root vectors.
• TauCeti.IsSl2System.structureConstant_mul_structureConstant: the root-string product formula.

References

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

noncomputable def TauCeti.IsSl2System.structureConstant {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αβ : ⇑γ = ⇑α + ⇑β) : K

The structure constant of a normalised root-vector system: the unique scalar N satisfying ⁅x α, x β⁆ = N • x γ when the non-zero root γ is the sum of α and β.

The public interface is the characteristic equation TauCeti.IsSl2System.lie_eq_structureConstant_smul and its uniqueness restatement TauCeti.IsSl2System.eq_structureConstant_iff; consumers need not unfold this choice.

Equations

• hx.structureConstant α β γ hγ hαβ = Classical.choose ⋯

theorem TauCeti.IsSl2System.lie_eq_structureConstant_smul {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αβ : ⇑γ = ⇑α + ⇑β) : ⁅x α, x β⁆ = hx.structureConstant α β γ hγ hαβ • x γ

The bracket equation defining the structure constant of a normalised root-vector system.

@[simp]

theorem TauCeti.IsSl2System.eq_structureConstant_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αβ : ⇑γ = ⇑α + ⇑β) (N : K) : N = hx.structureConstant α β γ hγ hαβ ↔ ⁅x α, x β⁆ = N • x γ

A scalar is the structure constant exactly when it gives the bracket of the corresponding root vectors.

theorem TauCeti.IsSl2System.structureConstant_ne_zero {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αβ : ⇑γ = ⇑α + ⇑β) (hα : α.IsNonZero) (hβ : β.IsNonZero) : hx.structureConstant α β γ hγ hαβ ≠ 0

The structure constant is non-zero when both input weights and their sum are roots.

theorem TauCeti.IsSl2System.structureConstant_skew {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αβ : ⇑γ = ⇑α + ⇑β) : hx.structureConstant β α γ hγ ⋯ = -hx.structureConstant α β γ hγ hαβ

Swapping the two input roots negates their structure constant.

theorem TauCeti.IsSl2System.mul_structureConstant_eq_of_eq_smul {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 y : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) (α β γ : LieModule.Weight K (↥H) L) (hγ : γ.IsNonZero) (hαβ : ⇑γ = ⇑α + ⇑β) (hy : IsSl2System y) (a b c : K) (ha : y α = a • x α) (hb : y β = b • x β) (hc : y γ = c • x γ) : c * hy.structureConstant α β γ hγ hαβ = a * b * hx.structureConstant α β γ hγ hαβ

Structure constants transform by the expected ratio under a rescaling of a normalised root-vector system. If y α = a • x α, y β = b • x β, and y γ = c • x γ, then c * N_y(α, β) = a * b * N_x(α, β).

The division-free form is valid over the ambient field without asking callers to supply the already implied fact c ≠ 0.

theorem TauCeti.IsSl2System.structureConstant_mul_structureConstant {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αβ : ⇑γ = ⇑α + ⇑β) (hα : α.IsNonZero) (hβ : β.IsNonZero) : hx.structureConstant α β γ hγ hαβ * hx.structureConstant (-α) γ β hβ ⋯ = ↑(LieModule.chainTopCoeff (⇑α) β * (LieModule.chainBotCoeff (⇑α) β + 1))

The two structure constants in one root string multiply to the combinatorial root-string coefficient. If γ = α + β, then

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

where β - pα, …, β, …, β + qα is the α-string through β.