Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.HalfFrobenius

The odd half-Frobenius power of a Suzuki--Ree index #

The Steinberg endomorphism of a Suzuki, Ree or Tits group is not a Frobenius but an odd power of a half-Frobenius: the exceptional isogeny τ of the pinned ambient group, which squares to the prime-field Frobenius, raised to the odd exponent 2 * m + 1. This file takes that odd power on root data, where τ already lives as TauCeti.SuzukiReeIndex.datumSpecialIsogeny, and proves the relation the CFSG roadmap requires of it,

steinberg (m) ^ 2 = Frob_(p ^ (2 * m + 1)).

The exponent is not a new parameter. TauCeti.LieTypeIndex.fieldExponent already writes the field order of an index as a power of its characteristic, and on all four half-Frobenius branches it is odd: it is 2 * m + 1 on the three Suzuki--Ree families and 1 on the Tits index, whose Steinberg map is τ itself. So TauCeti.SuzukiReeIndex.halfExponent reads off the m those four branches share, fieldExponent_eq_two_mul_halfExponent_add_one is the odd decomposition, and the Steinberg map is the fieldExponent-th power throughout. Squaring it then lands on the scaling by TauCeti.LieTypeIndex.fieldOrder rather than on some separately tabulated field order, which is the check that the exponent convention of milestone L2 and the numeric data of milestone I0 agree.

The odd power is genuinely a new map and not a rescaled identity: it is a scaling times τ, so it permutes the roots exactly as τ does, by the length-exchanging permutation TauCeti.SuzukiReeIndex.lengthPerm on the numbered simple roots, and merely multiplies the pinned exponents of τ by p ^ m. The resulting relations on the numbered simple roots and coroots are recorded below, since a consumer lifting this map to the pinned group scheme states its conventions against them.

Nothing here is a group. Lifting these isogenies from root data to the pinned Chevalley--Demazure group schemes, and the finite groups cut out as their fixed points, are later work.

Main definitions #

Main results #

References #

The odd half-Frobenius power and the relation steinberg (m) ^ 2 = Frob_(p ^ (2 * m + 1)) are milestone L2 of TauCetiRoadmap/CFSGStatement/README.md, which fixes the convention followed here, including the Tits index as the m = 0 member. The upstream exceptional isogeny is the Layer 9 target of TauCetiRoadmap/ReductiveGroups/README.md.

The odd exponent #

source
def TauCeti.SuzukiReeIndex.halfExponent (e : SuzukiReeIndex) :
ℕ

The odd-power parameter m of a Suzuki--Ree index: the m in the field order p ^ (2 * m + 1) recorded by the three Suzuki--Ree families, and 0 on the Tits index, whose Steinberg map is the half-Frobenius itself.

