The independence of the gluing from the data, and the exhaustion gluing

Włodarczyk: the canonical desingularization Ỹ_Z → Y_Z is independent of the choice of ambient manifold, and an open embedding of germs induces an open embedding of the desingularizations [Wlo09, §4, (3)⇒(4)]; Kollár: the local resolutions agree by the uniqueness of the comparison [Kol07, Theorem 36, proof] — applied piecewise on the common refinement of two local embedding data D (over U) and D' (over U'). The gluing along an exhaustion is Włodarczyk's [Wlo09, §4.3] and Kollár's passage from neighbourhoods of compact sets to an increasing union of compact subsets [Kol07, 44].

• GlueOver.exists_localTransition_glued, GlueOver.exists_isoOver_of_localTransitions (general, on two gluing data over the same base): local transitions between the pieces of two gluing data, each UNIQUE among the isomorphisms over X on its cover member, read into the glued spaces by partIso and glued by exists_isIso_over_of_cover — the uniqueness on every sub-open by hom_ext_of_cover and uniq_of_conj.
• LocalEmbeddingData.exists_isoOver_resolutionOnFull: for an open O ⊆ U ∩ U' the parts of the two glued spaces over O are isomorphic over X by a UNIQUE isomorphism — the mixed local transitions exists_localTransition_pair (the independence of the local resolution as hind) at the pieces i of D, i' of D' through z.
• exists_isoOver_resolutionOn: the same on the spaces resolutionOn, over X through resolutionOnToSpace (exists_iso_restrictOpen_restrictOpen_comap).
• resolutionOn_indep_of_independent: the independence of the glued resolution from the data, with hind — the core at O := U read into restrictSet/Hom.restrictSet.
• BEDanFamStar.resolutionGlues_of_isEmbeddedDesing_of_independent: the gluing along an exhaustion — the exhaustion, local embedding data over each member, the gluing data, and the gluing along the exhaustion from GlueOver.exists_glueOver_of_transitions with the transitions and the uniqueness of exists_isoOver_resolutionOn. The forms without hind are resolutionOn_indep and resolutionGlues_of_isEmbeddedDesing (GluingProperties.lean).

Not in the sources beyond the remarks cited; bookkeeping.

theorem AnalyticSpace.GlueOver.exists_localTransition_glued {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 ι] {ι' : Type u} {R' : ι' → AnalyticSpace K} {π' : (i' : ι') → (R' i').toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom' : ι' → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G' : X.GlueOver R' π' dom') [Countable ι'] (i : ι) (i' : ι') (P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hPi : P ≤ dom i) (hPi' : P ≤ dom' i') (θ : (R i).restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P) ⟶ (R' i').restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π' i'), continuous_toFun := ⋯ }) P)) (hθ : CategoryTheory.IsIso θ) (hθc : CategoryTheory.CategoryStruct.comp ((R i).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp θ ((R' i').ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π' i'), continuous_toFun := ⋯ }) P))) (π' i')) (hθu : ∀ (s : (R i).restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P) ⟶ (R' i').restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π' i'), continuous_toFun := ⋯ }) P)), CategoryTheory.IsIso s → CategoryTheory.CategoryStruct.comp ((R i).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s ((R' i').ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π' i'), continuous_toFun := ⋯ }) P))) (π' i') → s = θ) : ∃ (σ : G.gluedOver.restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G.descMap, continuous_toFun := ⋯ }) P) ⟶ G'.gluedOver.restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G'.descMap, continuous_toFun := ⋯ }) P)), CategoryTheory.IsIso σ ∧ CategoryTheory.CategoryStruct.comp (G.gluedOver.ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G.descMap, continuous_toFun := ⋯ }) P)) G.descMap = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp σ (G'.gluedOver.ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G'.descMap, continuous_toFun := ⋯ }) P))) G'.descMap ∧ ∀ (s : G.gluedOver.restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G.descMap, continuous_toFun := ⋯ }) P) ⟶ G'.gluedOver.restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G'.descMap, continuous_toFun := ⋯ }) P)), CategoryTheory.IsIso s → CategoryTheory.CategoryStruct.comp (G.gluedOver.ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G.descMap, continuous_toFun := ⋯ }) P)) G.descMap = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (G'.gluedOver.ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G'.descMap, continuous_toFun := ⋯ }) P))) G'.descMap → s = σ

