The Lie-type indices whose Dynkin diagram is unimodular #
TauCeti.ValidLieTypeIndex.GeckGroup gives every valid index a concrete matrix group with numbered
root subgroups and a Frobenius. That carrier is built from the adjoint representation, so the
characters occurring in it generate the root lattice and not, in general, the whole character
lattice of the pinned torus: it is expected to be the adjoint form of a Chevalley--Demazure group,
whereas the CFSG recipe has to be run in the simply connected form. The lattice condition that
separates the two forms -- that the weights span the whole character lattice -- holds by
TauCeti.DynkinType.span_range_geckWeight_eq_top_iff exactly in the types E₈, F₄ and G₂.
This file proves that span, and the closed immersion of the weight torus it buys, for
TauCeti.UnimodularLieIndex, the valid indices whose underlying diagram is one of those three.
Six of the seventeen Lie-type constructors qualify, and they are of two kinds:
E₈(q), F₄(q), G₂(q), ²G₂(3^(2m+1)), ²F₄(2^(2m+1)), ²F₄(2)'.
The three on the left are untwisted, and their Steinberg map is the q-power Frobenius
TauCeti.ValidLieTypeIndex.geckFrobenius; they are collected as
TauCeti.UnimodularExceptionalIndex and carried through the rest of the recipe here. The three on
the right take an odd power of a half-Frobenius instead, so their Steinberg map is not built in
this file.
The predicate TauCeti.LieTypeIndex.HasUnimodularDiagram is about the diagram alone, so it says
nothing about which Steinberg map an index takes. That is what makes it the right hypothesis here:
²F₄(2^(2m+1)) and ²F₄(2)' have the same character lattice as F₄(q), and ²G₂(3^(2m+1)) the
same as G₂(q), whatever endomorphism is later taken of their common carrier. The Suzuki family
²B₂(2^(2m+1)) does not appear: its underlying diagram is B₂, whose Cartan matrix has
determinant two, so the Geck carrier is not its simply connected form.
Identifying the carrier itself with the pinned simply connected Chevalley--Demazure group, and
proving it reductive, is the Layer 9 work of TauCetiRoadmap/ReductiveGroups/README.md that this
roadmap consumes rather than performs; no declaration below asserts either, nor that a constructed
group is finite, perfect, or simple.
Main definitions #
TauCeti.UnimodularExceptionalIndex: the unimodular indices whose Steinberg map is not a half-Frobenius power, that isE₈(q),F₄(q)andG₂(q), withTauCeti.UnimodularExceptionalIndex.AmbientGrouptheir ambient group,TauCeti.UnimodularExceptionalIndex.simpleRootSubgroupits numbered simple root subgroups,TauCeti.UnimodularExceptionalIndex.steinbergtheir Steinberg map andTauCeti.UnimodularExceptionalIndex.Groupthe candidate simple group, the derived subgroup of the fixed points of that map modulo the centre of that derived subgroup.
Main results #
TauCeti.UnimodularLieIndex.span_range_geckWeight_eq_top: the Geck weights of an index with unimodular diagram span the whole character lattice, the lattice condition the simply connected form requires.TauCeti.UnimodularLieIndex.isClosedImmersion_geckWeightTorus: consequently the pinned split torus is a closed subgroup scheme of the Geck carrier.TauCeti.UnimodularExceptionalIndex.steinberg_geckRootSubgroupandTauCeti.UnimodularExceptionalIndex.steinberg_geckWeightTorus: the Steinberg map raises the parameter of every numbered root subgroup, and every coordinate of a weight-torus point, to theq-th power, which is how the Steinberg map of an untwisted index acts on both halves of the pinned data of this carrier.TauCeti.UnimodularExceptionalIndex.mem_fixedSubgroup_steinberg_iff: the fixed points of that map are the points of the carrier whose matrix entries lie in the field of definition𝔽_qrecorded byTauCeti.ValidLieTypeIndex.fixedField.TauCeti.UnimodularExceptionalIndex.primeFrobenius, withTauCeti.UnimodularExceptionalIndex.coe_primeFrobenius_apply,TauCeti.UnimodularExceptionalIndex.primeFrobenius_geckRootSubgroup,TauCeti.UnimodularExceptionalIndex.primeFrobenius_geckWeightTorusandTauCeti.UnimodularExceptionalIndex.steinberg_eq_primeFrobenius_pow: the prime-field Frobenius, its entrywise action, its action on the numbered root subgroups and on the weight torus, and the Steinberg endomorphism as itse-th power.
References #
- R. W. Carter, Simple Groups of Lie Type, §§4.4 and 7.1.
- R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.17.
- R. Steinberg, Endomorphisms of Linear Algebraic Groups, Memoirs Amer. Math. Soc. 80 (1968), §11, for the Steinberg endomorphism conventions.
- M. Geck, On the construction of semisimple Lie algebras and Chevalley groups, Proc. Amer. Math. Soc. 145 (2017), 3233--3247, for the matrix realization of the carrier.
- N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plates VII--IX, for the unimodularity
of the
E₈,F₄andG₂Cartan matrices.
Carrier-level description #
For the three untwisted branches treated here, steinberg is the q-power Frobenius on the Geck
carrier. Thus mem_fixedSubgroup_steinberg_iff identifies its fixed points with the carrier points
whose matrix entries lie in 𝔽_q, and Group is the derived subgroup of those fixed points
modulo the centre of that derived subgroup. Both are formed on the Geck carrier, and they transfer
to the pinned simply connected group scheme of the diagram only along an identification of the two
carriers, which is not proved here. The other unimodular branches use half-Frobenius maps instead
and are therefore not included in UnimodularExceptionalIndex.
The Geck weights of an index with unimodular diagram span the whole character lattice. This
is the lattice condition that separates the simply connected form of a Chevalley--Demazure group
from the adjoint one, and it fails on every other diagram, which is why this subtype is the domain
of the results here. It is a statement about characters only: that the carrier is reductive, and
that it is the pinned simply connected group of TauCeti.DynkinType.simplyConnectedRootDatum, are
Layer 9 statements that this file consumes when they arrive rather than proving.
The pinned split torus is a closed subgroup scheme of the Geck carrier. This is the
torus half of the pinning, and it is exactly what the full character span of
TauCeti.UnimodularLieIndex.span_range_geckWeight_eq_top buys.
The untwisted families E₈(q), F₄(q) and G₂(q) #
An index with unimodular diagram whose Steinberg map is not an odd power of a half-Frobenius.
By TauCeti.LieTypeIndex.exists_eq_of_hasUnimodularDiagram_of_not_usesHalfFrobenius these are
exactly the three untwisted families E₈(q), F₄(q) and G₂(q); the condition removes the Ree
families ²G₂(3^(2m+1)) and ²F₄(2^(2m+1)) and the Tits index, which share their diagrams.
Equations
Instances For
The index E₈(q).
Equations
Instances For
The index F₄(q).
Equations
Instances For
The index G₂(q), for q at least three.
Equations
Instances For
The ambient group of an untwisted unimodular exceptional index: the points of the Geck
carrier of the underlying valid index over the algebraic closure of its prime field. In the types
E₈, F₄ and G₂ the adjoint module spans the full character lattice, which is what lets the
Geck carrier serve as the carrier of these branches. It is not identified with the pinned simply
connected group scheme of the diagram.
Equations
- d.AmbientGroup = (↑↑d).GeckGroup
Instances For
The positive simple-root subgroup at the Bourbaki-numbered node i of the diagram: the Geck
carrier's numbered root subgroup at the positive copy of i, as a homomorphism from the additive
group of the algebraic closure.
Equations
- d.simpleRootSubgroup i = (↑↑d).geckRootSubgroup (Sum.inl i)
Instances For
The Steinberg endomorphism of an untwisted unimodular exceptional index: the q-power
Frobenius of the Geck point group, where q is the field order recorded by the index. The three
families this covers are untwisted, so no diagram automorphism and no half-Frobenius enters.
Equations
- d.steinberg = (↑↑d).geckFrobenius
Instances For
The Steinberg map of an untwisted unimodular exceptional index is the Frobenius of its Geck point group. This is its unfolding lemma; the definition itself stays sealed.
It is deliberately not a simp lemma: steinberg_geckRootSubgroup and coe_steinberg_apply are
the normal forms the pinned equations of this file are stated against, and unfolding to
TauCeti.ValidLieTypeIndex.geckFrobenius would keep them from firing.
The Steinberg map acts on the Geck point group by raising every matrix entry to the q-th
power.
The Steinberg map raises the parameter of every numbered root subgroup to the q-th
power. On a simple root subgroup this is the equation Frob_q (x_α(t)) = x_α(t ^ q) that
milestone L1 asks of the untwisted families, proved here on the Geck carrier.
The prime-field Frobenius of the Geck point group, 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 = (↑↑d).geckPrimeFrobenius
Instances For
The prime-field Frobenius of an untwisted unimodular exceptional index is the prime-field Frobenius of its Geck point group.
The prime-field Frobenius acts on the Geck point group by raising every matrix entry to the
p-th power.
The prime-field Frobenius raises the parameter of every numbered root subgroup to the p-th
power. On a simple root subgroup this is Frob_p (x_α(t)) = x_α(t ^ 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 raises every coordinate of a weight-torus point to the p-th
power.
The Steinberg map raises every coordinate of a weight-torus point to the q-th power. It
is the untwisted case of the equation a Steinberg endomorphism satisfies on the second half of the
pinned data, the first half being TauCeti.UnimodularExceptionalIndex.steinberg_geckRootSubgroup
on the root subgroups.
A point of the Geck point group is fixed by the Steinberg map 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 fixed-point subgroup associated to this map is therefore the group of
points of the Geck carrier whose entries lie in 𝔽_q.
As for TauCeti.ValidLieTypeIndex.mem_fixedSubgroup_geckFrobenius_iff, this is not a simp lemma:
simp rewrites its left-hand side through MonoidHom.mem_eqLocus, and the simpNF linter rejects
the annotation.
The finite-group candidate #
The finite-simple-group candidate attached to an untwisted unimodular exceptional 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, nor any identification of the Geck carrier with the pinned simply connected group scheme of the diagram.