The descended map of a gluing is an isomorphism where the pieces are

The resolution is an isomorphism over the simple points (clause (2) of the resolution problem, [Hir64, Introduction, p. 111]; [Kol07, Theorem 45, (2)]; [Wlo09, Theorem 2.0.1, (1)]), read on a gluing datum G : GlueOver X R π dom: over an open subset V ⊆ dom i the glued space is the i-th piece (partIso, Hironaka.AnalyticSpace.Glue.OverPart), so the descended map is an isomorphism over V when the piece map is (isIsoOver_descMap_of_isIsoOver, through Hom.IsIsoOver.of_isIso_restrictSet_comm); over an open subset S, isomorphisms over S ∩ dom i for every piece assemble to one over S ∩ ⋃ dom i (isIsoOver_descMap_inter_iUnion). The latter is applied to the glued local resolutions in Hironaka.Resolution.Analytic.Kol07Thm45.ResolutionIsoReg.

theorem AnalyticSpace.GlueOver.isIsoOver_descMap_of_isIsoOver {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 : ι) {V : Set ↑↑X.toPresheafedSpace} (hV : IsOpen V) (hVi : V ⊆ ↑(dom i)) (h : Hom.IsIsoOver (π i) V) : Hom.IsIsoOver G.descMap V

The descended map is an isomorphism over an open subset V ⊆ dom i when the i-th piece map is ([Kol07, Theorem 45, (2)], piece by piece): the part of the glued space over dom i is the part of the piece (partIso, read between the restrictions openOf), over X; then Hom.IsIsoOver.of_isIso_restrictSet_comm at P := V.

theorem AnalyticSpace.GlueOver.isIsoOver_descMap_inter_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 ι] (S : Set ↑↑X.toPresheafedSpace) (hS : IsOpen S) (h : ∀ (i : ι), Hom.IsIsoOver (π i) (S ∩ ↑(dom i))) : Hom.IsIsoOver G.descMap (S ∩ ⋃ (i : ι), ↑(dom i))

Over an open subset S, isomorphisms over S ∩ dom i for every piece give one over S ∩ ⋃ dom i.