Fppf-local lifts of projective orbit points

For a reduced finite-type affine group over an algebraically closed field, every algebra-valued point of a projective orbit lifts to a group point after one faithfully flat, finitely presented extension of the value algebra. No reducedness assumption is made on the value algebra. Thus the geometric orbit map supplies the local lifts needed to identify the orbit with the fppf homogeneous quotient by the line stabilizer.

The orbit map is affine because its source is affine and its target is separated. Combine its flatness with Scheme.Hom.exists_faithfullyFlat_lift; the compatibility of the orbit map with the base field lets Mathlib's Spec.mapMulEquiv recover an algebra-valued group point from the lifted scheme morphism.

References

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

theorem TauCeti.Comodule.exists_faithfullyFlat_lift_toProjectiveOrbit {k H M : Type u} [Field k] [IsAlgClosed k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [AddCommGroup M] [Module k M] [Comodule k H M] [Module.Finite k M] [IsReduced H] (m : M) (hm : Module.IsUnimodular k m) (A : CommAlgCat k) (y : AlgebraicGeometry.Spec ↧↑A ⟶ projectiveOrbitScheme m hm) (hy : CategoryTheory.CategoryStruct.comp y (projectiveOrbitToSpec m hm) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap k ↑A))) : ∃ (B : CommAlgCat k) (φ : A ⟶ B) (g : WithConv (H →ₐ[k] ↑B)), (CommAlgCat.Hom.hom φ).FaithfullyFlat ∧ (CommAlgCat.Hom.hom φ).FinitePresentation ∧ CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom g.ofConv.toRingHom)) (toProjectiveOrbit m hm) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (CommAlgCat.Hom.hom φ).toRingHom)) y

Every algebra-valued point of the projective orbit lifts to a group point after a faithfully flat, finitely presented extension of the value algebra. The value algebra may be nonreduced, and no global lift over it is asserted.