The graph-twisted family ²E₆(q) on the doubled minuscule carrier

The classification list carries two families on the E₆ diagram: the untwisted E₆(q), whose Steinberg map is the q-power Frobenius, and the graph-twisted ²E₆(q), whose Steinberg map is that Frobenius composed with the order-two symmetry γ₂ of the diagram. The twisted construction needs a carrier on which that symmetry acts: the E₆ diagram symmetry exchanges the minuscule representation V(ϖ₁) with its contragredient V(ϖ₆) rather than preserving either, so it does not act on the 27-dimensional carrier TauCeti.E6Minuscule.groupScheme that TauCeti/GroupTheory/SpecificGroups/CFSG/TypeE6.lean runs the untwisted recipe on, and this file cannot reuse that carrier. The graph-stable carrier is TauCeti.E6DoubledMinuscule.groupScheme, built on V(ϖ₁) ⊕ V(ϖ₆) inside GL₅₄ over ℤ.

This file attaches that carrier to a validated ²E₆ index and forms the family's Steinberg endomorphism and candidate group on it. It supplies the group of algebraic-closure-valued points and the Bourbaki-numbered simple root subgroups, identifies the character of those subgroups with the corresponding simple root of the E₆ root datum, and builds the two factors of the Steinberg map. The first is the q-power Frobenius Frob_q, with the pinned equation Frob_q (x_i(u)) = x_i(u ^ q) and the description of its fixed points as the points all of whose 54 × 54 matrix entries lie in the field of definition 𝔽_q. The second is the graph automorphism γ₂, conjugation by the signed monomial matrix of the carrier that exchanges its two minuscule summands, with the pinned equation γ₂ (x_i(u)) = x_{σ i}(u) for σ the diagram permutation the index carries, which exchanges the Bourbaki nodes 1 ↔ 6 and 3 ↔ 5. The graph automorphism is an involution and commutes with the Frobenius, so the Steinberg map of the family is the composite

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

and the candidate group of ²E₆(q) is the derived subgroup of the fixed points of F, modulo the centre of that derived subgroup. The Frobenius fixed points are the points with entries in 𝔽_q; the fixed points of the composite are not characterized here.

The doubled minuscule carrier is not identified with the pinned simply connected Chevalley--Demazure group scheme of type E₆, and nothing here identifies the two: the constructions below transfer to that pinned group only along such an identification, once one is proved. Nor is it asserted that the carrier is reductive, that its weight torus is maximal, or that any group mentioned is finite, perfect, or simple.

Main declarations

• TauCeti.TypeTwistedE6LieIndex.AmbientGroup: the algebraic-closure-valued points of the doubled minuscule carrier, the group the classification recipe for ²E₆(q) is run inside.
• TauCeti.TypeTwistedE6LieIndex.simpleRootSubgroup: its positive simple-root subgroup at a Bourbaki-numbered node.
• TauCeti.TypeTwistedE6LieIndex.frobenius: the q-power Frobenius factor of the Steinberg map, at the field order the index records.
• TauCeti.TypeTwistedE6LieIndex.graphAut: the graph automorphism factor, realizing on the ambient group the diagram permutation the index carries.
• TauCeti.TypeTwistedE6LieIndex.steinberg: the Steinberg endomorphism γ₂ ∘ Frob_q of ²E₆(q).
• TauCeti.TypeTwistedE6LieIndex.FixedPoints and TauCeti.TypeTwistedE6LieIndex.Group: the fixed subgroup of the Steinberg map, and the candidate group FixedPointCandidate steinberg, the quotient [H, H] / Z([H, H]) of those fixed points H.

Main results

• TauCeti.TypeTwistedE6LieIndex.rootGeneratorWeight_eq_root_simpleIndex: the character of a simple-root subgroup is the corresponding simple root of TauCeti.DynkinType.simplyConnectedRootDatum at E₆.

• TauCeti.TypeTwistedE6LieIndex.frobenius_simpleRootSubgroup: the pinned equation Frob_q (x_i(u)) = x_i(u ^ q) on the numbered simple-root subgroups.

• TauCeti.TypeTwistedE6LieIndex.mem_fixedSubgroup_frobenius_iff: a point is fixed by Frob_q exactly when all entries of its 54 × 54 matrix lie in the field of definition.

