Chevalley systems for the pinned rational Lie algebra

The signed Geck involution exchanges the simple raising and lowering generators of the pinned Lie-algebra basis. The generic base-square propagation theorem therefore constructs a Chevalley system over ℚ itself; no extension to an algebraic closure is needed for this choice. This does not establish nondegeneracy of the rational Killing form, which is an independent input supplied by the imported Killing-form module.

Main results

• TauCeti.DynkinType.instIsTriangularizableLieAlgebra: the distinguished Cartan acts triangularizably on the pinned rational Lie algebra.
• TauCeti.DynkinType.exists_isChevalleySystem: the signed Geck involution admits a compatible Chevalley system over ℚ.

References

• M. Geck, On the construction of semisimple Lie algebras and Chevalley groups, Proc. Amer. Math. Soc. 145 (2017), 3233--3247.
• R. W. Carter, Simple Groups of Lie Type, §4.2.

instance TauCeti.DynkinType.instIsTriangularizableLieAlgebra (t : DynkinType) (ht : t.Valid) : LieModule.IsTriangularizable ℚ ↥(t.cartanSubalgebra ht) ↥(t.lieAlgebra ht)

The Cartan action on the pinned rational Lie algebra is triangularizable over ℚ.

theorem TauCeti.DynkinType.exists_isChevalleySystem (t : DynkinType) (ht : t.Valid) : ∃ (x : LieModule.Weight ℚ ↥(t.cartanSubalgebra ht) ↥(t.lieAlgebra ht) → ↥(t.lieAlgebra ht)), IsChevalleySystem (t.chevalleyInvolution ht) x

The pinned rational Lie algebra admits a root-vector system compatible with its signed Geck involution.