Orbits of algebraic group actions are locally closed

Let a group scheme G act on a scheme X over S. Global points of G act on the underlying space of X by the translation homeomorphisms, and they preserve every geometric orbit TauCeti.SchemeAction.orbit G x.

When G is of finite type and X is quasi-compact and locally Noetherian, the geometric orbit is constructible, by Chevalley's theorem. Over an algebraically closed field k, with G and X of finite type, the rational points of the orbit are exactly the translates g • x of x by the rational points g of G, and the closed points of the orbit are the corresponding points of the underlying space. Hence the rational points of G act transitively on the closed points of the orbit, and the orbit is locally closed: it is open in its closure, and its boundary is closed and of strictly smaller dimension.

No smoothness, reducedness, separatedness or connectedness hypothesis is needed, and X need not be irreducible. The orbit is the full topological image of the orbit morphism, including its nonclosed points; it is not replaced by the set of rational points. No subscheme structure on the orbit is constructed here.

The argument combines AlgebraicGeometry.Scheme.Hom.exists_comp_eq_iff_mem_range, which lifts rational points along morphisms, with TauCeti.isLocallyClosed_of_isConstructible_of_closedPoints_transitive, which only needs transitivity on closed points.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 1.65 and §7.c.

theorem TauCeti.SchemeAction.isConstructible_orbit {S : AlgebraicGeometry.Scheme} (G : CategoryTheory.Over S) {X : CategoryTheory.Over S} [CategoryTheory.MonObj G] [CategoryTheory.ModObj G X] [AlgebraicGeometry.LocallyOfFiniteType G.hom] [CompactSpace ↥G.left] [AlgebraicGeometry.IsLocallyNoetherian X.left] [CompactSpace ↥X.left] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ X) : Topology.IsConstructible (orbit G x)

The geometric orbit of a section is constructible when the group is of finite type and the acted-on scheme is quasi-compact and locally Noetherian.

theorem TauCeti.SchemeAction.left_apply_mem_orbit_iff {k : Type u} [Field k] [IsAlgClosed k] (G : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)} [CategoryTheory.MonObj G] [CategoryTheory.ModObj G X] [AlgebraicGeometry.LocallyOfFiniteType G.hom] [AlgebraicGeometry.LocallyOfFiniteType X.hom] (x y : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) ⟶ X) (a : ↥(CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))).left) : (CategoryTheory.Over.Hom.left y) a ∈ orbit G x ↔ ∃ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) ⟶ G), g • x = y

Over an algebraically closed field, a rational point of X lies in the geometric orbit of x exactly when it is a translate of x by a rational point of G.

theorem TauCeti.SchemeAction.orbit_inter_closedPoints {k : Type u} [Field k] [IsAlgClosed k] (G : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)} [CategoryTheory.MonObj G] [CategoryTheory.ModObj G X] [AlgebraicGeometry.LocallyOfFiniteType G.hom] [AlgebraicGeometry.LocallyOfFiniteType X.hom] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) ⟶ X) : orbit G x ∩ closedPoints ↥X.left = ⋃ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) ⟶ G), Set.range ⇑(CategoryTheory.Over.Hom.left (g • x))

Over an algebraically closed field, the closed points of the geometric orbit of x are exactly the points underlying its translates by rational points of G.

theorem TauCeti.SchemeAction.exists_translation_eq_of_mem_orbit_inter_closedPoints {k : Type u} [Field k] [IsAlgClosed k] (G : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] [AlgebraicGeometry.LocallyOfFiniteType G.hom] [AlgebraicGeometry.LocallyOfFiniteType X.hom] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) ⟶ X) {p q : ↥X.left} (hp : p ∈ orbit G x ∩ closedPoints ↥X.left) (hq : q ∈ orbit G x ∩ closedPoints ↥X.left) : ∃ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) ⟶ G), (CategoryTheory.Over.Hom.left (translation X g).hom) p = q

Over an algebraically closed field, with G and X locally of finite type, any two closed points of the geometric orbit of x are related by translation by a rational point of G.

