Constructible orbits are locally closed

For an action by homeomorphisms, local closedness of an orbit at one of its points implies local closedness everywhere on that orbit. If the orbit is constructible inside its closure, its relative interior is dense and hence nonempty, supplying such a point. In particular, constructible orbits in a Noetherian space are locally closed.

In a Noetherian Jacobson space it suffices for an invariant constructible set to be homogeneous on its closed points. Such a set need not be a single orbit on all points: this form applies to the full topological image of an algebraic orbit morphism.

This is the topological step in realizing homogeneous spaces as locally closed orbits: once constructibility of an orbit has been established, the orbit is open in its closure. Only continuity of each translation is required; the acting group need not carry a topology.

The constructible-set argument reuses Topology.IsConstructible.dense_interior.

References

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

theorem TauCeti.isLocallyClosed_orbit_of_isLocallyClosedAt {G : Type u_1} {X : Type u_2} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] (x : X) {y : X} (hy : y ∈ MulAction.orbit G x) (h : IsLocallyClosedAt (MulAction.orbit G x) y) : IsLocallyClosed (MulAction.orbit G x)

An orbit which is locally closed at one of its points is locally closed.

theorem TauCeti.isLocallyClosed_orbit_of_isConstructible_preimage_val_closure {G : Type u_1} {X : Type u_2} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] (x : X) (h : Topology.IsConstructible (Subtype.val ⁻¹' MulAction.orbit G x)) : IsLocallyClosed (MulAction.orbit G x)

An orbit constructible in its closure is locally closed, without a Noetherian or separation hypothesis on the ambient space.

theorem TauCeti.isLocallyClosed_orbit_of_isConstructible {G : Type u_1} {X : Type u_2} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] [TopologicalSpace.NoetherianSpace X] (x : X) (h : Topology.IsConstructible (MulAction.orbit G x)) : IsLocallyClosed (MulAction.orbit G x)

A constructible orbit in a Noetherian space is locally closed. This applies to actions by homeomorphisms on spaces with the Zariski topology.

theorem TauCeti.isLocallyClosed_of_isConstructible_of_closedPoints_transitive {G : Type u_1} {X : Type u_2} [Group G] [TopologicalSpace X] [MulAction G X] [ContinuousConstSMul G X] [TopologicalSpace.NoetherianSpace X] [JacobsonSpace X] {s : Set X} (hs : Topology.IsConstructible s) (hinvariant : ∀ (g : G), (fun (x : X) => g • x) ⁻¹' s = s) (htransitive : ∀ x ∈ s ∩ closedPoints X, ∀ y ∈ s ∩ closedPoints X, ∃ (g : G), g • x = y) : IsLocallyClosed s

An invariant constructible set in a Noetherian Jacobson space is locally closed if the action is transitive on its closed points. No transitivity on nonclosed points is needed.