Diagram permutations of the graph-twisted families

The Steinberg endomorphism of a finite group of Lie type that is not of Suzuki--Ree type is the field Frobenius composed with a graph automorphism γ of the underlying pinned Chevalley group. That automorphism is determined by a permutation of the Bourbaki-numbered simple roots, and this file attaches that permutation to every index it can occur for, namely to every TauCeti.GraphTwistedIndex.

The permutations themselves are pinned as Fin data by TauCeti/LinearAlgebra/RootSystem/DiagramPermutations.lean. What is new here is the assignment of one of them to each family: the identity on the nine untwisted families, the chain reversal on ²Aₙ, the fork exchange on ²Dₙ, the order-two symmetry on ²E₆, and triality on ³D₄. The assignment is total on TauCeti.GraphTwistedIndex and defined nowhere else: the Suzuki--Ree and Tits indices are excluded by that subtype, whose defining hypothesis discharges their branches, so no diagram permutation is invented for a family whose Steinberg map is an odd power of a half-Frobenius.

Two properties of the assignment are proved. Each permutation is an automorphism of the Cartan matrix of the underlying diagram, which is what lets it be realized by an automorphism of the pinned group; and its order is the superscript in the printed family name, recorded here as TauCeti.GraphTwistedIndex.twistOrder. The relations γ ^ 2 = 1 for ²Aₙ, ²Dₙ and ²E₆ and γ ^ 3 = 1 for ³D₄ are the uniform TauCeti.GraphTwistedIndex.diagramPerm_pow_twistOrder.

Main definitions

• TauCeti.GraphTwistedIndex.diagramPerm: the permutation of Bourbaki-numbered simple roots that the Steinberg map of a graph-twisted index composes with the field Frobenius.
• TauCeti.GraphTwistedIndex.twistOrder: the order of that permutation, which is the superscript in the family name.
• TauCeti.TypeALieIndex.toGraphTwistedIndex, TauCeti.TypeB2LieIndex.toGraphTwistedIndex, TauCeti.TypeCLieIndex.toGraphTwistedIndex, TauCeti.TypeE6LieIndex.toGraphTwistedIndex, TauCeti.TypeTwistedE6LieIndex.toGraphTwistedIndex, TauCeti.TypeE7LieIndex.toGraphTwistedIndex and TauCeti.TypeDDiagramLieIndex.toGraphTwistedIndex: the two type-A families, Aₙ(q) and ²Aₙ(q), the untwisted rank-two family B₂(q), the untwisted type-C family, the two families on the E₆ diagram, the untwisted family E₇(q), and the three families on a type-D diagram, as indices of that subtype, so that the permutations above are attached to them.

Main results

• TauCeti.GraphTwistedIndex.cartanMatrix_diagramPerm: the permutation attached to an index is an automorphism of the Cartan matrix of its underlying Dynkin diagram.
• TauCeti.GraphTwistedIndex.diagramPerm_pow_twistOrder, TauCeti.GraphTwistedIndex.orderOf_diagramPerm and TauCeti.GraphTwistedIndex.twistOrder_pos: the twist order annihilates the permutation, is exactly its order, and is positive.
• TauCeti.TypeB2LieIndex.diagramPerm_toGraphTwistedIndex: the untwisted family on the B₂ diagram takes the identity, the B₂ diagram having no symmetry to twist by.
• TauCeti.TypeE6LieIndex.diagramPerm_toGraphTwistedIndex and TauCeti.TypeTwistedE6LieIndex.diagramPerm_toGraphTwistedIndex: the two families on the E₆ diagram take the identity and TauCeti.graphPermE6 respectively, which is the distinction between them.
• TauCeti.TypeE7LieIndex.diagramPerm_toGraphTwistedIndex: the single family on the E₇ diagram takes the identity, that diagram having no symmetry to twist by.
• TauCeti.TypeDLieIndex.diagramPerm_toGraphTwistedIndex, TauCeti.TypeTwistedDLieIndex.twistOrder_toGraphTwistedIndex and TauCeti.TypeTrialityD4LieIndex.twistOrder_toGraphTwistedIndex: the three families on a type-D diagram are told apart by an untwisted permutation and by twist orders two and three.

Roadmap

