Entrywise classification of special-linear adjoint weights #
A nonzero matrix entry of an adjoint weight vector of SL_{r+1} determines its
character as the difference of the corresponding diagonal torus weights. This
entrywise criterion holds over every commutative base ring and supplies the
classification of the full root set in
TauCeti.Algebra.AlgebraicGroup.SpecialLinear.Root.Adjoint.
Weight membership is tested by the torus coaction, so it retains information that rational points alone may lose over rings with nilpotents or in positive characteristic.
References #
- J. S. Milne, Algebraic Groups (2017), §21.1 and Example 21.2.
- B. Conrad, Reductive Group Schemes (2014), §5.1.
- The entrywise argument follows
TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Adjoint.Classification.
theorem
TauCeti.SpecialLinear.weightCharacter_eq_of_mem_adjointWeightSpace_of_apply_ne_zero
{R : Type u}
[CommRing R]
{r : ℕ}
{α : Multiplicative (ULift.{u, 0} (Fin r) →₀ ℤ)}
{x : Module.Dual R (Bialgebra.CotangentSpace R ↑(coordinateHopfAlgebra R (r + 1)))}
(hx : x ∈ Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom (diagonalTorusCoordinateMap r R)) α)
{i j : Fin (r + 1)}
(hentry : ↑((tangentMatrix (r + 1)) (Derivation.cotangentLinearEquiv x)) i j ≠ 0)
:
A nonzero entry of an adjoint weight vector determines its character, over any commutative base ring.