Serre relations in the standard split Lie algebra of type B

The Bourbaki-numbered matrices in TauCeti.Algebra.Lie.Orthogonal.TypeB.RootGenerators give explicit positive-root, negative-root, and coroot generators for the standard integral split orthogonal Lie algebra of type B. This file proves the two families of Serre relations not supplied by the Cartan-action computations:

• positive and negative generators at distinct simple nodes commute;
• the iterated adjoint actions between two positive generators, and between two negative generators, vanish with the exponents prescribed by the type-B Cartan matrix.

All results hold over an arbitrary commutative ring, including in characteristic two. Together with the Cartan-action relations, they package the standard matrices as a TauCeti.IsSerreSystem, the input for mapping the integral Kostant form into the standard type-B representation.

Main results

• TauCeti.typeBSimpleRootGenerator_lie_negative_of_ne: distinct positive and negative simple-root generators commute.
• TauCeti.ad_pow_lie_typeBSimpleRootGenerator_typeBSimpleRootGenerator: the higher positive Serre relations.
• TauCeti.ad_pow_lie_typeBSimpleNegativeRootGenerator_typeBSimpleNegativeRootGenerator: the higher negative Serre relations.
• TauCeti.isSerreSystem_typeBSimpleRootGenerator: the standard type-B generators form a Serre system for the transposed type-B Cartan matrix.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate II.
• J.-P. Serre, Complex Semisimple Lie Algebras, Chapter VI, Appendix.

This supplies the mixed and higher generator relations needed by the Chevalley--Demazure construction and pinnings in Layer 9 of the ReductiveGroups roadmap.

@[simp]

theorem TauCeti.typeBSimpleRootGenerator_lie_negative_of_ne {K : Type u} [CommRing K] {n : ℕ} (i j : Fin (n + 1)) (hij : i ≠ j) : ⁅typeBSimpleRootGenerator i, typeBSimpleNegativeRootGenerator j⁆ = 0

Positive and negative simple-root generators at distinct Bourbaki nodes commute.

@[simp]

theorem TauCeti.ad_pow_lie_typeBSimpleRootGenerator_typeBSimpleRootGenerator {K : Type u} [CommRing K] {n : ℕ} (i j : Fin (n + 1)) : ((LieAlgebra.ad K ↥(LieAlgebra.Orthogonal.typeB (Fin (n + 1)) K)) (typeBSimpleRootGenerator i) ^ (-CartanMatrix.B (n + 1) j i).toNat) ⁅typeBSimpleRootGenerator i, typeBSimpleRootGenerator j⁆ = 0

The higher Serre relation for the positive simple-root generators of the standard split type-B Lie algebra.

@[simp]

theorem TauCeti.ad_pow_lie_typeBSimpleNegativeRootGenerator_typeBSimpleNegativeRootGenerator {K : Type u} [CommRing K] {n : ℕ} (i j : Fin (n + 1)) : ((LieAlgebra.ad K ↥(LieAlgebra.Orthogonal.typeB (Fin (n + 1)) K)) (typeBSimpleNegativeRootGenerator i) ^ (-CartanMatrix.B (n + 1) j i).toNat) ⁅typeBSimpleNegativeRootGenerator i, typeBSimpleNegativeRootGenerator j⁆ = 0

The higher Serre relation for the negative simple-root generators of the standard split type-B Lie algebra.

theorem TauCeti.isSerreSystem_typeBSimpleRootGenerator {K : Type u} [CommRing K] {n : ℕ} : IsSerreSystem K (CartanMatrix.B (n + 1)).transpose typeBSimpleCorootGenerator typeBSimpleRootGenerator typeBSimpleNegativeRootGenerator

The standard type-B Chevalley generators satisfy the Serre relations for the transposed type-B Cartan matrix, in the convention used by IsSerreSystem.