Non-singularity and properness of a glued space over a base

Two clauses of the resolution theorem for analytic spaces (the manifold clause (1) and the properness clause (3) of the resolution problem, [Hir64, Introduction, p. 111]; Kol07, Theorem 45, (1); [Wlo09, §4]: "des_V : Ṽ → V is bimeromorphic and proper") for a gluing datum G : GlueOver X R π dom:

• isNonsingular_gluedOver: a glued space of non-singular pieces is non-singular: every point comes from a piece through the open immersion ιGlued i (exists_ιGlued_eq), and an open immersion preserves the regularity of the stalk (mem_reg_iff_of_isOpenImmersion);
• isProperMap_descMap_of_iUnion: the descended map is proper when the base open subsets cover X and every piece map is proper onto its base open subset: properness is local on the target (isProperMap_of_restrictPreimage_cover), and over dom i the descended map is the i-th piece map (isProperMap_restrictPreimage_descMap, Hironaka.AnalyticSpace.Glue.OverProper).

Both are applied to the glued local resolutions in Hironaka.Resolution.Analytic.Kol07Thm45.ResolutionClauses.

theorem AnalyticSpace.GlueOver.isNonsingular_gluedOver {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (h : ∀ (i : ι), (R i).IsNonsingular) : G.gluedOver.IsNonsingular

A glued space of non-singular pieces is non-singular (the smoothness clause Kol07, Theorem 45, (1), piece by piece): every point of the glued space is the image of a point of a piece under the open immersion ιGlued i, and regularity of the stalk is carried across an open immersion (mem_reg_iff_of_isOpenImmersion).

theorem AnalyticSpace.GlueOver.isProperMap_descMap_of_iUnion {K : Type} [RCLike K] {X : AnalyticSpace K} {ι : Type u} {R : ι → AnalyticSpace K} {π : (i : ι) → (R i).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom : ι → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G : X.GlueOver R π dom) [Countable ι] (hcov : ⋃ (i : ι), ↑(dom i) = Set.univ) (hπ : ∀ (i : ι), IsProperMap fun (y : ↑↑(R i).toPresheafedSpace) => ⟨KLocallyRingedSpace.Hom.toFun (π i) y, ⋯⟩) : IsProperMap (KLocallyRingedSpace.Hom.toFun G.descMap)

The descended map is proper when the base open subsets cover X and every piece map is proper onto its base open subset ("des_V is proper", [Wlo09, §4]; the properness clause of the resolution problem, [Hir64, Introduction, p. 111]): properness is local on the target (isProperMap_of_restrictPreimage_cover), and over dom i the descended map is the i-th piece map (isProperMap_restrictPreimage_descMap).