This is the diagram-permutation half of item L1 of TauCetiRoadmap/CFSGStatement/README.md, whose table of families and permutations it transcribes; the remaining half, the equations γ (x_α(t)) = x_{γ α}(t) on the simple root subgroups, waits on the pinned ambient groups of L0. TauCetiRoadmap/CFSGStatement/Suggested.lean supplies the diagramPerm signature and its design on the subtype that excludes the Suzuki--Ree and Tits families. The conventions follow Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, and the Bourbaki numbering fixed by the root-systems roadmap.

def TauCeti.GraphTwistedIndex.diagramPerm (d : GraphTwistedIndex) : Equiv.Perm (Fin (↑d).rank)

The permutation γ of the Bourbaki-numbered simple roots that the Steinberg map of a graph-twisted index composes with the field Frobenius.

It is the identity on the untwisted families, the chain reversal TauCeti.graphPermA on ²Aₙ, the fork exchange TauCeti.graphPermD on ²Dₙ, TauCeti.graphPermE6 on ²E₆, and TauCeti.trialityPermD4 on ³D₄. The four Suzuki--Ree and Tits constructors are not indices of this subtype, and their branches are closed by that hypothesis rather than by a chosen value.

Equations

• TauCeti.GraphTwistedIndex.diagramPerm ⟨⟨TauCeti.LieTypeIndex.A rank q, property⟩, property_1⟩ = 1
• TauCeti.GraphTwistedIndex.diagramPerm ⟨⟨TauCeti.LieTypeIndex.B rank q, property⟩, property_1⟩ = 1
• TauCeti.GraphTwistedIndex.diagramPerm ⟨⟨TauCeti.LieTypeIndex.C rank q, property⟩, property_1⟩ = 1
• TauCeti.GraphTwistedIndex.diagramPerm ⟨⟨TauCeti.LieTypeIndex.D rank q, property⟩, property_1⟩ = 1
• TauCeti.GraphTwistedIndex.diagramPerm ⟨⟨TauCeti.LieTypeIndex.E6 q, property⟩, property_1⟩ = 1
• TauCeti.GraphTwistedIndex.diagramPerm ⟨⟨TauCeti.LieTypeIndex.E7 q, property⟩, property_1⟩ = 1
• TauCeti.GraphTwistedIndex.diagramPerm ⟨⟨TauCeti.LieTypeIndex.E8 q, property⟩, property_1⟩ = 1
• TauCeti.GraphTwistedIndex.diagramPerm ⟨⟨TauCeti.LieTypeIndex.F4 q, property⟩, property_1⟩ = 1
• TauCeti.GraphTwistedIndex.diagramPerm ⟨⟨TauCeti.LieTypeIndex.G2 q, property⟩, property_1⟩ = 1
• TauCeti.GraphTwistedIndex.diagramPerm ⟨⟨TauCeti.LieTypeIndex.twistedA n q, property⟩, property_1⟩ = TauCeti.graphPermA n
• TauCeti.GraphTwistedIndex.diagramPerm ⟨⟨TauCeti.LieTypeIndex.twistedD n q, hv⟩, property⟩ = TauCeti.graphPermD n ⋯
• TauCeti.GraphTwistedIndex.diagramPerm ⟨⟨TauCeti.LieTypeIndex.twistedE6 q, property⟩, property_1⟩ = TauCeti.graphPermE6
• TauCeti.GraphTwistedIndex.diagramPerm ⟨⟨TauCeti.LieTypeIndex.trialityD4 q, property⟩, property_1⟩ = TauCeti.trialityPermD4
• TauCeti.GraphTwistedIndex.diagramPerm ⟨⟨TauCeti.LieTypeIndex.suzuki m, property⟩, hh⟩ = absurd ⋯ hh
• TauCeti.GraphTwistedIndex.diagramPerm ⟨⟨TauCeti.LieTypeIndex.reeG2 m, property⟩, hh⟩ = absurd ⋯ hh
• TauCeti.GraphTwistedIndex.diagramPerm ⟨⟨TauCeti.LieTypeIndex.reeF4 m, property⟩, hh⟩ = absurd ⋯ hh
• TauCeti.GraphTwistedIndex.diagramPerm ⟨⟨TauCeti.LieTypeIndex.tits, property⟩, hh⟩ = absurd ⋯ hh

def TauCeti.GraphTwistedIndex.twistOrder : GraphTwistedIndex → ℕ

