Root spaces of the split even orthogonal Lie algebra

This file computes the root spaces of LieAlgebra.Orthogonal.typeD ι K relative to its diagonal Cartan subalgebra. The two copies of ι in the hyperbolic basis have coordinate weights εᵢ and -εᵢ. Hence a matrix entry in position (a, b) has weight equal to the difference of those two signed coordinate weights.

Over a reduced ring, generalized root spaces are honest simultaneous eigenspaces because each Cartan element acts diagonally on the ambient matrix units. This identifies the root space with the corresponding weight space. The support implication from entries of the requested signed weight to root-space membership holds over any commutative ring; the converse implication, from root-space membership to entrywise support, uses the stronger hypothesis that the coefficient ring is a domain.

Main results

• TauCeti.rootSpace_typeDDiagonalCartan_eq_weightSpace: generalized root spaces are honest simultaneous eigenspaces.
• TauCeti.mem_rootSpace_typeDDiagonalCartan_iff: over a domain, membership is equivalent to entrywise support on positions of the requested weight.

The diagonal action on ambient matrix units reduces generalized root-space membership to ordinary eigenvector equations over a reduced ring, after which those equations become entrywise support conditions for the signed matrix weights.

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.

Signed coordinate weights

noncomputable def TauCeti.typeDCoordinateWeight {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (a : ι ⊕ ι) : Module.Dual K ↥(typeDDiagonalCartan K ι)

The weight of a hyperbolic coordinate: εᵢ on the first summand and -εᵢ on the second.

Equations

• TauCeti.typeDCoordinateWeight (Sum.inl i) = TauCeti.typeDEpsilon i
• TauCeti.typeDCoordinateWeight (Sum.inr i) = -TauCeti.typeDEpsilon i

@[simp]

theorem TauCeti.typeDCoordinateWeight_inl {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i : ι) : typeDCoordinateWeight (Sum.inl i) = typeDEpsilon i

The signed coordinate weight on the first summand is εᵢ.

@[simp]

theorem TauCeti.typeDCoordinateWeight_inr {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i : ι) : typeDCoordinateWeight (Sum.inr i) = -typeDEpsilon i

The signed coordinate weight on the second summand is -εᵢ.

noncomputable def TauCeti.typeDMatrixWeight {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (a b : ι ⊕ ι) : Module.Dual K ↥(typeDDiagonalCartan K ι)

The weight of the matrix entry (a, b), namely the difference of its signed coordinate weights.

Equations

• TauCeti.typeDMatrixWeight a b = TauCeti.typeDCoordinateWeight a - TauCeti.typeDCoordinateWeight b

theorem TauCeti.typeDMatrixWeight_def {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (a b : ι ⊕ ι) : typeDMatrixWeight a b = typeDCoordinateWeight a - typeDCoordinateWeight b

The matrix-entry weight is the difference of its two signed coordinate weights.

@[simp]

theorem TauCeti.typeDCoordinateWeight_apply {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (a : ι ⊕ ι) (A : ↥(typeDDiagonalCartan K ι)) : (typeDCoordinateWeight a) A = ↑↑A a a

The signed coordinate weight evaluates through the corresponding diagonal entry.

@[simp]

theorem TauCeti.typeDMatrixWeight_apply {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (a b : ι ⊕ ι) (A : ↥(typeDDiagonalCartan K ι)) : (typeDMatrixWeight a b) A = ↑↑A a a - ↑↑A b b

The matrix-entry weight evaluates as the difference of the two signed diagonal coordinates.

noncomputable def TauCeti.typeDWeightSub {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i j : ι) : Module.Dual K ↥(typeDDiagonalCartan K ι)

The coordinate-difference weight εᵢ - εⱼ on the split diagonal Cartan.

Equations

• TauCeti.typeDWeightSub i j = TauCeti.typeDEpsilon i - TauCeti.typeDEpsilon j

theorem TauCeti.typeDWeightSub_def {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i j : ι) : typeDWeightSub i j = typeDEpsilon i - typeDEpsilon j

The coordinate-difference weight unfolds to εᵢ - εⱼ.

noncomputable def TauCeti.typeDWeightAdd {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i j : ι) : Module.Dual K ↥(typeDDiagonalCartan K ι)

The coordinate-sum weight εᵢ + εⱼ on the split diagonal Cartan.

Equations

• TauCeti.typeDWeightAdd i j = TauCeti.typeDEpsilon i + TauCeti.typeDEpsilon j

theorem TauCeti.typeDWeightAdd_def {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i j : ι) : typeDWeightAdd i j = typeDEpsilon i + typeDEpsilon j

The coordinate-sum weight unfolds to εᵢ + εⱼ.

theorem TauCeti.typeDWeightAdd_comm {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i j : ι) : typeDWeightAdd i j = typeDWeightAdd j i

Coordinate-sum weights are unchanged when their two coordinates are swapped.

@[simp]

theorem TauCeti.typeDWeightSub_apply {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i j : ι) (A : ↥(typeDDiagonalCartan K ι)) : (typeDWeightSub i j) A = ↑↑A (Sum.inl i) (Sum.inl i) - ↑↑A (Sum.inl j) (Sum.inl j)

The coordinate-difference weight evaluates as the difference of the corresponding diagonal entries.

@[simp]

theorem TauCeti.typeDWeightAdd_apply {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i j : ι) (A : ↥(typeDDiagonalCartan K ι)) : (typeDWeightAdd i j) A = ↑↑A (Sum.inl i) (Sum.inl i) + ↑↑A (Sum.inl j) (Sum.inl j)

The coordinate-sum weight evaluates as the sum of the corresponding diagonal entries.

@[simp]

theorem TauCeti.typeDWeightSub_self {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i : ι) : typeDWeightSub i i = 0

A coordinate-difference weight vanishes when its two coordinates agree.

@[simp]

theorem TauCeti.typeDMatrixWeight_self {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (a : ι ⊕ ι) : typeDMatrixWeight a a = 0

The matrix-entry weight on a diagonal entry is the zero functional.

@[simp]

theorem TauCeti.typeDMatrixWeight_inl_inl {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i j : ι) : typeDMatrixWeight (Sum.inl i) (Sum.inl j) = typeDWeightSub i j

The (inl i, inl j) matrix-entry weight is the coordinate difference εᵢ - εⱼ.

@[simp]

theorem TauCeti.typeDMatrixWeight_inl_inr {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i j : ι) : typeDMatrixWeight (Sum.inl i) (Sum.inr j) = typeDWeightAdd i j

The (inl i, inr j) matrix-entry weight is the coordinate sum εᵢ + εⱼ.

@[simp]

theorem TauCeti.typeDMatrixWeight_inr_inl {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i j : ι) : typeDMatrixWeight (Sum.inr i) (Sum.inl j) = -typeDWeightAdd i j

The (inr i, inl j) matrix-entry weight is the negative coordinate-sum weight.

@[simp]

theorem TauCeti.typeDMatrixWeight_inr_inr {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i j : ι) : typeDMatrixWeight (Sum.inr i) (Sum.inr j) = typeDWeightSub j i

The (inr i, inr j) matrix-entry weight is the reversed coordinate-difference weight.

Distinctness of the three root families

@[simp]

theorem TauCeti.typeDWeightSub_eq_typeDWeightSub_iff {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (h2 : 2 ≠ 0) {i j : ι} (hij : i ≠ j) (a b : ι) : typeDWeightSub a b = typeDWeightSub i j ↔ a = i ∧ b = j

Away from characteristic two, the nonzero coordinate-difference weights are pairwise distinct as ordered pairs.

@[simp]

theorem TauCeti.typeDWeightAdd_eq_typeDWeightAdd_iff {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] [Nontrivial K] {i j : ι} (hij : i ≠ j) (a b : ι) : typeDWeightAdd a b = typeDWeightAdd i j ↔ a = i ∧ b = j ∨ a = j ∧ b = i

Over a nontrivial ring, two coordinate-sum roots agree exactly when their unordered pairs of distinct coordinates agree.

@[simp]

theorem TauCeti.typeDWeightSub_ne_typeDWeightAdd {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (h2 : 2 ≠ 0) (a b i j : ι) : typeDWeightSub a b ≠ typeDWeightAdd i j

A coordinate-difference weight is never a coordinate-sum weight away from characteristic two.

@[simp]

theorem TauCeti.neg_typeDWeightAdd_ne_typeDWeightAdd {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (h2 : 2 ≠ 0) {i j : ι} (hij : i ≠ j) (a b : ι) : -typeDWeightAdd a b ≠ typeDWeightAdd i j

Away from characteristic two, a negative coordinate-sum weight is never a positive coordinate-sum weight whose coordinates are distinct.

@[simp]

theorem TauCeti.neg_typeDWeightAdd_ne_typeDWeightSub {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (h2 : 2 ≠ 0) (a b i j : ι) : -typeDWeightAdd a b ≠ typeDWeightSub i j

A negative coordinate-sum weight is never a coordinate-difference weight away from characteristic two.

Matrix positions carrying each root

@[simp]

theorem TauCeti.typeDMatrixWeight_eq_typeDWeightSub_iff {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (h2 : 2 ≠ 0) {i j : ι} (hij : i ≠ j) (a b : ι ⊕ ι) : typeDMatrixWeight a b = typeDWeightSub i j ↔ a = Sum.inl i ∧ b = Sum.inl j ∨ a = Sum.inr j ∧ b = Sum.inr i

The two matrix positions of weight εᵢ - εⱼ in the split type-D model.

@[simp]

theorem TauCeti.typeDMatrixWeight_eq_typeDWeightAdd_iff {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (h2 : 2 ≠ 0) {i j : ι} (hij : i ≠ j) (a b : ι ⊕ ι) : typeDMatrixWeight a b = typeDWeightAdd i j ↔ a = Sum.inl i ∧ b = Sum.inr j ∨ a = Sum.inl j ∧ b = Sum.inr i

The two matrix positions of weight εᵢ + εⱼ in the split type-D model.

@[simp]

theorem TauCeti.typeDMatrixWeight_eq_neg_typeDWeightAdd_iff {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (h2 : 2 ≠ 0) {i j : ι} (hij : i ≠ j) (a b : ι ⊕ ι) : typeDMatrixWeight a b = -typeDWeightAdd i j ↔ a = Sum.inr i ∧ b = Sum.inl j ∨ a = Sum.inr j ∧ b = Sum.inl i

The two matrix positions of weight -εᵢ - εⱼ in the split type-D model.

Honest weight spaces and entrywise support

theorem TauCeti.toEnd_typeDDiagonalCartan_matrix_eq_toLin_diagonal {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (A : ↥(typeDDiagonalCartan K ι)) : (LieModule.toEnd K (↥(typeDDiagonalCartan K ι)) (Matrix (ι ⊕ ι) (ι ⊕ ι) K)) A = (Matrix.toLin (Matrix.stdBasis K (ι ⊕ ι) (ι ⊕ ι)) (Matrix.stdBasis K (ι ⊕ ι) (ι ⊕ ι))) (Matrix.diagonal fun (p : (ι ⊕ ι) × (ι ⊕ ι)) => (typeDMatrixWeight p.1 p.2) A)

The adjoint action of an element of the split diagonal Cartan is diagonal in the ambient matrix-unit basis.

theorem TauCeti.rootSpace_typeDDiagonalCartan_eq_weightSpace {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] [IsReduced K] (χ : Module.Dual K ↥(typeDDiagonalCartan K ι)) : LieAlgebra.rootSpace (typeDDiagonalCartan K ι) ⇑χ = LieModule.weightSpace ↥(LieAlgebra.Orthogonal.typeD ι K) ⇑χ

Over a reduced ring, the root spaces for the split diagonal Cartan are honest simultaneous eigenspaces rather than merely generalized eigenspaces.

@[simp]

theorem TauCeti.typeDDiagonalCartan_lie_apply {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (A : ↥(typeDDiagonalCartan K ι)) (X : Matrix (ι ⊕ ι) (ι ⊕ ι) K) (a b : ι ⊕ ι) : ⁅↑↑A, X⁆ a b = (typeDMatrixWeight a b) A * X a b

The diagonal Cartan acts on each ambient matrix entry through its signed coordinate-difference weight. The matrix need not itself lie in the type-D subalgebra.

theorem TauCeti.rootSpace_typeDDiagonalCartan_apply_eq_zero_of_isRegular {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] {chi : Module.Dual K ↥(typeDDiagonalCartan K ι)} {X : ↥(LieAlgebra.Orthogonal.typeD ι K)} (hX : X ∈ LieAlgebra.rootSpace (typeDDiagonalCartan K ι) ⇑chi) (a b : ι ⊕ ι) (A : ↥(typeDDiagonalCartan K ι)) (hreg : IsRegular ((typeDMatrixWeight a b) A - chi A)) : ↑X a b = 0

An entry of a generalized root vector vanishes when its weight difference from the root is regular at some element of the diagonal Cartan.

theorem TauCeti.mem_rootSpace_typeDDiagonalCartan_of_forall {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] {χ : Module.Dual K ↥(typeDDiagonalCartan K ι)} {X : ↥(LieAlgebra.Orthogonal.typeD ι K)} (h : ∀ (a b : ι ⊕ ι), typeDMatrixWeight a b ≠ χ → ↑X a b = 0) : X ∈ LieAlgebra.rootSpace (typeDDiagonalCartan K ι) ⇑χ

A type-D matrix supported on entries of weight χ belongs to the χ root space.

@[simp]

theorem TauCeti.mem_rootSpace_typeDDiagonalCartan_iff {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] [IsDomain K] (χ : Module.Dual K ↥(typeDDiagonalCartan K ι)) (X : ↥(LieAlgebra.Orthogonal.typeD ι K)) : X ∈ LieAlgebra.rootSpace (typeDDiagonalCartan K ι) ⇑χ ↔ ∀ (a b : ι ⊕ ι), typeDMatrixWeight a b ≠ χ → ↑X a b = 0

Over a domain, a matrix in the split type-D Lie algebra belongs to the root space of χ exactly when all entries whose signed coordinate difference is not χ vanish.