A local transition between a piece of G and a piece of G' over P, unique among the isomorphisms over X, read into the glued spaces: conjugation by the identifications partIso of the parts over P preserves isomorphism, "over X" (over_of_conj_inv_hom) and uniqueness (uniq_of_conj).

theorem AnalyticSpace.GlueOver.exists_isoOver_of_localTransitions {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 ι] {ι' : Type u} {R' : ι' → AnalyticSpace K} {π' : (i' : ι') → (R' i').toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace} {dom' : ι' → TopologicalSpace.Opens ↑↑X.toPresheafedSpace} (G' : X.GlueOver R' π' dom') [Countable ι'] (O : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hloc : ∀ O' ≤ O, ∀ z ∈ O', ∃ (i : ι) (i' : ι') (P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (_ : z ∈ P) (_ : P ≤ O') (_ : P ≤ dom i) (_ : P ≤ dom' i') (θ : (R i).restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P) ⟶ (R' i').restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π' i'), continuous_toFun := ⋯ }) P)), CategoryTheory.IsIso θ ∧ CategoryTheory.CategoryStruct.comp ((R i).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp θ ((R' i').ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π' i'), continuous_toFun := ⋯ }) P))) (π' i') ∧ ∀ (s : (R i).restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P) ⟶ (R' i').restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π' i'), continuous_toFun := ⋯ }) P)), CategoryTheory.IsIso s → CategoryTheory.CategoryStruct.comp ((R i).ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π i), continuous_toFun := ⋯ }) P)) (π i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s ((R' i').ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun (π' i'), continuous_toFun := ⋯ }) P))) (π' i') → s = θ) : ∃ (s : G.gluedOver.restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G.descMap, continuous_toFun := ⋯ }) O) ⟶ G'.gluedOver.restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G'.descMap, continuous_toFun := ⋯ }) O)), CategoryTheory.IsIso s ∧ CategoryTheory.CategoryStruct.comp (G.gluedOver.ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G.descMap, continuous_toFun := ⋯ }) O)) G.descMap = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (G'.gluedOver.ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G'.descMap, continuous_toFun := ⋯ }) O))) G'.descMap ∧ ∀ (s' : G.gluedOver.restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G.descMap, continuous_toFun := ⋯ }) O) ⟶ G'.gluedOver.restrictOpen ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G'.descMap, continuous_toFun := ⋯ }) O)), CategoryTheory.IsIso s' → CategoryTheory.CategoryStruct.comp (G.gluedOver.ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G.descMap, continuous_toFun := ⋯ }) O)) G.descMap = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s' (G'.gluedOver.ofRestrict ((TopologicalSpace.Opens.comap { toFun := KLocallyRingedSpace.Hom.toFun G'.descMap, continuous_toFun := ⋯ }) O))) G'.descMap → s' = s

Two gluing data over X whose pieces carry unique local transitions on a cover of every sub-open of O have isomorphic parts over O, uniquely over X: exists_isIso_over_of_cover on the cover of O by the members, the local transitions read into the glued spaces (exists_localTransition_glued); the uniqueness on a sub-open O' by hom_ext_of_cover on its members (every isomorphism over X restricts to the unique local one).