The order of the diagram permutation of a graph-twisted index: the superscript in the printed family name. It is 1 on the untwisted families, 2 on ²Aₙ, ²Dₙ and ²E₆, and 3 on ³D₄.

Equations

• TauCeti.GraphTwistedIndex.twistOrder ⟨⟨TauCeti.LieTypeIndex.A rank q, property⟩, property_1⟩ = 1
• TauCeti.GraphTwistedIndex.twistOrder ⟨⟨TauCeti.LieTypeIndex.B rank q, property⟩, property_1⟩ = 1
• TauCeti.GraphTwistedIndex.twistOrder ⟨⟨TauCeti.LieTypeIndex.C rank q, property⟩, property_1⟩ = 1
• TauCeti.GraphTwistedIndex.twistOrder ⟨⟨TauCeti.LieTypeIndex.D rank q, property⟩, property_1⟩ = 1
• TauCeti.GraphTwistedIndex.twistOrder ⟨⟨TauCeti.LieTypeIndex.E6 q, property⟩, property_1⟩ = 1
• TauCeti.GraphTwistedIndex.twistOrder ⟨⟨TauCeti.LieTypeIndex.E7 q, property⟩, property_1⟩ = 1
• TauCeti.GraphTwistedIndex.twistOrder ⟨⟨TauCeti.LieTypeIndex.E8 q, property⟩, property_1⟩ = 1
• TauCeti.GraphTwistedIndex.twistOrder ⟨⟨TauCeti.LieTypeIndex.F4 q, property⟩, property_1⟩ = 1
• TauCeti.GraphTwistedIndex.twistOrder ⟨⟨TauCeti.LieTypeIndex.G2 q, property⟩, property_1⟩ = 1
• TauCeti.GraphTwistedIndex.twistOrder ⟨⟨TauCeti.LieTypeIndex.twistedA n q, property⟩, property_1⟩ = 2
• TauCeti.GraphTwistedIndex.twistOrder ⟨⟨TauCeti.LieTypeIndex.twistedD n q, hv⟩, property⟩ = 2
• TauCeti.GraphTwistedIndex.twistOrder ⟨⟨TauCeti.LieTypeIndex.twistedE6 q, property⟩, property_1⟩ = 2
• TauCeti.GraphTwistedIndex.twistOrder ⟨⟨TauCeti.LieTypeIndex.trialityD4 q, property⟩, property_1⟩ = 3
• TauCeti.GraphTwistedIndex.twistOrder ⟨⟨TauCeti.LieTypeIndex.suzuki m, property⟩, hh⟩ = absurd ⋯ hh
• TauCeti.GraphTwistedIndex.twistOrder ⟨⟨TauCeti.LieTypeIndex.reeG2 m, property⟩, hh⟩ = absurd ⋯ hh
• TauCeti.GraphTwistedIndex.twistOrder ⟨⟨TauCeti.LieTypeIndex.reeF4 m, property⟩, hh⟩ = absurd ⋯ hh
• TauCeti.GraphTwistedIndex.twistOrder ⟨⟨TauCeti.LieTypeIndex.tits, property⟩, hh⟩ = absurd ⋯ hh

The pinned table

The following two families of equations are the roadmap's table of families and permutations. They are exhaustive for TauCeti.GraphTwistedIndex, since the Suzuki--Ree and Tits constructors are not indices of that subtype.

@[simp]

theorem TauCeti.GraphTwistedIndex.diagramPerm_A {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.A n q).Valid) : diagramPerm ⟨⟨LieTypeIndex.A n q, hv⟩, ⋯⟩ = 1

The untwisted family Aₙ(q) is not graph-twisted.

@[simp]

theorem TauCeti.GraphTwistedIndex.twistOrder_A {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.A n q).Valid) : twistOrder ⟨⟨LieTypeIndex.A n q, hv⟩, ⋯⟩ = 1

@[simp]

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

The untwisted family Bₙ(q) is not graph-twisted.

@[simp]

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

@[simp]

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

The untwisted family Cₙ(q) is not graph-twisted.

@[simp]

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

@[simp]

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

The untwisted family Dₙ(q) is not graph-twisted; its fork exchange is ²Dₙ(q).

@[simp]

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

@[simp]

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

The untwisted family E₆(q) is not graph-twisted; its diagram symmetry is ²E₆(q).

@[simp]

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

@[simp]

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

The family E₇(q) is not graph-twisted; the E₇ diagram has no nontrivial symmetry.

