A Lie algebra basis for the split even orthogonal Lie algebra

The diagonal Cartan and the numbered simple-root matrices of the split even orthogonal Lie algebra form a LieAlgebra.Basis. Its Cartan matrix is the type-D Cartan matrix in Bourbaki numbering, its Cartan generators are the diagonal matrices associated to the simple roots, and its raising and lowering generators are the corresponding positive and negative root matrices.

This package makes the concrete matrix realization available to the generic Lie-basis API. In particular, it determines the upper and lower nilpotent subalgebras, proves triangularizability of the Cartan action in characteristic zero, and places the numbered generators in the simple-root spaces.

Main declarations

• TauCeti.TypeDStd.lieBasis: the standard type-D Lie algebra basis.
• TauCeti.TypeDStd.lieBasis_A_eq: its Cartan matrix is CartanMatrix.D n.

References

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

noncomputable def TauCeti.TypeDStd.lieBasis {K : Type u_1} [Field K] [NeZero 2] (n : ℕ) (hn : 4 ≤ n) : LieAlgebra.Basis (Fin n) (typeDDiagonalCartan K (Fin n))

The standard Chevalley-style basis of the split even orthogonal Lie algebra of type Dₙ.

The Cartan matrix and generators use Bourbaki's numbering. The two copies of Fin n indexing rootGenerator distinguish raising from lowering generators.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.TypeDStd.lieBasis_A_eq {K : Type u_1} [Field K] [NeZero 2] (n : ℕ) (hn : 4 ≤ n) : (lieBasis n hn).A = CartanMatrix.D n

The Cartan matrix of the standard split type-D basis is CartanMatrix.D n.

@[simp]

theorem TauCeti.TypeDStd.lieBasis_h {K : Type u_1} [Field K] [NeZero 2] (n : ℕ) (hn : 4 ≤ n) (i : Fin n) : (lieBasis n hn).h i = cartanGenerator n hn i

The Cartan generators of the standard split type-D basis are the numbered diagonal generators.

@[simp]

theorem TauCeti.TypeDStd.lieBasis_e {K : Type u_1} [Field K] [NeZero 2] (n : ℕ) (hn : 4 ≤ n) (i : Fin n) : (lieBasis n hn).e i = rootGenerator n hn (Sum.inl i)

The raising generators of the standard split type-D basis are the positive simple-root generators.

@[simp]

theorem TauCeti.TypeDStd.lieBasis_f {K : Type u_1} [Field K] [NeZero 2] (n : ℕ) (hn : 4 ≤ n) (i : Fin n) : (lieBasis n hn).f i = rootGenerator n hn (Sum.inr i)

The lowering generators of the standard split type-D basis are the negative simple-root generators.