Connectedness of the derived subgroup

The derived closed subgroup of a connected affine group of finite type over an algebraically closed field is geometrically connected. Neither smoothness nor reducedness is needed. This supplies the connectedness input for induction on the derived series in Lie--Kolchin.

The commutator morphism factors through the derived subgroup. Each slice obtained by fixing one argument is connected and contains the identity, so its image lies in the identity component of that subgroup. The defining universal property of the derived subgroup then forces that identity component to be the whole subgroup.

References

• J. S. Milne, Algebraic Groups (2017), §6d, for derived subgroups, and §2.a, for components.
• The identity-component construction used here is TauCeti.HopfAlgebra.identityComponentHopfIdeal.

theorem TauCeti.CommHopfAlgCat.connectedSpace_derived {k : Type u} [Field k] [IsAlgClosed k] (H : Type v) [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [ConnectedSpace (PrimeSpectrum H)] : ConnectedSpace (PrimeSpectrum (H ⧸ (derivedDefiningIdeal H).toIdeal))

The derived subgroup of a connected finite-type affine group over an algebraically closed field has connected spectrum. Smoothness and reducedness are not required.

theorem TauCeti.CommHopfAlgCat.geometricallyConnectedCommHopfAlgProperty_derived {k : Type u} [Field k] [IsAlgClosed k] (H : Type v) [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [ConnectedSpace (PrimeSpectrum H)] : geometricallyConnectedCommHopfAlgProperty k (quotient (↧H) (derivedDefiningIdeal H))

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

instance TauCeti.CommHopfAlgCat.geometricallyConnected_derivedGroupScheme {k : Type u} [Field k] [IsAlgClosed k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] [ConnectedSpace (PrimeSpectrum ↑H)] : AlgebraicGeometry.GeometricallyConnected (derivedGroupScheme H).X.hom

The structural morphism of the derived group scheme of a connected finite-type affine group over an algebraically closed field is geometrically connected.