Serre systems in a split semisimple Lie algebra

Let L be a finite-dimensional Lie algebra with nondegenerate Killing form over a field K of characteristic zero, let H be a splitting Cartan subalgebra, and let b be a base of the root system of (L, H). Choosing an sl₂ triple (αⱼ∨, eⱼ, fⱼ) for each simple root αⱼ produces a Serre system in the sense of TauCeti.IsSerreSystem: the three families satisfy exactly the relators of the Serre presentation of the Cartan matrix of b.

Four of the six relations are immediate from the choice of sl₂ triples together with the fact that αᵢ - αⱼ is never a root for distinct simple roots. The two higher relations

(ad eᵢ) ^ (1 - ⟨αⱼ, αᵢ∨⟩) eⱼ = 0

are the content here. They come from the αᵢ-root string through αⱼ: since αⱼ - αᵢ is not a root, that string has no lower part, so ⟨αⱼ, αᵢ∨⟩ is minus the length of its upper part, and one step past the top of the string the root space vanishes.

Together with TauCeti.serreLift this presents L as a quotient of the Serre algebra of its own Cartan matrix, TauCeti.exists_surjective_serreLift_of_base. The corresponding statement for Mathlib's bundled LieAlgebra.Basis avoids the Killing-form, finite-dimensionality, splitting Cartan and triangularizability hypotheses, but retains characteristic zero and requires the Lie algebra to be torsion-free and Noetherian over the coefficient domain. It is proved by sl₂-strings instead, in TauCeti/Algebra/Lie/Presentation/Serre/Basis.lean.

Note that the Cartan matrix is transposed on the way: TauCeti.IsSerreSystem follows Serre's convention ⁅Hᵢ, Eⱼ⁆ = CMᵢⱼ Eⱼ, whereas RootPairing.Base.cartanMatrix i j is ⟨αᵢ, αⱼ∨⟩.

Main results

• TauCeti.chainBotCoeff_eq_zero_of_rootSpace_sub_eq_bot: a root string has no lower part as soon as one step down from its base is not a root.
• TauCeti.ad_pow_lie_eq_zero_of_rootSpace_sub_eq_bot: the higher Serre relation for a pair of root vectors whose difference of roots is not a root.
• TauCeti.rootSpace_sub_eq_bot_of_base: the difference of two distinct simple roots is not a root.
• TauCeti.isSerreSystem_coroot: simple-root sl₂ triples form a Serre system for the transposed Cartan matrix of the base.
• TauCeti.exists_isSerreSystem_of_base: such a Serre system exists, and its raising and lowering families generate L.
• TauCeti.exists_surjective_serreLift_of_base: L is a quotient of the Serre algebra of its Cartan matrix, by a homomorphism sending Hᵢ to the simple coroot αᵢ∨.

References

• J.P. Serre, Complex Semisimple Lie Algebras, chapter VI
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §18.1

Roadmap

The Serre presentation is the explicit carrier of the split semisimple Lie algebra whose Chevalley basis and Kostant ℤ-form build the Chevalley--Demazure group scheme, Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, consumed in turn by milestone L0 of TauCetiRoadmap/CFSGStatement/README.md. TauCeti.IsSerreSystem had no consumer outside the presentation itself; this file supplies the one that matters there, namely that the split semisimple Lie algebras the construction is about really are Serre systems for their Cartan matrices.

The higher Serre relation from a root string

theorem TauCeti.chainBotCoeff_eq_zero_of_rootSpace_sub_eq_bot {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {α β : LieModule.Weight K (↥H) L} (hα : α.IsNonZero) (hsub : LieAlgebra.rootSpace H (⇑β - ⇑α) = ⊥) : LieModule.chainBotCoeff (⇑α) β = 0

If β - α is not a root then the α-root string through β has no lower part.

theorem TauCeti.ad_pow_lie_eq_zero_of_rootSpace_sub_eq_bot {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {α β : LieModule.Weight K (↥H) L} (hα : α.IsNonZero) (hsub : LieAlgebra.rootSpace H (⇑β - ⇑α) = ⊥) {n : ℤ} (hn : ↑n = β (LieAlgebra.IsKilling.coroot α)) {x y : L} (hx : x ∈ LieAlgebra.rootSpace H ⇑α) (hy : y ∈ LieAlgebra.rootSpace H ⇑β) : ((LieAlgebra.ad K L) x ^ (-n).toNat) ⁅x, y⁆ = 0

The higher Serre relation. If x and y are root vectors for roots α and β whose difference β - α is not a root, and n = ⟨β, α∨⟩, then ad x kills ⁅x, y⁆ after -n further steps: one step past the top of the α-root string through β.

Simple roots

theorem TauCeti.rootSpace_sub_eq_bot_of_base {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) {i j : ↥b.support} (hij : i ≠ j) : LieAlgebra.rootSpace H (⇑↑↑i - ⇑↑↑j) = ⊥

The difference of two distinct simple roots is not a root.

theorem TauCeti.cartanMatrix_eq_apply_coroot {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (i j : ↥b.support) : ↑(b.cartanMatrix j i) = ↑↑j (LieAlgebra.IsKilling.coroot ↑↑i)

The corresponding entry of the Cartan matrix of the base is the pairing of two simple roots.

Serre systems from simple-root sl₂ triples

theorem TauCeti.isSerreSystem_coroot {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) {e f : ↥b.support → L} (hsl2 : ∀ (i : ↥b.support), IsSl2Triple (↑((LieAlgebra.IsKilling.rootSystem H).coroot ↑i)) (e i) (f i)) (he : ∀ (i : ↥b.support), e i ∈ LieAlgebra.rootSpace H ⇑↑↑i) (hf : ∀ (i : ↥b.support), f i ∈ LieAlgebra.rootSpace H (-⇑↑↑i)) : IsSerreSystem K b.cartanMatrix.transpose (fun (i : ↥b.support) => ↑((LieAlgebra.IsKilling.rootSystem H).coroot ↑i)) e f

sl₂ triples for the simple roots of a base form a Serre system. The relevant Cartan matrix is the transpose of RootPairing.Base.cartanMatrix, because TauCeti.IsSerreSystem follows Serre's convention ⁅Hᵢ, Eⱼ⁆ = CMᵢⱼ Eⱼ.

theorem TauCeti.exists_isSerreSystem_of_base {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) : ∃ (e : ↥b.support → L) (f : ↥b.support → L), IsSerreSystem K b.cartanMatrix.transpose (fun (i : ↥b.support) => ↑((LieAlgebra.IsKilling.rootSystem H).coroot ↑i)) e f ∧ LieSubalgebra.lieSpan K L (Set.range e ∪ Set.range f) = ⊤

A split semisimple Lie algebra carries a Serre system for its Cartan matrix, whose raising and lowering families generate it.

theorem TauCeti.exists_surjective_serreLift_of_base {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) : ∃ (φ : Matrix.ToLieAlgebra K b.cartanMatrix.transpose →ₗ⁅K⁆ L), Function.Surjective ⇑φ ∧ ∀ (i : ↥b.support), φ (serreH K b.cartanMatrix.transpose i) = ↑((LieAlgebra.IsKilling.rootSystem H).coroot ↑i)

A split semisimple Lie algebra is a quotient of the Serre algebra of its Cartan matrix, by a homomorphism sending the generator Hᵢ to the simple coroot αᵢ∨.