The simple-root generators of the split type-D Cartan

The explicit type-D Chevalley generators use the Bourbaki simple roots as diagonal coordinates. This file records the ambient independence and Lie-span results for those generators, so later split-Cartan constructions can use them as simple-root coordinates. The generator membership and coordinate lemmas live with the generator definitions in Root/Generators.lean.

Independence over a commutative domain in which 2 is nonzero comes from DynkinType.linearIndependent_typeDSimpleRoot_cast: the doubled fundamental coweights pair with the simple roots diagonally by 2, which is regular in such a domain. The ambient independence and Lie-span theorems then expose the resulting split Cartan structure.

Main declarations

• TypeDStd.linearIndependent_cartanGenerator: the ambient Cartan generators are independent.
• TypeDStd.typeDDiagonalCartan_eq_lieSpan_cartanGenerator: they span the diagonal Cartan as a Lie subalgebra.

References

• N. Bourbaki, Groupes et algèbres de Lie, Chapters 4--6, Plate IV.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §13.

theorem TauCeti.TypeDStd.linearIndependent_cartanGenerator {K : Type u_1} [CommRing K] [IsDomain K] [NeZero 2] (n : ℕ) (hn : 4 ≤ n) : LinearIndependent K (cartanGenerator n hn)

The explicit simple-root Cartan generators are linearly independent in the ambient type-D Lie algebra.

theorem TauCeti.TypeDStd.typeDDiagonalCartan_eq_lieSpan_cartanGenerator {K : Type u_1} [Field K] [NeZero 2] (n : ℕ) (hn : 4 ≤ n) : typeDDiagonalCartan K (Fin n) = LieSubalgebra.lieSpan K (↥(LieAlgebra.Orthogonal.typeD (Fin n) K)) (Set.range (cartanGenerator n hn))

The explicit simple-root Cartan generators span the diagonal Cartan as a Lie subalgebra.