Smoothness of the derived subgroup

Over an algebraically closed field, the derived closed subgroup of a reduced finite-type affine group is reduced, and hence smooth. This supplies the smooth subgroup needed when applying representation-theoretic induction to the derived subgroup of a solvable group.

More generally, the derived coordinate ring is reduced over any commutative base when the ambient tensor square and the tensor square of the reduced derived coordinate ring are reduced. Neither connectedness nor solvability is required for these results.

References

• J. S. Milne, Algebraic Groups (2017), §6d, for derived algebraic groups, and §1.f, for reduction of group schemes.
• W. C. Waterhouse, Introduction to Affine Group Schemes, §11.4.

theorem TauCeti.CommHopfAlgCat.isReduced_quotient_derivedDefiningIdeal_of_isReduced_tensorProduct {R : Type u} [CommRing R] (H : CommHopfAlgCat R) [IsReduced (TensorProduct R ↑H ↑H)] [IsReduced (TensorProduct R (↑(quotient H (derivedDefiningIdeal ↑H)) ⧸ nilradical ↑(quotient H (derivedDefiningIdeal ↑H))) (↑(quotient H (derivedDefiningIdeal ↑H)) ⧸ nilradical ↑(quotient H (derivedDefiningIdeal ↑H))))] : IsReduced ↑(quotient H (derivedDefiningIdeal ↑H))

The derived closed subgroup has reduced coordinate ring over a commutative base if the ambient tensor square and the tensor square of the reduced derived coordinate ring are reduced.

theorem TauCeti.CommHopfAlgCat.isReduced_quotient_derivedDefiningIdeal {k : Type u} [Field k] [IsAlgClosed k] (H : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] [IsReduced ↑H] : IsReduced ↑(quotient H (derivedDefiningIdeal ↑H))

The derived closed subgroup of a reduced finite-type affine group over an algebraically closed field has reduced coordinate ring.

theorem TauCeti.CommHopfAlgCat.smoothCommHopfAlgProperty_quotient_derivedDefiningIdeal {k : Type u} [Field k] [IsAlgClosed k] (H : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] [IsReduced ↑H] : smoothCommHopfAlgProperty k (quotient H (derivedDefiningIdeal ↑H))

The derived closed subgroup of a reduced finite-type affine group over an algebraically closed field is smooth.