The character kernel of a connected solvable group is unipotent

Over an algebraically closed field, a point of a reduced connected solvable affine group of finite type is unipotent precisely when every algebraic character evaluates to one. Thus the common kernel of characters has geometrically unipotent points. No smoothness or reducedness of that kernel is assumed.

Lie--Kolchin makes every representation upper triangular with characters on the diagonal; trivial character values make its point action upper unitriangular. The triangular argument is shared with CommHopfAlgCat.isUnipotentPoint_derived_of_isSolvable. The kernel identifies the unipotent obstruction to detecting a connected solvable group by its characters.

References

• A. Borel, Linear Algebraic Groups, §10.
• T. A. Springer, Linear Algebraic Groups, §6.3.

theorem TauCeti.HopfAlgebra.isUnipotentPoint_iff_forall_apply_groupLike_eq_one {k : Type u} {H : Type v} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] [Group.IsSolvable (WithConv (H →ₐ[k] k))] {K : Type w} [CommRing K] [IsReduced K] [Algebra k K] (g : WithConv (H →ₐ[k] K)) : IsUnipotentPoint g ↔ ∀ (x : GroupLike k H), g.ofConv ↑x = 1

In a reduced connected solvable affine group over an algebraically closed field, a point valued in any reduced commutative algebra is unipotent exactly when every algebraic character has value one.

theorem TauCeti.CommHopfAlgCat.geometricallyUnipotentPointsCommHopfAlgProperty_characterKernelIdeal {k H : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] [ConnectedSpace (PrimeSpectrum H)] [Group.IsSolvable (WithConv (H →ₐ[k] k))] : geometricallyUnipotentPointsCommHopfAlgProperty k ((↧H).quotient (↧H).characterKernelIdeal)

Every geometric point of the common kernel of characters of a reduced connected solvable affine group is unipotent. The kernel may be nonreduced.