The matrix realization of the type-D Serre presentation

The standard split orthogonal Lie algebra has explicit Bourbaki-numbered raising, lowering, and Cartan generators in TauCeti.TypeDStd. This file packages their bracket relations as a TauCeti.IsSerreSystem and names the resulting homomorphism from the type-D Serre presentation.

Main definitions and results

• TauCeti.TypeDStd.isSerreSystem_rootGenerator: the standard matrix generators form a type-D Serre system.
• TauCeti.TypeDStd.serreRepresentation: the induced homomorphism from the type-D Serre presentation to the split orthogonal Lie algebra.
• TauCeti.TypeDStd.serreRepresentation_serreH, TauCeti.TypeDStd.serreRepresentation_serreE, and TauCeti.TypeDStd.serreRepresentation_serreF: the images of the presented generators.

References

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

@[simp]

theorem TauCeti.TypeDStd.ad_pow_lie_rootGenerator_inl_rootGenerator_inl {K : Type u_1} [CommRing K] (n : ℕ) (hn : 4 ≤ n) (i j : Fin n) : ((LieAlgebra.ad K ↥(LieAlgebra.Orthogonal.typeD (Fin n) K)) (rootGenerator n hn (Sum.inl i)) ^ (-CartanMatrix.D n i j).toNat) ⁅rootGenerator n hn (Sum.inl i), rootGenerator n hn (Sum.inl j)⁆ = 0

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

@[simp]

theorem TauCeti.TypeDStd.ad_pow_lie_rootGenerator_inr_rootGenerator_inr {K : Type u_1} [CommRing K] (n : ℕ) (hn : 4 ≤ n) (i j : Fin n) : ((LieAlgebra.ad K ↥(LieAlgebra.Orthogonal.typeD (Fin n) K)) (rootGenerator n hn (Sum.inr i)) ^ (-CartanMatrix.D n i j).toNat) ⁅rootGenerator n hn (Sum.inr i), rootGenerator n hn (Sum.inr j)⁆ = 0

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

theorem TauCeti.TypeDStd.isSerreSystem_rootGenerator {K : Type u_1} [CommRing K] (n : ℕ) (hn : 4 ≤ n) : IsSerreSystem K (CartanMatrix.D n) (cartanGenerator n hn) (fun (i : Fin n) => rootGenerator n hn (Sum.inl i)) fun (i : Fin n) => rootGenerator n hn (Sum.inr i)

The standard split type-D matrix generators satisfy the Serre relations.

noncomputable def TauCeti.TypeDStd.serreRepresentation {K : Type u_1} [CommRing K] (n : ℕ) (hn : 4 ≤ n) : Matrix.ToLieAlgebra K (CartanMatrix.D n) →ₗ⁅K⁆ ↥(LieAlgebra.Orthogonal.typeD (Fin n) K)

The matrix realization of the type-D Serre presentation, sending the presented Cartan, positive, and negative generators to the corresponding explicit split orthogonal matrices.

Equations

• TauCeti.TypeDStd.serreRepresentation n hn = TauCeti.serreLift ⋯

@[simp]

theorem TauCeti.TypeDStd.serreRepresentation_serreH {K : Type u_1} [CommRing K] (n : ℕ) (hn : 4 ≤ n) (i : Fin n) : (serreRepresentation n hn) (serreH K (CartanMatrix.D n) i) = cartanGenerator n hn i

The matrix realization sends a presented Cartan generator to the corresponding explicit coroot matrix.

@[simp]

theorem TauCeti.TypeDStd.serreRepresentation_serreE {K : Type u_1} [CommRing K] (n : ℕ) (hn : 4 ≤ n) (i : Fin n) : (serreRepresentation n hn) (serreE K (CartanMatrix.D n) i) = rootGenerator n hn (Sum.inl i)

The matrix realization sends a presented positive generator to the corresponding raising matrix.

@[simp]

theorem TauCeti.TypeDStd.serreRepresentation_serreF {K : Type u_1} [CommRing K] (n : ℕ) (hn : 4 ≤ n) (i : Fin n) : (serreRepresentation n hn) (serreF K (CartanMatrix.D n) i) = rootGenerator n hn (Sum.inr i)

The matrix realization sends a presented negative generator to the corresponding lowering matrix.