Finite generation of normal coinvariants

For a normal closed subgroup of a geometrically reduced finite-type affine group over a field, the invariant functions form a finite-type Hopf algebra. The corresponding affine quotient projection is faithfully flat and finitely presented. The subgroup may be nonreduced, and the field need not be perfect.

These statements concern the actual coinvariant algebra, rather than a chosen finite-type subalgebra of it. Identifying the kernel of this projection with the original normal subgroup is a separate assertion, required to identify the quotient with the fppf quotient by that subgroup.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §16.3.
• J. S. Milne, Algebraic Groups (2017), §5.c.

theorem TauCeti.HopfIdeal.IsNormal.finiteType_coinvariants {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] [Algebra.IsGeometricallyReduced k ↑H] {I : HopfIdeal k ↑H} (hI : I.IsNormal) : Algebra.FiniteType k ↥I.coinvariants

The coinvariants of a normal closed subgroup of a geometrically reduced finite-type affine group over a field are finitely generated as an algebra. The subgroup need not be smooth.

theorem TauCeti.CommHopfAlgCat.faithfullyFlat_coinvariantsι {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] [Algebra.IsGeometricallyReduced k ↑H] {I : HopfIdeal k ↑H} (hI : I.IsNormal) : (↑(CommHopfAlgCat.Hom.hom (coinvariantsι hI))).FaithfullyFlat

The affine quotient projection defined by normal coinvariants is faithfully flat when the ambient finite-type affine group is geometrically reduced, over any field.

theorem TauCeti.CommHopfAlgCat.finitePresentation_coinvariantsι {k : Type u} [Field k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] [Algebra.IsGeometricallyReduced k ↑H] {I : HopfIdeal k ↑H} (hI : I.IsNormal) : (↑(CommHopfAlgCat.Hom.hom (coinvariantsι hI))).FinitePresentation

The normal affine quotient projection is finitely presented.