The derived subgroup of a connected solvable group is unipotent

Over an algebraically closed field, the derived closed subgroup of a reduced connected solvable affine group of finite type is smooth, connected, and unipotent. Consequently it lies in the unipotent radical. No characteristic restriction is imposed.

Lie--Kolchin triangularizes every ambient representation. Its diagonal entries are characters, which restrict to one on the derived subgroup; hence every derived point acts by an upper unitriangular matrix. Reflection of unipotence along closed immersions then gives intrinsic unipotence of the derived subgroup, rather than just unipotence in ambient representations.

References

• A. Borel, Linear Algebraic Groups, §10.5.
• J. S. Milne, Algebraic Groups (2017), §§6d and 16.

theorem TauCeti.CommHopfAlgCat.isUnipotentPoint_derived_of_isSolvable {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))] (g : WithConv (H ⧸ (derivedDefiningIdeal H).toIdeal →ₐ[k] k)) : HopfAlgebra.IsUnipotentPoint g

Every rational point of the derived subgroup of a reduced connected solvable affine group over an algebraically closed field is unipotent.

theorem TauCeti.CommHopfAlgCat.geometricallyUnipotentPointsCommHopfAlgProperty_derived_of_isSolvable {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 (derivedDefiningIdeal H))

The derived subgroup of a reduced connected solvable affine group over an algebraically closed field is geometrically unipotent.

theorem TauCeti.CommHopfAlgCat.isUnipotentRadicalCandidate_derived_of_isSolvable {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))] : HopfIdeal.IsUnipotentRadicalCandidate (FiniteTypeCommHopfAlgCat.of k H) (derivedDefiningIdeal H)

The derived subgroup of a reduced connected solvable affine group is a connected normal smooth unipotent subgroup, so it is a candidate for its unipotent radical.

theorem TauCeti.CommHopfAlgCat.unipotentRadicalDefiningIdeal_le_derivedDefiningIdeal_of_isSolvable {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))] : (FiniteTypeCommHopfAlgCat.of k H).unipotentRadicalDefiningIdeal ≤ derivedDefiningIdeal H

The unipotent radical of a reduced connected solvable affine group over an algebraically closed field contains its derived subgroup. The inclusion reverses on defining Hopf ideals.