Joint weights of the commutator subgroup

For a reduced connected affine group of finite type over an algebraically closed field, every nonzero joint weight of the commutator subgroup in a finite-dimensional rational representation is trivial.

The ambient group preserves the joint weight space. On that space a commutator acts by a scalar whose power, with exponent the dimension of the weight space, is its determinant and hence one. Fixing one argument of the commutator makes that scalar a regular function on the connected group. Its image is finite, so it is constant and equal to one. This is the determinant step in the Lie--Kolchin induction; no characteristic-zero hypothesis is needed.

References

• A. Borel, Linear Algebraic Groups, §10.5.
• J. E. Humphreys, Linear Algebraic Groups, §17.6.

@[simp]

theorem TauCeti.Comodule.nonzeroJointWeight_commutator_eq_one {k : Type u_1} {H : Type u_2} {V : Type u_3} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] [AddCommGroup V] [Module k V] [Comodule k H V] [FiniteDimensional k V] (χ : NonzeroJointWeight (commutator (WithConv (H →ₐ[k] k))) (basePointsRepresentation V)) : ↑χ = 1

Every character of the commutator subgroup having a nonzero joint weight space in a finite-dimensional rational representation of a reduced connected affine group is trivial.