Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.Tits.Basic

The Tits Steinberg map and candidate group #

The Tits index uses the exceptional endomorphism itself, the first odd iterate of the characteristic-two F4 special isogeny. Its candidate is the derived subgroup of the 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, perfectness, or simplicity is assumed or proved here. See Carter, Simple Groups of Lie Type, §14.

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

The Tits Steinberg endomorphism is the exceptional endomorphism itself.

Equations
Instances For
    source
    theorem TauCeti.TitsLieIndex.steinberg_def (d : TitsLieIndex) :
    d.steinberg = F4ShortRoot.PrimeField.specialIsogeny (↑d).Closure

    The Tits Steinberg map is the characteristic-two carrier's special isogeny.

    source
    theorem TauCeti.TitsLieIndex.steinberg_eq_specialIsogeny_pow (d : TitsLieIndex) :
    d.steinberg = (have this := F4ShortRoot.PrimeField.specialIsogeny (↑d).Closure; this) ^ (↑d).fieldExponent

    The Tits map is the index's recorded odd iterate, whose exponent is one.

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

    Squaring the Tits Steinberg map gives the prime-field Frobenius.

    source
    @[simp]
    theorem TauCeti.TitsLieIndex.steinberg_simpleRootSubgroup (d : TitsLieIndex) (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.toSuzukiReeIndex.exponent i))

    The Tits map exchanges the numbered simple roots, with exponent one on long roots and two on short roots, matching the validated index.

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

    The fixed subgroup of the exceptional F4 endomorphism at the Tits index.

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

      The Tits candidate is the derived subgroup of the fixed points modulo its own centre. No finiteness or simplicity assertion is part of this definition.

      Equations
      Instances For