Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.Assembly.AmbientGroup

The ambient group of an arbitrary valid Lie-type index #

Every one of the seventeen Lie-type constructors of the classification list now has an explicit carrier: a matrix group over the algebraic closure of its prime field, together with its Bourbaki-numbered positive simple root subgroups and its q-power Frobenius, for q the field order the index records. The thirteen constructors with an ordinary or graph-twisted Steinberg endomorphism are already joined into TauCeti.GraphTwistedIndex.AmbientGroup; the remaining four, whose Steinberg endomorphism is an odd power of a half-Frobenius, have carriers of their own:

ConstructorFamily API
suzukiTauCeti.RankTwoBLieIndex, on the rank-two standard symplectic carrier
reeG2TauCeti.ReeG2LieIndex, on the short-root type-G₂ carrier over 𝔽₃
reeF4TauCeti.ReeF4LieIndex, on the short-root type-F₄ carrier over 𝔽₂
titsTauCeti.TitsLieIndex, on the same short-root type-F₄ carrier

This file joins all seventeen into one construction on TauCeti.ValidLieTypeIndex, by cases on the constructor: the ambient group TauCeti.ValidLieTypeIndex.AmbientGroup with its Group instance, its numbered simple root subgroups TauCeti.ValidLieTypeIndex.simpleRootSubgroup, and its Frobenius TauCeti.ValidLieTypeIndex.frobenius. Each branch is an existing construction, with no new carrier or map: the thirteen ordinary and graph-twisted branches are the graph-twisted assembly, and the four half-Frobenius branches are the family carriers. The branch equations TauCeti.ValidLieTypeIndex.simpleRootSubgroup_A, ..., TauCeti.ValidLieTypeIndex.simpleRootSubgroup_tits and TauCeti.ValidLieTypeIndex.frobenius_A, ..., TauCeti.ValidLieTypeIndex.frobenius_tits say which one on each constructor.

What the assembly buys is a single statement, for every valid index, of the Frobenius equation on the numbered simple root subgroups, TauCeti.ValidLieTypeIndex.frobenius_simpleRootSubgroup:

Frob_q (x_i(u)) = x_i(u ^ q).

The Frobenius is the Steinberg endomorphism on the nine untwisted families only. On the four graph-twisted families the Steinberg endomorphism is a graph automorphism composed with it, and on the four half-Frobenius families it is the odd power of an exceptional isogeny whose square is the prime-field Frobenius. The Suzuki and Ree G₂ family APIs expose such isogenies as TauCeti.SuzukiLieIndex.halfFrobenius and TauCeti.ReeG2LieIndex.halfFrobenius; exceptional isogenies remain separate from this Frobenius assembly. The uniform Steinberg endomorphism is not assembled here.

Beside it the assembly carries the prime-field Frobenius TauCeti.ValidLieTypeIndex.primeFrobenius, the p-power map for p the defining characteristic, of which the q-power map is the e-th power, TauCeti.ValidLieTypeIndex.frobenius_eq_primeFrobenius_pow:

Frob_q = Frob_p ^ e,        Frob_p (x_i(u)) = x_i(u ^ p).

The two agree on an index of prime field order, the Tits index among them. It is the prime-field map, and not the q-power one, that the exceptional isogeny of the Suzuki and Ree G₂ families squares to.

Every carrier used here is an explicit one, and none is identified with the pinned simply connected group scheme of its diagram; the constructions transfer to that pinned group only along such an identification, once one is proved. Nothing here asserts that any group is finite, perfect or simple, nor that any carrier is reductive.

Main definitions #

Main results #

References #

source
def TauCeti.ValidLieTypeIndex.AmbientGroup :
ValidLieTypeIndex → Type

