Generic flatness of projective orbit morphisms

For a reduced finite-type affine group over an algebraically closed field, the morphism onto the projective orbit of a line is flat over a dense open of the orbit scheme. Its restrictions are already surjective and locally of finite presentation, so this gives an fppf cover over that open. The flatness statement concerns all scheme points, rather than only rational points or reduced fibres.

This supplies the initial open set for the translation argument proving faithful flatness of the whole orbit morphism. The reducedness assumption makes the orbit scheme reduced, as required by generic flatness; no connectedness or characteristic assumption is imposed.

The application uses Scheme.Hom.exists_dense_open_flat and the locally closed scheme-theoretic image construction Comodule.projectiveOrbitScheme.

References

• J. S. Milne, Algebraic Groups (2017), §§7.c–7.f, orbits and homogeneous spaces.
• The Stacks Project, Tag 0529, generic flatness.

theorem TauCeti.Comodule.exists_dense_open_flat_toProjectiveOrbit {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] (m : M) (hm : Module.IsUnimodular k m) : ∃ (U : (projectiveOrbitScheme m hm).Opens), Dense ↑U ∧ AlgebraicGeometry.Flat (toProjectiveOrbit m hm ∣_ U)

The morphism onto the projective orbit scheme of a reduced finite-type affine group is flat over a dense open subset of the orbit scheme.