Documentation

TauCeti.GroupTheory.SpecificGroups.CFSG.Assembly.GraphTwisted

The candidate groups of the ordinary and graph-twisted Lie-type families #

Thirteen of the seventeen Lie-type constructors take an ordinary Steinberg endomorphism, the field Frobenius composed with a graph automorphism, and TauCeti.GraphTwistedIndex is exactly the subtype of those thirteen. Each of them already has its own carrier, numbered simple root subgroups, Steinberg endomorphism and candidate group, built family by family on the carrier assigned to it:

ConstructorsFamily API
A, twistedATauCeti.TypeALieIndex, on the special linear carrier
BTauCeti.TypeBLieIndex, on the full-weight type-B spin carrier
CTauCeti.TypeCLieIndex, on the standard symplectic carrier
DTauCeti.TypeDLieIndex, on the full-weight type-D spin carrier
twistedDTauCeti.TypeTwistedDLieIndex, on the same spin carrier
trialityD4TauCeti.TypeTrialityD4LieIndex, on the tripled D₄ carrier
E6TauCeti.TypeE6LieIndex, on the 27-dimensional minuscule carrier
twistedE6TauCeti.TypeTwistedE6LieIndex, on the doubled minuscule carrier
E7TauCeti.TypeE7LieIndex, on the 56-dimensional minuscule carrier
E8, F4, G2TauCeti.UnimodularExceptionalIndex, on the Geck carrier

This file joins them into one construction on TauCeti.GraphTwistedIndex, by cases on the constructor: the ambient group TauCeti.GraphTwistedIndex.AmbientGroup, its numbered simple root subgroups, its q-power Frobenius, the Steinberg endomorphism, its fixed points, and the candidate group TauCeti.GraphTwistedIndex.Group, the derived subgroup of the fixed points modulo its centre. Each branch is the family construction, with no new carrier or map; the branch equations TauCeti.GraphTwistedIndex.steinberg_A and its twelve siblings, and likewise for the simple root subgroups and the Frobenius, say which one. The four Suzuki--Ree and Tits constructors are not indices of the subtype, and their branches are closed by that hypothesis rather than by a chosen value.

Beside the q-power Frobenius the assembly carries the prime-field Frobenius TauCeti.GraphTwistedIndex.primeFrobenius, the p-power map for p the defining characteristic, of which the q-power map is the e-th power, for e the field exponent the index records. The two agree on an index of prime field order.

The two factors of the Steinberg endomorphism are assembled separately as well: its Frobenius factor is TauCeti.GraphTwistedIndex.frobenius and its graph factor is TauCeti.GraphTwistedIndex.graphAut, the automorphism of the ambient group realizing the diagram permutation the index carries, the identity on the nine untwisted families. They recompose by TauCeti.GraphTwistedIndex.steinberg_eq_graphAut_comp_frobenius, in either order since they commute.

What the assembly buys is a single statement of the pinned equations for all thirteen families, TauCeti.GraphTwistedIndex.frobenius_simpleRootSubgroup and TauCeti.GraphTwistedIndex.steinberg_simpleRootSubgroup:

Frob_q (x_i(u)) = x_i(u ^ q),        F (x_i(u)) = x_{σ i}(u ^ q),

where σ is TauCeti.GraphTwistedIndex.diagramPerm, the identity on the nine untwisted families, and q is the field order the index records. On those nine families the Steinberg endomorphism is the Frobenius itself, TauCeti.GraphTwistedIndex.steinberg_eq_frobenius: the A, B, C and D family APIs name their Frobenius separately and the assembly takes it, while the E₆, E₇, E₈, F₄ and G₂ family APIs name only the Steinberg endomorphism, which is the Frobenius, and the assembly takes that. On the four graph-twisted families the Steinberg endomorphism is the graph automorphism composed with the Frobenius, and the Frobenius is the right-hand factor of that composite.

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 a candidate group is finite, perfect or simple.

Main definitions #

Main results #

