The Steinberg endomorphism and candidate group of E₇(q) #
TauCeti/GroupTheory/SpecificGroups/CFSG/TypeE7/Basic.lean attaches to a validated E₇ index the
points of the explicit full-weight minuscule carrier TauCeti.E7Minuscule.groupScheme, with its
Bourbaki-numbered simple root subgroups. This file forms the Steinberg endomorphism of the
untwisted family E₇(q) on that carrier, which is its q-power Frobenius, records its fixed
points, and names the family's candidate group: the derived subgroup of those fixed points modulo
its centre.
The carrier Frobenius preserves the numbered simple root subgroups and split weight torus, raising
their parameters to the q-th power. Its fixed points are precisely the carrier points whose
matrix entries lie in the copy TauCeti.ValidLieTypeIndex.fixedField of 𝔽_q inside the closure.
The 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 the candidate group
asserted to be finite, perfect, or simple.
Main declarations #
TauCeti.TypeE7LieIndex.steinberg: the Steinberg endomorphism ofE₇(q), theq-power Frobenius of the minuscule carrier.TauCeti.TypeE7LieIndex.Group: the candidate groupFixedPointCandidate steinberg, the quotient[H, H] / Z([H, H])of the fixed pointsHofsteinberg.
Main results #
TauCeti.TypeE7LieIndex.steinberg_simpleRootSubgroupandTauCeti.TypeE7LieIndex.steinberg_weightTorusPoints: Frobenius raises the parameters of the carrier's numbered root subgroups and weight torus to theq-th power.TauCeti.TypeE7LieIndex.coe_steinberg_apply: Frobenius raises every matrix coefficient to theq-th power.TauCeti.TypeE7LieIndex.mem_fixedSubgroup_steinberg_iff: a carrier point is fixed exactly when its entries lie in the field of definition.TauCeti.TypeE7LieIndex.primeFrobenius, withTauCeti.TypeE7LieIndex.coe_primeFrobenius_apply,TauCeti.TypeE7LieIndex.primeFrobenius_simpleRootSubgroup,TauCeti.TypeE7LieIndex.primeFrobenius_weightTorusPointsandTauCeti.TypeE7LieIndex.steinberg_eq_primeFrobenius_pow: the prime-field Frobenius, its entrywise and pinned simple-root-subgroup equations, its action on the weight torus, and the Steinberg endomorphism as itse-th power.
References #
- R. W. Carter, Simple Groups of Lie Type, §§4.4 and 14.
- R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.17.
- N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VI.
The Steinberg endomorphism #
The Steinberg endomorphism of E₇(q) on the minuscule carrier: the q-power Frobenius of
the carrier, for q the field order recorded by the index. The family is untwisted, so its
Steinberg endomorphism is the Frobenius itself, with no graph automorphism.
Equations
- d.steinberg = TauCeti.E7Minuscule.frobenius (↑d).characteristic (↑d).fieldExponent (↑d).Closure
Instances For
The Steinberg endomorphism is the carrier Frobenius at the exponent recorded by the E₇
index.
The minuscule-carrier Frobenius raises every matrix entry to the q-th power.
The minuscule-carrier 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 prime-field Frobenius of the minuscule E₇ carrier, the p-power map for p the
defining characteristic. The Steinberg endomorphism of the family, which is its q-power
Frobenius, is the e-th power of this map, for e the field exponent the index records, by
steinberg_eq_primeFrobenius_pow.
Equations
- d.primeFrobenius = TauCeti.E7Minuscule.frobenius (↑d).characteristic 1 (↑d).Closure
Instances For
The prime-field Frobenius is the carrier's Frobenius at exponent one.
The prime-field Frobenius raises every matrix entry to the p-th power.
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).
The Steinberg endomorphism is the e-th power of the prime-field Frobenius, for e the
field exponent the index records.
The prime-field Frobenius preserves the weight torus and raises each coordinate to the
p-th power, that is, Frob_p (t(s)) = t(s ^ p).
The minuscule-carrier Frobenius preserves the weight torus and raises each coordinate to the
q-th power, that is, Frob_q (t(s)) = t(s ^ q).
The fixed subgroup contains the 𝔽_q-points of every numbered simple root subgroup. A
simple-root point x_i(u) is fixed by the carrier Frobenius as soon as its parameter lies in the
field of definition, so the group H below is at least as large as the subgroup those points
generate.
The fixed subgroup contains the weight-torus points with 𝔽_q coordinates. A torus point
t(s) is fixed by the carrier Frobenius as soon as each of its coordinates lies in the field of
definition.
A point of the minuscule carrier is fixed by Frobenius exactly when all of its matrix
entries lie in the field of definition. Writing 𝔽_q for
TauCeti.ValidLieTypeIndex.fixedField, the copy of the field of q elements inside the algebraic
closure, the group H cut out below is therefore the group of points of the minuscule carrier
whose entries lie in 𝔽_q.
The finite-group candidate #
The finite-simple-group candidate attached to an E₇ index: 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.