Degeneration into the boundary of a projective orbit

Over an algebraically closed field, the orbit through a rational boundary point stays in the boundary of the original orbit, including at nonclosed points of the new orbit. Consequently such an orbit has strictly smaller closure. This is the descent step in the closed-orbit argument for projective representations of affine algebraic groups.

First, a closed subset invariant under rational group translations contains the full orbit image as soon as it contains the identity image. Density of rational points in the group promotes invariance on rational points to this assertion on the full spectrum. Applying it to the closed boundary gives orbit containment and strict containment of closures.

Neither connectedness nor smoothness nor reducedness of the group is required.

References

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

theorem TauCeti.Comodule.range_projectiveOrbitMap_subset_iff_of_isClosed {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) {Z : Set ↥(AlgebraicGeometry.Proj (SymmetricAlgebra.homogeneousSubmodule k (Module.Dual k M)))} (hZ : IsClosed Z) (hinvariant : ∀ (g : WithConv (H →ₐ[k] k)), Set.MapsTo (⇑(projectivePointTranslation g).hom) Z Z) : Set.range ⇑(projectiveOrbitMap m hm) ⊆ Z ↔ (projectiveOrbitMap m hm) (Bialgebra.counitAlgHom k H).kernelPoint ∈ Z

A closed subset invariant under rational projective translations contains the full orbit image exactly when it contains the image of the identity point.

theorem TauCeti.Comodule.closure_range_projectiveOrbitMap_subset_boundary {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) (n : M) (hn : Module.IsUnimodular k n) (hboundary : (projectiveOrbitMap n hn) (Bialgebra.counitAlgHom k H).kernelPoint ∈ closure (Set.range ⇑(projectiveOrbitMap m hm)) \ Set.range ⇑(projectiveOrbitMap m hm)) : closure (Set.range ⇑(projectiveOrbitMap n hn)) ⊆ closure (Set.range ⇑(projectiveOrbitMap m hm)) \ Set.range ⇑(projectiveOrbitMap m hm)

The closure of an orbit through a boundary point is contained in the boundary of the original orbit. Both orbits are the full images of scheme morphisms.

theorem TauCeti.Comodule.closure_range_projectiveOrbitMap_ssubset_of_mem_boundary {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) (n : M) (hn : Module.IsUnimodular k n) (hboundary : (projectiveOrbitMap n hn) (Bialgebra.counitAlgHom k H).kernelPoint ∈ closure (Set.range ⇑(projectiveOrbitMap m hm)) \ Set.range ⇑(projectiveOrbitMap m hm)) : closure (Set.range ⇑(projectiveOrbitMap n hn)) ⊂ closure (Set.range ⇑(projectiveOrbitMap m hm))

Passing to an orbit through the boundary strictly decreases the orbit closure. This strict inclusion supports Noetherian induction in the closed-orbit argument.