Symmetries of root-vector structure constants

Let x be an IsSl2System, so that its root vectors satisfy ⁅x α, x (-α)⁆ = α∨. The structure constants of x were defined in TauCeti.Algebra.Lie.Weights.StructureConstant.Basic by

⁅x α, x β⁆ = N(α, β) x(α + β).

This file proves two symmetries of these constants. First, a Lie endomorphism exchanging each of the three root vectors with the negative of its opposite sends N(α, β) to -N(-α, -β). These hypotheses hold when the normalized family is a Chevalley system, chosen compatibly with the Chevalley involution. Second, invariance of the Killing form gives the cyclic relation

N(α, β) B(x(α + β), x(-α - β))
  = N(β, -α - β) B(x α, x(-α)).

The Killing factors are nonzero and explicitly evaluated by the preceding IsSl2System API, so this is a genuine relation between the two constants rather than a vacuous equality. Together these are the symmetry relations used when a normalized root-vector system is rescaled coherently to a Chevalley basis. They advance the explicit Chevalley--Demazure construction in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md; the existence of the coherent rescaling is not asserted here.

Main results

• TauCeti.IsSl2System.mul_structureConstant_eq_of_map_eq_smul_neg: the general scalar relation induced by a Lie endomorphism carrying three root vectors to their opposites.
• TauCeti.IsSl2System.structureConstant_neg_neg_of_hom: compatibility with a Lie endomorphism exchanging root vectors with the negatives of their opposites.
• TauCeti.IsSl2System.structureConstant_mul_killingForm_eq: the cyclic Killing-form symmetry.

References

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

theorem TauCeti.IsSl2System.mul_structureConstant_eq_of_map_eq_smul_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αβ : ⇑γ = ⇑α + ⇑β) (e : L →ₗ⁅K⁆ L) {a b c : K} (heα : e (x α) = a • x (-α)) (heβ : e (x β) = b • x (-β)) (heγ : e (x γ) = c • x (-γ)) : c * hx.structureConstant α β γ hγ hαβ = a * b * hx.structureConstant (-α) (-β) (-γ) ⋯ ⋯

The scalars are multiplicative along a root sum, up to the structure constants. Applying a Lie endomorphism to ⁅x α, x β⁆ = N(α, β) • x γ turns it into the bracket at the opposite roots.

theorem TauCeti.IsSl2System.structureConstant_neg_neg_of_hom {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αβ : ⇑γ = ⇑α + ⇑β) (e : L →ₗ⁅K⁆ L) (heα : e (x α) = -x (-α)) (heβ : e (x β) = -x (-β)) (heγ : e (x γ) = -x (-γ)) : hx.structureConstant (-α) (-β) (-γ) ⋯ ⋯ = -hx.structureConstant α β γ hγ hαβ

If a Lie endomorphism sends the root vectors at α, β, and γ = α + β to the negatives of their opposite root vectors, then it sends the corresponding structure constant to the negative of the structure constant at -α, -β, and -γ.

Only the three values used in the equation are hypotheses. They are supplied uniformly when x is a Chevalley system: a normalized family chosen compatibly with a Chevalley involution.

theorem TauCeti.IsSl2System.structureConstant_mul_killingForm_eq {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) : hx.structureConstant α β γ hγ hαβ * ((killingForm K L) (x γ)) (x (-γ)) = hx.structureConstant β (-γ) (-α) ⋯ ⋯ * ((killingForm K L) (x α)) (x (-α))

Cyclic symmetry of normalized structure constants. If γ = α + β, invariance of the Killing form relates the constants of (α, β, γ) and (β, -γ, -α) after weighting by the Killing pairings of opposite root vectors.

Both Killing factors are nonzero by TauCeti.killingForm_ne_zero_of_mem_rootSpace, and their exact values are given by TauCeti.IsSl2System.killingForm_root_neg_eq, so the equality can safely be cancelled or rewritten as a ratio downstream.