Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.ReeF4.Basic

The Ree F4 Steinberg map and candidate group #

The represented quotient constructs the exceptional endomorphism of the characteristic-two short-root carrier. Its odd power is the Steinberg map for a validated Ree F4 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 F4 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, §14.

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

The exceptional endomorphism of the Ree F4 ambient carrier.

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

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

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

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

    source
    @[simp]
    theorem TauCeti.ReeF4LieIndex.halfFrobenius_simpleRootSubgroup (d : ReeF4LieIndex) (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.ReeF4LieIndex.steinberg (d : ReeF4LieIndex) :
    d.AmbientGroup →* d.AmbientGroup

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

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

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

      source
      @[simp]
      theorem TauCeti.ReeF4LieIndex.steinberg_steinberg (d : ReeF4LieIndex) (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.ReeF4LieIndex.steinberg_simpleRootSubgroup (d : ReeF4LieIndex) (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.ReeF4LieIndex.FixedPoints (d : ReeF4LieIndex) :
      Type

      The fixed subgroup of the Ree F4 Steinberg endomorphism.

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

        The Ree F4 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