Unipotent points and algebraic characters

A group-like element of a coordinate Hopf algebra is the coordinate-ring incarnation of an algebraic character. Its associated rank-one comodule lets a point act by evaluation at that group-like element. Consequently a unipotent point valued in a reduced ring evaluates every algebraic character at one: the difference between that scalar action and the identity is nilpotent, so the scalar itself must be one.

This is the pointwise representation-theoretic input to the theorem that a connected unipotent group has no nontrivial characters. Promoting the pointwise conclusion to equality of characters requires the separate fact that algebraic-closure-valued points separate functions on a smooth finite-type affine group.

Main declaration

• TauCeti.HopfAlgebra.IsUnipotentPoint.apply_groupLike_eq_one: a unipotent point evaluates every group-like element at one.

References

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

This advances Layer 5, "Unipotent groups", of the ReductiveGroups roadmap, specifically the consequence that connected unipotent groups have no nontrivial characters.

@[simp]

theorem TauCeti.HopfAlgebra.IsUnipotentPoint.apply_groupLike_eq_one {F : Type u} {C : Type v} {L : Type w} [CommSemiring F] [Semiring C] [HopfAlgebra F C] [CommRing L] [IsReduced L] [Algebra F L] {g : WithConv (C →ₐ[F] L)} (hg : IsUnipotentPoint g) (x : GroupLike F C) : g.ofConv ↑x = 1

A unipotent point evaluates every group-like element of the coordinate Hopf algebra at one.

Group-like elements are the coordinate-ring incarnation of algebraic characters. The associated rank-one comodule turns evaluation at the group-like element into a scalar point action.