Closed-point homogeneity of projective orbit schemes

Every closed point of the projective orbit scheme lifts to a rational group point. Rational group translations therefore act transitively on its closed points, through automorphisms of the full scheme-theoretic orbit image. This is the homogeneity input for transporting flatness of the orbit morphism from a nonempty open to the whole orbit.

The group need not be reduced or smooth. Transitivity is asserted on closed points; rational translations need not act transitively on all scheme points.

The results use Scheme.Hom.image_closedPoints_eq_range_inter_closedPoints, range_kernelPoint_eq_closedPoints, and Comodule.projectiveOrbitTranslation.

References

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

theorem TauCeti.Comodule.range_toProjectiveOrbit_kernelPoint_eq_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)) => (toProjectiveOrbit m hm) (AlgHom.kernelPoint g.ofConv)) = closedPoints ↥(projectiveOrbitScheme m hm)

The rational group points map onto exactly the closed points of the orbit scheme.

@[simp]

theorem TauCeti.Comodule.projectiveOrbitTranslation_toProjectiveOrbit_kernelPoint {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) (g h : WithConv (H →ₐ[k] k)) : (projectiveOrbitTranslation m hm g).hom ((toProjectiveOrbit m hm) (AlgHom.kernelPoint h.ofConv)) = (toProjectiveOrbit m hm) (AlgHom.kernelPoint (g * h).ofConv)

On rational orbit images, orbit translation is left multiplication of group points.

theorem TauCeti.Comodule.exists_projectiveOrbitTranslation_eq_of_mem_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 : ↥(projectiveOrbitScheme m hm)} (hx : x ∈ closedPoints ↥(projectiveOrbitScheme m hm)) (hy : y ∈ closedPoints ↥(projectiveOrbitScheme m hm)) : ∃ (g : WithConv (H →ₐ[k] k)), (projectiveOrbitTranslation m hm g).hom x = y

Rational group translations act transitively on the closed points of the orbit scheme, as automorphisms retaining its full scheme structure.