Generation of the split odd orthogonal Lie algebra

This file proves that the positive and negative Bourbaki simple-root generators of the split type-B orthogonal Lie algebra generate the whole Lie algebra. Successive brackets along the long-root chain first produce every difference-root vector. Bracketing these with the terminal short-root vectors produces all short roots, and brackets between short roots then supply both families of long sum roots. Matching positive and negative short roots span the diagonal Cartan.

Finally, the standard block description of a matrix skew-adjoint for LieAlgebra.Orthogonal.JB decomposes an arbitrary element into the diagonal, short-root, difference-root, and sum-root families. The resulting generation theorem is the spanning input for the standard type-B Lie basis and its upper Borel.

Main declaration

• lieSpan_range_typeBSimpleRootGenerator_union_range_typeBSimpleNegativeRootGenerator_eq_top: the numbered positive and negative simple root generators span the split type-B Lie algebra.

References

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

theorem TauCeti.lieSpan_range_typeBSimpleRootGenerator_union_range_typeBSimpleNegativeRootGenerator_eq_top {K : Type u_1} [Field K] [NeZero 2] (n : ℕ) : LieSubalgebra.lieSpan K (↥(LieAlgebra.Orthogonal.typeB (Fin (n + 1)) K)) (Set.range typeBSimpleRootGenerator ∪ Set.range typeBSimpleNegativeRootGenerator) = ⊤

The positive and negative Bourbaki simple-root generators generate the split odd orthogonal Lie algebra of type B.