The weight basis of a Chevalley lattice #
TauCeti.UniversalEnvelopingAlgebra.kostantWeightBasis produces a basis of weight vectors for an
admissible lattice M ≤ V from three inputs: stability of M under the Kostant integral form,
finite generation of M over ℤ, and the requirement that M lie in the span of the integral
joint weight spaces of the designated Cartan vectors. Every consumer of a weight basis — the split
maximal torus, the matrix coordinates of a Kostant root subgroup, and the group scheme generated by
the root subgroups — therefore still carried those three as hypotheses.
This file discharges them for the Chevalley lattice L_ℤ = (rootCorootSpan x).toAddSubgroup of a
Chevalley system x, whose admissibility for the adjoint representation is
TauCeti.IsChevalleySystem.chevalleyKostantForm_apply_mem and whose finite generation is
TauCeti.instModuleFiniteRootCorootSpan read through TauCeti.instModuleFiniteToAddSubgroup. The
distinguished Cartan vectors are TauCeti.corootFamily, and the missing input is the weight datum:
L_ℤ is spanned by the root vectors and the coroots, and each of those is a joint eigenvector of
the operators ad α∨. A root vector x β has the integer weight TauCeti.rootCartanWeight β,
while a coroot is annihilated by every ad α∨ and so has weight zero. That is exactly the span
condition, so the Chevalley lattice acquires a weight basis with nothing left to assume. Only the
stability input needs the Chevalley system; the weight datum holds for any normalized system of
root vectors.
That the resulting basis is a basis of a full ℤ-form, rather than of a proper subspace, is
TauCeti.IsSl2System.span_rootCorootSpan_eq_top read through Submodule.coe_toAddSubgroup.
Two consequences are recorded. The lattice is the internal direct sum of the sublattices it cuts out
of the weight spaces, and over any commutative ring the torus of coroot cocharacters acts diagonally
on the base change of the lattice, scaling a weight vector by the value of its character. That last
equation identifies the character by which the torus acts on each weight component. It is not by
itself a pinning: the pinning equation t(s) xᵢ(u) t(s)⁻¹ = xᵢ(α(s) u) relating the torus to the
root subgroups needs the separate hypothesis that the root vectors act nilpotently, which this file
does not supply, and exhibiting the maximal torus of the pinning needs a rank-ℓ cocharacter
datum — equivalently the simply connected lattice — which the adjoint lattice does not provide.
A ℤ-basis of a lattice is not canonical and this one is no exception: the underlying
kostantWeightBasis chooses a basis of each weight sublattice. What is canonical is the weight
decomposition, and the Chevalley basis itself is one of the admissible choices rather than the one
this construction returns.
Main definitions #
TauCeti.rootCorootWeightBasisCard: the number of index values of the weight basis of the integral root--coroot span.TauCeti.IsChevalleySystem.chevalleyWeightBasisandTauCeti.IsChevalleySystem.chevalleyWeightBasisFin: the weight basis of the Chevalley lattice, the latter numbered byFin, paired withTauCeti.IsChevalleySystem.chevalleyWeightFin.TauCeti.IsChevalleySystem.chevalleyTorusPoints: the torus of coroot cocharacters on the points of the Chevalley lattice.
Main results #
TauCeti.IsSl2System.isCartanWeightVector_rootVectorandTauCeti.isCartanWeightVector_cartan, specialized to a coroot inTauCeti.isCartanWeightVector_coroot: the generators of the Chevalley lattice are joint eigenvectors of the coroot operators, of the stated integral weights.TauCeti.IsSl2System.mem_iSup_jointWeightSpace: the Chevalley lattice lies in the span of the integral joint weight spaces.TauCeti.IsChevalleySystem.kostantForm_apply_mem_rootCorootSpan: the Chevalley lattice is stable under its Kostant form, in the shape the weight-basis API consumes.TauCeti.IsChevalleySystem.isInternal_weightSublattice: the Chevalley lattice is the internal direct sum of its weight sublattices.TauCeti.IsChevalleySystem.isCartanWeightVector_chevalleyWeightBasisFin: the numbered weight basis consists of weight vectors of the recorded weights.TauCeti.IsChevalleySystem.chevalleyTorusPoints_tmul_of_isCartanWeightVector: a torus point scales a weight vector by the value of its character.
References #
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §27.1.
- R. W. Carter, Simple Groups of Lie Type, §4.4.
- J. C. Jantzen, Representations of Algebraic Groups, II.1.
This advances Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, which asks for a pinning
(G, T, B, {X_α}) of the explicitly constructed Chevalley--Demazure group scheme; the torus T
acts by a character on each weight component, so a weight basis of the admissible lattice is what
has to exist before it can be written down. Layer 9 is consumed by milestone L0 of
TauCetiRoadmap/CFSGStatement/README.md.
The generators of the Chevalley lattice are weight vectors #
An element of the Cartan subalgebra is a joint eigenvector of the coroot operators of weight
zero: the Cartan subalgebra is abelian, so every ad α∨ annihilates it.
A coroot is a joint eigenvector of the coroot operators of weight zero, being an element of the Cartan subalgebra.
A root vector is a joint eigenvector of the coroot operators, of the integral weight
TauCeti.rootCartanWeight β.
The integral root--coroot span lies in the span of the integral joint weight spaces. Its generators are the root vectors and the coroots, and each of them is a joint eigenvector of the coroot operators with integer eigenvalues.
The weight basis of the Chevalley lattice #
The number of index values of TauCeti.UniversalEnvelopingAlgebra.kostantWeightBasis for the
integral root--coroot span of x against the coroot family. For a Chevalley system this is the
rank of that lattice, by TauCeti.IsChevalleySystem.rootCorootWeightBasisCard_eq_finrank; for an
arbitrary family x no such claim is made.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Chevalley lattice is stable under its Kostant form, in the shape
TauCeti.UniversalEnvelopingAlgebra.kostantWeightBasis consumes.
The Chevalley lattice is the internal direct sum of its weight sublattices. This is Humphreys' Lemma 27.1 for the adjoint admissible lattice: the decomposition itself is canonical, unlike the bases of the summands chosen below.
A weight basis of the Chevalley lattice. All three hypotheses of
TauCeti.UniversalEnvelopingAlgebra.kostantWeightBasis hold for the adjoint admissible lattice of a
Chevalley system, so it has a basis of joint eigenvectors of the coroot operators.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The defining equation of TauCeti.IsChevalleySystem.chevalleyWeightBasis: it is the Kostant
weight basis of the Chevalley lattice, so the whole kostantWeightBasis API applies to it.
The weight basis consists of weight vectors of the weights recorded by the first component of its index.
The weight basis of the Chevalley lattice, numbered by Fin: the shape in which the split
torus, the matrix coordinates and the generated group scheme read a basis.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The defining equation of TauCeti.IsChevalleySystem.chevalleyWeightBasisFin, through which
TauCeti.UniversalEnvelopingAlgebra.kostantWeightBasisFin_apply and the rest of the numbered-basis
API apply to it.
The weight carried by each vector of the numbered weight basis of the Chevalley lattice.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The defining equation of TauCeti.IsChevalleySystem.chevalleyWeightFin.
The numbered weight basis consists of weight vectors of the recorded weights. Together with
TauCeti.IsChevalleySystem.chevalleyWeightBasisFin this is the weight datum that the split torus of
the pinning takes as given.
The rank of the Chevalley lattice is the number of vectors of its weight basis.
The torus of coroot cocharacters on the points of the Chevalley lattice #
The diagonal coroot-parameter torus action on the Chevalley lattice. Over any commutative
ring A it acts on A ⊗[ℤ] L_ℤ, scaling the base-changed weight-basis vector b i by the value at
s of its character chevalleyWeightFin i.
The parameter is indexed by all weights of L rather than by the roots alone; at the zero weight
the coroot vanishes, and with it both the cocharacter
(TauCeti.corootFamily_eq_zero_of_isZero) and the weights of the generators
(TauCeti.rootCartanWeight_eq_zero_of_isZero). This is not yet the maximal torus of the Layer 9
pinning: exhibiting that needs a rank-ℓ cocharacter datum, equivalently the simply connected
lattice, which the adjoint lattice does not supply.
Equations
Instances For
The image of the diagonal coroot-parameter action in the general linear group.
Equations
- hx.chevalleyTorusSubgroup A = (hx.chevalleyTorusPoints A).range
Instances For
The Chevalley torus subgroup is the range of the torus-points homomorphism.
A torus point acts on a weight vector of the Chevalley lattice by the value of its
character. In particular the root vector x β is scaled by
torusCharacter s (rootCartanWeight β), that is by ∏ α, (s α) ^ (β α∨). This is the equation
that identifies the character by which the torus acts on each weight component.
A Chevalley torus point scales a base-changed weight-basis vector by its recorded character.
A Chevalley torus point scales a base-changed root-vector generator by its Cartan character.
Naturality of the Chevalley torus action in the value ring.
Scalar extension carries a Chevalley torus point to the point with mapped parameters.
The Chevalley torus action in the coordinates of its numbered weight basis.
Equations
Instances For
In the Chevalley weight basis, a torus point is diagonal with its weight characters.