Smooth generated subgroups over perfect fields #
A finite-type closed subgroup generated by reduced affine group schemes over a perfect field is smooth over that field.
This concerns the generated subgroup over the original perfect field. Smoothness therefore persists on the scalar extension of that same subgroup, independently of whether its scalar extension is generated by the extended family.
References #
- W. C. Waterhouse, Introduction to Affine Group Schemes, §11.4.
- J. S. Milne, Algebraic Groups (2017), Proposition 1.26 and Corollary 1.27.
theorem
TauCeti.CommHopfAlgCat.smoothCommHopfAlgProperty_quotient_commonKernelHopfIdeal_of_perfectField
{k : Type u}
[Field k]
[PerfectField k]
{H : CommHopfAlgCat k}
{ι : Type w}
{K : ι → CommHopfAlgCat k}
(f : (i : ι) → H ⟶ K i)
[∀ (i : ι), IsReduced ↑(K i)]
[Algebra.FiniteType k ↑(quotient H (commonKernelHopfIdeal f))]
:
A finite-type subgroup generated by reduced affine group schemes over a perfect field is smooth. The generator algebras need not be finitely generated.