The Geck carrier of a Lie-type index #
Every valid Lie-type index names a valid Dynkin type through TauCeti.ValidLieTypeIndex.dynkinType
and dynkinType_valid, and the root-systems roadmap attaches to such a type the pinned Geck group
scheme TauCeti.DynkinType.geckGroupScheme: an explicit closed subgroup scheme of GLₙ over ℤ
generated by the divided-power exponential root subgroups of the Bourbaki-numbered Chevalley
generators together with its weight torus. This file evaluates that carrier at the data an index
records, giving every valid index a concrete matrix group over the algebraic closure of its prime
field, numbered root subgroups, and a q-power Frobenius endomorphism.
Nothing in the construction depends on which diagram the index names, so the whole API is stated
for TauCeti.ValidLieTypeIndex, exactly as TauCeti.ValidLieTypeIndex.frobeniusEquiv is: the
field-level and carrier-level maps are the same recipe on every branch, and the branches differ
only in which endomorphism of this group is later taken as the Steinberg map.
The names all carry the geck prefix because this carrier is not the uniform ambient group.
Geck's module is the adjoint module, so the characters occurring in it generate the root lattice
and not, in general, the whole character lattice of the pinned torus. This file does not identify
the carrier with the pinned simply connected Chevalley--Demazure group scheme of
TauCeti.DynkinType.simplyConnectedRootDatum. The uniform
TauCeti.ValidLieTypeIndex.AmbientGroup and TauCeti.ValidLieTypeIndex.simpleRootSubgroup are
assembled by cases in TauCeti.GroupTheory.SpecificGroups.CFSG.Assembly.AmbientGroup; this carrier
serves only the E₈, F₄ and G₂ branches through TauCeti.UnimodularExceptionalIndex. No
declaration below asserts that this carrier is reductive, that its root datum is the simply
connected one, that its weight torus is maximal, or that its point group is finite.
Main definitions #
TauCeti.ValidLieTypeIndex.geckPointsandTauCeti.ValidLieTypeIndex.GeckGroup: the points of the Geck carrier of the underlying Dynkin type over the algebraic closure of the prime field, as a subgroup ofGLₙand as a type.TauCeti.ValidLieTypeIndex.geckRootSubgroup: its Bourbaki-numbered root subgroups.TauCeti.ValidLieTypeIndex.geckWeightTorus: the split weight torus of the same carrier, of rank the rank of the index.TauCeti.ValidLieTypeIndex.geckFrobenius: itsq-power Frobenius, forqthe field order recorded by the index.
Main results #
TauCeti.ValidLieTypeIndex.geckWeightTorus_conj_geckRootSubgroup_root_simpleIndexand its negative-root counterpart: conjugation by a weight-torus point rescales the parameter of the numbered root subgroup at nodeiby the simple rootα_iof the root datumTauCeti.DynkinType.simplyConnectedRootDatumof the Dynkin type the index names, in the same Bourbaki numbering.TauCeti.ValidLieTypeIndex.coe_geckFrobenius_apply: the Frobenius raises every matrix entry to theq-th power.TauCeti.ValidLieTypeIndex.geckFrobenius_geckRootSubgroupandTauCeti.ValidLieTypeIndex.geckFrobenius_geckWeightTorus: it raises the parameter of every numbered root subgroup, and every coordinate of a weight-torus point, to theq-th power.TauCeti.ValidLieTypeIndex.mem_fixedSubgroup_geckFrobenius_iff: its fixed points are the points whose matrix entries lie in the field of definition𝔽_qofTauCeti.ValidLieTypeIndex.fixedField.TauCeti.ValidLieTypeIndex.geckWeightTorus_mem_fixedSubgroup_geckFrobenius: among those points are the weight-torus points all of whose coordinates lie in𝔽_q.TauCeti.ValidLieTypeIndex.geckPrimeFrobenius, withTauCeti.ValidLieTypeIndex.geckPrimeFrobenius_geckRootSubgroup,TauCeti.ValidLieTypeIndex.geckPrimeFrobenius_geckWeightTorusandTauCeti.ValidLieTypeIndex.geckFrobenius_eq_geckPrimeFrobenius_pow: the prime-field Frobenius of the Geck point group, its action on the numbered root subgroups and on the weight torus, and theq-power Frobenius as itse-th power.
References #
- M. Geck, On the construction of semisimple Lie algebras and Chevalley groups,
Proc. Amer. Math. Soc. 145 (2017), 3233--3247, for the matrix realization that
TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.GeckLatticesupplies. - R. W. Carter, Simple Groups of Lie Type, §4.4, for the pinned root-subgroup conventions and the entrywise action of the Frobenius.
Roadmap #
Milestone L0 of TauCetiRoadmap/CFSGStatement/README.md asks for the points of the pinned simply
connected Chevalley--Demazure group scheme, and milestone L1 for the equation
Frob_q (x_α(t)) = x_α(t ^ q) on it. This file closes neither: it supplies the explicit data in
the shape those milestones need it, on a carrier whose identification with the L0 one is owed by
Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. The lattice condition that identification
requires, namely that the Geck weights span the whole character lattice, holds only on the E₈,
F₄ and G₂ diagrams and is recorded in
TauCeti/GroupTheory/SpecificGroups/CFSG/Unimodular.lean.
The Geck point group and its root subgroups #
The points of the Geck carrier of a valid Lie-type index, taken over the algebraic closure
of its prime field: a subgroup of GLₙ, generally infinite, carrying the Bourbaki-numbered root
subgroups and weight torus that carrier comes with.
No finiteness, reductivity or maximality statement is attached to it, and it is not claimed to be
the pinned simply connected Chevalley--Demazure group of
TauCeti.DynkinType.simplyConnectedRootDatum that milestone L0 of
TauCetiRoadmap/CFSGStatement/README.md asks for: identifying the two is Layer 9 work of
TauCetiRoadmap/ReductiveGroups/README.md, and this file neither performs nor assumes it.
Equations
- d.geckPoints = d.dynkinType.geckPoints ⋯ d.Closure
Instances For
The Geck point group as a type, with the group structure it inherits as a subgroup of
GLₙ over the algebraic closure. It is named for the carrier it is built from rather than as an
ambient group, since the identification with the L0 carrier is not available.
Equations
- d.GeckGroup = ↥d.geckPoints
Instances For
The numbered root subgroups of the Geck point group. The left summand indexes the raising
generators and the right summand the lowering generators of the pinned Bourbaki numbering, so
geckRootSubgroup d (.inl i) is the simple root subgroup x_{α_i}.
Equations
- d.geckRootSubgroup i = d.dynkinType.geckRootSubgroupPoints ⋯ i d.Closure
Instances For
The general linear matrix underlying a root-subgroup point is the represented Geck root-subgroup matrix of the same parameter.
The pinned weight torus #
The split weight torus of the Geck point group of a valid Lie-type index, of rank the rank
of the index: the diagonal points through which the Geck coordinate weights act. Together with
TauCeti.ValidLieTypeIndex.geckRootSubgroup it is the pinned data of the carrier that the
conjugation equations below are stated against.
As for the point group itself, no maximality statement is attached to it, and it is not claimed to be the split maximal torus of a pinned simply connected Chevalley--Demazure group.
Equations
Instances For
The weight torus of an index is the represented weight torus of the pinned Geck carrier of the Dynkin type it names, over the algebraic closure of the prime field of the index.
The general linear matrix underlying a weight-torus point is the diagonal matrix of the Geck weight characters at that point.
The pinning equation of the Geck carrier of an index, at a named simple root. Conjugating
the numbered raising subgroup at Bourbaki node i by a weight-torus point s rescales its
parameter by α_i(s), where α_i is the simple root of the pinned simply connected root datum of
the Dynkin type the index names, at the same node.
The character is read in that root datum rather than as a row of the Cartan matrix: the datum is
the one attached to TauCeti.ValidLieTypeIndex.dynkinType, so it carries the Bourbaki node
numbering that numbers the root subgroups here, and node i on either side is the same node.
The pinning equation of the Geck carrier of an index, at the negative of a named simple root.
The Frobenius endomorphism #
The q-power Frobenius endomorphism of the Geck point group, for q the field order
recorded by the index. It is the carrier-level companion of the field-level
TauCeti.ValidLieTypeIndex.frobeniusEquiv, and like it is defined on every branch: the untwisted
branches take it as their Steinberg map, the graph-twisted branches compose it with a diagram
automorphism, and the Suzuki--Ree and Tits branches take an odd power of a half-Frobenius whose
square it is.
Equations
- d.geckFrobenius = d.dynkinType.geckFrobenius ⋯ d.characteristic d.fieldExponent d.Closure
Instances For
The Frobenius is that of the pinned Geck carrier at the exponent recorded by the index. This is its unfolding lemma; the definition itself stays sealed.
The Frobenius acts on the Geck point group by raising every matrix entry to the q-th
power.
The Frobenius 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 endomorphism of the Geck point group, the p-power map for p
the defining characteristic. The q-power Frobenius TauCeti.ValidLieTypeIndex.geckFrobenius is
its e-th power, for e the field exponent the index records, by
geckFrobenius_eq_geckPrimeFrobenius_pow, so the two agree on an index of prime field
order.
Equations
- d.geckPrimeFrobenius = d.dynkinType.geckFrobenius ⋯ d.characteristic 1 d.Closure
Instances For
The prime-field Frobenius is that of the pinned Geck carrier at exponent one. This is its unfolding lemma; the definition itself stays sealed.
The prime-field Frobenius acts on the Geck point group by raising every matrix entry to the
p-th power, for p the defining characteristic.
The prime-field Frobenius raises the parameter of every numbered root subgroup to the p-th
power. On a simple root subgroup this reads Frob_p (x_α(t)) = x_α(t ^ p).
The q-power Frobenius 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 Frobenius raises every coordinate of a weight-torus point to the q-th power.
A weight-torus point whose coordinates lie in the field of definition is fixed by the
Frobenius. Writing 𝔽_q for TauCeti.ValidLieTypeIndex.fixedField, these are the weight-torus
points with coordinates in 𝔽_q; that they exhaust the weight-torus points of the Frobenius-fixed
group, or that they form a maximal torus of it, is not claimed.
A point of the Geck point group is fixed by the 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 Frobenius-fixed group is
therefore the group of points of the Geck carrier whose entries lie in 𝔽_q.
This is deliberately not a simp lemma: TauCeti.fixedSubgroup is MonoidHom.eqLocus against the
identity, so simp rewrites its left-hand side to d.geckFrobenius g = g through the Mathlib
simp lemma MonoidHom.mem_eqLocus, and the simpNF linter rejects the annotation.