Solvability of semidirect products of affine groups

An internal action of affine groups equips the product of their underlying affine schemes with a semidirect-product group law. This file proves that the resulting affine group has solvable geometric points when both factors do.

On points over an algebraic closure, the internal semidirect product is the ordinary semidirect product of the two point groups. Its normal-factor inclusion and projection onto the acting factor form an extension, so Mathlib's extension closure for solvable groups applies. The result is also stated for the named conjugation semidirect product used to form the scheme-theoretic product of a normal closed subgroup with another closed subgroup.

Main declarations

• TauCeti.geometricallySolvablePointsCommHopfAlgProperty.semidirectProduct: internal semidirect products preserve solvability of geometric points.
• TauCeti.geometricallySolvablePointsCommHopfAlgProperty.normalSemidirectProduct: the conjugation semidirect-product source attached to two closed subgroups has solvable geometric points when both subgroups do.

References

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

This supplies the source-side extension step for the solvable radical in Layer 6 of the ReductiveGroups roadmap. To prove that the scheme-theoretic multiplication image is again solvable, it remains to descend solvability from this source to its image.

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

An internal semidirect product of affine groups with solvable geometric point groups again has a solvable geometric point group.

theorem TauCeti.geometricallySolvablePointsCommHopfAlgProperty.normalSemidirectProduct (k : Type u) [Field k] (H : CommHopfAlgCat k) (I J : HopfIdeal k ↑H) (hI : I.IsNormal) (hIs : geometricallySolvablePointsCommHopfAlgProperty k (CommHopfAlgCat.quotient H I)) (hJs : geometricallySolvablePointsCommHopfAlgProperty k (CommHopfAlgCat.quotient H J)) : geometricallySolvablePointsCommHopfAlgProperty k (CommHopfAlgCat.normalSemidirectProduct H I J hI)

The conjugation semidirect-product source associated to a normal closed subgroup and another closed subgroup has solvable geometric points when the two subgroup point groups are solvable.