Root vectors compatible with a Chevalley involution

Let L be a finite-dimensional Lie algebra with nondegenerate Killing form over a field of characteristic zero, and let H be a splitting Cartan subalgebra. A normalized root-vector system x satisfies

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

A Chevalley system additionally comes with a Lie automorphism ω exchanging opposite root vectors with a sign:

ω (x α) = -x (-α).

This file packages those two compatible pieces of data as TauCeti.IsChevalleySystem. The compatibility already forces ω to act by negation on the Cartan subalgebra and to be an involution on all of L: the coroots span H, while the root vectors together with H span L.

The main mathematical result is the integral normalization of every genuine root-sum bracket. If γ = α + β, then

⁅x α, x β⁆ = ±(p + 1) x γ,

where p = chainBotCoeff α β. The proof combines the Chevalley-involution symmetry and square calculation from TauCeti.Algebra.Lie.Weights.StructureConstant.Normalization with the root-length ratio from TauCeti.Algebra.Lie.Weights.RootString. The resulting integer-coefficient theorem is stated both for the named structure constant and directly for the bracket, in the form consumed by the integral root--coroot span.

Main definitions and results

• TauCeti.IsChevalleySystem: a normalized root-vector system compatible with a Lie automorphism exchanging opposite root vectors with a sign.
• TauCeti.IsChevalleySystem.map_coroot: the automorphism negates every coroot.
• TauCeti.IsChevalleySystem.map_cartan: the automorphism negates the Cartan subalgebra.
• TauCeti.IsChevalleySystem.involutive: compatibility on the root vectors forces the automorphism to be an involution on all of L.
• TauCeti.IsChevalleySystem.symm_eq: the automorphism is its own inverse.
• TauCeti.IsChevalleySystem.structureConstant_eq_natCast_or_eq_neg_natCast: every genuine root-sum structure constant is p + 1 or its negative.
• TauCeti.IsChevalleySystem.exists_int_lie_eq_smul: every root-sum bracket has an integral coefficient.
• TauCeti.IsChevalleySystem.intStructureConstant: that coefficient, named as an integer, with lie_eq_intStructureConstant_zsmul its defining equation and intStructureConstant_eq_natCast_or_eq_neg_natCast identifying it as ±(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 supplies the integral 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. The existence of a compatible Chevalley system remains downstream.

structure TauCeti.IsChevalleySystem {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (ω : L ≃ₗ⁅K⁆ L) (x : LieModule.Weight K (↥H) L → L) : Prop

A normalized family of root vectors compatible with a Chevalley involution. The Lie automorphism ω exchanges each root vector with the negative of its opposite.

There is no separate involutivity field: TauCeti.IsChevalleySystem.involutive proves it from this compatibility and the fact that the root vectors and Cartan subalgebra span the ambient Lie algebra.

• toIsSl2System : IsSl2System x

  The root vectors are normalized against the coroots.

• map_root (α : LieModule.Weight K (↥H) L) : ω (x α) = -x (-α)

  The automorphism exchanges each root vector with the negative of its opposite.

theorem TauCeti.IsChevalleySystem.map_coroot {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] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) (α : LieModule.Weight K (↥H) L) : ω ↑(LieAlgebra.IsKilling.coroot α) = -↑(LieAlgebra.IsKilling.coroot α)

A Chevalley-system automorphism sends every coroot to its negative. This follows from the normalization of opposite root vectors, rather than being separate data.

theorem TauCeti.IsChevalleySystem.map_cartan {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] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) (h : ↥H) : ω ↑h = -↑h

A Chevalley-system automorphism acts by negation on the splitting Cartan subalgebra. It is enough to check the coroots because they span H.

theorem TauCeti.IsChevalleySystem.involutive {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] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) : Function.Involutive ⇑ω

A Chevalley-system automorphism is an involution. The compatibility equation on root vectors forces this globally: the root vectors together with the Cartan subalgebra span L.

theorem TauCeti.IsChevalleySystem.symm_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] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) : ω.symm = ω

A Chevalley-system automorphism is its own inverse.

theorem TauCeti.IsChevalleySystem.structureConstant_eq_natCast_or_eq_neg_natCast {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] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) (α β γ : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) (hβ : β.IsNonZero) (hγ : γ.IsNonZero) (hαβ : ⇑γ = ⇑α + ⇑β) : ⋯.structureConstant α β γ hγ hαβ = ↑(LieModule.chainBotCoeff (⇑α) β + 1) ∨ ⋯.structureConstant α β γ hγ hαβ = -↑(LieModule.chainBotCoeff (⇑α) β + 1)

