Covering a closed set by neighbourhoods of its closed points

In a Jacobson space every point x of a closed set S specializes to a closed point p ∈ S (a closed point of the closed set closure {x}), and an open set containing p contains x. Hence open sets around the closed points of S cover S.

• exists_isClosed_singleton_mem_specializes: the closed point p with x ⤳ p.
• subset_iUnion_of_isOpen_of_closedPoints: the covering statement.

Kollár's proof of the uniqueness of maximal contact up to étale equivalence [Kol07, 95 (proof of Theorem 92)] constructs an étale neighbourhood U(p) at each point p and concludes that "the images of finitely many of the U(p) cover X"; the neighbourhoods are built at closed points, and this file supplies the topology that makes them cover. A scheme locally of finite type over a field is a Jacobson space (LocallyOfFiniteType.jacobsonSpace). Not stated in the source.

theorem exists_isClosed_singleton_mem_specializes {X : Type u_1} [TopologicalSpace X] [JacobsonSpace X] {S : Set X} (hS : IsClosed S) {x : X} (hx : x ∈ S) : ∃ (p : X), IsClosed {p} ∧ p ∈ S ∧ x ⤳ p

In a Jacobson space, every point x of a closed set S specializes to a closed point p ∈ S — a closed point of the closed set closure {x} ⊆ S.

theorem subset_iUnion_of_isOpen_of_closedPoints {X : Type u_1} [TopologicalSpace X] [JacobsonSpace X] {S : Set X} (hS : IsClosed S) (O : { p : X // IsClosed {p} ∧ p ∈ S } → Set X) (hO : ∀ (p : { p : X // IsClosed {p} ∧ p ∈ S }), IsOpen (O p)) (hpO : ∀ (p : { p : X // IsClosed {p} ∧ p ∈ S }), ↑p ∈ O p) : S ⊆ ⋃ (p : { p : X // IsClosed {p} ∧ p ∈ S }), O p

Open sets O p around the closed points p of a closed set S of a Jacobson space cover S: the closed points are dense in S, and each point of S lies in the open set attached to a closed point it specializes to.