The ambient group of a valid Lie-type index: the group of algebraic-closure-valued points of the explicit carrier assigned to its family. It is generally infinite, and it is not identified with the points of the pinned simply connected group scheme of the diagram. On the thirteen ordinary and graph-twisted constructors it is TauCeti.GraphTwistedIndex.AmbientGroup; the Suzuki family runs on the rank-two symplectic carrier, the Ree family of type G₂ on the short-root G₂ carrier over 𝔽₃, and the Ree family of type F₄ and the Tits construction on the short-root F₄ carrier over 𝔽₂.

Equations
Instances For
    source
    @[instance_reducible]
    noncomputable instance TauCeti.ValidLieTypeIndex.instGroupAmbientGroup (d : ValidLieTypeIndex) :
    Group d.AmbientGroup

    The ambient group carries the group structure of the carrier it is on.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    noncomputable def TauCeti.ValidLieTypeIndex.simpleRootSubgroup (d : ValidLieTypeIndex) :
    Fin d.rank → Multiplicative d.Closure →* d.AmbientGroup

    The positive simple root subgroup at the Bourbaki-numbered node i, as a homomorphism from the additive group of the algebraic closure. On each constructor it is the simple root subgroup of the graph-twisted assembly or of the half-Frobenius family, by simpleRootSubgroup_A and its siblings.

    Equations
    Instances For
      source
      noncomputable def TauCeti.ValidLieTypeIndex.frobenius (d : ValidLieTypeIndex) :
      d.AmbientGroup →* d.AmbientGroup

      The q-power Frobenius endomorphism of the ambient group of a valid Lie-type index, for q the field order the index records. On each constructor it is the Frobenius of the graph-twisted assembly or of the half-Frobenius family, by frobenius_A and its siblings; its action on the simple root subgroups is frobenius_simpleRootSubgroup.

      It is the Steinberg endomorphism of the nine untwisted families only. On the four graph-twisted families the Steinberg endomorphism composes a graph automorphism with it, and on the four half-Frobenius families the Steinberg endomorphism is an odd power of an exceptional isogeny whose square is the prime-field Frobenius primeFrobenius. The Frobenius defined here is distinct from those exceptional isogenies, which belong to the family APIs.

      Equations
      Instances For
        source
        noncomputable def TauCeti.ValidLieTypeIndex.primeFrobenius (d : ValidLieTypeIndex) :
        d.AmbientGroup →* d.AmbientGroup

        The prime-field Frobenius endomorphism of the ambient group of a valid Lie-type index, the p-power map for p the defining characteristic. On each constructor it is the prime-field Frobenius of the graph-twisted assembly or of the half-Frobenius family, by primeFrobenius_A and its siblings; its action on the simple root subgroups is primeFrobenius_simpleRootSubgroup.

        The q-power Frobenius is its e-th power, for e the field exponent the index records, by frobenius_eq_primeFrobenius_pow, so the two agree on an index of prime field order. On the Suzuki and Ree G₂ constructors it is the map that the family's exceptional isogeny (TauCeti.SuzukiLieIndex.halfFrobenius, TauCeti.ReeG2LieIndex.halfFrobenius) squares to. Exceptional isogenies are not part of this uniform API.

        Equations
        Instances For

          The branch equations #

          On each of the thirteen ordinary and graph-twisted constructors the simple root subgroups and the Frobenius are those of TauCeti.GraphTwistedIndex, and on each of the four half-Frobenius constructors they are those of the family API the constructor belongs to.

          source
          theorem TauCeti.ValidLieTypeIndex.simpleRootSubgroup_A {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.A n q).Valid) :
          simpleRootSubgroup ⟨LieTypeIndex.A n q, hv⟩ = GraphTwistedIndex.simpleRootSubgroup ⟨⟨LieTypeIndex.A n q, hv⟩, ⋯⟩

          On Aₙ(q) the simple root subgroups are those of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.frobenius_A {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.A n q).Valid) :
          frobenius ⟨LieTypeIndex.A n q, hv⟩ = GraphTwistedIndex.frobenius ⟨⟨LieTypeIndex.A n q, hv⟩, ⋯⟩

          On Aₙ(q) the Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.simpleRootSubgroup_twistedA {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.twistedA n q).Valid) :
          simpleRootSubgroup ⟨LieTypeIndex.twistedA n q, hv⟩ = GraphTwistedIndex.simpleRootSubgroup ⟨⟨LieTypeIndex.twistedA n q, hv⟩, ⋯⟩

          On ²Aₙ(q) the simple root subgroups are those of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.frobenius_twistedA {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.twistedA n q).Valid) :
          frobenius ⟨LieTypeIndex.twistedA n q, hv⟩ = GraphTwistedIndex.frobenius ⟨⟨LieTypeIndex.twistedA n q, hv⟩, ⋯⟩

          On ²Aₙ(q) the Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.simpleRootSubgroup_B {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.B n q).Valid) :
          simpleRootSubgroup ⟨LieTypeIndex.B n q, hv⟩ = GraphTwistedIndex.simpleRootSubgroup ⟨⟨LieTypeIndex.B n q, hv⟩, ⋯⟩

          On Bₙ(q) the simple root subgroups are those of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.frobenius_B {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.B n q).Valid) :
          frobenius ⟨LieTypeIndex.B n q, hv⟩ = GraphTwistedIndex.frobenius ⟨⟨LieTypeIndex.B n q, hv⟩, ⋯⟩

          On Bₙ(q) the Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.simpleRootSubgroup_C {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.C n q).Valid) :
          simpleRootSubgroup ⟨LieTypeIndex.C n q, hv⟩ = GraphTwistedIndex.simpleRootSubgroup ⟨⟨LieTypeIndex.C n q, hv⟩, ⋯⟩

          On Cₙ(q) the simple root subgroups are those of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.frobenius_C {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.C n q).Valid) :
          frobenius ⟨LieTypeIndex.C n q, hv⟩ = GraphTwistedIndex.frobenius ⟨⟨LieTypeIndex.C n q, hv⟩, ⋯⟩

          On Cₙ(q) the Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.simpleRootSubgroup_D {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.D n q).Valid) :
          simpleRootSubgroup ⟨LieTypeIndex.D n q, hv⟩ = GraphTwistedIndex.simpleRootSubgroup ⟨⟨LieTypeIndex.D n q, hv⟩, ⋯⟩

          On Dₙ(q) the simple root subgroups are those of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.frobenius_D {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.D n q).Valid) :
          frobenius ⟨LieTypeIndex.D n q, hv⟩ = GraphTwistedIndex.frobenius ⟨⟨LieTypeIndex.D n q, hv⟩, ⋯⟩

          On Dₙ(q) the Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.simpleRootSubgroup_twistedD {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.twistedD n q).Valid) :
          simpleRootSubgroup ⟨LieTypeIndex.twistedD n q, hv⟩ = GraphTwistedIndex.simpleRootSubgroup ⟨⟨LieTypeIndex.twistedD n q, hv⟩, ⋯⟩

          On ²Dₙ(q) the simple root subgroups are those of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.frobenius_twistedD {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.twistedD n q).Valid) :
          frobenius ⟨LieTypeIndex.twistedD n q, hv⟩ = GraphTwistedIndex.frobenius ⟨⟨LieTypeIndex.twistedD n q, hv⟩, ⋯⟩

          On ²Dₙ(q) the Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.simpleRootSubgroup_E6 {q : PrimePower} (hv : (LieTypeIndex.E6 q).Valid) :
          simpleRootSubgroup ⟨LieTypeIndex.E6 q, hv⟩ = GraphTwistedIndex.simpleRootSubgroup ⟨⟨LieTypeIndex.E6 q, hv⟩, ⋯⟩

          On E₆(q) the simple root subgroups are those of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.frobenius_E6 {q : PrimePower} (hv : (LieTypeIndex.E6 q).Valid) :
          frobenius ⟨LieTypeIndex.E6 q, hv⟩ = GraphTwistedIndex.frobenius ⟨⟨LieTypeIndex.E6 q, hv⟩, ⋯⟩

          On E₆(q) the Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.simpleRootSubgroup_E7 {q : PrimePower} (hv : (LieTypeIndex.E7 q).Valid) :
          simpleRootSubgroup ⟨LieTypeIndex.E7 q, hv⟩ = GraphTwistedIndex.simpleRootSubgroup ⟨⟨LieTypeIndex.E7 q, hv⟩, ⋯⟩

          On E₇(q) the simple root subgroups are those of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.frobenius_E7 {q : PrimePower} (hv : (LieTypeIndex.E7 q).Valid) :
          frobenius ⟨LieTypeIndex.E7 q, hv⟩ = GraphTwistedIndex.frobenius ⟨⟨LieTypeIndex.E7 q, hv⟩, ⋯⟩

          On E₇(q) the Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.simpleRootSubgroup_E8 {q : PrimePower} (hv : (LieTypeIndex.E8 q).Valid) :
          simpleRootSubgroup ⟨LieTypeIndex.E8 q, hv⟩ = GraphTwistedIndex.simpleRootSubgroup ⟨⟨LieTypeIndex.E8 q, hv⟩, ⋯⟩

          On E₈(q) the simple root subgroups are those of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.frobenius_E8 {q : PrimePower} (hv : (LieTypeIndex.E8 q).Valid) :
          frobenius ⟨LieTypeIndex.E8 q, hv⟩ = GraphTwistedIndex.frobenius ⟨⟨LieTypeIndex.E8 q, hv⟩, ⋯⟩

          On E₈(q) the Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.simpleRootSubgroup_F4 {q : PrimePower} (hv : (LieTypeIndex.F4 q).Valid) :
          simpleRootSubgroup ⟨LieTypeIndex.F4 q, hv⟩ = GraphTwistedIndex.simpleRootSubgroup ⟨⟨LieTypeIndex.F4 q, hv⟩, ⋯⟩

          On F₄(q) the simple root subgroups are those of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.frobenius_F4 {q : PrimePower} (hv : (LieTypeIndex.F4 q).Valid) :
          frobenius ⟨LieTypeIndex.F4 q, hv⟩ = GraphTwistedIndex.frobenius ⟨⟨LieTypeIndex.F4 q, hv⟩, ⋯⟩

          On F₄(q) the Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.simpleRootSubgroup_G2 {q : PrimePower} (hv : (LieTypeIndex.G2 q).Valid) :
          simpleRootSubgroup ⟨LieTypeIndex.G2 q, hv⟩ = GraphTwistedIndex.simpleRootSubgroup ⟨⟨LieTypeIndex.G2 q, hv⟩, ⋯⟩

          On G₂(q) the simple root subgroups are those of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.frobenius_G2 {q : PrimePower} (hv : (LieTypeIndex.G2 q).Valid) :
          frobenius ⟨LieTypeIndex.G2 q, hv⟩ = GraphTwistedIndex.frobenius ⟨⟨LieTypeIndex.G2 q, hv⟩, ⋯⟩

          On G₂(q) the Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.simpleRootSubgroup_twistedE6 {q : PrimePower} (hv : (LieTypeIndex.twistedE6 q).Valid) :
          simpleRootSubgroup ⟨LieTypeIndex.twistedE6 q, hv⟩ = GraphTwistedIndex.simpleRootSubgroup ⟨⟨LieTypeIndex.twistedE6 q, hv⟩, ⋯⟩

          On ²E₆(q) the simple root subgroups are those of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.frobenius_twistedE6 {q : PrimePower} (hv : (LieTypeIndex.twistedE6 q).Valid) :
          frobenius ⟨LieTypeIndex.twistedE6 q, hv⟩ = GraphTwistedIndex.frobenius ⟨⟨LieTypeIndex.twistedE6 q, hv⟩, ⋯⟩

          On ²E₆(q) the Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.simpleRootSubgroup_trialityD4 {q : PrimePower} (hv : (LieTypeIndex.trialityD4 q).Valid) :
          simpleRootSubgroup ⟨LieTypeIndex.trialityD4 q, hv⟩ = GraphTwistedIndex.simpleRootSubgroup ⟨⟨LieTypeIndex.trialityD4 q, hv⟩, ⋯⟩

          On ³D₄(q) the simple root subgroups are those of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.frobenius_trialityD4 {q : PrimePower} (hv : (LieTypeIndex.trialityD4 q).Valid) :
          frobenius ⟨LieTypeIndex.trialityD4 q, hv⟩ = GraphTwistedIndex.frobenius ⟨⟨LieTypeIndex.trialityD4 q, hv⟩, ⋯⟩

          On ³D₄(q) the Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.simpleRootSubgroup_suzuki {m : ℕ} (hv : (LieTypeIndex.suzuki m).Valid) :
          simpleRootSubgroup ⟨LieTypeIndex.suzuki m, hv⟩ = (RankTwoBLieIndex.ofSuzuki m hv).simpleRootSubgroup

          On ²B₂(2^(2m+1)) the simple root subgroups are those of the rank-two symplectic carrier.

          source
          theorem TauCeti.ValidLieTypeIndex.frobenius_suzuki {m : ℕ} (hv : (LieTypeIndex.suzuki m).Valid) :
          frobenius ⟨LieTypeIndex.suzuki m, hv⟩ = (RankTwoBLieIndex.ofSuzuki m hv).frobenius

          On ²B₂(2^(2m+1)) the Frobenius is that of the rank-two symplectic carrier.

          source
          theorem TauCeti.ValidLieTypeIndex.simpleRootSubgroup_reeG2 {m : ℕ} (hv : (LieTypeIndex.reeG2 m).Valid) :
          simpleRootSubgroup ⟨LieTypeIndex.reeG2 m, hv⟩ = (ReeG2LieIndex.of m hv).simpleRootSubgroup

          On ²G₂(3^(2m+1)) the simple root subgroups are those of the family.

          source
          theorem TauCeti.ValidLieTypeIndex.frobenius_reeG2 {m : ℕ} (hv : (LieTypeIndex.reeG2 m).Valid) :
          frobenius ⟨LieTypeIndex.reeG2 m, hv⟩ = (ReeG2LieIndex.of m hv).frobenius

          On ²G₂(3^(2m+1)) the Frobenius is that of the family.

          source
          theorem TauCeti.ValidLieTypeIndex.simpleRootSubgroup_reeF4 {m : ℕ} (hv : (LieTypeIndex.reeF4 m).Valid) :
          simpleRootSubgroup ⟨LieTypeIndex.reeF4 m, hv⟩ = (ReeF4LieIndex.of m hv).simpleRootSubgroup

          On ²F₄(2^(2m+1)) the simple root subgroups are those of the family.

          source
          theorem TauCeti.ValidLieTypeIndex.frobenius_reeF4 {m : ℕ} (hv : (LieTypeIndex.reeF4 m).Valid) :
          frobenius ⟨LieTypeIndex.reeF4 m, hv⟩ = (ReeF4LieIndex.of m hv).frobenius

          On ²F₄(2^(2m+1)) the Frobenius is that of the family.

          source
          theorem TauCeti.ValidLieTypeIndex.simpleRootSubgroup_tits (hv : LieTypeIndex.tits.Valid) :
          simpleRootSubgroup ⟨LieTypeIndex.tits, hv⟩ = TitsLieIndex.of.simpleRootSubgroup

          On the Tits index the simple root subgroups are those of the Tits construction.

          source
          theorem TauCeti.ValidLieTypeIndex.frobenius_tits (hv : LieTypeIndex.tits.Valid) :
          frobenius ⟨LieTypeIndex.tits, hv⟩ = TitsLieIndex.of.frobenius

          On the Tits index the Frobenius is that of the Tits construction.

          source
          theorem TauCeti.ValidLieTypeIndex.primeFrobenius_A {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.A n q).Valid) :
          primeFrobenius ⟨LieTypeIndex.A n q, hv⟩ = GraphTwistedIndex.primeFrobenius ⟨⟨LieTypeIndex.A n q, hv⟩, ⋯⟩

          On Aₙ(q) the prime-field Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.primeFrobenius_twistedA {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.twistedA n q).Valid) :
          primeFrobenius ⟨LieTypeIndex.twistedA n q, hv⟩ = GraphTwistedIndex.primeFrobenius ⟨⟨LieTypeIndex.twistedA n q, hv⟩, ⋯⟩

          On ²Aₙ(q) the prime-field Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.primeFrobenius_B {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.B n q).Valid) :
          primeFrobenius ⟨LieTypeIndex.B n q, hv⟩ = GraphTwistedIndex.primeFrobenius ⟨⟨LieTypeIndex.B n q, hv⟩, ⋯⟩

          On Bₙ(q) the prime-field Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.primeFrobenius_C {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.C n q).Valid) :
          primeFrobenius ⟨LieTypeIndex.C n q, hv⟩ = GraphTwistedIndex.primeFrobenius ⟨⟨LieTypeIndex.C n q, hv⟩, ⋯⟩

          On Cₙ(q) the prime-field Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.primeFrobenius_D {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.D n q).Valid) :
          primeFrobenius ⟨LieTypeIndex.D n q, hv⟩ = GraphTwistedIndex.primeFrobenius ⟨⟨LieTypeIndex.D n q, hv⟩, ⋯⟩

          On Dₙ(q) the prime-field Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.primeFrobenius_twistedD {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.twistedD n q).Valid) :
          primeFrobenius ⟨LieTypeIndex.twistedD n q, hv⟩ = GraphTwistedIndex.primeFrobenius ⟨⟨LieTypeIndex.twistedD n q, hv⟩, ⋯⟩

          On ²Dₙ(q) the prime-field Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.primeFrobenius_E6 {q : PrimePower} (hv : (LieTypeIndex.E6 q).Valid) :
          primeFrobenius ⟨LieTypeIndex.E6 q, hv⟩ = GraphTwistedIndex.primeFrobenius ⟨⟨LieTypeIndex.E6 q, hv⟩, ⋯⟩

          On E₆(q) the prime-field Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.primeFrobenius_E7 {q : PrimePower} (hv : (LieTypeIndex.E7 q).Valid) :
          primeFrobenius ⟨LieTypeIndex.E7 q, hv⟩ = GraphTwistedIndex.primeFrobenius ⟨⟨LieTypeIndex.E7 q, hv⟩, ⋯⟩

          On E₇(q) the prime-field Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.primeFrobenius_E8 {q : PrimePower} (hv : (LieTypeIndex.E8 q).Valid) :
          primeFrobenius ⟨LieTypeIndex.E8 q, hv⟩ = GraphTwistedIndex.primeFrobenius ⟨⟨LieTypeIndex.E8 q, hv⟩, ⋯⟩

          On E₈(q) the prime-field Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.primeFrobenius_F4 {q : PrimePower} (hv : (LieTypeIndex.F4 q).Valid) :
          primeFrobenius ⟨LieTypeIndex.F4 q, hv⟩ = GraphTwistedIndex.primeFrobenius ⟨⟨LieTypeIndex.F4 q, hv⟩, ⋯⟩

          On F₄(q) the prime-field Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.primeFrobenius_G2 {q : PrimePower} (hv : (LieTypeIndex.G2 q).Valid) :
          primeFrobenius ⟨LieTypeIndex.G2 q, hv⟩ = GraphTwistedIndex.primeFrobenius ⟨⟨LieTypeIndex.G2 q, hv⟩, ⋯⟩

          On G₂(q) the prime-field Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.primeFrobenius_twistedE6 {q : PrimePower} (hv : (LieTypeIndex.twistedE6 q).Valid) :
          primeFrobenius ⟨LieTypeIndex.twistedE6 q, hv⟩ = GraphTwistedIndex.primeFrobenius ⟨⟨LieTypeIndex.twistedE6 q, hv⟩, ⋯⟩

          On ²E₆(q) the prime-field Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.primeFrobenius_trialityD4 {q : PrimePower} (hv : (LieTypeIndex.trialityD4 q).Valid) :
          primeFrobenius ⟨LieTypeIndex.trialityD4 q, hv⟩ = GraphTwistedIndex.primeFrobenius ⟨⟨LieTypeIndex.trialityD4 q, hv⟩, ⋯⟩

          On ³D₄(q) the prime-field Frobenius is that of the graph-twisted assembly.

          source
          theorem TauCeti.ValidLieTypeIndex.primeFrobenius_suzuki {m : ℕ} (hv : (LieTypeIndex.suzuki m).Valid) :
          primeFrobenius ⟨LieTypeIndex.suzuki m, hv⟩ = (RankTwoBLieIndex.ofSuzuki m hv).primeFrobenius

          On ²B₂(2^(2m+1)) the prime-field Frobenius is that of the rank-two symplectic carrier.

          source
          theorem TauCeti.ValidLieTypeIndex.primeFrobenius_reeG2 {m : ℕ} (hv : (LieTypeIndex.reeG2 m).Valid) :
          primeFrobenius ⟨LieTypeIndex.reeG2 m, hv⟩ = (ReeG2LieIndex.of m hv).primeFrobenius

          On ²G₂(3^(2m+1)) the prime-field Frobenius is that of the family.

          source
          theorem TauCeti.ValidLieTypeIndex.primeFrobenius_reeF4 {m : ℕ} (hv : (LieTypeIndex.reeF4 m).Valid) :
          primeFrobenius ⟨LieTypeIndex.reeF4 m, hv⟩ = (ReeF4LieIndex.of m hv).primeFrobenius

          On ²F₄(2^(2m+1)) the prime-field Frobenius is that of the family.

          source
          theorem TauCeti.ValidLieTypeIndex.primeFrobenius_tits (hv : LieTypeIndex.tits.Valid) :
          primeFrobenius ⟨LieTypeIndex.tits, hv⟩ = TitsLieIndex.of.frobenius

          On the Tits index the prime-field Frobenius is the Frobenius of the Tits construction: that index records field order two, so its q-power Frobenius is already the 2-power one and the family names no second map.

          The Frobenius equation #

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

          The Frobenius has the pinned action on every simple root subgroup. It sends x_i(u) to x_i(u ^ q), where q is the field order the index records. This is the defining equation of the q-power Frobenius, now stated once for all seventeen constructors.

          source
          @[simp]
          theorem TauCeti.ValidLieTypeIndex.primeFrobenius_simpleRootSubgroup (d : ValidLieTypeIndex) (i : Fin d.rank) (u : Multiplicative d.Closure) :
          d.primeFrobenius ((d.simpleRootSubgroup i) u) = (d.simpleRootSubgroup i) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ d.characteristic))

          The prime-field Frobenius has the pinned action on every simple root subgroup. It sends x_i(u) to x_i(u ^ p), where p is the defining characteristic of the index. This is the defining equation of the prime-field Frobenius, stated once for all seventeen constructors.

          source
          theorem TauCeti.ValidLieTypeIndex.frobenius_eq_primeFrobenius_pow (d : ValidLieTypeIndex) :
          d.frobenius = (have this := d.primeFrobenius; this) ^ d.fieldExponent

          The q-power Frobenius is the e-th power of the prime-field Frobenius, for e the field exponent the index records, stated once for all seventeen constructors. On an index of prime field order, the Tits index among them, the exponent is one and the two maps agree.