Chevalley normalization of structure constants. If γ = α + β is a genuine root sum, then the structure constant of a Chevalley system is p + 1 or its negative, where p = chainBotCoeff α β.

The root-length ratio is automatic for normalized root vectors; compatibility with ω supplies the symmetry that turns the root-string product formula into a square.

theorem TauCeti.IsChevalleySystem.exists_int_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] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) (α β γ : LieModule.Weight K (↥H) L) (hγ : γ.IsNonZero) (hαβ : ⇑γ = ⇑α + ⇑β) : ∃ (z : ℤ), ⋯.structureConstant α β γ hγ hαβ = ↑z

The structure constant of a genuine root-sum bracket in a Chevalley system is the cast of an integer. The preceding theorem identifies that integer more precisely as ±(p + 1).

theorem TauCeti.IsChevalleySystem.exists_int_lie_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] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) (α β γ : LieModule.Weight K (↥H) L) (hγ : γ.IsNonZero) (hαβ : ⇑γ = ⇑α + ⇑β) : ∃ (z : ℤ), ⁅x α, x β⁆ = ↑z • x γ

Every genuine root-sum bracket in a Chevalley system has an integral coefficient. This is the form needed to prove that the integral span of root vectors and coroots is closed under the Lie bracket.

noncomputable def TauCeti.IsChevalleySystem.intStructureConstant {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] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) (α β γ : LieModule.Weight K (↥H) L) (hγ : γ.IsNonZero) (hαβ : ⇑γ = ⇑α + ⇑β) : ℤ

The integer structure constant of a Chevalley system: the unique integer N with ⁅x α, x β⁆ = N • x γ when the root γ is the sum of α and β.

The rational structure constant of a merely normalised system is a scalar of the base field. The Chevalley normalization pins it to the image of an integer, and it is the integer, not its cast, that a construction in characteristic p needs. The public interface is TauCeti.IsChevalleySystem.intStructureConstant_cast and its uniqueness restatement TauCeti.IsChevalleySystem.eq_intStructureConstant_iff; consumers need not unfold this choice.

Equations

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

@[simp]

theorem TauCeti.IsChevalleySystem.intStructureConstant_cast {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] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) (α β γ : LieModule.Weight K (↥H) L) (hγ : γ.IsNonZero) (hαβ : ⇑γ = ⇑α + ⇑β) : ↑(hx.intStructureConstant α β γ hγ hαβ) = ⋯.structureConstant α β γ hγ hαβ

The cast of the integer structure constant is the structure constant.

theorem TauCeti.IsChevalleySystem.lie_eq_intStructureConstant_zsmul {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] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) (α β γ : LieModule.Weight K (↥H) L) (hγ : γ.IsNonZero) (hαβ : ⇑γ = ⇑α + ⇑β) : ⁅x α, x β⁆ = hx.intStructureConstant α β γ hγ hαβ • x γ

The defining equation of the integer structure constant. The coefficient is an integer acting by ℤ-scalar multiplication, which is what survives reduction to a base of arbitrary characteristic.

@[simp]

theorem TauCeti.IsChevalleySystem.eq_intStructureConstant_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] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) (α β γ : LieModule.Weight K (↥H) L) (hγ : γ.IsNonZero) (hαβ : ⇑γ = ⇑α + ⇑β) (z : ℤ) : z = hx.intStructureConstant α β γ hγ hαβ ↔ ⁅x α, x β⁆ = z • x γ

An integer is the integer structure constant exactly when it gives the bracket of the corresponding root vectors.

theorem TauCeti.IsChevalleySystem.intStructureConstant_eq_natCast_or_eq_neg_natCast {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] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) (α β γ : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) (hβ : β.IsNonZero) (hγ : γ.IsNonZero) (hαβ : ⇑γ = ⇑α + ⇑β) : hx.intStructureConstant α β γ hγ hαβ = ↑(LieModule.chainBotCoeff (⇑α) β + 1) ∨ hx.intStructureConstant α β γ hγ hαβ = -↑(LieModule.chainBotCoeff (⇑α) β + 1)

The integer structure constant of a genuine root-sum bracket is ±(p + 1), for p the root-string coefficient chainBotCoeff α β.

theorem TauCeti.IsChevalleySystem.intStructureConstant_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] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) (α β γ : LieModule.Weight K (↥H) L) (hα : α.IsNonZero) (hβ : β.IsNonZero) (hγ : γ.IsNonZero) (hαβ : ⇑γ = ⇑α + ⇑β) : hx.intStructureConstant α β γ hγ hαβ ≠ 0

The integer structure constant of a genuine root-sum bracket is nonzero.