Documentation

TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.E8.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 8 → ℤ, out of the enumeration of the two hundred and forty roots in TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.E8.Basic. The character lattice is written in the fundamental-weight basis and the cocharacter lattice in the simple-coroot basis, so that the i-th simple root is the i-th row of the Bourbaki-numbered Cartan matrix CartanMatrix.E 8 and the i-th simple coroot is the i-th standard basis vector.

Reflection stability #

Reflection in a norm-two vector preserves the E₈ Gram form of the simple-coroot basis (TauCeti.reflect_vecMul_dotProduct_self, which needs nothing beyond symmetry of the matrix), so it maps norm-two vectors to norm-two vectors. The enumeration exhausts the norm-two vectors (TauCeti.DynkinType.exists_e8Coroot_eq), and hence the root and coroot families are stable under reflection. Mathlib's RootPairing.mk' then constructs the permutations of Fin 240 required by a root datum, without a two hundred and forty by two hundred and forty table.

The lattices #

Both families span their lattice here, so the datum carries a RootPairing.IsRootSystem instance: the roots by TauCeti.DynkinType.span_root_e8SimplyConnectedRootDatum_eq_top and the coroots by TauCeti.DynkinType.corootSpan_e8SimplyConnectedRootDatum_eq_top. It is the coroot half that the pinned Chevalley--Demazure construction consumes as its simply connected condition, and the datum is stated through that same coroot-side condition as its siblings, which is what the per-type dispatcher will collect. The root half is particular to E₈, one of the three types — with F₄ and G₂ — whose Cartan determinant is 1: its root lattice is already the whole weight lattice and the simply connected form is also the adjoint one. The F₄ and G₂ files carry an instance for that same reason. In the files of the remaining types, whose Cartan determinant is greater than 1, the roots span only the root lattice, sitting inside the weight lattice at the index recorded by that determinant, and no such instance exists.

Main definitions #

Main results #

References #

The coordinates and the node numbering follow Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VII, 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 TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.E6.Basic.

Reflection stability #

source
theorem TauCeti.DynkinType.e8Root_dotProduct_e8Coroot_comm (i j : Fin 240) :
e8Root i ⬝ᵥ e8Coroot j = e8Root j ⬝ᵥ e8Coroot i

The pairing of the pinned tables is symmetric. This is the simply-laced feature of E₈: both sides are the value at the simple-coroot coordinates of the symmetric form carried by CartanMatrix.E 8.

The pinned datum #

source
noncomputable def TauCeti.DynkinType.e8SimplyConnectedRootDatum :
RootDatum (Fin 240) (Fin 8 → ℤ) (Fin 8 → ℤ)

The pinned simply connected root datum of type E₈.

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

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

    The root embedding of the pinned E₈ datum is the explicit table e8Root.

    source
    @[simp]
    theorem TauCeti.DynkinType.e8SimplyConnectedRootDatum_coroot :
    e8SimplyConnectedRootDatum.coroot = e8Coroot

    The coroot embedding of the pinned E₈ datum is the explicit table e8Coroot.

    source
    @[simp]
    theorem TauCeti.DynkinType.e8SimplyConnectedRootDatum_toLinearMap_apply (x y : Fin 8 → ℤ) :
    (e8SimplyConnectedRootDatum.toLinearMap x) y = x ⬝ᵥ y

    The perfect pairing of the pinned E₈ datum is the dot product of coordinate vectors, the fundamental-weight and simple-coroot bases being dual to one another.

    source
    @[simp]
    theorem TauCeti.DynkinType.e8SimplyConnectedRootDatum_pairing (i j : Fin 240) :
    RootPairing.pairing e8SimplyConnectedRootDatum i j = e8Root i ⬝ᵥ e8Coroot j

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

    source
    theorem TauCeti.DynkinType.span_root_e8SimplyConnectedRootDatum_eq_top :
    Submodule.span ℤ (Set.range ⇑e8SimplyConnectedRootDatum.root) = ⊤

    The roots of the pinned type E₈ datum span the character lattice. The simple roots are the rows of the type E₈ Cartan matrix, whose determinant is 1, so its row map is surjective over ℤ. This is the integral distinction between E₈ and the other simply laced exceptional types: here the root lattice is already the full weight lattice.

    The pinned base #

    source
    theorem TauCeti.DynkinType.corootSpan_e8SimplyConnectedRootDatum_eq_top :
    RootPairing.corootSpan e8SimplyConnectedRootDatum ℤ = ⊤

    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
    instance TauCeti.DynkinType.instIsRootSystemFinOfNatNatIntForallE8SimplyConnectedRootDatum :
    RootPairing.IsRootSystem e8SimplyConnectedRootDatum

    The pinned type E₈ datum is a root system over ℤ: both its root and coroot families span their respective lattices.

    source
    noncomputable def TauCeti.DynkinType.e8SimplyConnectedBase :
    RootPairing.Base e8SimplyConnectedRootDatum

    The Bourbaki-numbered base of the pinned simply connected root datum of type E₈. Its support is the set of the first eight 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_e8SimplyConnectedBase {k : Fin 240} :
      k ∈ e8SimplyConnectedBase.support ↔ ↑k < 8

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

      source
      theorem TauCeti.DynkinType.pairing_e8SimpleIndex (i j : Fin 8) :
      RootPairing.pairing e8SimplyConnectedRootDatum (e8SimpleIndex i) (e8SimpleIndex j) = CartanMatrix.E 8 i j

      The Cartan integers at the first eight root indices are Mathlib's Bourbaki-numbered E₈ matrix. This pins the node order independently of the existential relabelling in TauCeti.HasCartanType.

      source
      theorem TauCeti.DynkinType.hasCartanType_e8SimplyConnectedRootDatum :
      HasCartanType e8SimplyConnectedRootDatum e8SimplyConnectedBase E8

      The pinned datum of type E₈ has Cartan type E8. Its Bourbaki-numbered base realizes the standard Cartan matrix CartanMatrix.E 8, with the node numbering of TauCeti.DynkinType.