@[simp]

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

@[simp]

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

The family E₈(q) is not graph-twisted; the E₈ diagram has no nontrivial symmetry.

@[simp]

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

@[simp]

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

The family F₄(q) is not graph-twisted; the length-exchanging symmetry of the F₄ diagram is not an automorphism of its Cartan matrix, and enters only through the half-Frobenius of ²F₄.

@[simp]

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

@[simp]

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

The family G₂(q) is not graph-twisted; the length-exchanging symmetry of the G₂ diagram is not an automorphism of its Cartan matrix, and enters only through the half-Frobenius of ²G₂.

@[simp]

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

@[simp]

theorem TauCeti.GraphTwistedIndex.diagramPerm_twistedA {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.twistedA n q).Valid) : diagramPerm ⟨⟨LieTypeIndex.twistedA n q, hv⟩, ⋯⟩ = graphPermA n

The unitary family ²Aₙ(q) twists by the reversal of the Aₙ chain.

@[simp]

theorem TauCeti.GraphTwistedIndex.twistOrder_twistedA {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.twistedA n q).Valid) : twistOrder ⟨⟨LieTypeIndex.twistedA n q, hv⟩, ⋯⟩ = 2

@[simp]

theorem TauCeti.GraphTwistedIndex.diagramPerm_twistedD {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.twistedD n q).Valid) : diagramPerm ⟨⟨LieTypeIndex.twistedD n q, hv⟩, ⋯⟩ = graphPermD n ⋯

The family ²Dₙ(q) twists by the exchange of the two fork nodes of the Dₙ diagram.

@[simp]

theorem TauCeti.GraphTwistedIndex.twistOrder_twistedD {n : ℕ} {q : PrimePower} (hv : (LieTypeIndex.twistedD n q).Valid) : twistOrder ⟨⟨LieTypeIndex.twistedD n q, hv⟩, ⋯⟩ = 2

@[simp]

theorem TauCeti.GraphTwistedIndex.diagramPerm_twistedE6 {q : PrimePower} (hv : (LieTypeIndex.twistedE6 q).Valid) : diagramPerm ⟨⟨LieTypeIndex.twistedE6 q, hv⟩, ⋯⟩ = graphPermE6

The family ²E₆(q) twists by the order-two symmetry of the E₆ diagram.

@[simp]

theorem TauCeti.GraphTwistedIndex.twistOrder_twistedE6 {q : PrimePower} (hv : (LieTypeIndex.twistedE6 q).Valid) : twistOrder ⟨⟨LieTypeIndex.twistedE6 q, hv⟩, ⋯⟩ = 2

@[simp]

theorem TauCeti.GraphTwistedIndex.diagramPerm_trialityD4 {q : PrimePower} (hv : (LieTypeIndex.trialityD4 q).Valid) : diagramPerm ⟨⟨LieTypeIndex.trialityD4 q, hv⟩, ⋯⟩ = trialityPermD4

The family ³D₄(q) twists by triality, the order-three symmetry of the D₄ diagram.

@[simp]

theorem TauCeti.GraphTwistedIndex.twistOrder_trialityD4 {q : PrimePower} (hv : (LieTypeIndex.trialityD4 q).Valid) : twistOrder ⟨⟨LieTypeIndex.trialityD4 q, hv⟩, ⋯⟩ = 3

Properties of the assignment

@[simp]

theorem TauCeti.GraphTwistedIndex.cartanMatrix_diagramPerm (d : GraphTwistedIndex) (i j : Fin (↑d).rank) : (↑d).dynkinType.cartanMatrix (d.diagramPerm i) (d.diagramPerm j) = (↑d).dynkinType.cartanMatrix i j

The permutation attached to a graph-twisted index is an automorphism of the Cartan matrix of its underlying Dynkin diagram. This is what allows it to be realized, on the pinned Chevalley group of that diagram, by an automorphism permuting the simple root subgroups accordingly.

@[simp]

theorem TauCeti.GraphTwistedIndex.orderOf_diagramPerm (d : GraphTwistedIndex) : orderOf d.diagramPerm = d.twistOrder

The twist order of an index is exactly the order of its diagram permutation, so the superscript in the family name is not an independent convention.

@[simp]

theorem TauCeti.GraphTwistedIndex.diagramPerm_pow_twistOrder (d : GraphTwistedIndex) : d.diagramPerm ^ d.twistOrder = 1

