Documentation

TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.G2.Length

Squared lengths of the pinned G₂ roots #

TauCeti.DynkinType.g2SimplyConnectedRootDatum tabulates its twelve roots in the fundamental-weight basis and its twelve coroots in the simple-coroot basis, and TauCeti.DynkinType.g2Coeff records their simple-root coordinates. None of those tables displays how long a root is, which a consumer that has to distinguish long roots from short ones needs, and which is what a characteristic-three special isogeny of type G₂ does.

This file supplies the missing squared-length table, in the pinned index order

α₁,  α₂,  α₁ + α₂,  2 α₁ + α₂,  3 α₁ + α₂,  3 α₁ + 2 α₂

on the positive roots, index k + 6 being the negative of index k.

TauCeti.DynkinType.g2Length is normalised as TauCeti.DynkinType.rootLength normalises the simple roots: 1 on the six short roots ± α₁, ± (α₁ + α₂), ± (2 α₁ + α₂) and 3 on the six long ones ± α₂, ± (3 α₁ + α₂), ± (3 α₁ + 2 α₂). That normalisation is not a stipulation: TauCeti.DynkinType.g2Length_mul_g2Coroot derives the whole table from the two simple lengths by expanding β∨ = 2 β / (β, β) on the simple coroots, and TauCeti.DynkinType.eq_g2Length_of_mul_g2Coroot shows those equations determine it.

Main definitions #

Main results #

References #

The coordinates and the node numbering follow Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IX. The tables are the type G₂ input asked for by the "special isogenies in characteristics two and three" bullet of Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, matching the rank-two type B tables of TauCeti/LinearAlgebra/RootSystem/SimplyConnectedRootDatum/B/RankTwo.lean.

source
def TauCeti.DynkinType.g2Length :
Fin 12 → ℤ

The squared lengths of the twelve roots of the pinned G₂ datum, normalised as TauCeti.DynkinType.rootLength normalises the simple ones: 1 on the six short roots ± α₁, ± (α₁ + α₂), ± (2 α₁ + α₂) and 3 on the six long ones ± α₂, ± (3 α₁ + α₂), ± (3 α₁ + 2 α₂).

Equations
Instances For
    source
    theorem TauCeti.DynkinType.g2Length_apply (i : Fin 12) :
    g2Length i = ![1, 3, 1, 1, 3, 3, 1, 3, 1, 1, 3, 3] i

    The explicit entries of the squared-length table.

    source
    theorem TauCeti.DynkinType.g2Length_mul_g2Coroot (k : Fin 12) (i : Fin 2) :
    g2Length k * g2Coroot k i = g2Coeff k i * G2.rootLength i

    The length table is the one forced by the simple lengths. Writing β = Σ cᵢ αᵢ and β∨ = Σ dᵢ αᵢ∨, the identity β∨ = 2 β / (β, β) reads ℓ(β) dᵢ = cᵢ ℓ(αᵢ) once both sides are expanded on the simple coroots.

    source
    theorem TauCeti.DynkinType.eq_g2Length_of_mul_g2Coroot {k : Fin 12} {c : ℤ} (h : ∀ (i : Fin 2), c * g2Coroot k i = g2Coeff k i * G2.rootLength i) :
    c = g2Length k

    No coroot vanishes, so TauCeti.DynkinType.g2Length_mul_g2Coroot determines the length table.

    source
    @[simp]
    theorem TauCeti.DynkinType.g2Length_castLE (i : Fin 2) :
    g2Length (Fin.castLE g2Length_castLE._proof_2 i) = G2.rootLength i

    On the two simple roots the length table is TauCeti.DynkinType.rootLength.

    source
    @[simp]
    theorem TauCeti.DynkinType.g2Length_add_six (k : Fin 12) :
    g2Length (k + 6) = g2Length k

    A root and its negative have the same length.

    source
    theorem TauCeti.DynkinType.g2Length_eq_one_or_eq_three (k : Fin 12) :
    g2Length k = 1 ∨ g2Length k = 3

    Every root of the pinned G₂ datum is short or long, of squared length 1 or 3.

    source
    theorem TauCeti.DynkinType.g2Length_pos (k : Fin 12) :
    0 < g2Length k

    Every root of the pinned G₂ datum has positive squared length.

    source
    theorem TauCeti.DynkinType.isLongSimpleRoot_iff_g2Length_eq_three (i : Fin 2) :
    G2.IsLongSimpleRoot i ↔ g2Length (Fin.castLE g2Length_castLE._proof_2 i) = 3

    The long simple root is the one of length three, which is the convention TauCeti.DynkinType.rootLength fixes and the one a length-exchanging map is pinned against.

    source
    theorem TauCeti.DynkinType.g2Length_castLE_eq_one_iff (i : Fin 2) :
    g2Length (Fin.castLE g2Length_castLE._proof_2 i) = 1 ↔ ¬G2.IsLongSimpleRoot i

    The short simple root is the one of length one. This is the form in which a characteristic-three special isogeny states which of its two rescaling exponents it attaches to which node.