The Chevalley lattice is stable under divided powers of the adjoint action

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over a field of characteristic zero, let H be a splitting Cartan subalgebra, and let x be a Chevalley system of root vectors. TauCeti.IsChevalleySystem.chevalleyLieLattice is the ℤ-span of the root vectors and the coroots; it is a finite free full integral form of L.

This file proves that this lattice is stable under the divided powers

(ad (x α)) ^ n / n !

of the adjoint action of each root vector. Stability under ad (x α) itself is the statement that the lattice is a Lie subalgebra, and it already follows from integrality of the structure constants; the content here is that the factorial in the denominator cancels.

The mechanism is the root string. Writing p = chainBotCoeff α β for the length of the descending part of the α-chain through β, an induction along that chain gives

(ad (x α)) ^ n (x β) = ± (p + 1)(p + 2) ⋯ (p + n) • x (β + n α),

or zero once the chain has been left. The coefficient is a rising factorial, hence is divisible by n ! — this is the classical computation of Humphreys §25.5. Two ingredients make the induction go through: Mathlib's LieAlgebra.IsKilling.chainBotCoeff_of_eq_zsmul_add, which says that moving one step up a root string lengthens its descending part by exactly one, and the Chevalley normalization TauCeti.IsChevalleySystem.structureConstant_eq_natCast_or_eq_neg_natCast, which identifies each bracket coefficient as ± (p + 1).

The remaining generators of the lattice are handled directly: x (-α) spans an sl₂-triple with x α, where the chain is short enough to compute by hand, and a coroot β∨ is sent by the first bracket to -α β∨ • x α, an integral multiple of x α because Cartan integers are integers, and by the second bracket to zero.

Together with the binomial coefficients of the Cartan generators, which act diagonally on root vectors, this is exactly the invariance needed to make L a module over the Kostant ℤ-form of U(L) preserving a finite free lattice; that consequence is drawn in TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.Adjoint.Basic. This advances Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, consumed by milestone L0 of CFSGStatement.

Main results

• TauCeti.coe_add_natCast_smul_ne_zero: an ascending root string through a root other than -α never meets the zero weight.
• TauCeti.IsChevalleySystem.ad_pow_rootVector_eq_zero_or_exists: the root-string form of the iterated adjoint action, with its rising-factorial coefficient.
• TauCeti.IsChevalleySystem.inv_factorial_smul_ad_pow_mem_chevalleyLieLattice: the Chevalley lattice is stable under every divided power of ad (x α).

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §25.5.
• R. W. Carter, Simple Groups of Lie Type, §4.4.

theorem TauCeti.coe_add_natCast_smul_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] {α β : LieModule.Weight K (↥H) L} (hα : α.IsNonZero) (hβ : β.IsNonZero) (hαβ : ⇑α + ⇑β ≠ 0) (n : ℕ) : ⇑β + ↑n • ⇑α ≠ 0

Root strings avoid the zero weight. If α and β are roots with β ≠ -α, then no weight β + n α of the ascending α-string through β is zero.

Only ± α are multiples of a root α, so a vanishing member of the string would force β = α and then (n + 1) α = 0.

theorem TauCeti.IsChevalleySystem.ad_pow_rootVector_eq_zero_or_exists {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αβ : ⇑α + ⇑β ≠ 0) (n : ℕ) : ((LieAlgebra.ad K L) (x α) ^ n) (x β) = 0 ∨ ∃ (γ : LieModule.Weight K (↥H) L), ⇑γ = ⇑β + ↑n • ⇑α ∧ LieModule.chainBotCoeff (⇑α) γ = LieModule.chainBotCoeff (⇑α) β + n ∧ ∃ (z : ℤ), z.natAbs = (LieModule.chainBotCoeff (⇑α) β + 1).ascFactorial n ∧ ((LieAlgebra.ad K L) (x α) ^ n) (x β) = ↑z • x γ

The iterated adjoint action along a root string. For roots α and β with β ≠ -α, the n-th power of ad (x α) sends x β either to zero or to an integer multiple of the root vector at β + n α, and the integer is the rising factorial (p + 1)(p + 2) ⋯ (p + n), where p is the descending α-chain coefficient at β.

Each step multiplies the coefficient by a Chevalley structure constant, which is ± (p + n + 1) by the normalization of a Chevalley system.

theorem TauCeti.IsChevalleySystem.inv_factorial_smul_ad_pow_rootVector_mem {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) (n : ℕ) : (↑n.factorial)⁻¹ • ((LieAlgebra.ad K L) (x α) ^ n) (x β) ∈ hx.chevalleyLieLattice

Divided powers of the adjoint action of a root vector send root vectors into the Chevalley lattice. The rising factorial produced by the root-string computation is divisible by n !, and the two exceptional strings — the one through -α and the degenerate ones — are handled directly.

theorem TauCeti.IsChevalleySystem.inv_factorial_smul_ad_pow_coroot_mem {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) (n : ℕ) : (↑n.factorial)⁻¹ • ((LieAlgebra.ad K L) (x α) ^ n) ↑(LieAlgebra.IsKilling.coroot β) ∈ hx.chevalleyLieLattice

Divided powers of the adjoint action of a root vector send coroots into the Chevalley lattice. A coroot is annihilated after two brackets, and the single surviving coefficient is a Cartan integer.

theorem TauCeti.IsChevalleySystem.inv_factorial_smul_ad_pow_mem_chevalleyLieLattice {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) (n : ℕ) {y : L} (hy : y ∈ hx.chevalleyLieLattice) : (↑n.factorial)⁻¹ • ((LieAlgebra.ad K L) (x α) ^ n) y ∈ hx.chevalleyLieLattice

The Chevalley lattice is stable under the divided powers of the adjoint action of a root vector. Every divided power (ad (x α)) ^ n / n ! maps the lattice into itself.

Since the lattice is spanned over ℤ by the root vectors and the coroots, and each divided power is an additive map, it suffices to check the two families of generators.

This is stability under the root-vector generators of the Kostant form only; the binomial coefficients of the Cartan generators are treated separately, and stability under the whole Kostant form is TauCeti.IsChevalleySystem.chevalleyKostantForm_le_stabilizer.