Projective orbit images are locally closed

The full topological image of a finite-type affine group's projective orbit morphism is locally closed over an algebraically closed field. This includes its nonclosed points; it is not a statement only about the orbit of rational points. Neither smoothness nor reducedness of the group is required.

This supplies the locally closed subset on which to construct the orbit scheme, a geometric model for the homogeneous space of the stabilizer of the chosen line. It does not identify scheme-theoretic fibers or prove flatness or representability of a quotient sheaf.

The argument combines isConstructible_range_projectiveOrbitMap, range_projectiveOrbitMap_kernelPoint_eq_range_inter_closedPoints, translation invariance, and isLocallyClosed_of_isConstructible_of_closedPoints_transitive. Rational translations are transitive on the closed points of the image, even though they need not be transitive on all its points.

References

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

theorem TauCeti.Comodule.exists_smul_eq_of_mem_range_projectiveOrbitMap_inter_closedPoints {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] (m : M) (hm : Module.IsUnimodular k m) {x y : ↥(AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule k (Module.Dual k M)))} (hx : x ∈ Set.range ⇑(projectiveOrbitMap m hm) ∩ closedPoints ↥(AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule k (Module.Dual k M)))) (hy : y ∈ Set.range ⇑(projectiveOrbitMap m hm) ∩ closedPoints ↥(AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule k (Module.Dual k M)))) : ∃ (g : WithConv (H →ₐ[k] k)), g • x = y

Rational translations are transitive on the closed points of the full projective orbit image.

theorem TauCeti.Comodule.isLocallyClosed_range_projectiveOrbitMap {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] (m : M) (hm : Module.IsUnimodular k m) : IsLocallyClosed (Set.range ⇑(projectiveOrbitMap m hm))

The entire topological image of a finite-type affine group's projective orbit morphism is locally closed over an algebraically closed field, including for nonreduced groups.