Properties local on an open cover: non-singularity and properness

Two locality statements used when a resolution is assembled from pieces: the glued space is covered by the images of its pieces, and the resolution morphism is covered on the target by an exhaustion, so both non-singularity ([Kol07, Theorem 45 (1)]) and properness ([Kol07, Theorem 45 (4)]; the properness of the glued desingularization in [Wlo09, §4]) are checked piecewise.

• AnalyticSpace.isNonsingular_of_openCover: an analytic K-space covered by opens whose open subspaces are non-singular is non-singular, since the stalk of an open subspace at a point is the stalk of the space (isRegularLocalRing_stalk_restrictOpen_iff, Hironaka/AnalyticSpace/RegDensityLemmas.lean).
• isProperMap_of_restrictPreimage_cover: a continuous map whose restrictions over the members of an open cover of the target are proper is proper — Mathlib's isProperMap_iff_isClosedMap_and_compact_fibers with isClosedMap_iff_restrictPreimage, the fibres being those of the restrictions.

Used by Hironaka/AnalyticSpace/ProperRestrict.lean and Hironaka/Resolution/Analytic/Functor/LimitProperties.lean.

theorem AnalyticSpace.isNonsingular_of_openCover {K : Type} [RCLike K] (X : AnalyticSpace K) {ι : Type u_1} (V : ι → Set ↑↑X.toPresheafedSpace) (hV : ∀ (i : ι), IsOpen (V i)) (hcov : ⋃ (i : ι), V i = Set.univ) (h : ∀ (i : ι), (X.restrictSet (V i)).IsNonsingular) : X.IsNonsingular

Non-singularity is local: an analytic K-space covered by opens whose open subspaces are non-singular is non-singular ([Kol07, Theorem 45 (1)], checked on the pieces of a gluing).

theorem AnalyticSpace.isProperMap_of_restrictPreimage_cover {Y : Type u_1} {X : Type u_2} [TopologicalSpace Y] [TopologicalSpace X] (f : Y → X) (hf : Continuous f) {ι : Type u_3} (V : ι → Set X) (hV : ∀ (i : ι), IsOpen (V i)) (hcov : ⋃ (i : ι), V i = Set.univ) (h : ∀ (i : ι), IsProperMap ((V i).restrictPreimage f)) : IsProperMap f

Properness is local on the target: a continuous map whose restrictions over the members of an open cover of the target are proper is proper — closedness by Mathlib's isClosedMap_iff_restrictPreimage, the fibres being the fibres of the restrictions. Compare the properness of the glued desingularization in [Wlo09, §4].