The simple-coroot basis of the split type-B Cartan

The Bourbaki simple coroots of Bₙ₊₁ have diagonal coordinates ε₀ - ε₁, …, εₙ₋₁ - εₙ, 2εₙ. They form a basis of the diagonal Cartan over any commutative ring in which 2 is invertible. This identifies the concrete Cartan with the simple-coroot coordinates used by highest-weight theory, and supplies its independence and Lie-span statements for the construction of a split Lie algebra basis.

The change-of-basis determinant is 2, including in rank one. Thus the ring hypothesis is essential: in characteristic two the final coroot vanishes.

References

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

noncomputable def TauCeti.typeBSimpleCorootBasis {K : Type u_1} [CommRing K] [Invertible 2] (n : ℕ) : Module.Basis (Fin (n + 1)) K ↥(typeBDiagonalCartan K (Fin (n + 1)))

The Bourbaki simple coroots as a basis of the split type-Bₙ₊₁ diagonal Cartan.

Equations

• TauCeti.typeBSimpleCorootBasis n = Module.Basis.mk ⋯ ⋯

@[simp]

theorem TauCeti.coe_typeBSimpleCorootBasis_apply {K : Type u_1} [CommRing K] {n : ℕ} [Invertible 2] (i : Fin (n + 1)) : ↑((typeBSimpleCorootBasis n) i) = typeBSimpleCorootGenerator i

The simple-coroot basis has the existing numbered coroot generators as its vectors.

theorem TauCeti.linearIndependent_typeBSimpleCorootGenerator {K : Type u_1} [CommRing K] {n : ℕ} [Invertible 2] : LinearIndependent K typeBSimpleCorootGenerator

The numbered simple coroots are linearly independent in the split type-B Lie algebra.

theorem TauCeti.typeBDiagonalCartan_eq_lieSpan_typeBSimpleCorootGenerator {K : Type u_1} [CommRing K] {n : ℕ} [Invertible 2] : typeBDiagonalCartan K (Fin (n + 1)) = LieSubalgebra.lieSpan K (↥(LieAlgebra.Orthogonal.typeB (Fin (n + 1)) K)) (Set.range typeBSimpleCorootGenerator)

The Lie subalgebra generated by the simple coroots is the entire diagonal Cartan.