Faithfully flat projective orbit morphisms

For a reduced finite-type affine group over an algebraically closed field, the morphism onto the projective orbit scheme of a line is flat. Together with its existing surjectivity and local finite presentation, this makes it an fppf cover, the cover needed to descend morphisms to the homogeneous space of the line stabilizer.

Generic flatness supplies a dense open subset of the orbit over which the morphism is flat. Rational group translations preserve the scheme morphism and move any closed orbit point to any other. Their translates of the flat open cover the Jacobson orbit scheme, so flatness holds at every stalk, including nonclosed points. No connectedness or characteristic-zero assumption is needed. Reducedness is used to apply generic flatness to the orbit scheme.

The proof combines Comodule.exists_projectiveOrbitTranslation_eq_of_mem_closedPoints and Scheme.Hom.flat_of_transitive_closedPoints_of_finiteType.

References

• J. S. Milne, Algebraic Groups (2017), §§7.c–7.f, orbits and homogeneous spaces.

instance TauCeti.Comodule.instFlatToProjectiveOrbit {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) : AlgebraicGeometry.Flat (toProjectiveOrbit m hm)

The surjective morphism from a reduced finite-type affine group onto the projective orbit scheme of a line is flat. In particular, it is an fppf cover.