References #

source
def TauCeti.GraphTwistedIndex.AmbientGroup :
GraphTwistedIndex → Type

The ambient group of an ordinary or graph-twisted 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. The two families on a type-D diagram other than ³D₄(q) share the spin carrier of TauCeti.TypeDDiagramLieIndex, while ³D₄(q) runs on the tripled carrier that carries triality.

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

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

    Equations
    source
    noncomputable def TauCeti.GraphTwistedIndex.simpleRootSubgroup (d : GraphTwistedIndex) :
    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 family's carrier, by simpleRootSubgroup_A and its siblings.

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

      The q-power Frobenius endomorphism of an ordinary or graph-twisted index, for q the field order the index records. On each constructor it is the Frobenius of the family, by frobenius_A and its siblings: the family's own frobenius where the family API names one (A, twistedA, B, C, D, twistedD, twistedE6, trialityD4), and the family's Steinberg endomorphism on E6, E7, E8, F4 and G2, where that endomorphism is the Frobenius itself. On the nine untwisted families it agrees with steinberg, by steinberg_eq_frobenius; on the four graph-twisted ones it is the Frobenius factor of the family's Steinberg composite. Its action on the simple root subgroups is frobenius_simpleRootSubgroup.

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

        The prime-field Frobenius endomorphism of an ordinary or graph-twisted index, the p-power map for p the defining characteristic. On each constructor it is the prime-field Frobenius of the family, by primeFrobenius_A and its siblings. 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. Its action on the simple root subgroups is primeFrobenius_simpleRootSubgroup.

        Equations
        Instances For
          source
          noncomputable def TauCeti.GraphTwistedIndex.steinberg (d : GraphTwistedIndex) :
          d.AmbientGroup →* d.AmbientGroup

          The Steinberg endomorphism of an ordinary or graph-twisted index: the q-power Frobenius on the nine untwisted families, and the graph automorphism of the family composed with it on ²Aₙ(q), ²Dₙ(q), ²E₆(q) and ³D₄(q). On each constructor it is the Steinberg endomorphism of the family, by steinberg_A and its siblings; its action on the simple root subgroups is steinberg_simpleRootSubgroup.

          Equations
          Instances For

            The branch equations #

            On each of the thirteen constructors the Steinberg endomorphism, the simple root subgroups and the Frobenius are those of the family API the constructor belongs to.

            source
            theorem TauCeti.GraphTwistedIndex.steinberg_A {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.A n q).Valid) :
            steinberg ⟨⟨LieTypeIndex.A n q, hv⟩, ⋯⟩ = TypeALieIndex.steinberg ⟨⟨LieTypeIndex.A n q, hv⟩, ⋯⟩

            On Aₙ(q) the Steinberg endomorphism is that of the family.

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

            On Aₙ(q) the simple root subgroups are those of the family.

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

            On Aₙ(q) the Frobenius is that of the family.

            source
            theorem TauCeti.GraphTwistedIndex.steinberg_twistedA {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.twistedA n q).Valid) :
            steinberg ⟨⟨LieTypeIndex.twistedA n q, hv⟩, ⋯⟩ = TypeALieIndex.steinberg ⟨⟨LieTypeIndex.twistedA n q, hv⟩, ⋯⟩

            On ²Aₙ(q) the Steinberg endomorphism is that of the family.

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

            On ²Aₙ(q) the simple root subgroups are those of the family.

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

            On ²Aₙ(q) the Frobenius is that of the family.

            source
            theorem TauCeti.GraphTwistedIndex.steinberg_B {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.B n q).Valid) :
            steinberg ⟨⟨LieTypeIndex.B n q, hv⟩, ⋯⟩ = TypeBLieIndex.steinberg ⟨⟨LieTypeIndex.B n q, hv⟩, trivial⟩

            On Bₙ(q) the Steinberg endomorphism is that of the family.

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

            On Bₙ(q) the simple root subgroups are those of the family.

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

            On Bₙ(q) the Frobenius is that of the family.

            source
            theorem TauCeti.GraphTwistedIndex.steinberg_C {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.C n q).Valid) :
            steinberg ⟨⟨LieTypeIndex.C n q, hv⟩, ⋯⟩ = TypeCLieIndex.steinberg ⟨⟨LieTypeIndex.C n q, hv⟩, trivial⟩

            On Cₙ(q) the Steinberg endomorphism is that of the family.

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

            On Cₙ(q) the simple root subgroups are those of the family.

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

            On Cₙ(q) the Frobenius is that of the family.

            source
            theorem TauCeti.GraphTwistedIndex.steinberg_D {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.D n q).Valid) :
            steinberg ⟨⟨LieTypeIndex.D n q, hv⟩, ⋯⟩ = TypeDLieIndex.steinberg ⟨⟨LieTypeIndex.D n q, hv⟩, ⋯⟩

            On Dₙ(q) the Steinberg endomorphism is that of the family.

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

            On Dₙ(q) the simple root subgroups are those of the family.

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

            On Dₙ(q) the Frobenius is that of the family.

            source
            theorem TauCeti.GraphTwistedIndex.steinberg_twistedD {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.twistedD n q).Valid) :
            steinberg ⟨⟨LieTypeIndex.twistedD n q, hv⟩, ⋯⟩ = TypeTwistedDLieIndex.steinberg ⟨⟨LieTypeIndex.twistedD n q, hv⟩, ⋯⟩

            On ²Dₙ(q) the Steinberg endomorphism is that of the family.

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

            On ²Dₙ(q) the simple root subgroups are those of the family.

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

            On ²Dₙ(q) the Frobenius is that of the family.

            source
            theorem TauCeti.GraphTwistedIndex.steinberg_E6 {q : PrimePower} (hv : (LieTypeIndex.E6 q).Valid) :
            steinberg ⟨⟨LieTypeIndex.E6 q, hv⟩, ⋯⟩ = TypeE6LieIndex.steinberg ⟨⟨LieTypeIndex.E6 q, hv⟩, ⋯⟩

            On E₆(q) the Steinberg endomorphism is that of the family.

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

            On E₆(q) the simple root subgroups are those of the family.

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

            On E₆(q) the Frobenius is the Steinberg endomorphism of the family, that family being untwisted.

            source
            theorem TauCeti.GraphTwistedIndex.steinberg_E7 {q : PrimePower} (hv : (LieTypeIndex.E7 q).Valid) :
            steinberg ⟨⟨LieTypeIndex.E7 q, hv⟩, ⋯⟩ = TypeE7LieIndex.steinberg ⟨⟨LieTypeIndex.E7 q, hv⟩, ⋯⟩

            On E₇(q) the Steinberg endomorphism is that of the family.

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

            On E₇(q) the simple root subgroups are those of the family.

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

            On E₇(q) the Frobenius is the Steinberg endomorphism of the family, that family being untwisted.

            source
            theorem TauCeti.GraphTwistedIndex.steinberg_E8 {q : PrimePower} (hv : (LieTypeIndex.E8 q).Valid) :
            steinberg ⟨⟨LieTypeIndex.E8 q, hv⟩, ⋯⟩ = UnimodularExceptionalIndex.steinberg ⟨⟨⟨LieTypeIndex.E8 q, hv⟩, ⋯⟩, ⋯⟩

            On E₈(q) the Steinberg endomorphism is that of the family.

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

            On E₈(q) the simple root subgroups are those of the family.

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

            On E₈(q) the Frobenius is the Steinberg endomorphism of the family, that family being untwisted.

            source
            theorem TauCeti.GraphTwistedIndex.steinberg_F4 {q : PrimePower} (hv : (LieTypeIndex.F4 q).Valid) :
            steinberg ⟨⟨LieTypeIndex.F4 q, hv⟩, ⋯⟩ = UnimodularExceptionalIndex.steinberg ⟨⟨⟨LieTypeIndex.F4 q, hv⟩, ⋯⟩, ⋯⟩

            On F₄(q) the Steinberg endomorphism is that of the family.

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

            On F₄(q) the simple root subgroups are those of the family.

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

            On F₄(q) the Frobenius is the Steinberg endomorphism of the family, that family being untwisted.

            source
            theorem TauCeti.GraphTwistedIndex.steinberg_G2 {q : PrimePower} (hv : (LieTypeIndex.G2 q).Valid) :
            steinberg ⟨⟨LieTypeIndex.G2 q, hv⟩, ⋯⟩ = UnimodularExceptionalIndex.steinberg ⟨⟨⟨LieTypeIndex.G2 q, hv⟩, ⋯⟩, ⋯⟩

            On G₂(q) the Steinberg endomorphism is that of the family.

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

            On G₂(q) the simple root subgroups are those of the family.

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

            On G₂(q) the Frobenius is the Steinberg endomorphism of the family, that family being untwisted.

            source
            theorem TauCeti.GraphTwistedIndex.steinberg_twistedE6 {q : PrimePower} (hv : (LieTypeIndex.twistedE6 q).Valid) :
            steinberg ⟨⟨LieTypeIndex.twistedE6 q, hv⟩, ⋯⟩ = TypeTwistedE6LieIndex.steinberg ⟨⟨LieTypeIndex.twistedE6 q, hv⟩, ⋯⟩

            On ²E₆(q) the Steinberg endomorphism is that of the family.

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

            On ²E₆(q) the simple root subgroups are those of the family.

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

            On ²E₆(q) the Frobenius is that of the family.

            source
            theorem TauCeti.GraphTwistedIndex.steinberg_trialityD4 {q : PrimePower} (hv : (LieTypeIndex.trialityD4 q).Valid) :
            steinberg ⟨⟨LieTypeIndex.trialityD4 q, hv⟩, ⋯⟩ = TypeTrialityD4LieIndex.steinberg ⟨⟨LieTypeIndex.trialityD4 q, hv⟩, ⋯⟩

            On ³D₄(q) the Steinberg endomorphism is that of the family.

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

            On ³D₄(q) the simple root subgroups are those of the family.

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

            On ³D₄(q) the Frobenius is that of the family.

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

            On Aₙ(q) the prime-field Frobenius is that of the family.

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

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

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

            On Bₙ(q) the prime-field Frobenius is that of the family.

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

            On Cₙ(q) the prime-field Frobenius is that of the family.

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

            On Dₙ(q) the prime-field Frobenius is that of the family.

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

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

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

            On E₆(q) the prime-field Frobenius is that of the family.

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

            On E₇(q) the prime-field Frobenius is that of the family.

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

            On E₈(q) the prime-field Frobenius is that of the Geck carrier family.

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

            On F₄(q) the prime-field Frobenius is that of the Geck carrier family.

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

            On G₂(q) the prime-field Frobenius is that of the Geck carrier family.

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

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

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

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

            The pinned equations #

            source
            @[simp]
            theorem TauCeti.GraphTwistedIndex.frobenius_simpleRootSubgroup (d : GraphTwistedIndex) (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 thirteen families.

            source
            @[simp]
            theorem TauCeti.GraphTwistedIndex.primeFrobenius_simpleRootSubgroup (d : GraphTwistedIndex) (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. This is the defining equation of the prime-field Frobenius, stated once for all thirteen families.

            source
            theorem TauCeti.GraphTwistedIndex.frobenius_eq_primeFrobenius_pow (d : GraphTwistedIndex) :
            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 thirteen families. On an index of prime field order the exponent is one and the two maps agree.

            source
            @[simp]
            theorem TauCeti.GraphTwistedIndex.steinberg_simpleRootSubgroup (d : GraphTwistedIndex) (i : Fin (↑d).rank) (u : Multiplicative (↑d).Closure) :
            d.steinberg ((d.simpleRootSubgroup i) u) = (d.simpleRootSubgroup (d.diagramPerm i)) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ (↑d).fieldOrder))

            The Steinberg endomorphism has the pinned action on every simple root subgroup. It sends x_i(u) to x_{σ i}(u ^ q), where σ is the diagram permutation of the index, the identity on the nine untwisted families, and q is its recorded field order. This is the defining equation of an ordinary or graph-twisted Steinberg endomorphism, now stated once for all thirteen families.

            source
            theorem TauCeti.GraphTwistedIndex.steinberg_eq_frobenius (d : GraphTwistedIndex) (hd : d.twistOrder = 1) :
            d.steinberg = d.frobenius

            On an untwisted index the Steinberg endomorphism is the Frobenius. The hypothesis d.twistOrder = 1 picks out the nine untwisted families, on which the diagram permutation is trivial; on the four graph-twisted families the two maps differ by the graph automorphism, the family relations TauCeti.TypeALieIndex.steinberg_eq_graphAut_comp_frobenius, TauCeti.TypeTwistedDLieIndex.steinberg_def, TauCeti.TypeTwistedE6LieIndex.steinberg_def and TauCeti.TypeTrialityD4LieIndex.steinberg_def.

            The graph automorphism factor #

            The Steinberg endomorphism assembled above factors as γ ∘ Frob_q, and its Frobenius factor is frobenius. This section assembles the remaining factor, the automorphism γ of the ambient group realizing the diagram permutation the index carries, together with the three equations that make it that factor rather than an unrelated automorphism.

            source
            noncomputable def TauCeti.GraphTwistedIndex.graphAut (d : GraphTwistedIndex) :
            MulAut d.AmbientGroup

            The graph automorphism of an ordinary or graph-twisted index: the automorphism of the ambient group realizing the diagram permutation TauCeti.GraphTwistedIndex.diagramPerm the index carries. On the four graph-twisted constructors it is the graph automorphism of the family, by graphAut_twistedA and its siblings; on the nine untwisted constructors, whose diagram permutation is trivial, it is the identity automorphism. Its action on the simple root subgroups is graphAut_simpleRootSubgroup, and it is the left-hand factor of the Steinberg endomorphism, by steinberg_eq_graphAut_comp_frobenius.

            Equations
            Instances For

              The branch equations of the graph automorphism #

              On each of the thirteen constructors the graph automorphism is that of the family the constructor belongs to, or the identity automorphism where the family API names none.

              source
              theorem TauCeti.GraphTwistedIndex.graphAut_A {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.A n q).Valid) :
              graphAut ⟨⟨LieTypeIndex.A n q, hv⟩, ⋯⟩ = TypeALieIndex.graphAut ⟨⟨LieTypeIndex.A n q, hv⟩, ⋯⟩

              On Aₙ(q) the graph automorphism is that of the type-A family, which is trivial there.

              source
              theorem TauCeti.GraphTwistedIndex.graphAut_twistedA {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.twistedA n q).Valid) :
              graphAut ⟨⟨LieTypeIndex.twistedA n q, hv⟩, ⋯⟩ = TypeALieIndex.graphAut ⟨⟨LieTypeIndex.twistedA n q, hv⟩, ⋯⟩

              On ²Aₙ(q) the graph automorphism is that of the type-A family, signed reverse inverse transpose.

              source
              theorem TauCeti.GraphTwistedIndex.graphAut_B {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.B n q).Valid) :
              graphAut ⟨⟨LieTypeIndex.B n q, hv⟩, ⋯⟩ = 1

              On Bₙ(q) the graph automorphism is the identity, the Bₙ diagram having no automorphism: its two root lengths are not exchanged by any permutation of the nodes preserving the Cartan matrix.

              source
              theorem TauCeti.GraphTwistedIndex.graphAut_C {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.C n q).Valid) :
              graphAut ⟨⟨LieTypeIndex.C n q, hv⟩, ⋯⟩ = 1

              On Cₙ(q) the graph automorphism is the identity, the Cₙ diagram having no automorphism.

              source
              theorem TauCeti.GraphTwistedIndex.graphAut_D {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.D n q).Valid) :
              graphAut ⟨⟨LieTypeIndex.D n q, hv⟩, ⋯⟩ = 1

              On Dₙ(q) the graph automorphism is the identity: the fork exchange of the Dₙ diagram is the twist of ²Dₙ(q), and the untwisted family does not use it.

              source
              theorem TauCeti.GraphTwistedIndex.graphAut_twistedD {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.twistedD n q).Valid) :
              graphAut ⟨⟨LieTypeIndex.twistedD n q, hv⟩, ⋯⟩ = TypeTwistedDLieIndex.graphAut ⟨⟨LieTypeIndex.twistedD n q, hv⟩, ⋯⟩

              On ²Dₙ(q) the graph automorphism is that of the family, the fork exchange of the spin carrier.

              source
              theorem TauCeti.GraphTwistedIndex.graphAut_E6 {q : PrimePower} (hv : (LieTypeIndex.E6 q).Valid) :
              graphAut ⟨⟨LieTypeIndex.E6 q, hv⟩, ⋯⟩ = 1

              On E₆(q) the graph automorphism is the identity: the E₆ diagram symmetry is the twist of ²E₆(q), and the untwisted family does not use it.

              source
              theorem TauCeti.GraphTwistedIndex.graphAut_E7 {q : PrimePower} (hv : (LieTypeIndex.E7 q).Valid) :
              graphAut ⟨⟨LieTypeIndex.E7 q, hv⟩, ⋯⟩ = 1

              On E₇(q) the graph automorphism is the identity, the E₇ diagram having no automorphism.

              source
              theorem TauCeti.GraphTwistedIndex.graphAut_E8 {q : PrimePower} (hv : (LieTypeIndex.E8 q).Valid) :
              graphAut ⟨⟨LieTypeIndex.E8 q, hv⟩, ⋯⟩ = 1

              On E₈(q) the graph automorphism is the identity, the E₈ diagram having no automorphism.

              source
              theorem TauCeti.GraphTwistedIndex.graphAut_F4 {q : PrimePower} (hv : (LieTypeIndex.F4 q).Valid) :
              graphAut ⟨⟨LieTypeIndex.F4 q, hv⟩, ⋯⟩ = 1

              On F₄(q) the graph automorphism is the identity: the length-exchanging symmetry of the F₄ diagram is not a diagram automorphism, and this family is untwisted.

              source
              theorem TauCeti.GraphTwistedIndex.graphAut_G2 {q : PrimePower} (hv : (LieTypeIndex.G2 q).Valid) :
              graphAut ⟨⟨LieTypeIndex.G2 q, hv⟩, ⋯⟩ = 1

              On G₂(q) the graph automorphism is the identity: the length-exchanging symmetry of the G₂ diagram is not a diagram automorphism, and this family is untwisted.

              source
              theorem TauCeti.GraphTwistedIndex.graphAut_twistedE6 {q : PrimePower} (hv : (LieTypeIndex.twistedE6 q).Valid) :
              graphAut ⟨⟨LieTypeIndex.twistedE6 q, hv⟩, ⋯⟩ = TypeTwistedE6LieIndex.graphAut ⟨⟨LieTypeIndex.twistedE6 q, hv⟩, ⋯⟩

              On ²E₆(q) the graph automorphism is that of the family, the exchange of the two minuscule summands of the doubled carrier.

              source
              theorem TauCeti.GraphTwistedIndex.graphAut_trialityD4 {q : PrimePower} (hv : (LieTypeIndex.trialityD4 q).Valid) :
              graphAut ⟨⟨LieTypeIndex.trialityD4 q, hv⟩, ⋯⟩ = TypeTrialityD4LieIndex.graphAut ⟨⟨LieTypeIndex.trialityD4 q, hv⟩, ⋯⟩

              On ³D₄(q) the graph automorphism is that of the family, triality on the tripled carrier.

              The pinned equations of the graph automorphism #

              source
              theorem TauCeti.GraphTwistedIndex.graphAut_eq_one_of_twistOrder_eq_one (d : GraphTwistedIndex) (hd : d.twistOrder = 1) :
              d.graphAut = 1

              On an untwisted index the graph automorphism is the identity. The hypothesis d.twistOrder = 1 picks out the nine untwisted families, whose diagram permutation is trivial and whose Steinberg endomorphism is the Frobenius outright; on the four graph-twisted families the twist order is two or three.

              source
              @[simp]
              theorem TauCeti.GraphTwistedIndex.graphAut_simpleRootSubgroup (d : GraphTwistedIndex) (i : Fin (↑d).rank) (u : Multiplicative (↑d).Closure) :
              d.graphAut ((d.simpleRootSubgroup i) u) = (d.simpleRootSubgroup (d.diagramPerm i)) u

              The graph automorphism has the pinned action on every simple root subgroup. It sends x_i(u) to x_{σ i}(u), where σ is the diagram permutation of the index, the identity on the nine untwisted families. The parameter is carried across unchanged, with neither a field power nor a sign; on a general root the equation would acquire a sign forced by the Chevalley structure constants.

              source
              theorem TauCeti.GraphTwistedIndex.graphAut_pow_twistOrder (d : GraphTwistedIndex) :
              d.graphAut ^ d.twistOrder = 1

              The twist order of the index annihilates its graph automorphism, so γ = 1 on the nine untwisted families, γ ^ 2 = 1 on ²Aₙ(q), ²Dₙ(q) and ²E₆(q), and γ ^ 3 = 1 on ³D₄(q). This matches TauCeti.GraphTwistedIndex.diagramPerm_pow_twistOrder on the diagram permutation that γ realizes.

              source
              theorem TauCeti.GraphTwistedIndex.graphAut_comp_frobenius (d : GraphTwistedIndex) :
              (MulEquiv.toMonoidHom d.graphAut).comp d.frobenius = d.frobenius.comp (MulEquiv.toMonoidHom d.graphAut)

              The graph automorphism commutes with the Frobenius, as an identity of endomorphisms: γ ∘ Frob_q = Frob_q ∘ γ. This is what makes the order of composition immaterial in steinberg_eq_graphAut_comp_frobenius, and on the graph-twisted families it is the relation that lets a power of the Steinberg endomorphism be computed factor by factor.

              source
              theorem TauCeti.GraphTwistedIndex.steinberg_eq_graphAut_comp_frobenius (d : GraphTwistedIndex) :
              d.steinberg = (MulEquiv.toMonoidHom d.graphAut).comp d.frobenius

              The Steinberg endomorphism is the graph automorphism composed with the Frobenius, uniformly in the thirteen ordinary and graph-twisted families. On the nine untwisted ones the graph factor is trivial and the composite is the Frobenius itself, which is TauCeti.GraphTwistedIndex.steinberg_eq_frobenius.

              source
              theorem TauCeti.GraphTwistedIndex.steinberg_eq_frobenius_comp_graphAut (d : GraphTwistedIndex) :
              d.steinberg = d.frobenius.comp (MulEquiv.toMonoidHom d.graphAut)

              The Steinberg endomorphism may equally be read with its Frobenius factor last, the two factors commuting.

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

              The fixed subgroup of the Steinberg endomorphism of an ordinary or graph-twisted index.

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

                The finite-simple-group candidate attached to an ordinary or graph-twisted index: the derived subgroup of the fixed points of its Steinberg endomorphism, modulo the centre of that derived subgroup. On each constructor it is the candidate group of the family, the Steinberg endomorphisms agreeing by steinberg_A and its siblings. No finiteness or simplicity assertion is part of this definition, nor any identification of the carrier with the pinned simply connected group scheme of the diagram.

                Equations
                Instances For