Integral adjoint root lines of the special linear group

The diagonal torus of SL_{r+1} acts on its tangent Lie algebra by conjugation. Over any commutative base ring, its root character ε_i - ε_j has exactly the matrix-unit line R E_ij as its eigenspace. The assertion uses the universal torus point over its coordinate ring, rather than just rational points: distinct characters remain distinguishable in small characteristic and over nonreduced rings.

adDerivation_universalDiagonalTorus_eq_iff characterizes every character's eigenspace by vanishing of matrix entries of the wrong weight. adDerivation_universalDiagonalTorus_root_iff identifies each root eigenspace with the span of the normalized matrix unit in the existing tangent-matrix equivalence. In particular, this supplies the integral root-line calculation needed to normalize root vectors in a pinning.

References

• J. S. Milne, Algebraic Groups (2017), §21.1 and Example 21.2.
• B. Conrad, Reductive Group Schemes, §5.1 (root spaces and pinnings).
• The entrywise character comparison follows TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Adjoint.Classification, here applied to the tangent Lie functor over arbitrary commutative rings.

theorem TauCeti.SpecialLinear.adDerivation_universalDiagonalTorus_eq_iff {R : Type u} [CommRing R] {r : ℕ} (α : Multiplicative (ULift.{u, 0} (Fin r) →₀ ℤ)) (d : Derivation R (↑(coordinateHopfAlgebra R (r + 1))) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R (r + 1))) R)) : Derivation.adDerivation (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin r) →₀ ℤ))) ((Bialgebra.CounitAlgebra.pointsMulEquiv R (↑(coordinateHopfAlgebra R (r + 1))) (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin r) →₀ ℤ)))).symm ((diagonalTorusPoints r R (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin r) →₀ ℤ)))) (WithConv.toConv (AlgHom.id R (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin r) →₀ ℤ))))))) ((Derivation.mapValue (Algebra.ofId R (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin r) →₀ ℤ))))) d) = MonoidAlgebra.single α 1 • (Derivation.mapValue (Algebra.ofId R (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin r) →₀ ℤ))))) d ↔ ∀ (i j : Fin (r + 1)), SplitTorus.weightCharacter (diagonalTorusWeight r i - diagonalTorusWeight r j) ≠ α → ↑((tangentMatrix (r + 1)) d) i j = 0

A tangent vector transforms by the character α of the diagonal torus exactly when all its entries of a different character vanish. The action is tested at the universal torus point, after extending the coefficients to the torus coordinate algebra.

@[simp]

theorem TauCeti.SpecialLinear.adDerivation_universalDiagonalTorus_root_iff {R : Type u} [CommRing R] {r : ℕ} (p : SplitTorus.CoordinateRootIndex (Fin (r + 1))) (d : Derivation R (↑(coordinateHopfAlgebra R (r + 1))) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R (r + 1))) R)) : Derivation.adDerivation (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin r) →₀ ℤ))) ((Bialgebra.CounitAlgebra.pointsMulEquiv R (↑(coordinateHopfAlgebra R (r + 1))) (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin r) →₀ ℤ)))).symm ((diagonalTorusPoints r R (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin r) →₀ ℤ)))) (WithConv.toConv (AlgHom.id R (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin r) →₀ ℤ))))))) ((Derivation.mapValue (Algebra.ofId R (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin r) →₀ ℤ))))) d) = MonoidAlgebra.single (Multiplicative.ofAdd ((diagonalRootDatum r).root p)) 1 • (Derivation.mapValue (Algebra.ofId R (MonoidAlgebra R (Multiplicative (ULift.{u, 0} (Fin r) →₀ ℤ))))) d ↔ (tangentMatrix (r + 1)) d ∈ R ∙ (LieAlgebra.SpecialLinear.single (↑p).1 (↑p).2 ⋯) 1

The adjoint eigenspace of every root of SL_{r+1} over any commutative base ring is exactly the line spanned by its normalized matrix unit. The tangent-matrix equivalence identifies this with a line in the tangent Lie algebra of the group scheme.