Smooth unipotence of semidirect products

An internal action of affine groups equips the product of their underlying affine schemes with the semidirect-product group law. This file proves that if both factors are geometrically unipotent, then so is the semidirect product, and consequently that semidirect products of smooth unipotent affine groups are smooth unipotent.

The pointwise argument works in an arbitrary finite-dimensional representation of the semidirect product. The images of the two factors act unipotently by restriction. The first factor is normal, and the two factor images generate the whole semidirect product, so the normal-join theorem makes every element act unipotently. Smoothness depends only on the underlying algebra, which is the tensor product of the coordinate algebras.

Main declarations

• TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.semidirectProduct: internal semidirect products preserve geometric-point unipotence.
• TauCeti.smoothUnipotentCommHopfAlgProperty.semidirectProduct: internal semidirect products of smooth unipotent affine groups are smooth unipotent.

References

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

This supplies the smooth-unipotence step in Layer 5, "The unipotent radical", of the ReductiveGroups roadmap. The binary product of two radical candidates is formed as the image of multiplication from their conjugation semidirect product; the source must first be known to be smooth unipotent.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.semidirectProduct (k : Type u) [Field k] (H K : CommHopfAlgCat k) (A : GrpObj.Action (CommHopfAlgCat.grpObj K) (CommHopfAlgCat.grpObj H)) (hH : geometricallyUnipotentPointsCommHopfAlgProperty k H) (hK : geometricallyUnipotentPointsCommHopfAlgProperty k K) : geometricallyUnipotentPointsCommHopfAlgProperty k A.coordinateHopfAlgebra

An internal semidirect product of affine groups with geometrically unipotent points again has geometrically unipotent points.

theorem TauCeti.smoothUnipotentCommHopfAlgProperty.semidirectProduct (k : Type u) [Field k] (H K : FiniteTypeCommHopfAlgCat k) (A : GrpObj.Action (CommHopfAlgCat.grpObj K.obj) (CommHopfAlgCat.grpObj H.obj)) (hH : smoothUnipotentCommHopfAlgProperty k H) (hK : smoothUnipotentCommHopfAlgProperty k K) : smoothUnipotentCommHopfAlgProperty k (FiniteTypeCommHopfAlgCat.of k ↑A.coordinateHopfAlgebra)

An internal semidirect product of smooth unipotent finite-type affine groups is smooth unipotent.