Unipotence of normal products

Let I and J cut out smooth unipotent closed subgroups of a finite-type affine group, with I normal. Multiplication is a homomorphism from their conjugation semidirect product into the ambient group, and CommHopfAlgCat.productOfNormal is its scheme-theoretic image.

The semidirect-product source is again smooth unipotent. In particular, its coordinate algebra is reduced. The coordinate algebra of the multiplication image embeds in that reduced algebra, so every geometric point of the image is unipotent. This avoids any appeal to faithful flatness of the source-to-image morphism.

Together with connectedness and smoothness of the multiplication image, this is the remaining geometric input for binary-product closure of unipotent-radical candidates. Containment and normality of the image are supplied by the normal-product API.

Main declarations

• TauCeti.smoothUnipotentCommHopfAlgProperty.normalSemidirectProduct: the named normal semidirect product of two smooth unipotent groups is smooth unipotent.
• TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.productOfNormal: the multiplication image of two smooth unipotent subgroups has geometrically unipotent points.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 6.42 and Sections 5.a, 6.a.
• A. Borel, Linear Algebraic Groups, Proposition 14.4 and Section 11.21.

This advances Layer 5, "The unipotent radical", of the ReductiveGroups roadmap by supplying the geometric-unipotence part of binary-product closure for connected normal smooth unipotent closed subgroups.

theorem TauCeti.smoothUnipotentCommHopfAlgProperty.normalSemidirectProduct {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) (I J : HopfIdeal k ↑H.obj) (hI : I.IsNormal) (hIu : smoothUnipotentCommHopfAlgProperty k (H.quotient I)) (hJu : smoothUnipotentCommHopfAlgProperty k (H.quotient J)) : smoothUnipotentCommHopfAlgProperty k (FiniteTypeCommHopfAlgCat.of k ↑(CommHopfAlgCat.normalSemidirectProduct H.obj I J hI))

The named normal semidirect product of two smooth unipotent closed subgroups is smooth unipotent.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.productOfNormal {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) (I J : HopfIdeal k ↑H.obj) (hI : I.IsNormal) (hIu : smoothUnipotentCommHopfAlgProperty k (H.quotient I)) (hJu : smoothUnipotentCommHopfAlgProperty k (H.quotient J)) : geometricallyUnipotentPointsCommHopfAlgProperty k (CommHopfAlgCat.productOfNormal H.obj I J hI)

The scheme-theoretic multiplication image of two smooth unipotent closed subgroups has geometrically unipotent points when the first subgroup is normal.

The semidirect-product source is smooth unipotent, hence reduced. Unipotence then descends to its scheme-theoretic image through the canonical embedding of coordinate algebras.