The structure constants of the pinned Chevalley system

TauCeti.DynkinType.chevalleySystem names a root vector e_α of the pinned rational Lie algebra TauCeti.DynkinType.lieAlgebra for every root number α : Fin t.numRoots of TauCeti.DynkinType.simplyConnectedRootDatum, and these root vectors form a Chevalley system for the signed Chevalley involution ω. This file records the integers N_{α,β} with

⁅e_α, e_β⁆ = N_{α,β} e_{α+β}      whenever α + β is a root,

as the integer-valued function TauCeti.DynkinType.structureConstant on pairs of root numbers, with the convention N_{α,β} = 0 when α + β is not a root. Chevalley's theorem pins the value up to sign: N_{α,β} = ±(r + 1), where r is the largest integer with β - r α a root, the descending root-string coefficient chainBotCoeff α β of the pinned datum. The constants are skew-symmetric, and compatibility of the root vectors with ω gives the Chevalley relation N_{-α,-β} = -N_{α,β}. Root sums and root strings are read in the integral datum throughout, so that the constants can be used in the root numbering without passing through the Lie weights.

When α + β is neither a root nor zero the bracket ⁅e_α, e_β⁆ vanishes, so together with the normalization ⁅e_α, e_{-α}⁆ = h_α of TauCeti.DynkinType.lie_chevalleySystem_reflectionPerm_self the structure constants describe every bracket of two root vectors. These integers are the input to the Chevalley commutator formula for the root subgroups x_α(u) = Σₙ uⁿ ρ(e_α)⁽ⁿ⁾.

Main definitions

• TauCeti.DynkinType.structureConstant: the integer N_{α,β}.

Main results

• TauCeti.DynkinType.lie_chevalleySystem_eq_structureConstant_zsmul and TauCeti.DynkinType.eq_structureConstant_iff: the defining bracket equation and its uniqueness.
• TauCeti.DynkinType.structureConstant_eq_natCast_or_eq_neg_natCast: N_{α,β} = ±(r + 1).
• TauCeti.DynkinType.chainBotCoeff_add_one_dvd_structureConstant: r + 1 divides N_{α,β}.
• TauCeti.DynkinType.structureConstant_eq_two_or_neg_two_of_pairingIn_eq_zero: N_{α,β} = ±2 for orthogonal roots whose sum is a root.
• TauCeti.DynkinType.structureConstant_ne_zero and TauCeti.DynkinType.structureConstant_eq_zero: the constant vanishes exactly when α + β is not a root.
• TauCeti.DynkinType.structureConstant_skew: N_{β,α} = -N_{α,β}.
• TauCeti.DynkinType.structureConstant_reflectionPerm_self_reflectionPerm_self: N_{-α,-β} = -N_{α,β}.
• TauCeti.DynkinType.two_dvd_structureConstant_mul_structureConstant: N_{α,β} N_{α,α+β} is even.
• TauCeti.DynkinType.lie_chevalleySystem_eq_zero: ⁅e_α, e_β⁆ = 0 when α + β is neither a root nor zero.
• TauCeti.DynkinType.lie_chevalleySystem_eq_zero_of_add_eq: if γ = α + β is a root and α + γ is not a root, then ⁅e_α, e_γ⁆ = 0, with no separate nonzero hypothesis.

References

• R. Steinberg, Lectures on Chevalley Groups, Chapter 1, Theorem 1.
• R. W. Carter, Simple Groups of Lie Type, §4.2.

noncomputable def TauCeti.DynkinType.structureConstant (t : DynkinType) (ht : t.Valid) (α β : Fin t.numRoots) : ℤ

The structure constants of the pinned Chevalley system. For root numbers α and β, the integer N_{α,β} with ⁅e_α, e_β⁆ = N_{α,β} e_γ when root γ of the pinned datum is the sum of roots α and β, and 0 when α + β is not a root. Here e is TauCeti.DynkinType.chevalleySystem. When α + β is a root, the value is ±(r + 1) for r = chainBotCoeff α β, by TauCeti.DynkinType.structureConstant_eq_natCast_or_eq_neg_natCast.

theorem TauCeti.DynkinType.lie_chevalleySystem_eq_structureConstant_zsmul {t : DynkinType} {ht : t.Valid} {α β γ : Fin t.numRoots} (h : (t.simplyConnectedRootDatum ht).root γ = (t.simplyConnectedRootDatum ht).root α + (t.simplyConnectedRootDatum ht).root β) : ⁅t.chevalleySystem ht α, t.chevalleySystem ht β⁆ = t.structureConstant ht α β • t.chevalleySystem ht γ

The structure-constant equation. If root γ of the pinned datum is the sum of roots α and β, then ⁅e_α, e_β⁆ = N_{α,β} e_γ.

theorem TauCeti.DynkinType.eq_structureConstant_iff {t : DynkinType} {ht : t.Valid} {α β γ : Fin t.numRoots} (h : (t.simplyConnectedRootDatum ht).root γ = (t.simplyConnectedRootDatum ht).root α + (t.simplyConnectedRootDatum ht).root β) (z : ℤ) : z = t.structureConstant ht α β ↔ ⁅t.chevalleySystem ht α, t.chevalleySystem ht β⁆ = z • t.chevalleySystem ht γ

The structure constant is determined by the bracket. If root γ of the pinned datum is the sum of roots α and β, an integer is N_{α,β} exactly when it is the coefficient of e_γ in ⁅e_α, e_β⁆.

