Roots of the split even orthogonal Lie algebra

This file classifies the nonzero roots of the split type-D Lie algebra relative to its diagonal Cartan. The coordinate-difference root εᵢ - εⱼ is spanned by the standard paired diagonal-block matrix, while εᵢ + εⱼ and -εᵢ - εⱼ are spanned by the standard skew matrices in the two off-diagonal blocks. Conversely, every nonzero functional whose root space is nontrivial belongs to one of these three families.

These line descriptions provide the concrete root spaces needed to describe the positive nilradical, construct a compatible Borel subalgebra, and match the resulting split Cartan data to the abstract type-D root datum.

Main results

• TauCeti.TypeDStd.rootSpace_typeDWeightSub_eq_span: the root space of εᵢ - εⱼ is the line through differenceRootGenerator i j.
• TauCeti.TypeDStd.rootSpace_typeDWeightAdd_eq_span: the root space of εᵢ + εⱼ is the line through sumRootGenerator i j.
• TauCeti.TypeDStd.rootSpace_neg_typeDWeightAdd_eq_span: the root space of -εᵢ - εⱼ is the line through negSumRootGenerator i j.
• TauCeti.TypeDStd.rootSpace_typeDDiagonalCartan_ne_bot_iff: the three displayed families exhaust the nonzero roots.

References

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

Root-space lines

@[simp]

theorem TauCeti.TypeDStd.rootSpace_typeDWeightSub_eq_span {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] [Nontrivial K] (h2 : IsRegular 2) {i j : ι} (hij : i ≠ j) : ↑(LieAlgebra.rootSpace (typeDDiagonalCartan K ι) ⇑(typeDWeightSub i j)) = K ∙ differenceRootGenerator i j

Over a nontrivial ring in which 2 is regular, the root space of εᵢ - εⱼ, for i ≠ j, is the line through the standard difference-root generator.

@[simp]

theorem TauCeti.TypeDStd.rootSpace_typeDWeightAdd_eq_span {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] [Nontrivial K] (h2 : IsRegular 2) {i j : ι} (hij : i ≠ j) : ↑(LieAlgebra.rootSpace (typeDDiagonalCartan K ι) ⇑(typeDWeightAdd i j)) = K ∙ sumRootGenerator i j

Over a nontrivial ring in which 2 is regular, the root space of εᵢ + εⱼ, for i ≠ j, is the line through the standard positive sum-root generator.

@[simp]

theorem TauCeti.TypeDStd.rootSpace_neg_typeDWeightAdd_eq_span {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] [Nontrivial K] (h2 : IsRegular 2) {i j : ι} (hij : i ≠ j) : ↑(LieAlgebra.rootSpace (typeDDiagonalCartan K ι) (-⇑(typeDWeightAdd i j))) = K ∙ negSumRootGenerator i j

Over a nontrivial ring in which 2 is regular, the root space of -εᵢ - εⱼ, for i ≠ j, is the line through the standard negative sum-root generator.

Exhaustion of the nonzero roots

theorem TauCeti.TypeDStd.rootSpace_typeDDiagonalCartan_ne_bot_iff {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] [IsDomain K] (h2 : 2 ≠ 0) (chi : Module.Dual K ↥(typeDDiagonalCartan K ι)) (hchi : chi ≠ 0) : LieAlgebra.rootSpace (typeDDiagonalCartan K ι) ⇑chi ≠ ⊥ ↔ ∃ (i : ι) (j : ι), i ≠ j ∧ (chi = typeDWeightSub i j ∨ chi = typeDWeightAdd i j ∨ chi = -typeDWeightAdd i j)

The nonzero roots of the split even orthogonal Lie algebra are exactly the type-D roots.

Over a domain away from characteristic two, a nonzero functional on the diagonal Cartan has a nontrivial root space precisely when it is εᵢ - εⱼ, εᵢ + εⱼ, or -εᵢ - εⱼ for two distinct coordinates.

Dimensions

@[simp]

theorem TauCeti.TypeDStd.finrank_rootSpace_typeDWeightSub_eq_one {ι : Type u_2} [DecidableEq ι] [Fintype ι] {K : Type u_3} [Field K] (h2 : 2 ≠ 0) {i j : ι} (hij : i ≠ j) : Module.finrank K ↥(LieAlgebra.rootSpace (typeDDiagonalCartan K ι) ⇑(typeDWeightSub i j)) = 1

Over a field away from characteristic two, the root space of a coordinate-difference root εᵢ - εⱼ with i ≠ j has dimension one.

@[simp]

theorem TauCeti.TypeDStd.finrank_rootSpace_typeDWeightAdd_eq_one {ι : Type u_2} [DecidableEq ι] [Fintype ι] {K : Type u_3} [Field K] (h2 : 2 ≠ 0) {i j : ι} (hij : i ≠ j) : Module.finrank K ↥(LieAlgebra.rootSpace (typeDDiagonalCartan K ι) ⇑(typeDWeightAdd i j)) = 1

Over a field away from characteristic two, the root space of a positive coordinate-sum root εᵢ + εⱼ with i ≠ j has dimension one.

@[simp]

theorem TauCeti.TypeDStd.finrank_rootSpace_neg_typeDWeightAdd_eq_one {ι : Type u_2} [DecidableEq ι] [Fintype ι] {K : Type u_3} [Field K] (h2 : 2 ≠ 0) {i j : ι} (hij : i ≠ j) : Module.finrank K ↥(LieAlgebra.rootSpace (typeDDiagonalCartan K ι) (-⇑(typeDWeightAdd i j))) = 1

Over a field away from characteristic two, the root space of a negative coordinate-sum root -εᵢ - εⱼ with i ≠ j has dimension one.