The special isogenies of the pinned B₂, G₂ and F₄ root data #
The root data of B₂ and F₄ over a field of characteristic two, and that of G₂ over a
field of characteristic three, admit an isogeny with themselves which exchanges the two root
lengths. These three types are the only ones: exchanging the two lengths identifies the root
system with its dual, and among the non-simply-laced irreducible types only B₂, F₄ and G₂
are self-dual, the ratio of the two lengths then fixing the characteristic. The resulting
special isogenies of the pinned Chevalley groups are the ones whose odd powers cut out the
Suzuki and Ree groups. This file constructs all three, on the pinned root data
TauCeti.DynkinType.typeBSimplyConnectedRootDatum at rank two,
TauCeti.DynkinType.g2SimplyConnectedRootDatum and
TauCeti.DynkinType.f4SimplyConnectedRootDatum.
The construction #
All three are instances of TauCeti.RootPairingIsogeny.ofMatrix, so all four pieces of data are
explicit integer tables and no carrier is chosen from an existence theorem. The character and
cocharacter lattices are Fin t.rank → ℤ in the fundamental-weight and simple-coroot bases, and
the whole isogeny is determined by the single matrix acting on the character lattice: the
cocharacter map is its transpose, and the index bijection and exponents are then forced.
That matrix is itself forced by the length-exchanging permutation σ of the Bourbaki-numbered
simple roots and by the normalised squared lengths ℓ of TauCeti.DynkinType.rootLength. Writing
x for a character in the fundamental-weight basis, it is
(A x) i = ℓ (σ i) * x (σ i),
with σ the pinned TauCeti.lengthPermRankTwo for B₂ and G₂ and TauCeti.lengthPermF4 for
F₄. On the simple roots this reads A (α (σ i)) = ℓ (σ i) • α i, which is the defining relation
f (b α) = q α · α of a special isogeny of root data, with the isogeny exponent q at a simple
root the other length; squaring it gives A ^ 2 = p, since ℓ takes the two values 1 and p
and σ exchanges them. TauCeti.DynkinType.b2SpecialIsogeny_mul_self and its G₂ and F₄
counterparts are that square relation, in the form τ ∘ τ = Frob_p on root data.
The index tables extend σ from the simple roots to all eight, twelve, respectively forty-eight,
roots. They are not free choices either: A is invertible over ℚ, so the index bijection and
the exponents are determined by the matrix, and the tables merely record the resulting values so
that the defining equations reduce.
All three sets of tables and their matrix equations already exist, in
TauCeti/LinearAlgebra/RootSystem/SimplyConnectedRootDatum/B/SpecialMap.lean,
TauCeti/LinearAlgebra/RootSystem/SimplyConnectedRootDatum/G2/SpecialMap.lean and
TauCeti/LinearAlgebra/RootSystem/SimplyConnectedRootDatum/F4/SpecialMap.lean: they supply the
matrices, the index bijections, and the exponents. The G₂ and F₄ data are tabulated on the
root indices of their own pinned datum, so the squared-length tables
TauCeti.DynkinType.g2Length and TauCeti.DynkinType.f4Length are the exponents outright, while
the rank-two specialisation of the uniform type Bₙ enumeration carries its own transported
exponent TauCeti.DynkinType.b2SpecialIsogenyExponent. All this file adds is the bundled isogeny
in each case, and the relations that are statements about it.
Main definitions #
TauCeti.DynkinType.b2SpecialIsogeny: the special isogeny of the pinnedB₂root datum, belonging to characteristic two.TauCeti.DynkinType.g2SpecialIsogeny: the special isogeny of the pinnedG₂root datum, belonging to characteristic three.TauCeti.DynkinType.f4SpecialIsogeny: the special isogeny of the pinnedF₄root datum, belonging to characteristic two.
Main results #
TauCeti.DynkinType.b2SpecialIsogeny_mul_self,TauCeti.DynkinType.g2SpecialIsogeny_mul_selfandTauCeti.DynkinType.f4SpecialIsogeny_mul_self: composing the special isogeny with itself gives scaling by the characteristic, which is the root-datum form ofτ ^ 2 = Frob_p.TauCeti.DynkinType.b2SpecialIsogeny_pow_mul_self,TauCeti.DynkinType.g2SpecialIsogeny_pow_mul_selfandTauCeti.DynkinType.f4SpecialIsogeny_pow_mul_self: the same relation at every power, which at an odd exponent is the square relation the Suzuki and Ree groups are cut out by.TauCeti.DynkinType.b2SpecialIsogeny_weightMap_root_typeBSimpleIndex,TauCeti.DynkinType.g2SpecialIsogeny_weightMap_root_castLEandTauCeti.DynkinType.f4SpecialIsogeny_weightMap_root_castAdd: the defining relation on the simple roots, in the form the group-scheme isogeny is pinned by.TauCeti.DynkinType.b2SpecialIsogeny_exponent_typeBSimpleIndex_eq_one_iff,TauCeti.DynkinType.g2SpecialIsogeny_exponent_castLE_eq_one_iffand itsF₄counterpart: on the simple roots the exponent is1exactly at a short node, read off asTauCeti.DynkinType.IsLongSimpleRoot.
Roadmap and references #
This is the target "Special isogenies in characteristics two and three" of Layer 9 of
TauCetiRoadmap/ReductiveGroups/README.md, at the level of root data; the group-scheme isogeny
τ is built from it. Its consumer is milestone L2 of TauCetiRoadmap/CFSGStatement/README.md,
which selects τ_X for a TauCeti.SuzukiReeIndex and takes odd powers of it, and whose exponent
convention is stated against TauCeti.DynkinType.IsLongSimpleRoot and the length permutations
pinned in TauCeti/LinearAlgebra/RootSystem/DiagramPermutations.lean. With B₂ here the
root-datum half of that target is complete, since
TauCeti.DynkinType.exists_isSpecialNodePerm_iff shows that no other valid Dynkin type admits a
length-exchanging node permutation at all; what the target still asks for is the lift of these
three to morphisms of the pinned group schemes, and their action on the root subgroups.
- R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.
- Schémas en groupes (SGA 3), Exposé XXI, 6.8, and Exposé XXII.
- R. W. Carter, Simple Groups of Lie Type, §§12.3--12.4.
B₂ in characteristic two #
The special isogeny of the pinned B₂ root datum, belonging to characteristic two. Its
character-lattice map is TauCeti.DynkinType.b2SpecialIsogenyMatrix; the map on cocharacters is
the transposed matrix, and the two are related by the dot-product pairing of the datum. Unlike the
G₂ and F₄ cases the rescaling exponent is not a squared-length table read off the coordinate
enumeration, because the pinned type Bₙ datum indexes its roots uniformly in the rank: it is the
transported table TauCeti.DynkinType.b2SpecialIsogenyExponent, still 1 on a short root and 2
on a long one.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The square of the special isogeny of B₂ is scaling by two. This is the root-datum form of
the relation τ ^ 2 = Frob_p that identifies the exceptional isogeny in characteristic p; the
square relation is the root-datum input for constructing the exceptional Steinberg endomorphisms
used to define the Suzuki groups.
The powers of the special isogeny of B₂ square to the powers of two. At n = 2 * m + 1
this is the root-datum form of the square relation satisfied by the Steinberg endomorphism whose
fixed points are the Suzuki group ²B₂(2 ^ (2 * m + 1)).
The defining relation of the special isogeny of B₂ on the simple roots. The character
map carries the simple root at the length-exchanged node to the simple root at i, rescaled by
the squared length of that other node. This is the root-datum form of
τ (x_α (t)) = x_{σ(α)} (t ^ q) for α the simple root at i: the character map is the
pullback along τ, so the coefficient (B 2).rootLength (lengthPermRankTwo i) here is q,
indexed by α and not by σ(α). Since σ exchanges the two lengths, q is 1 when α is long
and 2 when α is short. Read instead at the pullback index σ(α), which is how the isogeny's
exponent field is indexed, the same table takes the value 1 at the short node; that is
TauCeti.DynkinType.b2SpecialIsogeny_exponent_typeBSimpleIndex_eq_one_iff.
The exponent of the special isogeny of B₂ at a simple root is 1 exactly at the short node.
The exponent field is indexed by the source of the character map, which is σ(α) and not α in
τ (x_α (t)) = x_{σ(α)} (t ^ q); as σ exchanges the two lengths, the value 1 at the short node
σ(α) is the exponent q = 1 at the long simple root α. So this is the convention that the
exceptional isogeny raises a long root parameter to the first power and a short one to the
characteristic.
G₂ in characteristic three #
The special isogeny of the pinned G₂ root datum, belonging to characteristic three. Its
character-lattice map is TauCeti.DynkinType.g2SpecialIsogenyMatrix; the map on cocharacters is
the transposed matrix, and the two are related by the dot-product pairing of the datum. The
rescaling exponent needs no table of its own: the pinned datum is tabulated on its own root
indices, so the squared-length table TauCeti.DynkinType.g2Length already is it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The square of the special isogeny of G₂ is scaling by three. This is the root-datum form
of the relation τ ^ 2 = Frob_p that identifies the exceptional isogeny in characteristic p.
The powers of the special isogeny of G₂ square to the powers of three. At n = 2 * m + 1
this is the root-datum form of the square relation satisfied by the Steinberg endomorphism whose
fixed points are the Ree group ²G₂(3 ^ (2 * m + 1)).
The defining relation of the special isogeny of G₂ on the simple roots. The character
map carries the simple root at the length-exchanged node to the simple root at i, rescaled by
the squared length of that other node. This is the root-datum form of
τ (x_α (t)) = x_{σ(α)} (t ^ q) with q = 1 at a long simple root and q = 3 at a short one.
The exponent of the special isogeny of G₂ at a simple root is 1 exactly at the short
node, which is the convention that the exceptional isogeny raises a long root parameter to the
first power and a short one to the characteristic.
F₄ in characteristic two #
The special isogeny of the pinned F₄ root datum, belonging to characteristic two. Its
character-lattice map is TauCeti.DynkinType.f4SpecialIsogenyMatrix; the map on cocharacters is
the transposed matrix, and the two are related by the dot-product pairing of the datum. The
rescaling exponent needs no table of its own: the pinned datum is tabulated on its own root
indices, so the squared-length table TauCeti.DynkinType.f4Length already is it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The square of the special isogeny of F₄ is scaling by two. This is the root-datum form of
the relation τ ^ 2 = Frob_p that identifies the exceptional isogeny in characteristic p.
The powers of the special isogeny of F₄ square to the powers of two. At n = 2 * m + 1
this is the root-datum form of the square relation satisfied by the Steinberg endomorphism whose
fixed points are the Ree group ²F₄(2 ^ (2 * m + 1)); at n = 1 it underlies ²F₄(2), whose
derived subgroup is the Tits group.
The defining relation of the special isogeny of F₄ on the simple roots. The character
map carries the simple root at the length-exchanged node to the simple root at i, rescaled by
the squared length of that other node. This is the root-datum form of
τ (x_α (t)) = x_{σ(α)} (t ^ q) with q = 1 at a long simple root and q = 2 at a short one.
The exponent of the special isogeny of F₄ at a simple root is 1 exactly at a short node,
which is the convention that the exceptional isogeny raises a long root parameter to the first
power and a short one to the characteristic.