Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.SuzukiRee

Numbered data for the Suzuki--Ree isogenies #

The exceptional isogenies used to construct the Suzuki and Ree groups exchange long and short simple roots. Their action on a simple root subgroup also raises its parameter to an exponent: the exponent is 1 on a long simple root and the defining characteristic on a short simple root. This file attaches both the length-exchanging permutation and the exponent convention to TauCeti.SuzukiReeIndex.

The assignment is a genuine choice. Reversing the two exponents would still make the square of the exceptional isogeny a prime-field Frobenius, so the square relation alone does not determine which isogeny the later construction uses. Defining the exponent through TauCeti.DynkinType.IsLongSimpleRoot ties it to the Bourbaki numbering and root-length convention already fixed by the root-systems development, without introducing a second table for B₂, G₂, and F₄.

The permutation selector has only the four half-Frobenius branches: Suzuki and Ree G₂ use the rank-two node swap, while Ree F₄ and Tits use diagram reversal. Milestone L2 must reduce every branch to the corresponding pinned permutation when selecting the upstream special isogeny, so the four branch equations are simp lemmas rather than the selector body being exposed.

Main definitions and results #

source
def TauCeti.SuzukiReeIndex.lengthPerm (e : SuzukiReeIndex) :
Equiv.Perm (Fin (↑e).rank)

The length-exchanging permutation used by the exceptional isogeny attached to a Suzuki--Ree index: the node swap for B₂ and G₂, and reversal for F₄.

