Solvability of normal products

Let I and J cut out smooth solvable closed subgroups of an 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 smooth and has solvable geometric points. Its coordinate map from the multiplication image is injective, so solvability descends by the derived-word identity criterion for schematically dense morphisms. No faithful-flatness hypothesis on the source-to-image morphism is needed.

Main declaration

• TauCeti.geometricallySolvablePointsCommHopfAlgProperty.productOfNormal: the multiplication image of two smooth solvable subgroups has solvable geometric points.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 6.42 and Sections 5.a, 6.a.
• J. C. Jantzen, Representations of Algebraic Groups, I.2.

This supplies the geometric-solvability part of binary-product closure for connected normal smooth solvable closed subgroups in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap.

theorem TauCeti.geometricallySolvablePointsCommHopfAlgProperty.productOfNormal {k : Type u} [Field k] (H : CommHopfAlgCat k) (I J : HopfIdeal k ↑H) (hI : I.IsNormal) (hIs : smoothCommHopfAlgProperty k (CommHopfAlgCat.quotient H I)) (hJs : smoothCommHopfAlgProperty k (CommHopfAlgCat.quotient H J)) (hIsolv : geometricallySolvablePointsCommHopfAlgProperty k (CommHopfAlgCat.quotient H I)) (hJsolv : geometricallySolvablePointsCommHopfAlgProperty k (CommHopfAlgCat.quotient H J)) : geometricallySolvablePointsCommHopfAlgProperty k (CommHopfAlgCat.productOfNormal H I J hI)

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

The conjugation semidirect-product source is smooth and solvable. The canonical coordinate map from the image into that source is injective, so the derived-word identity for solvability descends to the image.