The adjoint elementary Chevalley group of a Chevalley system #
The Kostant root-subgroup machinery is parameterized over a quadruple (e, h, ρ, M): a family of
distinguished nilpotent root vectors, a family of distinguished Cartan vectors, a rational
representation, and a lattice in it stable under the Kostant integral form. Every consumer so far
has taken that quadruple as a hypothesis. This file supplies one, from a Chevalley system x with
Chevalley involution ω in a Lie algebra L with nondegenerate Killing form over ℚ:
e = x, h = α ↦ α∨, ρ = the adjoint action of U(L), M = the Chevalley lattice.
TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.Adjoint.Basic proved that the Chevalley lattice
is admissible for that action. What was missing is the third hypothesis, nilpotency of the acting
root vectors, and it is now TauCeti.IsSl2System.isNilpotent_ad_rootVector. With all three in
place the divided-power exponentials
x_α(t) = exp (t · ad (x α))
are automorphisms of A ⊗[ℤ] M over every commutative value ring A, and the subgroup they
generate is the elementary Chevalley group E(A) of Carter, Simple Groups of Lie Type, §4.4.
Nothing is chosen here: the carrier of E(A) is read off the Chevalley system supplied by the
caller.
The relations these root subgroups satisfy are the point of the construction, and they are the
Chevalley relations rather than generic consequences of nilpotency. Two root vectors bracket to
zero when the sum of their roots is not a root, so their root subgroups commute; and when the sum
is a root γ, the bracket is N x γ for the integer structure constant N of the Chevalley
system, so
⁅x_α(s), x_β(t)⁆ = x_γ(N s t)
whenever α + γ and β + γ are not roots, which is the condition that makes the two sides class
two. When α and β are nonzero roots, that integer is ±(p + 1) for p the root-string
coefficient chainBotCoeff α β, by
TauCeti.IsChevalleySystem.intStructureConstant_eq_natCast_or_eq_neg_natCast, and it is nonzero.
Functoriality in the value ring, the Frobenius endomorphism, the split torus, and the group scheme
generated by the root subgroups are all stated for a general (e, h, ρ, M) in the
RootSubgroup files and apply to this instance verbatim; they are not restated here.
Main declarations #
TauCeti.IsChevalleySystem.chevalleyLatticeAddSubgroup: the Chevalley lattice in the shape the root-subgroup machinery takes its admissible lattice in.TauCeti.IsChevalleySystem.adjointRootSubgroup: the root subgroupx_αover a value ring.TauCeti.IsChevalleySystem.adjointElementaryGroup: the elementary Chevalley groupE(A).TauCeti.IsChevalleySystem.commute_adjointRootSubgroup: root subgroups whose roots do not add to a root commute.TauCeti.IsChevalleySystem.commutatorElement_adjointRootSubgroup: the class-two Chevalley commutator relation.
References #
- R. W. Carter, Simple Groups of Lie Type, §4.4 and Theorem 5.2.2.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §25.5 and §27.
- J. C. Jantzen, Representations of Algebraic Groups, II.1.
This advances Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, "pinned Chevalley--Demazure
group schemes over ℤ", specifically its "Chevalley--Demazure construction" and "root subgroup
maps" targets, by giving the first instance of the Kostant root-subgroup data that is not a
hypothesis. This is the adjoint-form instance; milestone L0 of
TauCetiRoadmap/CFSGStatement/README.md additionally needs the simply connected representation
and admissible lattice before it can obtain its pinned ambient group and root-subgroup maps.
Every root vector of a normalised system acts nilpotently in the adjoint representation of the enveloping algebra. This is the nilpotency hypothesis for the divided-power exponential; lattice stability supplies its integrality separately.
The Kostant data of a Chevalley system #
The integral root--coroot span read as an additive subgroup of L. This is the shape in which
the Kostant root-subgroup machinery takes its admissible lattice. It is an abbreviation so the
finite and free module instances on rootCorootSpan x remain available to consumers.
Equations
Instances For
The additive-subgroup form of the Chevalley lattice agrees with the underlying additive
subgroup of chevalleyLieLattice.
The Lie-subalgebra and additive-subgroup presentations of a Chevalley lattice are linearly equivalent.
Equations
Instances For
The Chevalley lattice is admissible in the shape the root subgroups consume. This is
TauCeti.IsChevalleySystem.chevalleyKostantForm_apply_mem with the Kostant form written out as the
generic one of the root vectors and the coroots.
The root subgroups and the elementary group #
The root subgroup x_α of the adjoint elementary Chevalley group. Over a value ring A it
sends a parameter t to the divided-power exponential of t · ad (x α) acting on A ⊗[ℤ] M, so
x_α(s + t) = x_α(s) x_α(t).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The adjoint root subgroup is the generic parametrized Kostant root subgroup of the data attached to a Chevalley system.
The adjoint root-subgroup element acts through the base-changed divided-power exponential.
A zero weight contributes the trivial element to the adjoint root subgroup.
The adjoint elementary Chevalley group E(A): the subgroup of the automorphisms of
A ⊗[ℤ] M generated by all root subgroups of a Chevalley system.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The adjoint elementary Chevalley group is the generic Kostant elementary subgroup of the data attached to a Chevalley system.
Every root-subgroup element belongs to the adjoint elementary Chevalley group.
The adjoint elementary Chevalley group is generated by the root subgroups.
The adjoint elementary Chevalley group is generated by the root subgroups at nonzero roots; the remaining weight indices contribute only the identity.
The Chevalley relations #
Root subgroups whose roots do not add to a root commute. The hypothesis is exactly that the
root space at α + β vanishes, so the two root vectors bracket to zero. It also excludes the
opposite case β = -α, where the sum is the zero weight and the corresponding weight space is the
Cartan subalgebra rather than ⊥. For nonzero α, the bracket in that excluded case is the
coroot; no converse to this commuting criterion is asserted here.
The class-two Chevalley commutator relation in the adjoint elementary group. If γ = α + β
is a root and neither α + γ nor β + γ is one, then
⁅x_α(s), x_β(t)⁆ = x_γ(N s t),
with N the integer structure constant of the Chevalley system. The two vanishing hypotheses are
what confine the commutator to the single root subgroup at γ; a root string long enough to reach
2α + β contributes a further factor and is the multiply-laced relation instead.