Torus characters of the type E6 minuscule carrier in its named root datum #
TauCeti.E6Minuscule.groupScheme is the full-weight Chevalley carrier obtained from the
twenty-seven-dimensional minuscule representation of the type-E₆ Serre presentation. Its
numbered raising and lowering subgroups and its rank-six split weight torus are explicit, and
their conjugation equation is stated in terms of the corresponding row of CartanMatrix.E 6.
This file identifies that table with the uniform simply connected root datum used by downstream
consumers.
For a validity proof ht : TauCeti.DynkinType.E6.Valid, the root character of the i-th raising
subgroup is
(E6.simplyConnectedRootDatum ht).root (E6.simpleIndex ht i),
and the character of the matching lowering subgroup is its negative. Rewriting the carrier's conjugation equation by these identifications gives the two torus conjugation equations against the named positive and negative simple roots.
The distinction from the equations already in GroupScheme.lean is the dispatcher in the target:
DynkinType.simplyConnectedRootDatum is the root datum reached from a validated Lie-type index,
whereas the carrier was constructed directly from the concrete tables
TauCeti.DynkinType.e6Root and TauCeti.DynkinType.e6SimpleIndex. These results certify that the
two routes use the same Bourbaki numbering and the same character lattice.
This file does not assert reductivity, maximality of the weight torus, existence of all root subgroups, or an identification of the carrier with an independently defined algebraic group. It packages only the torus-character compatibility that the explicit construction already proves.
Main results #
TauCeti.E6Minuscule.rootGeneratorWeight_inl_eq_root_simpleIndex: the raising-subgroup character is the corresponding simple root of the uniform simply connected datum.TauCeti.E6Minuscule.rootGeneratorWeight_inr_eq_neg_root_simpleIndex: the lowering-subgroup character is the negative of that simple root.TauCeti.E6Minuscule.weightTorus_conj_rootSubgroup_root_simpleIndexandTauCeti.E6Minuscule.weightTorus_conj_rootSubgroup_neg_root_simpleIndex: the positive and negative simple-root torus conjugation equations.
References #
- R. W. Carter, Simple Groups of Lie Type, Sections 4.4 and 7.1.
- J. E. Humphreys, Linear Algebraic Groups, Sections 26--27.
- N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate V.
The root-identification proofs and torus-conjugation wrapper patterns are adapted from
TauCeti/Algebra/Lie/SpecialLinear/StandardCarrier/RootDatum.lean, added in
TauCetiProject/TauCeti#5198, and
TauCeti/Algebra/Lie/Symplectic/StandardCarrier/RootDatum.lean, developed in
TauCetiProject/TauCeti#5203.
This advances the "Pinnings" and "Root subgroup maps" targets of Layer 9 of
TauCetiRoadmap/ReductiveGroups/README.md. Its consumer is milestone L0 of
TauCetiRoadmap/CFSGStatement/README.md: ValidLieTypeIndex.AmbientGroup must be traceable through
ValidLieTypeIndex.dynkinType to DynkinType.simplyConnectedRootDatum, with its root subgroups
identified by characters of that same datum.
The numbered subgroups sit at the named simple roots #
The i-th raising subgroup sits at the i-th simple root of the uniform type-E₆
datum. Its character for the action of the carrier's split weight torus is the root selected by
the uniform Bourbaki simple-root index.
The i-th lowering subgroup sits at the negative of the i-th simple root of the uniform
type-E₆ datum.
Torus conjugation equations against the named simple roots #
The torus conjugation equation at a named positive simple root. A point of
the split weight torus conjugates the raising-subgroup element of parameter u at node i to the
same subgroup with parameter α_i(s)u, where α_i is the corresponding root of the uniform
simply connected type-E₆ datum.
The torus conjugation equation at a named negative simple root. A point of
the split weight torus conjugates the lowering-subgroup element of parameter u at node i to
the same subgroup with parameter (-α_i)(s)u.