Generic points of a preimage under an open surjective map

Włodarczyk's embedded desingularization commutes with smooth morphisms [Wlo05, Theorem 1.0.2 (d), and §4.1]. The resolution of a subvariety Y = V(I) is driven by the irreducible components of Y (the closures of the generic points of its support), and along a smooth surjection h : X' → X the components of h⁻¹(Y) are finer than the preimages of the components of Y (an étale cover may split a component). Transporting the construction along h therefore needs the topology of generic points under an open surjective continuous map f:

• mem_genericPoints_of_mem_genericPoints_preimage: the image of a generic point of f⁻¹(Z) is a generic point of Z. The component closure {η'} of f⁻¹(Z) maps onto a dense subset of the component C of Z through f η': the finitely many other components of f⁻¹(C) (the source is Noetherian) leave an open neighbourhood O of η' on which f⁻¹(C) ∩ O ⊆ closure {η'}; f(O) is open and meets C, hence contains the generic point of C.
• exists_mem_genericPoints_preimage_of_mem_genericPoints: every generic point of Z is the image of a generic point of f⁻¹(Z) (surjectivity and a generization inside the preimage).

Pure topology, not stated in the sources; the schemes to which it is applied are sober and, being of finite type over a field, Noetherian.

theorem eq_of_specializes_of_isGenericPoint {X : Type u_1} [TopologicalSpace X] [T0Space X] {S : Set X} {ξ x : X} (hξ : IsGenericPoint ξ S) (hx : x ∈ S) (h : x ⤳ ξ) : x = ξ

The generic point of an irreducible closed set is the unique point of the set generizing all of it: a point of the set that generizes the generic point is the generic point.

theorem notMem_closure_singleton_of_mem_genericPoints {X : Type u_1} [TopologicalSpace X] [T0Space X] [QuasiSober X] (Z : TopologicalSpace.Closeds X) {g η : X} (hg : g ∈ Z.genericPoints) (hη : η ∈ Z.genericPoints) (hne : g ≠ η) : η ∉ closure {g}

A generic point of a closed set lies in no other component: if g ≠ η are generic points of Z, then η ∉ closure {g} (both are maximal irreducible closed subsets of Z).

theorem mem_genericPoints_of_mem_genericPoints_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] [QuasiSober X] [T0Space Y] [QuasiSober Y] [TopologicalSpace.NoetherianSpace Y] {f : Y → X} (hf : Continuous f) (ho : IsOpenMap f) (Z : TopologicalSpace.Closeds X) {η' : Y} (hη' : η' ∈ (Z.preimage hf).genericPoints) : f η' ∈ Z.genericPoints

The image of a generic point of the preimage of a closed set under an open surjective continuous map is a generic point of the closed set.

theorem exists_mem_genericPoints_preimage_of_mem_genericPoints {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] [QuasiSober X] [T0Space Y] [QuasiSober Y] {f : Y → X} (hf : Continuous f) (hs : Function.Surjective f) (Z : TopologicalSpace.Closeds X) {η : X} (hη : η ∈ Z.genericPoints) : ∃ η' ∈ (Z.preimage hf).genericPoints, f η' = η

Every generic point of Z is the image of a generic point of f⁻¹(Z) when f is surjective and continuous: lift the point and generize inside the preimage.