The twist order annihilates the diagram permutation. On the twisted families this is the relation γ ^ 2 = 1 for ²Aₙ, ²Dₙ and ²E₆ and γ ^ 3 = 1 for ³D₄ required of a Steinberg map of the form γ ∘ Frob_q.

theorem TauCeti.GraphTwistedIndex.twistOrder_pos (d : GraphTwistedIndex) : 0 < d.twistOrder

The twist order of an index is positive, being the order of a permutation of a finite set. It is 1, 2 or 3, and never 0.

The type-A families as graph-twisted indices

@[reducible, inline]

abbrev TauCeti.TypeALieIndex.toGraphTwistedIndex (d : TypeALieIndex) : GraphTwistedIndex

A type-A index, regarded as an ordinary-or-graph-twisted index. Neither Aₙ(q) nor ²Aₙ(q) uses a half-Frobenius, so both carry a diagram permutation: the identity on the untwisted family and the chain reversal on the twisted one.

Equations

• d.toGraphTwistedIndex = ⟨↑d, ⋯⟩

The untwisted family B₂(q) as a graph-twisted index

@[reducible, inline]

abbrev TauCeti.TypeB2LieIndex.toGraphTwistedIndex (d : TypeB2LieIndex) : GraphTwistedIndex

The untwisted rank-two family B₂(q), regarded as an ordinary-or-graph-twisted index. Of the two classification-list families on the B₂ diagram it is the one that uses no half-Frobenius, which is exactly the membership condition of TauCeti.GraphTwistedIndex; the other, the Suzuki family, is excluded by that same condition.

Equations

• d.toGraphTwistedIndex = ⟨↑↑d, ⋯⟩

@[simp]

theorem TauCeti.TypeB2LieIndex.diagramPerm_toGraphTwistedIndex (d : TypeB2LieIndex) : d.toGraphTwistedIndex.diagramPerm = 1

The diagram permutation of the untwisted family B₂(q) is the identity, so its Steinberg map composes with no twist and is the q-power Frobenius outright. The B₂ diagram has no symmetry to twist by in any case: its two nodes have different root lengths.

The type-C family as graph-twisted indices

@[reducible, inline]

abbrev TauCeti.TypeCLieIndex.toGraphTwistedIndex (d : TypeCLieIndex) : GraphTwistedIndex

A type-C index, regarded as an ordinary-or-graph-twisted index. The untwisted family does not use a half-Frobenius and its diagram permutation is the identity.

Equations

• d.toGraphTwistedIndex = ⟨↑d, ⋯⟩

@[simp]

theorem TauCeti.TypeCLieIndex.diagramPerm_eq_one (d : TypeCLieIndex) : d.toGraphTwistedIndex.diagramPerm = 1

The diagram permutation of an untwisted type-C index is the identity.

The untwisted family E₆(q) as graph-twisted indices

@[reducible, inline]

abbrev TauCeti.TypeE6LieIndex.toGraphTwistedIndex (d : TypeE6LieIndex) : GraphTwistedIndex

The untwisted family E₆(q), regarded as an ordinary-or-graph-twisted index. It uses no half-Frobenius, so it carries a diagram permutation, namely the identity.

Equations

• d.toGraphTwistedIndex = ⟨↑d, ⋯⟩

@[simp]

theorem TauCeti.TypeE6LieIndex.diagramPerm_toGraphTwistedIndex (d : TypeE6LieIndex) : d.toGraphTwistedIndex.diagramPerm = 1

The diagram permutation of the untwisted family E₆(q) is the identity, which is what places it in the untwisted row of milestone L1's table, where the Steinberg map is Frob_q outright. The nontrivial symmetry of the E₆ diagram belongs to ²E₆(q).

The graph-twisted family ²E₆(q) as a graph-twisted index

@[reducible, inline]

abbrev TauCeti.TypeTwistedE6LieIndex.toGraphTwistedIndex (d : TypeTwistedE6LieIndex) : GraphTwistedIndex

The graph-twisted family ²E₆(q), regarded as an ordinary-or-graph-twisted index. It uses no half-Frobenius, so it carries a diagram permutation, namely the nontrivial one.

Equations

• d.toGraphTwistedIndex = ⟨↑d, ⋯⟩

@[simp]