The four branch equations below name it on each family, so no consumer needs this body.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.halfExponent_suzuki (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) :
    halfExponent ⟨⟨LieTypeIndex.suzuki m, hvalid⟩, ⋯⟩ = m

    A Suzuki index contributes its own parameter.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.halfExponent_reeG2 (m : ℕ) (hvalid : (LieTypeIndex.reeG2 m).Valid) :
    halfExponent ⟨⟨LieTypeIndex.reeG2 m, hvalid⟩, ⋯⟩ = m

    A Ree G₂ index contributes its own parameter.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.halfExponent_reeF4 (m : ℕ) (hvalid : (LieTypeIndex.reeF4 m).Valid) :
    halfExponent ⟨⟨LieTypeIndex.reeF4 m, hvalid⟩, ⋯⟩ = m

    A Ree F₄ index contributes its own parameter.

    source
    @[simp]
    theorem TauCeti.SuzukiReeIndex.halfExponent_tits :
    halfExponent ⟨⟨LieTypeIndex.tits, halfExponent_tits._proof_1⟩, halfExponent_tits._proof_2⟩ = 0

    The Tits index is the m = 0 member of the F₄ half-Frobenius family.

    source
    theorem TauCeti.SuzukiReeIndex.fieldExponent_eq_two_mul_halfExponent_add_one (e : SuzukiReeIndex) :
    (↑e).fieldExponent = 2 * e.halfExponent + 1

    The field exponent of a half-Frobenius index is 2 * m + 1. The Steinberg map is the fieldExponent-th power of the half-Frobenius, so this is what makes it an odd power.

    source
    theorem TauCeti.SuzukiReeIndex.odd_fieldExponent (e : SuzukiReeIndex) :
    Odd (↑e).fieldExponent

    The field exponent of a half-Frobenius index is odd.

    source
    theorem TauCeti.SuzukiReeIndex.halfExponent_eq_zero_iff (e : SuzukiReeIndex) :
    e.halfExponent = 0 ↔ ↑↑e = LieTypeIndex.tits

    The odd-power parameter vanishes exactly on the Tits index. The three Suzuki--Ree families start at m = 1: their m = 0 members are the nonsimple ²B₂(2), the likewise nonsimple ²G₂(3), whose derived subgroup is the group the list carries as A₁(8), and ²F₄(2), whose derived subgroup the list carries under the separate Tits name. So the Tits index is the only half-Frobenius index whose Steinberg map is the special isogeny itself.

    The Steinberg map on the root datum #

    source
    noncomputable def TauCeti.SuzukiReeIndex.datumSteinberg (e : SuzukiReeIndex) :
    RootPairingIsogeny ((↑e).dynkinType.simplyConnectedRootDatum ⋯) ((↑e).dynkinType.simplyConnectedRootDatum ⋯)

    The Steinberg map of a Suzuki--Ree index on its pinned simply connected root datum: the odd power τ ^ (2 * m + 1) of the special isogeny selected by the index, written as its fieldExponent-th power. On the Tits index the exponent is 1 and the map is τ itself.

    Equations
    Instances For
      source
      theorem TauCeti.SuzukiReeIndex.datumSteinberg_eq_smulId_mul (e : SuzukiReeIndex) :
      e.datumSteinberg = RootPairingIsogeny.smulId ((↑e).dynkinType.simplyConnectedRootDatum ⋯) (⟨(↑e).characteristic, ⋯⟩ ^ e.halfExponent) * e.datumSpecialIsogeny

      The Steinberg map is a scaling times the special isogeny, by p ^ m. Every computation below is read off this decomposition.

      source
      @[simp]
      theorem TauCeti.SuzukiReeIndex.datumSteinberg_tits :
      datumSteinberg ⟨⟨LieTypeIndex.tits, halfExponent_tits._proof_1⟩, halfExponent_tits._proof_2⟩ = datumSpecialIsogeny ⟨⟨LieTypeIndex.tits, halfExponent_tits._proof_1⟩, halfExponent_tits._proof_2⟩

      On the Tits index the Steinberg map is the special isogeny of F₄ itself, the m = 0 case of the odd power.

      The square relation #

      source
      @[simp]
      theorem TauCeti.SuzukiReeIndex.datumSteinberg_mul_self (e : SuzukiReeIndex) :
      e.datumSteinberg * e.datumSteinberg = RootPairingIsogeny.smulId ((↑e).dynkinType.simplyConnectedRootDatum ⋯) (↑↑e).fieldOrderPNat

      The square of the Steinberg map is the scaling by the field order of the index. This is the root-datum form of steinberg (m) ^ 2 = Frob_(p ^ (2 * m + 1)): squaring the odd power of the half-Frobenius returns the Frobenius of the field the index names, 2 ^ (2 * m + 1) for the Suzuki and Ree F₄ families, 3 ^ (2 * m + 1) for Ree G₂, and 2 for the Tits index.

      The four pieces of data #

      source
      @[simp]
      theorem TauCeti.SuzukiReeIndex.datumSteinberg_indexEquiv (e : SuzukiReeIndex) :
      e.datumSteinberg.indexEquiv = e.datumSpecialIsogeny.indexEquiv

      The Steinberg map permutes the roots exactly as the special isogeny does, since the scaling separating the two fixes every index.

      source
      @[simp]
      theorem TauCeti.SuzukiReeIndex.datumSteinberg_exponent (e : SuzukiReeIndex) (i : Fin (↑e).dynkinType.numRoots) :
      e.datumSteinberg.exponent i = e.datumSpecialIsogeny.exponent i * ↑(↑e).characteristic ^ e.halfExponent

      The rescaling exponents of the Steinberg map are those of the special isogeny multiplied by p ^ m. At a numbered simple root the exponent of the special isogeny is the squared length of that node, so this is p ^ m at a short simple root and p ^ (m + 1) at a long one.

      The exponent field is indexed by the source of the character map, which is the image node of the group-scheme isogeny, so this indexing is the one exchanged against the simple-root relation below: the factor there is TauCeti.SuzukiReeIndex.exponent i, the squared length of the node paired with i, and is therefore p ^ m at a long node and p ^ (m + 1) at a short one.

      source
      @[simp]
      theorem TauCeti.SuzukiReeIndex.datumSteinberg_weightMap (e : SuzukiReeIndex) :
      e.datumSteinberg.weightMap = (↑e).characteristic ^ e.halfExponent • e.datumSpecialIsogeny.weightMap

      The character map of the Steinberg map is p ^ m times that of the special isogeny.

      source
      @[simp]
      theorem TauCeti.SuzukiReeIndex.datumSteinberg_coweightMap (e : SuzukiReeIndex) :
      e.datumSteinberg.coweightMap = (↑e).characteristic ^ e.halfExponent • e.datumSpecialIsogeny.coweightMap

      The cocharacter map of the Steinberg map is p ^ m times that of the special isogeny.

      The defining relations on the numbered simple roots #

      source
      theorem TauCeti.SuzukiReeIndex.datumSteinberg_weightMap_root_simpleIndex (e : SuzukiReeIndex) (i : Fin (↑e).rank) :
      e.datumSteinberg.weightMap (((↑e).dynkinType.simplyConnectedRootDatum ⋯).root ((↑e).dynkinType.simpleIndex ⋯ (e.lengthPerm i))) = (↑(e.exponent i) * ↑(↑e).characteristic ^ e.halfExponent) • ((↑e).dynkinType.simplyConnectedRootDatum ⋯).root ((↑e).dynkinType.simpleIndex ⋯ i)

      The relation defining the Steinberg map on the simple roots. The character map carries the simple root at the length-exchanged node to the simple root at i, rescaled by p ^ m * TauCeti.SuzukiReeIndex.exponent i, which is p ^ m at a long node and p ^ (m + 1) at a short one.

      The character map is the pullback along the group-scheme isogeny, so this is the root-datum shadow of steinberg (x_{α_i}(t)) = x_{α_{σ i}}(t ^ (p ^ m * exponent i)), with the exponent indexed by i rather than by its image.

      source
      theorem TauCeti.SuzukiReeIndex.datumSteinberg_coweightMap_coroot_simpleIndex (e : SuzukiReeIndex) (i : Fin (↑e).rank) :
      e.datumSteinberg.coweightMap (((↑e).dynkinType.simplyConnectedRootDatum ⋯).coroot ((↑e).dynkinType.simpleIndex ⋯ i)) = (↑(e.exponent i) * ↑(↑e).characteristic ^ e.halfExponent) • ((↑e).dynkinType.simplyConnectedRootDatum ⋯).coroot ((↑e).dynkinType.simpleIndex ⋯ (e.lengthPerm i))

      The relation defining the Steinberg map on the simple coroots. Dually to TauCeti.SuzukiReeIndex.datumSteinberg_weightMap_root_simpleIndex, the cocharacter map runs the other way, so it carries the simple coroot at i to the one at the length-exchanged node, rescaled by the same factor.