theorem Hironaka.Manifold.LocalEmbeddingData.exists_localTransition_of_glues {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U U' : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (D' : LocalEmbeddingData 𝕜 X U') (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) (Gd : D.ResolutionGluing bed) (Gd' : D'.ResolutionGluing bed) (O' : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hO' : ↑O' ⊆ U ∩ U') {z : ↑↑X.toPresheafedSpace} (hz : z ∈ O') : ∃ (i : D.ι) (i' : D'.ι) (P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (_ : z ∈ P) (_ : P ≤ O') (_ : P ≤ D.pieceDom i (Gd.W i)) (_ : P ≤ D'.pieceDom i' (Gd'.W i')) (θ : ((D.embedding i).localResolution bed (Gd.W i) ⋯).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.pieceToSpace bed i (Gd.W i) ⋯), continuous_toFun := ⋯ }) P) ⟶ ((D'.embedding i').localResolution bed (Gd'.W i') ⋯).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D'.pieceToSpace bed i' (Gd'.W i') ⋯), continuous_toFun := ⋯ }) P)), CategoryTheory.IsIso θ ∧ CategoryTheory.CategoryStruct.comp (((D.embedding i).localResolution bed (Gd.W i) ⋯).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.pieceToSpace bed i (Gd.W i) ⋯), continuous_toFun := ⋯ }) P)) (D.pieceToSpace bed i (Gd.W i) ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp θ (((D'.embedding i').localResolution bed (Gd'.W i') ⋯).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D'.pieceToSpace bed i' (Gd'.W i') ⋯), continuous_toFun := ⋯ }) P))) (D'.pieceToSpace bed i' (Gd'.W i') ⋯) ∧ ∀ (s : ((D.embedding i).localResolution bed (Gd.W i) ⋯).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.pieceToSpace bed i (Gd.W i) ⋯), continuous_toFun := ⋯ }) P) ⟶ ((D'.embedding i').localResolution bed (Gd'.W i') ⋯).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D'.pieceToSpace bed i' (Gd'.W i') ⋯), continuous_toFun := ⋯ }) P)), CategoryTheory.IsIso s → CategoryTheory.CategoryStruct.comp (((D.embedding i).localResolution bed (Gd.W i) ⋯).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.pieceToSpace bed i (Gd.W i) ⋯), continuous_toFun := ⋯ }) P)) (D.pieceToSpace bed i (Gd.W i) ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s (((D'.embedding i').localResolution bed (Gd'.W i') ⋯).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D'.pieceToSpace bed i' (Gd'.W i') ⋯), continuous_toFun := ⋯ }) P))) (D'.pieceToSpace bed i' (Gd'.W i') ⋯) → s = θ

The mixed local transitions of two gluing data, in the form the assembly wants (with the independence of the local resolution as hind): for z in an open O' ⊆ U ∩ U', pieces i of D, i' of D' with z in their base opens (the inner opens cover U, their closures lie in the base opens) and a cover member P ∋ z, P ≤ O', inside both base opens, carrying the unique local transition (exists_localTransition_pair).

theorem Hironaka.Manifold.LocalEmbeddingData.exists_isoOver_resolutionOnFull {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U U' : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (D' : LocalEmbeddingData 𝕜 X U') (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) (O : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hO : ↑O ⊆ U ∩ U') : ∃ (s : (D.resolutionOnFull bed).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resolutionOnFullMap bed), continuous_toFun := ⋯ }) O) ⟶ (D'.resolutionOnFull bed).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D'.resolutionOnFullMap bed), continuous_toFun := ⋯ }) O)), CategoryTheory.IsIso s ∧ CategoryTheory.CategoryStruct.comp ((D.resolutionOnFull bed).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resolutionOnFullMap bed), continuous_toFun := ⋯ }) O)) (D.resolutionOnFullMap bed) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s ((D'.resolutionOnFull bed).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D'.resolutionOnFullMap bed), continuous_toFun := ⋯ }) O))) (D'.resolutionOnFullMap bed) ∧ ∀ (s' : (D.resolutionOnFull bed).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resolutionOnFullMap bed), continuous_toFun := ⋯ }) O) ⟶ (D'.resolutionOnFull bed).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D'.resolutionOnFullMap bed), continuous_toFun := ⋯ }) O)), CategoryTheory.IsIso s' → CategoryTheory.CategoryStruct.comp ((D.resolutionOnFull bed).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resolutionOnFullMap bed), continuous_toFun := ⋯ }) O)) (D.resolutionOnFullMap bed) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s' ((D'.resolutionOnFull bed).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D'.resolutionOnFullMap bed), continuous_toFun := ⋯ }) O))) (D'.resolutionOnFullMap bed) → s' = s

The unique isomorphism over X between the parts of the two glued spaces over an open O ⊆ U ∩ U' ([Wlo09, §4, (3)⇒(4)]; [Kol07, Theorem 36, proof]) — the assembly exists_isoOver_of_localTransitions for the two chosen gluing data with the mixed local transitions exists_localTransition_of_glues; the spaces resolutionOnFull unfold to the chosen data's glued spaces (resolutionOnFullPair_eq_of_glues).

theorem Hironaka.Manifold.LocalEmbeddingData.exists_isoOver_resolutionOn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U U' : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (D' : LocalEmbeddingData 𝕜 X U') (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) (O : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hO : ↑O ⊆ U ∩ U') : ∃ (s : (D.resolutionOn bed).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resolutionOnToSpace bed), continuous_toFun := ⋯ }) O) ⟶ (D'.resolutionOn bed).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D'.resolutionOnToSpace bed), continuous_toFun := ⋯ }) O)), CategoryTheory.IsIso s ∧ CategoryTheory.CategoryStruct.comp ((D.resolutionOn bed).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resolutionOnToSpace bed), continuous_toFun := ⋯ }) O)) (D.resolutionOnToSpace bed) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s ((D'.resolutionOn bed).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D'.resolutionOnToSpace bed), continuous_toFun := ⋯ }) O))) (D'.resolutionOnToSpace bed) ∧ ∀ (s' : (D.resolutionOn bed).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resolutionOnToSpace bed), continuous_toFun := ⋯ }) O) ⟶ (D'.resolutionOn bed).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D'.resolutionOnToSpace bed), continuous_toFun := ⋯ }) O)), CategoryTheory.IsIso s' → CategoryTheory.CategoryStruct.comp ((D.resolutionOn bed).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resolutionOnToSpace bed), continuous_toFun := ⋯ }) O)) (D.resolutionOnToSpace bed) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s' ((D'.resolutionOn bed).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D'.resolutionOnToSpace bed), continuous_toFun := ⋯ }) O))) (D'.resolutionOnToSpace bed) → s' = s

The same on the spaces resolutionOn, over X through resolutionOnToSpace: the parts of resolutionOn D bed = Ṽ_D|Π⁻¹U over O ⊆ U ∩ U' are the parts of the full glued spaces (exists_iso_restrictOpen_restrictOpen_comap), and the isomorphism, its compatibility and its uniqueness transport by conjugation.

theorem Hironaka.Manifold.LocalEmbeddingData.resolutionOn_indep_of_independent {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U U' : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (D' : LocalEmbeddingData 𝕜 X U') (bed : BEDanFamStar 𝕜) (hU : IsOpen U) (hUU' : U ⊆ U') (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) : ∃! ψ : D.resolutionOn bed ⟶ (D'.resolutionOnFull bed).restrictSet (↑(D'.resolutionOnFullMap bed) ⁻¹' U), CategoryTheory.IsIso ψ ∧ CategoryTheory.CategoryStruct.comp ψ (AnalyticSpace.Hom.restrictSet (D'.resolutionOnFullMap bed) U) = D.resolutionOnMap bed

The independence of the glued resolution from the local embedding data ([Wlo09, §4, (3)⇒(4)]; [Kol07, Theorem 36, proof]), with the independence of the local resolution as the hypothesis hind: for data D over the OPEN U and D' over U' ⊇ U, a UNIQUE isomorphism of resolutionOn D bed with the resolution of D' restricted over U, over X|U — exists_isoOver_resolutionOnFull at O := U read into the spaces (restrictOpenIsoOfSetEq between the spelling openOf (Π⁻¹U) and comap Π U; the composite ≫ and Hom.restrictSet through Hom.restrictTo_comp_ofRestrict and Hom.ext_of_comp_ofRestrict). The form without hind is resolutionOn_indep (GluingProperties.lean).

theorem Hironaka.Manifold.BEDanFamStar.resolutionGlues_of_isEmbeddedDesing_of_independent {𝕜 : Type} [RCLike 𝕜] (X : AnalyticSpace 𝕜) (hX : X.IsReduced) (bed : BEDanFamStar 𝕜) (hbed : IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) : bed.ResolutionGlues X

The resolution glues along an exhaustion ([Wlo09, §4.3]; [Kol07, 44]; an analytic space is countable at infinity, [Hir64, Ch. 0, §1, p. 120]), with the independence of the local resolution as the hypothesis hind — an exhaustion U_0 ⋐ U_1 ⋐ ⋯ of X, local embedding data D_n over each U_n (exists_localEmbeddingData_of_padTools), their gluing data, and the gluing over X of the resolutionOn (D n) bed along U_n ∩ U_m by GlueOver.exists_glueOver_of_transitions, whose transitions and uniqueness hypothesis are exists_isoOver_resolutionOn at U_n ⊓ U_m (resp. at every sub-open). The form without hind is resolutionGlues_of_isEmbeddedDesing (GluingProperties.lean).