Detecting unipotent points in a faithful representation

The definition of a unipotent point of an affine group quantifies over every finite-dimensional representation. This file proves the usable faithful-representation criterion over a perfect value field: if one finite-dimensional comodule defines a closed immersion into a general linear group, then a point is unipotent exactly when it acts unipotently on that comodule.

The substantive direction uses the Jordan decomposition of the point. If its action in the faithful comodule is unipotent, its semisimple part acts trivially there. The same is true on the inverse point, so the semisimple part agrees with the identity both on the matrix coefficients and on their antipode images. Faithfulness says that these two coefficient algebras generate the whole coordinate Hopf algebra; hence the semisimple part is the identity, which characterizes a unipotent point.

This is the bridge needed by Layer 5, "Unipotent groups", of the ReductiveGroups roadmap: a point of a group given with a faithful representation can now be tested for unipotence in that one representation instead of in every representation. The upper-unitriangular embedding characterization is still to come.

Main declaration

• TauCeti.HopfAlgebra.isUnipotentPoint_iff_isUnipotent_pointsAction_of_isFaithful: a faithful finite-dimensional representation detects unipotence of points over a perfect value field.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, §2.4.

theorem TauCeti.HopfAlgebra.isUnipotentPoint_iff_isUnipotent_pointsAction_of_isFaithful {k H K : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (M : FGComoduleCat k H) (hM : Comodule.IsFaithful) (g : WithConv (H →ₐ[k] K)) : IsUnipotentPoint g ↔ (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) g)).IsUnipotent

Over a perfect value field, a faithful finite-dimensional representation detects unipotent points.

The forward implication is the defining universal property of a unipotent point. For the converse, faithfulness ensures that the comodule's matrix coefficients and their antipode images generate the coordinate Hopf algebra, so triviality of the semisimple part on this one comodule forces triviality of the semisimple part as a point.