Smoothness of the identity component

The identity component of a smooth affine group of finite type over an algebraically closed field is smooth. Its coordinate algebra is the localization at the idempotent selecting the identity component. This supplies smooth connected subgroups to which radical and semisimplicity criteria apply.

instance TauCeti.FiniteTypeCommHopfAlgCat.smooth_identityComponent {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) [Algebra.Smooth k ↑H.obj] : Algebra.Smooth k ↑H.identityComponent.obj

The identity component of a smooth finite-type affine group is smooth.