• TauCeti.TypeTwistedE6LieIndex.e6DoubledMinusculeWeight_e6DoubledMinusculeGraphPerm_diagramPerm: the coordinate involution of the doubled index set is equivariant for the diagram permutation that the index itself carries, read in the index's copy Fin d.1.rank of the Bourbaki index type.

• TauCeti.TypeTwistedE6LieIndex.e6DoubledMinusculeGraphPerm_pow_twistOrder: the twist order the index records annihilates that involution.

• TauCeti.TypeTwistedE6LieIndex.graphAut_simpleRootSubgroup: the pinned equation γ₂ (x_i(u)) = x_{σ i}(u), with no field power and no sign.

• TauCeti.TypeTwistedE6LieIndex.graphAut_sq, TauCeti.TypeTwistedE6LieIndex.graphAut_pow_twistOrder and TauCeti.TypeTwistedE6LieIndex.graphAut_comp_frobenius: γ₂ ^ 2 = 1, also in the form the twist order of the index states it, and γ₂ commutes with Frob_q.

• TauCeti.TypeTwistedE6LieIndex.steinberg_simpleRootSubgroup: the pinned equation F (x_i(u)) = x_{σ i}(u ^ q) of the Steinberg map.

• TauCeti.TypeTwistedE6LieIndex.steinberg_def and TauCeti.TypeTwistedE6LieIndex.steinberg_eq_frobenius_comp_graphAut: the Steinberg map is the composite of its two factors, in either order.

• TauCeti.TypeTwistedE6LieIndex.primeFrobenius, with TauCeti.TypeTwistedE6LieIndex.primeFrobenius_simpleRootSubgroup and TauCeti.TypeTwistedE6LieIndex.frobenius_eq_primeFrobenius_pow: the prime-field Frobenius, its pinned equation Frob_p (x_i(u)) = x_i(u ^ p), and the q-power Frobenius as its e-th power.

References

• R. W. Carter, Simple Groups of Lie Type, §§12.2 and 13, for the graph automorphism of E₆ and the twisted family it defines.
• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §§1.15 and 1.17, for the Steinberg endomorphisms of the graph-twisted families.
• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate V, for the numbering of the E₆ diagram that the root subgroups below are indexed by.

The ambient group and its simple root subgroups

@[reducible, inline]

abbrev TauCeti.TypeTwistedE6LieIndex.AmbientGroup (d : TypeTwistedE6LieIndex) : Type

The ambient group this file attaches to a validated ²E₆ index: the points of the explicit full-weight graph-stable type-E₆ doubled minuscule Chevalley carrier over the algebraic closure of its prime field. No finiteness, reductivity, pinning or maximality statement is attached to it, and it is not identified with the points of the pinned simply connected E₆ group scheme, as the module docstring describes.

Equations

• d.AmbientGroup = ↥(TauCeti.E6DoubledMinuscule.points (↑d).Closure)

noncomputable def TauCeti.TypeTwistedE6LieIndex.simpleRootSubgroup (d : TypeTwistedE6LieIndex) (i : Fin (↑d).rank) : Multiplicative (↑d).Closure →* d.AmbientGroup

The positive simple-root subgroup at the Bourbaki-numbered node i of the E₆ diagram. It is the carrier's numbered raising subgroup at the same node, the index type Fin d.1.rank being the upstream Bourbaki index type of the index's own Dynkin type.

Equations

• d.simpleRootSubgroup i = TauCeti.E6DoubledMinuscule.rootSubgroupPoints (Sum.inl ((finCongr ⋯) i)) (↑d).Closure

theorem TauCeti.TypeTwistedE6LieIndex.simpleRootSubgroup_def (d : TypeTwistedE6LieIndex) (i : Fin (↑d).rank) : d.simpleRootSubgroup i = E6DoubledMinuscule.rootSubgroupPoints (Sum.inl ((finCongr ⋯) i)) (↑d).Closure

The simple-root subgroup is the carrier's numbered raising subgroup at the corresponding node. This is the equation through which the upstream root-subgroup API reaches simpleRootSubgroup. It is deliberately not a simp lemma: the pinned equations γ₂ (x_i(u)) = x_{σ i}(u) and Frob_q (x_i(u)) = x_i(u ^ q) of this branch's Steinberg map are stated against simpleRootSubgroup itself, and unfolding to TauCeti.E6DoubledMinuscule.rootSubgroupPoints would keep them from firing, as it does on the branches already assembled.

