Existence of closed orbits #
Let a group scheme G of finite type over an algebraically closed field k act on a scheme X
of finite type over k. The geometric orbit O_x of a rational point x of X is locally
closed, and its boundary Z_x \ O_x in the orbit closure Z_x is closed, stable under
translation by the rational points of G, and of strictly smaller dimension than O_x
(TauCeti.SchemeAction.topologicalKrullDim_orbitBoundary_lt).
A closed subset of X stable under rational translations contains the whole geometric orbit of
a rational point as soon as it contains that point: the closed points of the orbit are its
rational translates, and they are dense in the locally closed orbit. Hence the orbit of a
rational point y of the boundary of O_x lies in that boundary, and has strictly smaller
dimension than O_x. Since a nonempty closed subset of X contains a rational point, an orbit
whose dimension is minimal among the orbits of the rational points of its closure has empty
boundary, that is, it is closed. By induction on the dimension, every orbit closure contains a
closed orbit; in particular every nonempty closed subset of X stable under rational
translations, and every nonempty X, contains one.
No smoothness, reducedness, connectedness or separatedness hypothesis is needed, and X need not
be irreducible. The orbits are the full topological images of the orbit morphisms, including
their nonclosed points. The closed orbit produced is not claimed to be unique.
Main declarations #
TauCeti.SchemeAction.orbit_subset_iff_of_isClosed: a closed translation-stable subset contains the orbit of a rational point exactly when it contains the point.TauCeti.SchemeAction.orbitClosure_subset_iff_of_isClosed: the same criterion for the orbit closure.TauCeti.SchemeAction.orbitClosure_subset_orbitBoundary: the orbit closure of a rational point of the boundary ofO_xlies in that boundary.TauCeti.SchemeAction.exists_rationalPoint_mem_orbitBoundary_of_not_isClosed: a nonclosed orbit has a rational point in its boundary.TauCeti.SchemeAction.isClosed_orbit_of_forall_mem_orbitClosure: an orbit of minimal dimension is closed.TauCeti.SchemeAction.exists_isClosed_orbit_subset_orbitClosure: every orbit closure contains a closed orbit.TauCeti.SchemeAction.exists_isClosed_orbit: a nonemptyXhas a closed orbit.
References #
- A. Borel, Linear Algebraic Groups, 2nd ed., GTM 126, §1.8, the closed orbit lemma.
- J. E. Humphreys, Linear Algebraic Groups, GTM 21, §8.3.
A closed subset of X stable under translation by the rational points of G contains the
geometric orbit of a rational point y, including its nonclosed points, exactly when it contains
y.
A closed subset of X stable under translation by the rational points of G contains the
orbit closure of a rational point y exactly when it contains y.
The orbit closure of a rational point y lies in the orbit closure of x exactly when y
does.
The orbit closure of a rational point y of the boundary of the orbit of x lies in that
boundary.
The orbit of a rational point y of the boundary of the orbit of x has strictly smaller
dimension than the orbit of x.
A nonclosed orbit has a rational point in its boundary.
Closed-orbit lemma. If the orbit of x has minimal dimension among the orbits of the
rational points of its closure, then it is closed.
Existence of closed orbits. The closure of the orbit of every rational point contains the closed orbit of a rational point.
Every nonempty closed subset of X stable under translation by the rational points of G
contains the closed orbit of a rational point.
Existence of closed orbits. A nonempty scheme of finite type over an algebraically closed field, acted on by a group scheme of finite type, contains the closed orbit of a rational point.