Documentation

TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.G2.ShortRootWeight

The short-root weight diagram of type G2 #

This file records the seven weights of the fundamental type-G₂ module V(ϖ₁) in fundamental-weight coordinates. They are the six short roots and zero, ordered from the highest weight to its negative. The table is root-datum data used by the integral representation in TauCeti.Algebra.Lie.G2.ShortRoot.Basic.

The numbering and coordinates follow N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IX. The weight diagram follows J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §19.3 (the G₂ algebra) and §21.3 (weight strings and diagrams).

source
def TauCeti.G2ShortRoot.weight :
Fin 7 → Fin 2 → ℤ

The seven weights of the fundamental module V(ϖ₁) of type G₂ in fundamental-weight coordinates: the six short roots and zero, ordered as 2α₁ + α₂, α₁ + α₂, α₁, 0, -α₁, -(α₁ + α₂), -(2α₁ + α₂).

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.G2ShortRoot.weight_apply (a : Fin 7) (i : Fin 2) :
    weight a i = ![![1, 0], ![-1, 1], ![2, -1], ![0, 0], ![-2, 1], ![1, -1], ![-1, 0]] a i

    The entrywise definition of the short-root weight table.

    source
    theorem TauCeti.G2ShortRoot.weight_zero :
    weight 0 = Pi.single 0 1

    The first listed weight is the highest weight ϖ₁.

    source
    theorem TauCeti.G2ShortRoot.weight_three :
    weight 3 = 0

    The middle listed weight is zero.

    source
    theorem TauCeti.G2ShortRoot.weight_zero_add_weight_one :
    weight 0 + weight 1 = Pi.single 1 1

    The first two listed weights sum to the second fundamental weight.

    source
    theorem TauCeti.G2ShortRoot.weight_injective :
    Function.Injective weight

    The seven weights are injective in their index.

    source
    @[simp]
    theorem TauCeti.G2ShortRoot.weight_rev (a : Fin 7) :
    weight a.rev = -weight a

    The weight diagram is symmetric about the origin. Reversing the index negates the weight, the middle index being the fixed point of that symmetry. Nothing is claimed here about a pairing carrying that symmetry.

    source
    theorem TauCeti.G2ShortRoot.sum_weight :
    ∑ a : Fin 7, weight a = 0

    The weights sum to zero.

    source
    theorem TauCeti.G2ShortRoot.range_weight :
    Set.range weight = insert 0 (⇑DynkinType.g2Root '' {k : Fin 12 | DynkinType.g2Length k = 1})

    The weights are the short roots and zero. The nonzero weights are exactly the roots of the pinned type-G₂ datum of squared length one.

    source
    theorem TauCeti.G2ShortRoot.span_range_weight_eq_top :
    Submodule.span ℤ (Set.range weight) = ⊤

    The weights span the full character lattice. The highest weight is the first fundamental weight, and it and the next weight sum to the second.