Documentation

TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.E7.MinusculeWeight

The minuscule weight orbit of type E7 #

This file enumerates the Weyl orbit of the seventh fundamental weight of the pinned simply connected root datum TauCeti.DynkinType.e7SimplyConnectedRootDatum. The fifty-six weights are expressed in the fundamental-weight basis Fin 7 → ℤ. The first weight is ϖ₇, and the table is closed under the seven Bourbaki-numbered simple reflections through explicit permutations of Fin 56.

The table is the weight diagram of the 56-dimensional minuscule representation. Every simple- coroot coordinate is -1, 0, or 1; the table is exactly the Weyl orbit of ϖ₇; and its weights span the complete character lattice. The spanning statement is the input that lets the weight torus in the eventual integral minuscule carrier be a closed immersion, rather than seeing only the index-two root lattice of the adjoint representation.

Main declarations #

References #

The node numbering and the choice of the minuscule weight ϖ₇ follow Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VI. The 56-dimensional minuscule weight diagram follows J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §13.4, and J. C. Jantzen, Representations of Algebraic Groups, II.2. The formal organization follows the type-E₆ minuscule orbit in TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.E6.MinusculeWeight.

The weight table #

source
def TauCeti.DynkinType.e7MinusculeWeight :
Fin 56 → Fin 7 → ℤ

The fifty-six weights in the Weyl orbit of the type-E₇ minuscule weight ϖ₇.

Coordinates are pairings with the seven Bourbaki-numbered simple coroots. The ordering begins at ϖ₇ = (0, 0, 0, 0, 0, 0, 1) and then lists weights reached successively by simple reflections; no mathematical structure depends on the ordering.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.DynkinType.e7MinusculeWeight_injective :
    Function.Injective e7MinusculeWeight

    The fifty-six minuscule weights are pairwise distinct.

    source
    @[simp]
    theorem TauCeti.DynkinType.e7MinusculeWeight_zero :
    e7MinusculeWeight 0 = Pi.single 6 1

    The first weight in the table is the seventh fundamental weight ϖ₇.

    source
    theorem TauCeti.DynkinType.e7MinusculeWeight_apply_eq_neg_one_or_eq_zero_or_eq_one (a : Fin 56) (i : Fin 7) :
    e7MinusculeWeight a i = -1 ∨ e7MinusculeWeight a i = 0 ∨ e7MinusculeWeight a i = 1

    Every pairing of an E₇ minuscule weight with a simple coroot is -1, 0, or 1.

    Simple reflections #

    source
    def TauCeti.DynkinType.e7MinusculeReflection (i : Fin 7) :
    Equiv.Perm (Fin 56)

    The permutation of the fifty-six minuscule weights induced by the i-th simple reflection.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.DynkinType.e7MinusculeReflection_apply_apply (i : Fin 7) (a : Fin 56) :
      (e7MinusculeReflection i) ((e7MinusculeReflection i) a) = a

      Applying the same simple reflection twice fixes every index in the weight table.

      source
      theorem TauCeti.DynkinType.exists_e7MinusculeWeight_apply_eq_neg_one (i : Fin 7) :
      ∃ (a : Fin 56), e7MinusculeWeight a i = -1

      Every simple coroot has pairing -1 with some minuscule weight.

      source
      theorem TauCeti.DynkinType.exists_e7MinusculeWeight_apply_eq_one (i : Fin 7) :
      ∃ (a : Fin 56), e7MinusculeWeight a i = 1

      Every simple coroot has pairing 1 with some minuscule weight.

      source
      theorem TauCeti.DynkinType.e7MinusculeWeight_reflection (i : Fin 7) (a : Fin 56) :
      e7MinusculeWeight ((e7MinusculeReflection i) a) = e7MinusculeWeight a - e7MinusculeWeight a i • e7Root (e7SimpleIndex i)

      The coordinate equation for a simple reflection on the minuscule weights. Reflection in the i-th simple root subtracts the pairing with the i-th simple coroot times that root.

      source
      @[simp]
      theorem TauCeti.DynkinType.e7MinusculeReflection_eq_self_iff (i : Fin 7) (a : Fin 56) :
      (e7MinusculeReflection i) a = a ↔ e7MinusculeWeight a i = 0

      A simple reflection fixes a minuscule weight exactly when its simple-coroot coordinate is zero.

      source
      @[simp]
      theorem TauCeti.DynkinType.e7SimplyConnectedRootDatum_reflection_e7MinusculeWeight (i : Fin 7) (a : Fin 56) :
      (RootPairing.reflection e7SimplyConnectedRootDatum (e7SimpleIndex i)) (e7MinusculeWeight a) = e7MinusculeWeight ((e7MinusculeReflection i) a)

      The explicit permutation agrees with reflection in the pinned simply connected root datum.

      The Weyl orbit #

      source
      theorem TauCeti.DynkinType.exists_e7MinusculeReflections_eq (a : Fin 56) :
      ∃ (l : List (Fin 7)), List.foldl (fun (b : Fin 56) (i : Fin 7) => (e7MinusculeReflection i) b) 0 l = a

      Every index in the minuscule weight table is reached from the highest-weight index by a finite sequence of simple reflections.

      source
      theorem TauCeti.DynkinType.range_e7MinusculeWeight :
      Set.range e7MinusculeWeight = MulAction.orbit (↥(RootPairing.weylGroup e7SimplyConnectedRootDatum)) (Pi.single 6 1)

      The explicit table is exactly the Weyl orbit of the seventh fundamental weight ϖ₇.

      source
      theorem TauCeti.DynkinType.ncard_orbit_e7MinusculeWeight :
      (MulAction.orbit (↥(RootPairing.weylGroup e7SimplyConnectedRootDatum)) (Pi.single 6 1)).ncard = 56

      The Weyl orbit of ϖ₇ has fifty-six elements.

      Generation of the character lattice #

      source
      theorem TauCeti.DynkinType.span_range_e7MinusculeWeight_eq_top :
      Submodule.span ℤ (Set.range e7MinusculeWeight) = ⊤

      The fifty-six minuscule weights span the full type-E₇ character lattice. In particular, a diagonal torus acting with these weights is represented faithfully.