Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.Tits.Carrier

The ambient group of the Tits construction #

The Tits group Β²Fβ‚„(2)' is built inside the group of algebraic-closure-valued points of the short-root type-Fβ‚„ carrier over 𝔽₂. This is the closed subgroup scheme of GL₂₆ generated over 𝔽₂ by the reductions of the numbered simple root subgroups and the weight torus of the Kostant toral closure of the twenty-six-dimensional module V(Ο–β‚„). This file attaches that carrier to the validated Tits index and supplies its numbered simple root subgroups and prime-field Frobenius.

The carrier is taken over 𝔽₂ because the exceptional isogeny used by the Tits construction exists in characteristic two. Carrying that isogeny from matrices to the carrier requires the defining Hopf ideal to be the largest one killed by the generator coordinate maps over 𝔽₂; the base change of the integral toral closure is only known to contain this carrier, since new equations can appear under a non-flat base change.

The Frobenius below squares matrix entries. It is not the Steinberg endomorphism of the Tits construction: the latter is the characteristic-two exceptional isogeny itself, whose square is this Frobenius. The fixed-point candidate is formed only after that exceptional isogeny has been attached to the carrier.

The carrier uses the Bourbaki numbering of the Fβ‚„ diagram carried by the index. The character by which its split torus rescales the parameter of the i-th raising subgroup is the i-th simple root of TauCeti.DynkinType.simplyConnectedRootDatum, so no reindexing adapter is needed.

This explicit carrier is not identified here with the pinned simply connected group scheme of type Fβ‚„. Constructions on it transfer to the pinned group only along such an identification, once one is proved. Nothing here asserts that the carrier is reductive, that its weight torus is maximal, or that any group is finite, perfect, or simple.

Main definitions #

Main results #

References #

The ambient group and its simple root subgroups #

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

The ambient group of the Tits construction: the algebraic-closure-valued points of the short-root type-Fβ‚„ carrier over 𝔽₂, as a subgroup of GL₂₆.

This ambient group is generally infinite. No finiteness, reductivity, pinning, or maximality statement is attached to it, and it is not identified here with the points of the pinned simply connected group scheme of type Fβ‚„.

Equations
Instances For
    source
    noncomputable def TauCeti.TitsLieIndex.simpleRootSubgroup (d : TitsLieIndex) (i : Fin (↑d).rank) :
    Multiplicative (↑d).Closure β†’* d.AmbientGroup

    The positive simple-root subgroup at the Bourbaki-numbered node i of the Fβ‚„ diagram.

    Equations
    Instances For
      source
      theorem TauCeti.TitsLieIndex.simpleRootSubgroup_def (d : TitsLieIndex) (i : Fin (↑d).rank) :
      d.simpleRootSubgroup i = F4ShortRoot.PrimeField.rootSubgroupPoints (Sum.inl ((finCongr β‹―) i)) (↑d).Closure

      The simple-root subgroup is the carrier's raising subgroup at the corresponding numbered node.

      source
      theorem TauCeti.TitsLieIndex.rootGeneratorWeight_eq_root_simpleIndex (d : TitsLieIndex) (i : Fin (↑d).rank) :
      DynkinType.F4.rootGeneratorWeight DynkinType.valid_F4 (Sum.inl ((finCongr β‹―) i)) = (DynkinType.F4.simplyConnectedRootDatum DynkinType.valid_F4).root (DynkinType.F4.simpleIndex DynkinType.valid_F4 ((finCongr β‹―) i))

      The carrier's numbered root characters are the simple roots of the Fβ‚„ root datum. Thus simpleRootSubgroup i uses the Bourbaki node represented by i, rather than a separately chosen numbering of the explicit carrier.

      The prime-field Frobenius #

      source
      noncomputable def TauCeti.TitsLieIndex.frobenius (d : TitsLieIndex) :
      d.AmbientGroup β†’* d.AmbientGroup

      The prime-field Frobenius of the Tits ambient group, which squares every matrix entry.

      This is not the Steinberg endomorphism. The Tits Steinberg endomorphism is the exceptional isogeny whose square is this map.

      Equations
      Instances For
        source
        theorem TauCeti.TitsLieIndex.frobenius_def (d : TitsLieIndex) :
        d.frobenius = F4ShortRoot.PrimeField.frobenius 1 (↑d).Closure

        The Tits Frobenius is the carrier's Frobenius at exponent one.

        source
        @[simp]
        theorem TauCeti.TitsLieIndex.coe_frobenius_apply (d : TitsLieIndex) (g : d.AmbientGroup) (r c : Fin 26) :
        ↑↑(d.frobenius g) r c = ↑↑g r c ^ 2

        The Frobenius squares every matrix entry of the ambient group.

        source
        @[simp]
        theorem TauCeti.TitsLieIndex.frobenius_simpleRootSubgroup (d : TitsLieIndex) (i : Fin (↑d).rank) (u : Multiplicative (↑d).Closure) :
        d.frobenius ((d.simpleRootSubgroup i) u) = (d.simpleRootSubgroup i) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ 2))

        The Frobenius fixes the numbered simple-root subgroup and squares its parameter: Frobβ‚‚ (x_i(u)) = x_i(uΒ²).

        source
        theorem TauCeti.TitsLieIndex.mem_fixedSubgroup_frobenius_iff (d : TitsLieIndex) (g : d.AmbientGroup) :
        g ∈ fixedSubgroup d.frobenius ↔ βˆ€ (r c : Fin 26), ↑↑g r c ∈ (↑d).fixedField

        A carrier point is fixed by the prime-field Frobenius exactly when all matrix entries lie in the index's field of definition, the copy of 𝔽₂ inside its algebraic closure.