Geometric unipotence under base change

Let H be the coordinate Hopf algebra of a smooth unipotent affine group over a field k. For every field extension K / k, the scalar extension K ⊗[k] H is again smooth unipotent.

Choose a faithful finite-dimensional H-comodule and extend it to K. Its coordinate morphism remains surjective, hence the extended comodule is faithful. The universal coefficient matrix of the extended comodule is obtained from the original one by scalar extension. Its characteristic polynomial therefore remains a power of X - 1, and the faithful-representation criterion detects unipotence of every geometric point of the base-changed group.

Main declaration

• TauCeti.smoothUnipotentCommHopfAlgProperty.baseChange: smooth geometric unipotence is preserved by arbitrary field extension.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 14.5.
• A. Borel, Linear Algebraic Groups, Section 15.4.

This supplies scalar-extension preservation for the unipotent radical in Layer 5 of the ReductiveGroups roadmap.

theorem TauCeti.smoothUnipotentCommHopfAlgProperty.baseChange {k K : Type u} [Field k] [Field K] [Algebra k K] (H : FiniteTypeCommHopfAlgCat k) (hH : smoothUnipotentCommHopfAlgProperty k H) : smoothUnipotentCommHopfAlgProperty K H.baseChange

Smooth geometric unipotence is preserved by arbitrary extension of the ground field.