Closed points of a projective orbit image

Over an algebraically closed field, every closed point in the full image of a finite-type affine group's projective orbit morphism is the image of a rational group point. Conversely, all rational orbit images are closed. The existing rational-fiber characterization therefore describes every closed point of the image, rather than only a possibly smaller rational subset.

This is the closed-point lifting input for realizing homogeneous spaces as locally closed projective orbits. The full image may also include nonclosed points. No smoothness or reducedness hypothesis is imposed on the group.

The comparison uses range_kernelPoint_eq_closedPoints and the closed-point image theorem for locally finite-type morphisms. Together with projectiveOrbitMap_kernelPoint_eq_iff_span_eq, it identifies closed orbit images with the lines through translated vectors.

References

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

theorem TauCeti.Comodule.range_projectiveOrbitMap_kernelPoint_eq_range_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) : (Set.range fun (g : WithConv (H →ₐ[k] k)) => (projectiveOrbitMap m hm) (AlgHom.kernelPoint g.ofConv)) = Set.range ⇑(projectiveOrbitMap m hm) ∩ closedPoints ↥(AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule k (Module.Dual k M)))

Rational orbit images are exactly the closed points in the full topological image of the projective orbit morphism.