Documentation

TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.E7.Datum

The simply connected root datum of type E₇ #

This file builds the pinned integral root datum of type E₇ on the character and cocharacter lattices Fin 7 → ℤ. The character lattice is written in the fundamental-weight basis and the cocharacter lattice in the simple-coroot basis. Thus the i-th simple root is the i-th row of the Bourbaki-numbered Cartan matrix CartanMatrix.E 7, while the i-th simple coroot is the i-th standard basis vector.

Reflection in a norm-two vector preserves the E₇ Gram form. The completeness theorem TauCeti.DynkinType.exists_e7Coroot_eq therefore supplies the reflected coroot from the pinned enumeration, and Mathlib's RootPairing.mk' constructs the required permutations of the 126 root indices. In particular, no reflection table is needed.

The coroots span their lattice, which is the simply connected condition consumed by the pinned Chevalley--Demazure construction. The roots instead span a sublattice of index two in the weight lattice, as recorded by the determinant of CartanMatrix.E 7.

Main definitions #

Main results #

References #

The coordinates and node numbering follow Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VI, and Humphreys, Introduction to Lie Algebras and Representation Theory, section 12.1. This is the E₇ branch of the target "a named datum per valid type" in Layer 6 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. Its assembly follows the existing E₈ construction in this directory.

Reflection stability #

source
theorem TauCeti.DynkinType.e7Root_dotProduct_e7Coroot_comm (i j : Fin 126) :
e7Root i ⬝ᵥ e7Coroot j = e7Root j ⬝ᵥ e7Coroot i

The pairing of the pinned root and coroot tables is symmetric, as type E₇ is simply laced.

The pinned datum #

source
noncomputable def TauCeti.DynkinType.e7SimplyConnectedRootDatum :
RootDatum (Fin 126) (Fin 7 → ℤ) (Fin 7 → ℤ)

The pinned simply connected root datum of type E₇.

Both lattices are Fin 7 → ℤ: the character lattice in the fundamental-weight basis and the cocharacter lattice in the simple-coroot basis. Root indices 0 through 6 are the Bourbaki simple roots; see TauCeti.DynkinType.root_e7SimpleIndex.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.DynkinType.e7SimplyConnectedRootDatum_root :
    e7SimplyConnectedRootDatum.root = e7Root

    The root embedding of the pinned E₇ datum is the explicit table e7Root.

    source
    @[simp]
    theorem TauCeti.DynkinType.e7SimplyConnectedRootDatum_coroot :
    e7SimplyConnectedRootDatum.coroot = e7Coroot

    The coroot embedding of the pinned E₇ datum is the explicit table e7Coroot.

    source
    @[simp]
    theorem TauCeti.DynkinType.e7SimplyConnectedRootDatum_toLinearMap_apply (x y : Fin 7 → ℤ) :
    (e7SimplyConnectedRootDatum.toLinearMap x) y = x ⬝ᵥ y

    The perfect pairing is the dot product in the dual coordinate bases.

    source
    @[simp]
    theorem TauCeti.DynkinType.e7SimplyConnectedRootDatum_pairing (i j : Fin 126) :
    RootPairing.pairing e7SimplyConnectedRootDatum i j = e7Root i ⬝ᵥ e7Coroot j

    Pairing a pinned E₇ root with a coroot computes as their coordinate dot product.

    The pinned base #

    source
    theorem TauCeti.DynkinType.corootSpan_e7SimplyConnectedRootDatum_eq_top :
    RootPairing.corootSpan e7SimplyConnectedRootDatum ℤ = ⊤

    The coroots of the pinned type E₇ datum span the cocharacter lattice. This is the simply connected lattice condition required by the pinned Chevalley--Demazure construction.

    source
    noncomputable def TauCeti.DynkinType.e7SimplyConnectedBase :
    RootPairing.Base e7SimplyConnectedRootDatum

    The Bourbaki-numbered base of the pinned simply connected root datum of type E₇. Its support is the first seven root indices, carrying the simple roots in Bourbaki order.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.DynkinType.mem_support_e7SimplyConnectedBase {k : Fin 126} :
      k ∈ e7SimplyConnectedBase.support ↔ ↑k < 7

      Membership in the pinned base support is exactly membership among the first seven root indices.

      source
      theorem TauCeti.DynkinType.pairing_e7SimpleIndex (i j : Fin 7) :
      RootPairing.pairing e7SimplyConnectedRootDatum (e7SimpleIndex i) (e7SimpleIndex j) = CartanMatrix.E 7 i j

      The Cartan integers at the first seven root indices are Mathlib's Bourbaki-numbered E₇ matrix.

      source
      theorem TauCeti.DynkinType.hasCartanType_e7SimplyConnectedRootDatum :
      HasCartanType e7SimplyConnectedRootDatum e7SimplyConnectedBase E7

      The pinned datum of type E₇ has Cartan type E7, in Bourbaki node order.