Root vectors of a Lie algebra basis

This file relates a LieAlgebra.Basis to the root-space decomposition of its Cartan subalgebra. The raising and lowering generators lie in the expected simple-root spaces. Moreover, the three-part Cartan/lower-Borel/upper-Borel decomposition already constructed by Mathlib lies in generalized weight spaces. It follows that the Cartan action is triangularizable over the ground field, without passing to an algebraic closure. Positive roots are also expressed as nonzero natural combinations of the simple roots supplied by the basis, providing the coordinate form used by the nilradical and Borel bridges.

Main results

• LieAlgebra.Basis.isTriangularizable: the Cartan action associated to a Lie-algebra basis is triangularizable over the ground field.
• LieAlgebra.Basis.exists_root_eq_sum_nat_baseSupp_of_mem_posRoots: every positive root is a nonzero natural-number combination of the basis's simple roots.
• TauCeti.lieBasis_e_mem_rootSpace and TauCeti.lieBasis_f_mem_rootSpace: the simple raising and lowering generators lie in their expected root spaces.

References

• M. Geck, On the construction of semisimple Lie algebras and Chevalley groups, Proc. Amer. Math. Soc. 145 (2017), 3233--3247, Lemma 4.4.

theorem LieAlgebra.Basis.isTriangularizable {ι : Type u_1} {K : Type u_2} {L : Type u_3} [Finite ι] [CommRing K] [IsDomain K] [CharZero K] [LieRing L] [LieAlgebra K L] {H : LieSubalgebra K L} (b : Basis ι H) : LieModule.IsTriangularizable K (↥H) L

The Cartan action associated to a Lie-algebra basis is triangularizable over the ground field. The three-part decomposition from the basis is already contained in generalized weight spaces, so every Cartan element has a full decomposition into generalized eigenspaces.

theorem LieAlgebra.Basis.exists_root_eq_sum_nat_baseSupp_of_mem_posRoots {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} {ι : Type u_4} [Fintype ι] (b : Basis ι H) {α : ↥LieSubalgebra.root} : α ∈ TauCeti.posRoots (IsKilling.rootSystem H) b.base → ∃ (n : ι → ℕ), n ≠ 0 ∧ ⇑(LieModule.Weight.toLinear K (↥H) L ↑α) = ∑ i : ι, n i • ⇑(b.baseSupp i)

A positive root for the base associated to a Lie algebra basis is a nonzero natural-number combination of the basis's simple roots.

theorem TauCeti.lieBasis_e_mem_rootSpace {ι : Type u_1} {K : Type u_2} {L : Type u_3} [Fintype ι] [CommRing K] [LieRing L] [LieAlgebra K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (b : LieAlgebra.Basis ι H) (i : ι) : b.e i ∈ LieAlgebra.rootSpace H ⇑(b.baseSupp i)

The raising generator eᵢ of a Lie algebra basis is a root vector for its simple root.

theorem TauCeti.lieBasis_f_mem_rootSpace {ι : Type u_1} {K : Type u_2} {L : Type u_3} [Fintype ι] [CommRing K] [LieRing L] [LieAlgebra K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (b : LieAlgebra.Basis ι H) (i : ι) : b.f i ∈ LieAlgebra.rootSpace H (-⇑(b.baseSupp i))

The lowering generator fᵢ of a Lie algebra basis is a root vector for minus its simple root.