The descended map of a gluing over a base is proper over the base open subsets

"des_V : Ṽ → V … is proper" [Wlo09, §4]: the map descended from proper piece maps π i : R i → dom i is proper over the union of the base open subsets. Two facts about a gluing datum G : GlueOver X R π dom:

• mem_range_toFun_ιGlued_iff: the part of the glued space over dom i is exactly the image of the i-th piece under the open immersion ιGlued i: a point of the j-th piece over dom i lies over dom i ∩ dom j, where the transition t j i carries it into the i-th piece (the glue condition KGlueData.ofRestrict_comp_ιK);
• isProperMap_restrictPreimage_descMap: hence over dom i the descended map is π i read through the homeomorphism R i ≃ₜ des⁻¹(dom i), and it is proper there when π i : R i → dom i is; isProperMap_restrictPreimage_descMap_of_subset assembles the base open subsets into properness over every V ⊆ ⋃ dom i (isProperMap_restrictPreimage_of_cover).

Both properness statements enter the gluing datum of the local resolutions (Hironaka.Resolution.Analytic.Kol07Thm45.PieceGlueDatum), and through Hironaka.AnalyticSpace.Glue.OverReg the properness clause of the resolution (Hironaka.Resolution.Analytic.Kol07Thm45.ResolutionClauses).

theorem AnalyticSpace.GlueOver.mem_range_toFun_ιGlued_iff {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 ι] (i : ι) (z : ↑↑G.gluedOver.toPresheafedSpace) : z ∈ Set.range (KLocallyRingedSpace.Hom.toFun (G.ιGlued i)) ↔ KLocallyRingedSpace.Hom.toFun G.descMap z ∈ dom i

The part of the glued space over dom i is the image of the i-th piece (the part of Ṽ over V_i is Ṽ_i, [Wlo09, §4]): a point over dom i coming from the j-th piece lies over dom i ∩ dom j, where the transition t j i carries it into the i-th piece (the glue condition KGlueData.ofRestrict_comp_ιK).

theorem AnalyticSpace.GlueOver.preimage_toFun_descMap_dom {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 ι] (i : ι) : KLocallyRingedSpace.Hom.toFun G.descMap ⁻¹' ↑(dom i) = Set.range (KLocallyRingedSpace.Hom.toFun (G.ιGlued i))

The part of the glued space over dom i, as a set: the image of the i-th piece.

theorem AnalyticSpace.GlueOver.isProperMap_restrictPreimage_descMap {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 ι] (i : ι) (hπ : IsProperMap fun (y : ↑↑(R i).toPresheafedSpace) => ⟨KLocallyRingedSpace.Hom.toFun (π i) y, ⋯⟩) : IsProperMap ((↑(dom i)).restrictPreimage (KLocallyRingedSpace.Hom.toFun G.descMap))

The descended map is proper over dom i when the i-th piece map is ("des_V is proper", [Wlo09, §4]): over dom i the glued space is the i-th piece (ιGlued i, an open embedding onto the part over dom i), and the descended map is π i there (toFun_descMap_ιGlued).

theorem AnalyticSpace.GlueOver.isProperMap_restrictPreimage_descMap_of_subset {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 : ι), IsProperMap fun (y : ↑↑(R i).toPresheafedSpace) => ⟨KLocallyRingedSpace.Hom.toFun (π i) y, ⋯⟩) (V : Set ↑↑X.toPresheafedSpace) (hVsub : V ⊆ ⋃ (i : ι), ↑(dom i)) : IsProperMap (V.restrictPreimage (KLocallyRingedSpace.Hom.toFun G.descMap))

The descended map is proper over every V ⊆ ⋃ dom i when every piece map is proper over its base open subset (isProperMap_restrictPreimage_of_cover on the base open subsets).