Documentation

TauCeti.Algebra.Lie.E6.RootCharacters

Type-E₆ simple-root characters #

The positive and negative numbered Serre generators have the corresponding simple-root characters for the Cartan action. Each positive character is primitive, as witnessed by an explicit Bézout certificate for its row of the type-E₆ Cartan matrix.

These characters and the certificate depend only on the type-E₆ Serre presentation, so they apply to both the minuscule and doubled minuscule carriers.

The root numbering follows N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate V.

source
def TauCeti.E6.rootGeneratorWeight :
Fin 6 ⊕ Fin 6 → Fin 6 → ℤ

The character through which the Cartan torus acts on a positive or negative numbered type-E₆ root generator.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.E6.rootGeneratorWeight_inl (i j : Fin 6) :
    rootGeneratorWeight (Sum.inl i) j = CartanMatrix.E 6 i j
    source
    @[simp]
    theorem TauCeti.E6.rootGeneratorWeight_inr (i j : Fin 6) :
    rootGeneratorWeight (Sum.inr i) j = -CartanMatrix.E 6 i j
    source
    def TauCeti.E6.cartanBezout (i j : Fin 6) :
    ℤ

    A Bézout certificate for the rows of the type-E₆ Cartan matrix: the coefficient -1 at a neighbour of i whose Cartan entry is -1, and 0 elsewhere.

    Equations
    Instances For
      source
      theorem TauCeti.E6.rootGeneratorWeight_sum_mul_cartanBezout (i : Fin 6) :
      ∑ j : Fin 6, rootGeneratorWeight (Sum.inl i) j * cartanBezout i j = 1

      Every positive simple-root character of type E₆ is primitive, with the explicit certificate TauCeti.E6.cartanBezout.

      source
      theorem TauCeti.E6.rootGeneratorWeight_inr_eq_neg_inl (i : Fin 6) :
      rootGeneratorWeight (Sum.inr i) = -rootGeneratorWeight (Sum.inl i)

      The negative simple-root character at a node is the negative of the positive one.

      source
      theorem TauCeti.E6.rootGeneratorWeight_inl_eq_e6Root_e6SimpleIndex (i : Fin 6) :
      rootGeneratorWeight (Sum.inl i) = DynkinType.e6Root (DynkinType.e6SimpleIndex i)

      The character of a raising generator is the corresponding simple root of the pinned simply connected type-E₆ root datum.

      source
      theorem TauCeti.E6.rootGeneratorWeight_inr_eq_neg_e6Root_e6SimpleIndex (i : Fin 6) :
      rootGeneratorWeight (Sum.inr i) = -DynkinType.e6Root (DynkinType.e6SimpleIndex i)

      The character of a lowering generator is the negative of the corresponding simple root.

      source
      theorem TauCeti.E6.lie_serreH_rootGenerator (k : Fin 6 ⊕ Fin 6) (j : Fin 6) :
      ⁅serreH ℚ (CartanMatrix.E 6).transpose j, serreRootGenerator (CartanMatrix.E 6).transpose k⁆ = ↑(rootGeneratorWeight k j) • serreRootGenerator (CartanMatrix.E 6).transpose k

      The numbered Serre root generators are weight vectors for the Cartan generators.