Generation of the split even orthogonal Lie algebra

This file proves that the positive and negative simple root generators of the split type-D orthogonal Lie algebra generate the whole Lie algebra. The proof first obtains every positive root generator from the positive simple generators. Root-string brackets of the negative simple generators then produce every negative root generator, while mixed simple brackets produce the diagonal Cartan. Finally, the standard block description of the orthogonal Lie algebra decomposes an arbitrary element into its three root-matrix families.

The resulting generation theorem supplies the spanning field for the standard type-D basis and the Lie-algebraic input for its Borel subalgebra.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, §1.8
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §25

theorem TauCeti.TypeDStd.lieSpan_rootGenerator_eq_top {K : Type u_1} [Field K] [NeZero 2] (n : ℕ) (hn : 4 ≤ n) : LieSubalgebra.lieSpan K (↥(LieAlgebra.Orthogonal.typeD (Fin n) K)) ((Set.range fun (i : Fin n) => rootGenerator n hn (Sum.inl i)) ∪ Set.range fun (i : Fin n) => rootGenerator n hn (Sum.inr i)) = ⊤

The positive and negative simple root generators generate the split even orthogonal Lie algebra.