Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.ReeG2.Basic

The Ree G2 Steinberg map and candidate group #

The signed-minor construction gives the exceptional endomorphism of the characteristic-three short-root carrier. Its odd power is the Steinberg map for a validated Ree G2 index. The candidate is the derived subgroup of its fixed points modulo the centre of that derived subgroup.

The ambient group consists of algebraic-closure points of the explicit prime-field short-root carrier. A comparison with the pinned simply connected G2 group scheme requires an isomorphism preserving the root subgroups and exceptional endomorphism. No finiteness or simplicity is assumed or proved here. The conventions follow Carter, Simple Groups of Lie Type, §12.4.

source
noncomputable def TauCeti.ReeG2LieIndex.halfFrobenius (d : ReeG2LieIndex) :
d.AmbientGroup →* d.AmbientGroup

The exceptional endomorphism of the Ree G2 ambient carrier.

Equations
Instances For
    source
    theorem TauCeti.ReeG2LieIndex.halfFrobenius_def (d : ReeG2LieIndex) :
    d.halfFrobenius = G2ShortRoot.PrimeField.specialIsogeny (↑d).Closure

    The half-Frobenius is the characteristic-three carrier's special isogeny.

    source
    @[simp]
    theorem TauCeti.ReeG2LieIndex.halfFrobenius_halfFrobenius (d : ReeG2LieIndex) (g : d.AmbientGroup) :
    d.halfFrobenius (d.halfFrobenius g) = d.primeFrobenius g

    The half-Frobenius squares to the prime-field Frobenius.

    source
    @[simp]
    theorem TauCeti.ReeG2LieIndex.halfFrobenius_simpleRootSubgroup (d : ReeG2LieIndex) (i : Fin (↑d).rank) (u : Multiplicative (↑d).Closure) :
    d.halfFrobenius ((d.simpleRootSubgroup i) u) = (d.simpleRootSubgroup (d.toSuzukiReeIndex.lengthPerm i)) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ d.toSuzukiReeIndex.exponent i))

    The half-Frobenius has the index's own root permutation and long/short exponents.

    source
    noncomputable def TauCeti.ReeG2LieIndex.steinberg (d : ReeG2LieIndex) :
    d.AmbientGroup →* d.AmbientGroup

    The Steinberg endomorphism is the recorded odd power of the exceptional endomorphism.

    Equations
    Instances For
      source
      theorem TauCeti.ReeG2LieIndex.steinberg_def (d : ReeG2LieIndex) :
      d.steinberg = d.halfFrobenius ^ (↑d).fieldExponent

      The Steinberg map is the recorded power in the monoid of endomorphisms.

      source
      @[simp]
      theorem TauCeti.ReeG2LieIndex.steinberg_steinberg (d : ReeG2LieIndex) (g : d.AmbientGroup) :
      d.steinberg (d.steinberg g) = d.frobenius g

      The square of the Steinberg endomorphism is the field-order Frobenius.

      source
      @[simp]
      theorem TauCeti.ReeG2LieIndex.steinberg_simpleRootSubgroup (d : ReeG2LieIndex) (i : Fin (↑d).rank) (u : Multiplicative (↑d).Closure) :
      d.steinberg ((d.simpleRootSubgroup i) u) = (d.simpleRootSubgroup (d.toSuzukiReeIndex.lengthPerm i)) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ ((↑d).characteristic ^ d.toSuzukiReeIndex.halfExponent * d.toSuzukiReeIndex.exponent i)))

      The odd iterate exchanges the numbered roots with the prescribed parameter power.

      source
      @[reducible, inline]
      abbrev TauCeti.ReeG2LieIndex.FixedPoints (d : ReeG2LieIndex) :
      Type

      The fixed subgroup of the Ree G2 Steinberg endomorphism.

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev TauCeti.ReeG2LieIndex.Group (d : ReeG2LieIndex) :
        Type

        The Ree G2 candidate: the derived subgroup of the Steinberg fixed points modulo its own centre. This definition carries no assertion of finiteness, perfectness, or simplicity.

        Equations
        Instances For