theorem TauCeti.TypeTwistedE6LieIndex.rootGeneratorWeight_eq_root_simpleIndex (d : TypeTwistedE6LieIndex) (i : Fin (↑d).rank) : E6.rootGeneratorWeight (Sum.inl ((finCongr ⋯) i)) = (DynkinType.E6.simplyConnectedRootDatum DynkinType.valid_E6).root (DynkinType.E6.simpleIndex DynkinType.valid_E6 ((finCongr ⋯) i))

The simple-root subgroups sit at the simple roots of the E₆ root datum. The character by which the carrier's split torus rescales the parameter of simpleRootSubgroup i, pinned by TauCeti.E6DoubledMinuscule.weightTorus_conj_rootSubgroup, is the i-th simple root of TauCeti.DynkinType.simplyConnectedRootDatum at E₆, in the same Bourbaki numbering.

The characters themselves are shared with the 27-dimensional carrier, TauCeti.E6Minuscule having defined them from the E₆ Cartan matrix alone, so this is the same identification the untwisted branch records in TauCeti.TypeE6LieIndex.rootGeneratorWeight_eq_root_simpleIndex, on the index subtype of this branch. It is not a claim that the doubled carrier is the pinned group of that diagram, no pinning being constructed for it.

The diagram symmetry on the carrier's coordinates

theorem TauCeti.TypeTwistedE6LieIndex.e6DoubledMinusculeWeight_e6DoubledMinusculeGraphPerm_diagramPerm (d : TypeTwistedE6LieIndex) (x : Fin 27 ⊕ Fin 27) (i : Fin (↑d).rank) : DynkinType.e6DoubledMinusculeWeight (DynkinType.e6DoubledMinusculeGraphPerm x) ((finCongr ⋯) (d.toGraphTwistedIndex.diagramPerm i)) = DynkinType.e6DoubledMinusculeWeight x ((finCongr ⋯) i)

The coordinate involution of the doubled index set realizes the diagram permutation that the index carries. TauCeti.DynkinType.e6DoubledMinusculeGraphPerm exchanges the two minuscule summands, and this is the equivariance wt (π x) (σ i) = wt x i of the doubled weight family for it, with σ read as TauCeti.GraphTwistedIndex.diagramPerm of this index rather than as TauCeti.graphPermE6 directly. That equivariance is the hypothesis under which a numbered permutation of the coordinates extends to an automorphism of a Kostant toral-closure carrier, and stating it against the index's own permutation is what identifies the resulting automorphism graphAut as the graph factor γ₂ of this family's Steinberg map rather than an unrelated symmetry.

The minuscule weight family alone admits no such equivariance, by TauCeti.DynkinType.e6MinusculeWeight_comp_graphPermE6_notMem_range; that is why this branch is built on the doubled carrier.

theorem TauCeti.TypeTwistedE6LieIndex.e6DoubledMinusculeGraphPerm_pow_twistOrder (d : TypeTwistedE6LieIndex) : DynkinType.e6DoubledMinusculeGraphPerm ^ d.toGraphTwistedIndex.twistOrder = 1

The twist order of the index annihilates the coordinate involution. Together with TauCeti.GraphTwistedIndex.diagramPerm_pow_twistOrder on the diagram side, this is the pair of order relations that graphAut_pow_twistOrder below matches on the carrier: γ₂ ^ 2 = 1.

The Frobenius factor of the Steinberg map

noncomputable def TauCeti.TypeTwistedE6LieIndex.frobenius (d : TypeTwistedE6LieIndex) : d.AmbientGroup →* d.AmbientGroup

The q-power Frobenius endomorphism of the ambient group of a validated ²E₆ index, q being the field order the index records.

It is not the Steinberg map of the family, which for a graph-twisted family is γ₂ ∘ Frob_q. On this branch the two genuinely differ: the composite acts on the simple-root subgroups through the diagram permutation the index carries, which is TauCeti.graphPermE6 by TauCeti.TypeTwistedE6LieIndex.diagramPerm_toGraphTwistedIndex and has order two by TauCeti.orderOf_graphPermE6. This is the right-hand factor of that composite, and the subgroup of points it fixes, characterized below, is correspondingly the untwisted one and not the fixed subgroup of the composite.

Equations

• d.frobenius = TauCeti.E6DoubledMinuscule.frobenius (↑d).characteristic (↑d).fieldExponent (↑d).Closure

theorem TauCeti.TypeTwistedE6LieIndex.frobenius_def (d : TypeTwistedE6LieIndex) : d.frobenius = E6DoubledMinuscule.frobenius (↑d).characteristic (↑d).fieldExponent (↑d).Closure