The four branch equations lengthPerm_suzuki, lengthPerm_reeG2, lengthPerm_reeF4, and lengthPerm_tits name the selected permutation on each family, so no consumer needs this body.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.lengthPerm_suzuki (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) :
    lengthPerm ⟨⟨LieTypeIndex.suzuki m, hvalid⟩, ⋯⟩ = (finCongr ⋯).symm.permCongr lengthPermRankTwo

    A Suzuki index selects the rank-two node swap, transported along the B₂ numbering.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.lengthPerm_reeG2 (m : ℕ) (hvalid : (LieTypeIndex.reeG2 m).Valid) :
    lengthPerm ⟨⟨LieTypeIndex.reeG2 m, hvalid⟩, ⋯⟩ = (finCongr ⋯).symm.permCongr lengthPermRankTwo

    A Ree G₂ index selects the rank-two node swap, transported along the G₂ numbering.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.lengthPerm_reeF4 (m : ℕ) (hvalid : (LieTypeIndex.reeF4 m).Valid) :
    lengthPerm ⟨⟨LieTypeIndex.reeF4 m, hvalid⟩, ⋯⟩ = (finCongr ⋯).symm.permCongr lengthPermF4

    A Ree F₄ index selects the F₄ diagram reversal.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.lengthPerm_tits :
    lengthPerm ⟨⟨LieTypeIndex.tits, lengthPerm_tits._proof_1⟩, lengthPerm_tits._proof_2⟩ = (finCongr lengthPerm_tits._proof_3).symm.permCongr lengthPermF4

    The Tits index selects the F₄ diagram reversal.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.isLongSimpleRoot_lengthPerm (e : SuzukiReeIndex) (i : Fin (↑e).rank) :
    (↑e).dynkinType.IsLongSimpleRoot (e.lengthPerm i) ↔ ¬(↑e).dynkinType.IsLongSimpleRoot i

    The length permutation selected by a Suzuki--Ree index exchanges long and short simple roots in the Bourbaki numbering of its underlying untwisted Dynkin diagram.

    source
    def TauCeti.SuzukiReeIndex.exponent (e : SuzukiReeIndex) (i : Fin (↑e).rank) :
    ℕ

    The exponent attached to a numbered simple root subgroup by the exceptional isogeny: 1 on a long simple root and the defining characteristic on a short simple root.

    The long-root predicate is the root-systems development's Bourbaki-numbered predicate, rather than a second family-by-family table.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.SuzukiReeIndex.exponent_of_isLongSimpleRoot (e : SuzukiReeIndex) (i : Fin (↑e).rank) (hi : (↑e).dynkinType.IsLongSimpleRoot i) :
      e.exponent i = 1

      The exceptional isogeny uses exponent 1 on long simple root subgroups.

      source
      @[simp]
      theorem TauCeti.SuzukiReeIndex.exponent_of_not_isLongSimpleRoot (e : SuzukiReeIndex) (i : Fin (↑e).rank) (hi : ¬(↑e).dynkinType.IsLongSimpleRoot i) :
      e.exponent i = (↑e).characteristic

      The exceptional isogeny uses the defining characteristic as its exponent on short simple root subgroups.

      source
      @[simp]
      theorem TauCeti.SuzukiReeIndex.exponent_eq_one_iff (e : SuzukiReeIndex) (i : Fin (↑e).rank) :
      e.exponent i = 1 ↔ (↑e).dynkinType.IsLongSimpleRoot i

      A root-subgroup exponent is 1 exactly on a long simple root.

      source
      @[simp]
      theorem TauCeti.SuzukiReeIndex.exponent_eq_characteristic_iff (e : SuzukiReeIndex) (i : Fin (↑e).rank) :
      e.exponent i = (↑e).characteristic ↔ ¬(↑e).dynkinType.IsLongSimpleRoot i

      A root-subgroup exponent is the defining characteristic exactly on a short simple root.

      source
      theorem TauCeti.SuzukiReeIndex.exponent_pos (e : SuzukiReeIndex) (i : Fin (↑e).rank) :
      0 < e.exponent i

      Every root-subgroup exponent is positive.

      source
      theorem TauCeti.SuzukiReeIndex.exponent_le_characteristic (e : SuzukiReeIndex) (i : Fin (↑e).rank) :
      e.exponent i ≤ (↑e).characteristic

      Every root-subgroup exponent is at most the defining characteristic.

      source
      theorem TauCeti.SuzukiReeIndex.exponent_eq_one_or_eq_characteristic (e : SuzukiReeIndex) (i : Fin (↑e).rank) :
      e.exponent i = 1 ∨ e.exponent i = (↑e).characteristic

      The two possible values of a root-subgroup exponent.

      The length permutation is an involution transposing the Cartan matrix #

      source
      @[simp]
      theorem TauCeti.SuzukiReeIndex.lengthPerm_lengthPerm (e : SuzukiReeIndex) (i : Fin (↑e).rank) :
      e.lengthPerm (e.lengthPerm i) = i

      The length permutation selected by a Suzuki--Ree index is an involution: the exceptional isogeny exchanges the long and short simple roots, so applying it twice returns each node.

      source
      @[simp]
      theorem TauCeti.SuzukiReeIndex.cartanMatrix_lengthPerm (e : SuzukiReeIndex) (i j : Fin (↑e).rank) :
      (↑e).dynkinType.cartanMatrix (e.lengthPerm i) (e.lengthPerm j) = (↑e).dynkinType.cartanMatrix j i

      The length permutation selected by a Suzuki--Ree index carries the Cartan matrix of its underlying untwisted diagram to the transposed matrix.

      This is what distinguishes it from the graph automorphisms of TauCeti.GraphTwistedIndex.diagramPerm, which preserve their Cartan matrix (TauCeti.GraphTwistedIndex.cartanMatrix_diagramPerm). A permutation transposing the Cartan matrix is a symmetry of the dual diagram, so it is not realized by an automorphism of the pinned group; it is realized by a special isogeny, which is why these four families need a half-Frobenius.

      source
      @[simp]
      theorem TauCeti.SuzukiReeIndex.exponent_mul_exponent_lengthPerm (e : SuzukiReeIndex) (i : Fin (↑e).rank) :
      e.exponent i * e.exponent (e.lengthPerm i) = (↑e).characteristic

      The exponents attached to a simple root and to its partner under the length permutation multiply to the defining characteristic.

      This is the relation that makes the square of the exceptional isogeny the prime-field Frobenius: one factor is 1 and the other is the characteristic, in one order or the other.