theorem TauCeti.DynkinType.structureConstant_eq_natCast_or_eq_neg_natCast {t : DynkinType} {ht : t.Valid} {α β : Fin t.numRoots} (h : (t.simplyConnectedRootDatum ht).root α + (t.simplyConnectedRootDatum ht).root β ∈ Set.range ⇑(t.simplyConnectedRootDatum ht).root) : t.structureConstant ht α β = ↑(RootPairing.chainBotCoeff α β + 1) ∨ t.structureConstant ht α β = -↑(RootPairing.chainBotCoeff α β + 1)

Chevalley's theorem on structure constants. If α + β is a root, then N_{α,β} = ±(r + 1), where r = chainBotCoeff α β is the largest integer with β - r α a root of the pinned datum.

theorem TauCeti.DynkinType.structureConstant_eq_zero {t : DynkinType} {ht : t.Valid} {α β : Fin t.numRoots} (h : (t.simplyConnectedRootDatum ht).root α + (t.simplyConnectedRootDatum ht).root β ∉ Set.range ⇑(t.simplyConnectedRootDatum ht).root) : t.structureConstant ht α β = 0

The structure constant vanishes when α + β is not a root.

theorem TauCeti.DynkinType.two_dvd_structureConstant_mul_structureConstant {t : DynkinType} {ht : t.Valid} {α β γ : Fin t.numRoots} (hγ : (t.simplyConnectedRootDatum ht).root γ = (t.simplyConnectedRootDatum ht).root α + (t.simplyConnectedRootDatum ht).root β) : 2 ∣ t.structureConstant ht α β * t.structureConstant ht α γ

The product of consecutive structure constants in a root string is even. Thus the coefficient of e_{2α+β} in (ad e_α)² e_β / 2 is an integer.

theorem TauCeti.DynkinType.structureConstant_ne_zero {t : DynkinType} {ht : t.Valid} {α β : Fin t.numRoots} (h : (t.simplyConnectedRootDatum ht).root α + (t.simplyConnectedRootDatum ht).root β ∈ Set.range ⇑(t.simplyConnectedRootDatum ht).root) : t.structureConstant ht α β ≠ 0

The structure constant of a genuine root sum is nonzero.

theorem TauCeti.DynkinType.chainBotCoeff_add_one_dvd_structureConstant {t : DynkinType} {ht : t.Valid} {α β : Fin t.numRoots} : ↑(RootPairing.chainBotCoeff α β + 1) ∣ t.structureConstant ht α β

For every root pair, the descending root-string length plus one divides the structure constant.

theorem TauCeti.DynkinType.structureConstant_skew {t : DynkinType} {ht : t.Valid} (α β : Fin t.numRoots) : t.structureConstant ht β α = -t.structureConstant ht α β

Skew-symmetry of the structure constants: N_{β,α} = -N_{α,β}.

@[simp]

theorem TauCeti.DynkinType.structureConstant_reflectionPerm_self_reflectionPerm_self {t : DynkinType} {ht : t.Valid} (α β : Fin t.numRoots) : t.structureConstant ht (((t.simplyConnectedRootDatum ht).reflectionPerm α) α) (((t.simplyConnectedRootDatum ht).reflectionPerm β) β) = -t.structureConstant ht α β

The Chevalley relation: N_{-α,-β} = -N_{α,β}, where the negative of a root number α is its reflection reflectionPerm α α in itself. It holds because the Chevalley involution sends e_α to -e_{-α}.

theorem TauCeti.DynkinType.structureConstant_eq_two_or_neg_two_of_pairingIn_eq_zero {t : DynkinType} {ht : t.Valid} {α β : Fin t.numRoots} (hsum : (t.simplyConnectedRootDatum ht).root α + (t.simplyConnectedRootDatum ht).root β ∈ Set.range ⇑(t.simplyConnectedRootDatum ht).root) (horth : RootPairing.pairingIn (t.simplyConnectedRootDatum ht) ℤ β α = 0) : t.structureConstant ht α β = 2 ∨ t.structureConstant ht α β = -2

The structure constant of orthogonal roots whose sum is a root is two up to sign.

theorem TauCeti.DynkinType.lie_chevalleySystem_eq_zero {t : DynkinType} {ht : t.Valid} {α β : Fin t.numRoots} (h : (t.simplyConnectedRootDatum ht).root α + (t.simplyConnectedRootDatum ht).root β ∉ Set.range ⇑(t.simplyConnectedRootDatum ht).root) (h₀ : (t.simplyConnectedRootDatum ht).root α + (t.simplyConnectedRootDatum ht).root β ≠ 0) : ⁅t.chevalleySystem ht α, t.chevalleySystem ht β⁆ = 0

Brackets at non-roots vanish. If α + β is neither a root of the pinned datum nor zero, then ⁅e_α, e_β⁆ = 0.

theorem TauCeti.DynkinType.lie_chevalleySystem_eq_zero_of_add_eq {t : DynkinType} {ht : t.Valid} {α β γ : Fin t.numRoots} (hadd : (t.simplyConnectedRootDatum ht).root γ = (t.simplyConnectedRootDatum ht).root α + (t.simplyConnectedRootDatum ht).root β) (h : (t.simplyConnectedRootDatum ht).root α + (t.simplyConnectedRootDatum ht).root γ ∉ Set.range ⇑(t.simplyConnectedRootDatum ht).root) : ⁅t.chevalleySystem ht α, t.chevalleySystem ht γ⁆ = 0

If γ = α + β is a root but α + γ is not, then e_α commutes with e_γ. Reducedness makes the summands linearly independent, so α + γ cannot be zero.