Documentation

TauCeti.Algebra.Lie.Orthogonal.TypeB.Root.Space

Root-space coordinates for the split odd orthogonal Lie algebra #

The standard coordinates of the split type-B module have weights 0, εᵢ, and -εᵢ. An ambient matrix entry therefore has weight equal to its row weight minus its column weight. This file characterizes generalized root-space membership by those entry weights. These computations are the coordinate input for classifying the roots and matching them to the abstract type-B root datum. TauCeti.Algebra.Lie.Orthogonal.TypeB.Root.AllGenerators locates all five standard root-generator families in their root spaces.

Generalized root spaces are honest simultaneous eigenspaces over a reduced ring. Over a domain, a root vector is supported exactly on entries of the requested weight. Neither statement requires characteristic zero or invertibility of two.

The diagonal-operator argument follows the existing type-D construction in TauCeti.Algebra.Lie.Orthogonal.TypeD.Root.Space, reusing the ambient diagonal action from TauCeti.Algebra.Lie.GeneralLinear.RootSpace.

References #

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

The coordinate weight in the split odd orthogonal module: zero in the middle, followed by εᵢ and -εᵢ on the paired isotropic summands.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.typeBCoordinateWeight_inl {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i : Unit) :
    typeBCoordinateWeight (Sum.inl i) = 0

    The middle coordinate has zero weight.

    source
    @[simp]
    theorem TauCeti.typeBCoordinateWeight_inr_inl {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i : ι) :
    typeBCoordinateWeight (Sum.inr (Sum.inl i)) = typeBEpsilon i

    The first isotropic summand has coordinate weights εᵢ.

    source
    @[simp]
    theorem TauCeti.typeBCoordinateWeight_inr_inr {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i : ι) :
    typeBCoordinateWeight (Sum.inr (Sum.inr i)) = -typeBEpsilon i

    The second isotropic summand has coordinate weights -εᵢ.

    source
    @[simp]
    theorem TauCeti.typeBCoordinateWeight_apply {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (a : Unit ⊕ ι ⊕ ι) (A : ↥(typeBDiagonalCartan K ι)) :
    (typeBCoordinateWeight a) A = ↑↑A a a

    Coordinate weights evaluate as the corresponding diagonal entries.

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

    The weight of a matrix entry is its row weight minus its column weight.

    Equations
    Instances For
      source
      theorem TauCeti.typeBMatrixWeight_def {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (a b : Unit ⊕ ι ⊕ ι) :
      typeBMatrixWeight a b = typeBCoordinateWeight a - typeBCoordinateWeight b

      The defining equation of a matrix-entry weight.

      source
      @[simp]
      theorem TauCeti.typeBMatrixWeight_inl_inr_inl {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (u : Unit) (j : ι) :
      typeBMatrixWeight (Sum.inl u) (Sum.inr (Sum.inl j)) = -typeBEpsilon j

      The middle-to-positive entry has weight -εⱼ.

      source
      @[simp]
      theorem TauCeti.typeBMatrixWeight_inl_inr_inr {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (u : Unit) (j : ι) :
      typeBMatrixWeight (Sum.inl u) (Sum.inr (Sum.inr j)) = typeBEpsilon j

      The middle-to-negative entry has weight εⱼ.

      source
      @[simp]
      theorem TauCeti.typeBMatrixWeight_inr_inl_inl {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i : ι) (u : Unit) :
      typeBMatrixWeight (Sum.inr (Sum.inl i)) (Sum.inl u) = typeBEpsilon i

      The positive-to-middle entry has weight εᵢ.

      source
      @[simp]
      theorem TauCeti.typeBMatrixWeight_inr_inl_inr_inl {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i j : ι) :
      typeBMatrixWeight (Sum.inr (Sum.inl i)) (Sum.inr (Sum.inl j)) = typeBEpsilon i - typeBEpsilon j

      The positive-to-positive entry has weight εᵢ - εⱼ.

      source
      @[simp]
      theorem TauCeti.typeBMatrixWeight_inr_inl_inr_inr {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i j : ι) :
      typeBMatrixWeight (Sum.inr (Sum.inl i)) (Sum.inr (Sum.inr j)) = typeBEpsilon i + typeBEpsilon j

      The positive-to-negative entry has weight εᵢ + εⱼ.

      source
      @[simp]
      theorem TauCeti.typeBMatrixWeight_inr_inr_inl {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i : ι) (u : Unit) :
      typeBMatrixWeight (Sum.inr (Sum.inr i)) (Sum.inl u) = -typeBEpsilon i

      The negative-to-middle entry has weight -εᵢ.

      source
      @[simp]
      theorem TauCeti.typeBMatrixWeight_inr_inr_inr_inl {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i j : ι) :
      typeBMatrixWeight (Sum.inr (Sum.inr i)) (Sum.inr (Sum.inl j)) = -(typeBEpsilon i + typeBEpsilon j)

      The negative-to-positive entry has weight -(εᵢ + εⱼ).

      source
      @[simp]
      theorem TauCeti.typeBMatrixWeight_inr_inr_inr_inr {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (i j : ι) :
      typeBMatrixWeight (Sum.inr (Sum.inr i)) (Sum.inr (Sum.inr j)) = typeBEpsilon j - typeBEpsilon i

      The negative-to-negative entry has weight εⱼ - εᵢ.

      source
      @[simp]
      theorem TauCeti.typeBMatrixWeight_apply {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (a b : Unit ⊕ ι ⊕ ι) (A : ↥(typeBDiagonalCartan K ι)) :
      (typeBMatrixWeight a b) A = ↑↑A a a - ↑↑A b b

      Matrix-entry weights evaluate as differences of diagonal entries.

      source
      @[simp]
      theorem TauCeti.typeBMatrixWeight_self {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (a : Unit ⊕ ι ⊕ ι) :
      typeBMatrixWeight a a = 0

      Diagonal entries have zero weight.

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

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

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

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

      source
      @[simp]
      theorem TauCeti.typeBDiagonalCartan_lie_apply {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] (A : ↥(typeBDiagonalCartan K ι)) (X : Matrix (Unit ⊕ ι ⊕ ι) (Unit ⊕ ι ⊕ ι) K) (a b : Unit ⊕ ι ⊕ ι) :
      ⁅↑↑A, X⁆ a b = (typeBMatrixWeight 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-B subalgebra.

      source
      theorem TauCeti.rootSpace_typeBDiagonalCartan_apply_eq_zero_of_isRegular {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] {χ : Module.Dual K ↥(typeBDiagonalCartan K ι)} {X : ↥(LieAlgebra.Orthogonal.typeB ι K)} (hX : X ∈ LieAlgebra.rootSpace (typeBDiagonalCartan K ι) ⇑χ) (a b : Unit ⊕ ι ⊕ ι) (A : ↥(typeBDiagonalCartan K ι)) (hreg : IsRegular ((typeBMatrixWeight a b) A - χ 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. No reducedness or domain hypothesis is needed.

      source
      theorem TauCeti.mem_rootSpace_typeBDiagonalCartan_of_forall {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] {χ : Module.Dual K ↥(typeBDiagonalCartan K ι)} {X : ↥(LieAlgebra.Orthogonal.typeB ι K)} (h : ∀ (a b : Unit ⊕ ι ⊕ ι), typeBMatrixWeight a b ≠ χ → ↑X a b = 0) :
      X ∈ LieAlgebra.rootSpace (typeBDiagonalCartan K ι) ⇑χ

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

      source
      @[simp]
      theorem TauCeti.mem_rootSpace_typeBDiagonalCartan_iff {K : Type u_1} {ι : Type u_2} [CommRing K] [DecidableEq ι] [Fintype ι] [IsDomain K] (χ : Module.Dual K ↥(typeBDiagonalCartan K ι)) (X : ↥(LieAlgebra.Orthogonal.typeB ι K)) :
      X ∈ LieAlgebra.rootSpace (typeBDiagonalCartan K ι) ⇑χ ↔ ∀ (a b : Unit ⊕ ι ⊕ ι), typeBMatrixWeight a b ≠ χ → ↑X a b = 0

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