The ambient group of the Ree family of type F₄ #
The Ree family ²F₄(2^(2m+1)) is built inside the group of algebraic-closure-valued points of
the short-root type-F₄ carrier over the prime field 𝔽₂: the closed subgroup scheme of GL₂₆
generated over 𝔽₂ by the reductions of the numbered simple root subgroups and of the weight
torus of the Kostant toral closure of the twenty-six-dimensional module V(ϖ₄). This file
attaches that carrier to a validated Ree index of type F₄, and supplies the numbered simple
root subgroups and the two Frobenius endomorphisms the family's construction runs against.
The carrier is taken over 𝔽₂ rather than over ℤ because the exceptional isogeny defining the
family's Steinberg map lives in characteristic two. Realizing that isogeny as an endomorphism of
the carrier needs the defining Hopf ideal to be the largest one killed by the generator
coordinate maps over 𝔽₂; the base change of the integral toral closure is only known to contain
the carrier, new equations being possible over a base that is not flat.
The two Frobenius maps #
TauCeti.ReeF4LieIndex.frobenius is the q-power Frobenius, for q = 2^(2m+1) the field order
the index records, and TauCeti.ReeF4LieIndex.primeFrobenius is the 2-power one; the former is
the (2m+1)-st power of the latter, frobenius_eq_primeFrobenius_pow.
Neither is the family's Steinberg endomorphism. In the literature that map is an odd power of an
exceptional isogeny of the carrier, available only in characteristic two and exchanging the two
root lengths, rather than a Frobenius (Steinberg, §11). The two maps here are named after what they
are.
TauCeti.ReeF4LieIndex.mem_fixedSubgroup_frobenius_iff describes the group the q-power one
fixes: the points whose matrix entries lie in the field of definition 𝔽_q.
The carrier is numbered by the Bourbaki numbering of the F₄ diagram that the index itself
carries: the character by which the carrier's split torus rescales the parameter of its i-th
numbered raising subgroup is TauCeti.DynkinType.rootGeneratorWeight at .inl i, which
TauCeti.ReeF4LieIndex.rootGeneratorWeight_eq_root_simpleIndex identifies with the i-th simple
root of TauCeti.DynkinType.simplyConnectedRootDatum at F₄. No renumbering adapter is needed,
and every numbered object below is indexed by Fin d.1.rank, the upstream Bourbaki index type of
the index's own Dynkin type.
The carrier is not identified with the pinned simply connected group scheme of type F₄, and the
constructions below transfer to that group scheme only along such an identification, once one is
proved. Nothing here asserts that the carrier is reductive, that its weight torus is maximal, or
that any group below is finite, perfect, or simple.
Main definitions #
TauCeti.ReeF4LieIndex.AmbientGroup: the algebraic-closure-valued points of the carrier, with the group structure it inherits as a subgroup ofGL₂₆.TauCeti.ReeF4LieIndex.simpleRootSubgroup: its positive simple-root subgroup at a Bourbaki-numbered node.TauCeti.ReeF4LieIndex.frobeniusandTauCeti.ReeF4LieIndex.primeFrobenius: theq-power and2-power Frobenius endomorphisms of the ambient group.
Main results #
TauCeti.ReeF4LieIndex.rootGeneratorWeight_eq_root_simpleIndex: the character by which the carrier's torus rescales the parameter of thei-th simple-root subgroup is thei-th simple root of theF₄root datum, in the same Bourbaki numbering.TauCeti.ReeF4LieIndex.frobenius_simpleRootSubgroupandTauCeti.ReeF4LieIndex.primeFrobenius_simpleRootSubgroup: both Frobenius maps fix the numbering of a simple-root subgroup and raise its parameter,Frob_q (x_i(u)) = x_i(u ^ q)andFrob_2 (x_i(u)) = x_i(u ^ 2).TauCeti.ReeF4LieIndex.frobenius_eq_primeFrobenius_pow: theq-power Frobenius is the(2m+1)-st power of the2-power one.TauCeti.ReeF4LieIndex.mem_fixedSubgroup_frobenius_iff: theq-power Frobenius fixes exactly the points whose matrix entries lie in the field of definition.
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.
- R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.
- N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VIII, for the numbering of the
F₄diagram the index's rank and root lengths are read in.
The ambient group and its simple root subgroups #
The ambient group this file attaches to a validated Ree index of type F₄: the points,
over the algebraic closure of the prime field, of the short-root type-F₄ carrier over 𝔽₂. It
is a subgroup of GL₂₆ over that closure.
It is infinite, and it is the same group for every Ree index of type F₄, the parameter m
entering only through the endomorphism whose fixed points are taken. No finiteness, reductivity,
pinning or maximality statement is attached to it, and it is not identified with the points of the
pinned simply connected F₄ group scheme.
Equations
Instances For
The positive simple-root subgroup at the Bourbaki-numbered node i of the F₄ 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.F4ShortRoot.PrimeField.rootSubgroupPoints (Sum.inl ((finCongr ⋯) i)) (↑d).Closure
Instances For
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.
The simple-root subgroups sit at the simple roots of the F₄ root datum. The character by
which the carrier's split weight torus rescales the parameter of simpleRootSubgroup i is the
i-th simple root of TauCeti.DynkinType.simplyConnectedRootDatum at F₄, in the same Bourbaki
numbering; TauCeti.F4ShortRoot.weightTorusPoints_conj_rootSubgroupPoints_root_simpleIndex is the
carrier-level conjugation equation this character governs. This is the sense in which the carrier
serves the diagram the index names; it is not a claim that the carrier is the pinned group of that
diagram, no pinning being constructed for it.
The Frobenius endomorphisms #
The q-power Frobenius endomorphism of the ambient group of a Ree index of type F₄, for
q = 2^(2m+1) the field order the index records.
It is not the family's Steinberg endomorphism, which is an odd power of an exceptional isogeny rather than a Frobenius.
Equations
Instances For
The Frobenius of a Ree index of type F₄ is the carrier's Frobenius at the exponent the index
records.
The Frobenius acts on the ambient group by raising every matrix entry to the q-th power.
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). In particular it does
not permute the numbered nodes: the length exchange of this family belongs to its Steinberg map,
which is not built here.
A point of the ambient group is fixed by the q-power 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, these are the points of the carrier with entries in 𝔽_q.
The prime-field Frobenius endomorphism of the ambient group of a Ree index of type F₄,
squaring each matrix entry. The q-power Frobenius is its (2m+1)-st power, by
frobenius_eq_primeFrobenius_pow.
Equations
Instances For
The prime-field Frobenius of a Ree index of type F₄ is the carrier's Frobenius at exponent
one.
The prime-field Frobenius acts on the ambient group by squaring every matrix entry.
The prime-field Frobenius fixes the Bourbaki numbering of a simple-root subgroup and squares
its parameter, that is, Frob_2 (x_i(u)) = x_i(u ^ 2).
The q-power Frobenius is the (2m+1)-st power of the prime-field Frobenius, the
exponent being the one the index records.