theorem TauCeti.SchemeAction.exists_eq_of_equivariant_of_range_subset_orbit {k : Type u} [Field k] [IsAlgClosed k] (G : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] [AlgebraicGeometry.LocallyOfFiniteType G.hom] [AlgebraicGeometry.LocallyOfFiniteType X.hom] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) ⟶ X) {Y : AlgebraicGeometry.Scheme} (i : Y ⟶ X.left) [AlgebraicGeometry.IsImmersion i] (hrange : Set.range ⇑i ⊆ orbit G x) (e : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) ⟶ G) → (Y ≅ Y)) (he : ∀ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) ⟶ G), CategoryTheory.CategoryStruct.comp (e g).hom i = CategoryTheory.CategoryStruct.comp i (CategoryTheory.Over.Hom.left (translation X g).hom)) {y z : ↥Y} (hy : y ∈ closedPoints ↥Y) (hz : z ∈ closedPoints ↥Y) : ∃ (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) ⟶ G), (e g).hom y = z

Over an algebraically closed field, with G and X locally of finite type, an immersed scheme lying in the geometric orbit of x inherits transitivity on closed points from any family of automorphisms intertwining the ambient translations by rational points of G.

theorem TauCeti.SchemeAction.isLocallyClosed_orbit {k : Type u} [Field k] [IsAlgClosed k] (G : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] [AlgebraicGeometry.LocallyOfFiniteType G.hom] [CompactSpace ↥G.left] [AlgebraicGeometry.LocallyOfFiniteType X.hom] [CompactSpace ↥X.left] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) ⟶ X) : IsLocallyClosed (orbit G x)

Over an algebraically closed field, the geometric orbit of a rational point under a finite-type group scheme acting on a finite-type scheme is locally closed.

theorem TauCeti.SchemeAction.isOpen_orbitClosure_preimage_orbit {k : Type u} [Field k] [IsAlgClosed k] (G : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] [AlgebraicGeometry.LocallyOfFiniteType G.hom] [CompactSpace ↥G.left] [AlgebraicGeometry.LocallyOfFiniteType X.hom] [CompactSpace ↥X.left] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) ⟶ X) : IsOpen (Subtype.val ⁻¹' orbit G x)

Over an algebraically closed field, the geometric orbit of a rational point is open in its closure.

theorem TauCeti.SchemeAction.isClosed_orbitBoundary {k : Type u} [Field k] [IsAlgClosed k] (G : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] [AlgebraicGeometry.LocallyOfFiniteType G.hom] [CompactSpace ↥G.left] [AlgebraicGeometry.LocallyOfFiniteType X.hom] [CompactSpace ↥X.left] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) ⟶ X) : IsClosed (orbitBoundary G x)

Over an algebraically closed field, the boundary of the geometric orbit of a rational point is closed.

theorem TauCeti.SchemeAction.topologicalKrullDim_orbitClosure {k : Type u} [Field k] [IsAlgClosed k] (G : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] [AlgebraicGeometry.LocallyOfFiniteType G.hom] [CompactSpace ↥G.left] [AlgebraicGeometry.LocallyOfFiniteType X.hom] [CompactSpace ↥X.left] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) ⟶ X) : topologicalKrullDim ↑(orbitClosure G x) = topologicalKrullDim ↑(orbit G x)

Over an algebraically closed field, the closure of the geometric orbit of a rational point has the same dimension as the orbit.

theorem TauCeti.SchemeAction.topologicalKrullDim_orbitBoundary_lt {k : Type u} [Field k] [IsAlgClosed k] (G : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] [AlgebraicGeometry.LocallyOfFiniteType G.hom] [CompactSpace ↥G.left] [AlgebraicGeometry.LocallyOfFiniteType X.hom] [CompactSpace ↥X.left] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) ⟶ X) : topologicalKrullDim ↑(orbitBoundary G x) < topologicalKrullDim ↑(orbit G x)

Over an algebraically closed field, the boundary of the geometric orbit of a rational point has strictly smaller dimension than the orbit, even when the orbit closure is reducible.