The Frobenius of a ²E₆ index is the doubled minuscule carrier's Frobenius at the characteristic and the exponent the index records.

@[simp]

theorem TauCeti.TypeTwistedE6LieIndex.coe_frobenius_apply (d : TypeTwistedE6LieIndex) (g : d.AmbientGroup) (r c : Fin 54) : ↑↑(d.frobenius g) r c = ↑↑g r c ^ (↑d).fieldOrder

The Frobenius acts on the ambient group by raising each entry of the 54 × 54 matrix of a point to the q-th power. This is the coefficient-level form from which the commutation of Frob_q with a coordinate symmetry of the carrier is read.

@[simp]

theorem TauCeti.TypeTwistedE6LieIndex.frobenius_simpleRootSubgroup (d : TypeTwistedE6LieIndex) (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 fixes the Bourbaki numbering of a simple-root subgroup and raises its parameter to the q-th power, that is, Frob_q (x_i(u)) = x_i(u ^ q). The diagram permutation of the twisted family enters through the other factor γ₂ of the Steinberg map, and not through this one.

noncomputable def TauCeti.TypeTwistedE6LieIndex.primeFrobenius (d : TypeTwistedE6LieIndex) : d.AmbientGroup →* d.AmbientGroup

The prime-field Frobenius of the doubled minuscule carrier, the p-power map for p the defining characteristic. The q-power Frobenius is its e-th power, for e the field exponent the index records, by frobenius_eq_primeFrobenius_pow.

Equations

• d.primeFrobenius = TauCeti.E6DoubledMinuscule.frobenius (↑d).characteristic 1 (↑d).Closure

theorem TauCeti.TypeTwistedE6LieIndex.primeFrobenius_def (d : TypeTwistedE6LieIndex) : d.primeFrobenius = E6DoubledMinuscule.frobenius (↑d).characteristic 1 (↑d).Closure

The prime-field Frobenius is the doubled minuscule carrier's Frobenius at exponent one.

@[simp]

theorem TauCeti.TypeTwistedE6LieIndex.coe_primeFrobenius_apply (d : TypeTwistedE6LieIndex) (g : d.AmbientGroup) (r c : Fin 54) : ↑↑(d.primeFrobenius g) r c = ↑↑g r c ^ (↑d).characteristic

The prime-field Frobenius acts on the ambient group by raising every entry of its 54 × 54 matrix to the p-th power, for p the defining characteristic.

@[simp]

theorem TauCeti.TypeTwistedE6LieIndex.primeFrobenius_simpleRootSubgroup (d : TypeTwistedE6LieIndex) (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 fixes the Bourbaki numbering of a simple-root subgroup and raises its parameter to the p-th power, that is, Frob_p (x_i(u)) = x_i(u ^ p).

theorem TauCeti.TypeTwistedE6LieIndex.frobenius_eq_primeFrobenius_pow (d : TypeTwistedE6LieIndex) : 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.

theorem TauCeti.TypeTwistedE6LieIndex.mem_fixedSubgroup_frobenius_iff (d : TypeTwistedE6LieIndex) (g : d.AmbientGroup) : g ∈ fixedSubgroup d.frobenius ↔ ∀ (r c : Fin 54), ↑↑g r c ∈ (↑d).fixedField

A point of the ambient group is fixed by the Frobenius exactly when every entry of its 54 × 54 matrix lies in the field of definition. Writing 𝔽_q for TauCeti.ValidLieTypeIndex.fixedField, the copy of the field of q elements inside the algebraic closure, the Frobenius-fixed subgroup is therefore the group of points of the doubled minuscule carrier with coordinates in 𝔽_q. It is not the group of points fixed by the twisted composite γ₂ ∘ Frob_q, which is the one the classification recipe for this branch is run inside.

The graph automorphism factor of the Steinberg map

noncomputable def TauCeti.TypeTwistedE6LieIndex.graphAut (d : TypeTwistedE6LieIndex) : MulAut d.AmbientGroup

The graph automorphism of the ambient group of a validated ²E₆ index: conjugation by the signed monomial matrix of the doubled minuscule carrier that exchanges its two minuscule summands. It realizes on the ambient group the diagram permutation the index carries, sending the Bourbaki-numbered simple-root subgroup at i to the one at σ i without changing its parameter, and it is the left-hand factor γ₂ of the Steinberg map γ₂ ∘ Frob_q of the family.

Equations

• d.graphAut = TauCeti.E6DoubledMinuscule.graphAutomorphismPoints (↑d).Closure

theorem TauCeti.TypeTwistedE6LieIndex.graphAut_def (d : TypeTwistedE6LieIndex) : d.graphAut = E6DoubledMinuscule.graphAutomorphismPoints (↑d).Closure

The graph automorphism of a ²E₆ index is the doubled minuscule carrier's graph automorphism on points over the index's closure. This is its unfolding lemma; the definition itself stays sealed.

@[simp]

theorem TauCeti.TypeTwistedE6LieIndex.graphAut_simpleRootSubgroup (d : TypeTwistedE6LieIndex) (i : Fin (↑d).rank) (u : Multiplicative (↑d).Closure) : d.graphAut ((d.simpleRootSubgroup i) u) = (d.simpleRootSubgroup (d.toGraphTwistedIndex.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 the index carries. 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.

@[simp]

theorem TauCeti.TypeTwistedE6LieIndex.graphAut_sq (d : TypeTwistedE6LieIndex) : d.graphAut ^ 2 = 1

The graph automorphism squares to the identity: γ₂ ^ 2 = 1.

theorem TauCeti.TypeTwistedE6LieIndex.graphAut_pow_twistOrder (d : TypeTwistedE6LieIndex) : d.graphAut ^ d.toGraphTwistedIndex.twistOrder = 1

The twist order of the index annihilates its graph automorphism. This is the order relation on the graph factor of the Steinberg map of a graph-twisted family, and it matches TauCeti.GraphTwistedIndex.diagramPerm_pow_twistOrder on the diagram permutation that γ₂ realizes.

theorem TauCeti.TypeTwistedE6LieIndex.graphAut_comp_frobenius (d : TypeTwistedE6LieIndex) : (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 ∘ γ₂. The graph automorphism is natural in the value ring, and the Frobenius is the map on points induced by a ring endomorphism of the closure.

The Steinberg endomorphism

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

The Steinberg endomorphism of ²E₆(q) on the doubled minuscule carrier: the graph automorphism composed with the q-power Frobenius, γ₂ ∘ Frob_q, for q the field order the index records. The two factors commute, so the order of composition is immaterial, by steinberg_eq_frobenius_comp_graphAut.

Equations

• d.steinberg = (MulEquiv.toMonoidHom d.graphAut).comp d.frobenius

theorem TauCeti.TypeTwistedE6LieIndex.steinberg_def (d : TypeTwistedE6LieIndex) : d.steinberg = (MulEquiv.toMonoidHom d.graphAut).comp d.frobenius

The Steinberg map of ²E₆(q) is its graph automorphism composed with its Frobenius. This is its unfolding lemma; the definition itself stays sealed, and it is through this equation that the two factors reach the Steinberg map.

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

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

@[simp]

theorem TauCeti.TypeTwistedE6LieIndex.steinberg_simpleRootSubgroup (d : TypeTwistedE6LieIndex) (i : Fin (↑d).rank) (u : Multiplicative (↑d).Closure) : d.steinberg ((d.simpleRootSubgroup i) u) = (d.simpleRootSubgroup (d.toGraphTwistedIndex.diagramPerm i)) (Multiplicative.ofAdd (Multiplicative.toAdd u ^ (↑d).fieldOrder))

The Steinberg map has the pinned action on every simple-root subgroup. It sends x_i(u) to x_{σ i}(u ^ q), where σ is the diagram permutation the index carries and q is its recorded field order.

The finite-group candidate

@[reducible, inline]

abbrev TauCeti.TypeTwistedE6LieIndex.FixedPoints (d : TypeTwistedE6LieIndex) : Type

The fixed subgroup of the Steinberg endomorphism of ²E₆(q). Its points are not the points with entries in 𝔽_q, which are the fixed points of the Frobenius factor alone.

Equations

• d.FixedPoints = ↥(TauCeti.fixedSubgroup d.steinberg)

@[reducible, inline]

abbrev TauCeti.TypeTwistedE6LieIndex.Group (d : TypeTwistedE6LieIndex) : Type

The finite-simple-group candidate attached to ²E₆(q): the derived subgroup of the Steinberg fixed points, modulo the centre of that derived subgroup. No finiteness or simplicity assertion is part of this definition.

Equations

• d.Group = TauCeti.FixedPointCandidate d.steinberg