theorem TauCeti.TypeTwistedE6LieIndex.diagramPerm_toGraphTwistedIndex (d : TypeTwistedE6LieIndex) (i : Fin (↑d).rank) : d.toGraphTwistedIndex.diagramPerm i = (finCongr ⋯) (graphPermE6 ((finCongr ⋯) i))

The diagram permutation of the graph-twisted family ²E₆(q) is TauCeti.graphPermE6, the order-two symmetry of the E₆ diagram, read in the index's own copy Fin d.1.rank of the Bourbaki index type. This is what places the family in the γ₂ ∘ Frob_q row of milestone L1's table; the untwisted family E₆(q) takes the identity instead.

@[simp]

theorem TauCeti.TypeTwistedE6LieIndex.twistOrder_toGraphTwistedIndex (d : TypeTwistedE6LieIndex) : d.toGraphTwistedIndex.twistOrder = 2

The twist order of ²E₆(q) is two, the superscript in the printed family name.

The untwisted family E₇(q) as a graph-twisted index

@[reducible, inline]

abbrev TauCeti.TypeE7LieIndex.toGraphTwistedIndex (d : TypeE7LieIndex) : GraphTwistedIndex

The untwisted family E₇(q), regarded as an ordinary-or-graph-twisted index. It uses no half-Frobenius, so it carries a diagram permutation, namely the identity.

Equations

• d.toGraphTwistedIndex = ⟨↑d, ⋯⟩

@[simp]

theorem TauCeti.TypeE7LieIndex.diagramPerm_toGraphTwistedIndex (d : TypeE7LieIndex) : d.toGraphTwistedIndex.diagramPerm = 1

The diagram permutation of the untwisted family E₇(q) is the identity, so the Steinberg map of the family is the field Frobenius outright. The E₇ diagram is a tree with no nontrivial symmetry, so no second family shares it to be told apart from.

The families on a type-D diagram as graph-twisted indices

The three classification-list families on a Dₙ diagram all take an ordinary Steinberg map, and they are told apart by the permutation it composes with: the identity, the fork exchange, and triality. What is recorded below of an abstract index of each subtype is the family-defining reading: the permutation itself on the untwisted family, where it is the identity at every rank, and its order on the two twisted families, where the permutation lives on Fin d.1.rank and the pinned TauCeti.graphPermD and TauCeti.trialityPermD4 on Fin n and Fin 4. Those two permutations are named on the constructor form by GraphTwistedIndex.diagramPerm_twistedD and GraphTwistedIndex.diagramPerm_trialityD4, which the eliminators exists_eq_ofTwistedD and exists_eq_of reduce an abstract index to.

@[reducible, inline]

abbrev TauCeti.TypeDDiagramLieIndex.toGraphTwistedIndex (d : TypeDDiagramLieIndex) : GraphTwistedIndex

An index on a type-D diagram, regarded as an ordinary-or-graph-twisted index. None of the three families uses a half-Frobenius, so each carries a diagram permutation.

Equations

• d.toGraphTwistedIndex = ⟨↑d, ⋯⟩

@[simp]

theorem TauCeti.TypeDLieIndex.diagramPerm_toGraphTwistedIndex (d : TypeDLieIndex) : d.toTypeDDiagramLieIndex.toGraphTwistedIndex.diagramPerm = 1

The diagram permutation of the untwisted family Dₙ(q) is the identity, which places it in the untwisted row of milestone L1's table, where the Steinberg map is Frob_q outright. The two symmetries of the Dₙ diagram belong to ²Dₙ(q) and, at rank four, to ³D₄(q).

@[simp]

theorem TauCeti.TypeTwistedDLieIndex.twistOrder_toGraphTwistedIndex (d : TypeTwistedDLieIndex) : d.toTypeDDiagramLieIndex.toGraphTwistedIndex.twistOrder = 2

The family ²Dₙ(q) has twist order two, its diagram permutation being the exchange of the two fork nodes of the Dₙ diagram.

@[simp]

theorem TauCeti.TypeTrialityD4LieIndex.twistOrder_toGraphTwistedIndex (d : TypeTrialityD4LieIndex) : d.toTypeDDiagramLieIndex.toGraphTwistedIndex.twistOrder = 3

The family ³D₄(q) has twist order three, its diagram permutation being triality, the order-three symmetry of the D₄ diagram that three-cycles the outer nodes and fixes the centre. It is the one family on the classification list whose twist order is three.