Documentation

TauCeti.LinearAlgebra.RootSystem.NumberOfRoots

Numbers of roots of Dynkin types #

This file records the number of roots in each irreducible crystallographic Dynkin type. The value TauCeti.DynkinType.numRoots fixes Fin t.numRoots as the root-index type intended for the pinned simply connected root datum, which is not constructed here: unlike an abstract finite index type, this makes that index type explicit for every family.

The classical formulas are n(n+1) for Aₙ, 2n² for Bₙ and Cₙ, and 2n(n-1) for Dₙ. The exceptional types have respectively 72, 126, 240, 48, and 12 roots. For a valid Dynkin type, TauCeti.DynkinType.rank_le_numRoots ensures that the simple roots can occupy the first t.rank indices of Fin t.numRoots, as that future datum will require.

Main definitions #

Main results #

References #

This is the DynkinType.numRoots target of Layer 6 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. The formulas follow N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, plates I--IX, and J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Chapter 11.

source
def TauCeti.DynkinType.numRoots :
DynkinType → ℕ

The number of roots of a Dynkin type. This is exposed because it is meant to appear in the root-index type Fin t.numRoots of the future pinned simply connected root datum, whose construction must reduce to the explicit family data rather than an abstract finite type.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.DynkinType.numRoots_A (n : ℕ) :
    (A n).numRoots = n * (n + 1)
    source
    @[simp]
    theorem TauCeti.DynkinType.numRoots_B (n : ℕ) :
    (B n).numRoots = 2 * n ^ 2
    source
    @[simp]
    theorem TauCeti.DynkinType.numRoots_C (n : ℕ) :
    (C n).numRoots = 2 * n ^ 2
    source
    @[simp]
    theorem TauCeti.DynkinType.numRoots_D (n : ℕ) :
    (D n).numRoots = 2 * n * (n - 1)
    source
    @[simp]
    theorem TauCeti.DynkinType.numRoots_E6 :
    E6.numRoots = 72
    source
    @[simp]
    theorem TauCeti.DynkinType.numRoots_E7 :
    E7.numRoots = 126
    source
    @[simp]
    theorem TauCeti.DynkinType.numRoots_E8 :
    E8.numRoots = 240
    source
    @[simp]
    theorem TauCeti.DynkinType.numRoots_F4 :
    F4.numRoots = 48
    source
    @[simp]
    theorem TauCeti.DynkinType.numRoots_G2 :
    G2.numRoots = 12
    source
    theorem TauCeti.DynkinType.rank_le_numRoots {t : DynkinType} (ht : t.Valid) :
    t.rank ≤ t.numRoots

    A valid Dynkin type has at least as many roots as simple roots. This is the bound needed to regard the Bourbaki-numbered simple nodes as the first indices of Fin t.numRoots.

    source
    theorem TauCeti.DynkinType.numRoots_pos {t : DynkinType} (ht : t.Valid) :
    0 < t.numRoots

    A valid Dynkin type has at least one root.