Local closedness detected at closed points

In a Noetherian Jacobson space, every nonempty constructible set contains a closed point at which it is locally closed. Consequently, local closedness of a constructible set can be checked just at its closed points. This permits arguments about rational points of algebraic group orbits to control the whole topological image, including its nonclosed points.

The argument uses Topology.IsConstructible.dense_interior in the closure of the set, and Mathlib's closed-point existence theorem for locally closed subsets of Jacobson spaces.

References

• J. S. Milne, Algebraic Groups (2017), §7.c, locally closed orbits.

theorem Topology.IsConstructible.exists_isLocallyClosedAt_mem_closedPoints {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.NoetherianSpace X] [JacobsonSpace X] {s : Set X} (hs : IsConstructible s) (hne : s.Nonempty) : ∃ x ∈ s ∩ closedPoints X, IsLocallyClosedAt s x

A nonempty constructible set contains a closed point at which it is locally closed.

theorem Topology.IsConstructible.isLocallyClosed_iff_forall_mem_closedPoints {X : Type u_1} [TopologicalSpace X] [TopologicalSpace.NoetherianSpace X] [JacobsonSpace X] {s : Set X} (hs : IsConstructible s) : IsLocallyClosed s ↔ ∀ x ∈ s ∩ closedPoints X, IsLocallyClosedAt s x

A constructible set in a Noetherian Jacobson space is locally closed precisely when it is locally closed at each of its closed points.