The roots of the split even orthogonal Lie algebra as a type-D root datum

The roots of the split even orthogonal Lie algebra relative to its diagonal Cartan are already classified in coordinate form as εᵢ - εⱼ, εᵢ + εⱼ, and -εᵢ - εⱼ. This file indexes those functionals by the full root enumeration of the pinned simply connected type-D root datum.

For a classical root vector x, the corresponding Cartan functional has diagonal coordinates x. Evaluating it on the numbered Cartan generator associated to a simple root αⱼ therefore gives the dot product x · αⱼ. These are exactly the fundamental-weight coordinates used by the pinned root datum. Over a nontrivial coefficient ring, every enumerated functional has a nonzero root space. The enumeration is injective when 2 ≠ 0, and over an integral domain with 2 ≠ 0 it exhausts every nonzero concrete root.

Main declarations

• TauCeti.TypeDStd.typeDRootWeight: the Cartan functional indexed by a root of the pinned type-D datum.
• TauCeti.TypeDStd.typeDWeightEquiv_symm_typeDRootWeight: its diagonal-basis coordinates are the corresponding classical root vector.
• TauCeti.TypeDStd.typeDRootWeight_apply_cartanGenerator: its coordinates on the numbered Cartan generators are the coordinates of the corresponding abstract root.
• TauCeti.TypeDStd.rootSpace_typeDDiagonalCartan_ne_bot_iff_exists_eq_typeDRootWeight: every nonzero root of the concrete diagonal Cartan occurs exactly in this enumeration.

References

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

noncomputable def TauCeti.TypeDStd.typeDRootWeight {K : Type u_1} [CommRing K] (n : ℕ) (hn : 4 ≤ n) (k : Fin (2 * n * (n - 1))) : Module.Dual K ↥(typeDDiagonalCartan K (Fin n))

The concrete diagonal-Cartan functional indexed by the k-th root of the pinned type-D root datum. Its diagonal coordinates are the corresponding classical root vector.

Equations

• TauCeti.TypeDStd.typeDRootWeight n hn k = TauCeti.typeDWeightEquiv fun (i : Fin n) => ↑(↑((TauCeti.DynkinType.typeDRootEquiv n hn) k) i)

@[simp]

theorem TauCeti.TypeDStd.typeDWeightEquiv_symm_typeDRootWeight {K : Type u_1} [CommRing K] (n : ℕ) (hn : 4 ≤ n) (k : Fin (2 * n * (n - 1))) : typeDWeightEquiv.symm (typeDRootWeight n hn k) = fun (i : Fin n) => ↑(↑((DynkinType.typeDRootEquiv n hn) k) i)

The diagonal-basis coordinates of the Cartan functional indexed by k are the corresponding classical type-D root vector.

@[simp]

theorem TauCeti.TypeDStd.typeDRootWeight_apply_cartanGenerator {K : Type u_1} [CommRing K] (n : ℕ) (hn : 4 ≤ n) (k : Fin (2 * n * (n - 1))) (j : Fin n) : (typeDRootWeight n hn k) ⟨cartanGenerator n hn j, ⋯⟩ = ↑((DynkinType.typeDSimplyConnectedRootDatum n hn).root k j)

The Cartan functional indexed by k, evaluated on the j-th numbered Cartan generator, is the j-th fundamental-weight coordinate of the k-th root of the pinned type-D datum.

theorem TauCeti.TypeDStd.typeDRootWeight_injective {K : Type u_1} [CommRing K] (n : ℕ) (hn : 4 ≤ n) (h2 : 2 ≠ 0) : Function.Injective (typeDRootWeight n hn)

Away from characteristic two, distinct roots of the pinned type-D datum give distinct concrete Cartan functionals.

theorem TauCeti.TypeDStd.typeDRootWeight_ne_zero {K : Type u_1} [CommRing K] (n : ℕ) (hn : 4 ≤ n) [Nontrivial K] (k : Fin (2 * n * (n - 1))) : typeDRootWeight n hn k ≠ 0

Every functional in the concrete type-D root enumeration is nonzero.

theorem TauCeti.TypeDStd.rootSpace_typeDRootWeight_ne_bot {K : Type u_1} [CommRing K] (n : ℕ) (hn : 4 ≤ n) [Nontrivial K] (k : Fin (2 * n * (n - 1))) : LieAlgebra.rootSpace (typeDDiagonalCartan K (Fin n)) ⇑(typeDRootWeight n hn k) ≠ ⊥

Every root in the pinned type-D enumeration has a nontrivial root space in the concrete split orthogonal Lie algebra.

theorem TauCeti.TypeDStd.rootSpace_typeDDiagonalCartan_ne_bot_iff_exists_eq_typeDRootWeight {K : Type u_1} [CommRing K] (n : ℕ) (hn : 4 ≤ n) (chi : Module.Dual K ↥(typeDDiagonalCartan K (Fin n))) [IsDomain K] (h2 : 2 ≠ 0) (hchi : chi ≠ 0) : LieAlgebra.rootSpace (typeDDiagonalCartan K (Fin n)) ⇑chi ≠ ⊥ ↔ ∃ (k : Fin (2 * n * (n - 1))), chi = typeDRootWeight n hn k

The nonzero roots of the concrete split diagonal Cartan are exactly the roots of the pinned type-D root datum. The index on the right is the datum's full root index, and typeDRootWeight_apply_cartanGenerator identifies its fundamental-weight coordinates.