The transitions of the gluing datum

Włodarczyk glues the canonical desingularizations along the isomorphisms over the overlaps Ṽ_i ∩ Ṽ_j [Wlo09, §4, (3)⇒(4)]; Kollár glues the local resolutions by a formal property of blow-up sequence functors [Kol07, Theorem 36, proof]. The transition of the gluing datum between two pieces i, j is an isomorphism over X between the parts of their local resolutions over the common base open pieceDom i ⊓ pieceDom j, and it is unique among such. Both are assembled from the LOCAL transitions of PieceTransition.lean (the independence of the local resolution from the embedding, transported to the cover members P_z) by the gluing of local isomorphisms over X, exists_isIso_over_of_cover (Hironaka/AnalyticSpace/Glue/GlueIsoOver.lean), and by hom_ext_of_cover (Hironaka/AnalyticSpace/HomLocal.lean):

• LocalEmbeddingData.exists_localTransition: at a point z of an open O' of the common base open, a cover member P ∋ z, P ≤ O', with the unique local transition over P;
• LocalEmbeddingData.transition_unique (with the independence as the hypothesis hind): two isomorphisms over X between the parts over an open O ≤ pieceDom i ⊓ pieceDom j agree — their restrictions (restrictOver) to every cover member P_z are the unique local transition, and morphisms agreeing on a cover agree (hom_ext_of_cover);
• LocalEmbeddingData.exists_transition (with hind): the transition over pieceDom i ⊓ pieceDom j — exists_isIso_over_of_cover applied to the local transitions with transition_unique as its uniqueness hypothesis, read onto the gluing opens pieceGlueOpens (the two spellings of the same open, restrictOpenIsoOfSetEq).

Not in the sources beyond the gluing remarks; bookkeeping.

theorem CategoryTheory.comp_eq_of_restrict_eq {C : Type u_1} [Category.{u_2, u_1} C] {A₀ A₁ A B₁ B : C} (pi : A₀ ⟶ A₁) (ri : A₁ ⟶ A) (o : A₀ ⟶ A) (s s' : A ⟶ B) (r r' : A₁ ⟶ B₁) (rj : B₁ ⟶ B) (hpi : CategoryStruct.comp pi ri = o) (h1 : CategoryStruct.comp r rj = CategoryStruct.comp ri s) (h1' : CategoryStruct.comp r' rj = CategoryStruct.comp ri s') (hrr : r = r') : CategoryStruct.comp o s = CategoryStruct.comp o s'

Two morphisms whose restrictions along a common inclusion agree, agree after the inclusion.

theorem CategoryTheory.over_of_conj {C : Type u_1} [Category.{u_2, u_1} C] {A' A B B' Y Y' Z : C} (εi_inv : A' ⟶ A) (εj_hom : B ⟶ B') (s : A ⟶ B) (ofRA : A ⟶ Y) (ofRA' : A' ⟶ Y) (ofRB : B ⟶ Y') (ofRB' : B' ⟶ Y') (πA : Y ⟶ Z) (πB : Y' ⟶ Z) (hεi : CategoryStruct.comp εi_inv ofRA = ofRA') (hεj : CategoryStruct.comp εj_hom ofRB' = ofRB) (hs : CategoryStruct.comp ofRA πA = CategoryStruct.comp (CategoryStruct.comp s ofRB) πB) : CategoryStruct.comp ofRA' πA = CategoryStruct.comp (CategoryStruct.comp (CategoryStruct.comp εi_inv (CategoryStruct.comp s εj_hom)) ofRB') πB

A morphism over the base, conjugated by two identifications over the base, is over the base.

theorem AnalyticSpace.KLocallyRingedSpace.pieceIncl_comp_restrictIncl {K : Type} [RCLike K] {A Z : KLocallyRingedSpace K} (πA : A ⟶ Z) (O : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) {ι : Type u_1} (N : ι → TopologicalSpace.Opens ↑↑Z.toPresheafedSpace) (hN : ∀ (i : ι), N i ≤ O) (i : ι) : CategoryTheory.CategoryStruct.comp (pieceIncl πA O N i) (A.restrictIncl ⋯) = (A.restrictOpen ((TopologicalSpace.Opens.comap { toFun := Hom.toFun πA, continuous_toFun := ⋯ }) O)).ofRestrict (glueCoverOpens πA O N i)

For the cover of A|πA⁻¹O by the parts over the N i: the inclusion of a member of the cover into the part over N i, followed by the inclusion of that part into A|πA⁻¹O, is the open immersion of the member (both agree after the open immersion into A).

theorem Hironaka.Manifold.PieceEmbedding.exists_localTransition_pair {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {n m : ℕ} {V V' : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (E' : PieceEmbedding 𝕜 m X V') (hV : IsOpen V) (hV' : IsOpen V') (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW : IsCompact (closure ↑W)) (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 E'.G).carrier) (hW' : IsCompact (closure ↑W')) (O' : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hO' : O' ≤ E.domOpens W ⊓ E'.domOpens W') {z : ↑↑X.toPresheafedSpace} (hz : z ∈ O') : ∃ (P : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (_ : z ∈ P) (_ : P ≤ O') (θ : (E.localResolution bed W hW).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (E.toSpaceMap bed W hW), continuous_toFun := ⋯ }) P) ⟶ (E'.localResolution bed W' hW').restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (E'.toSpaceMap bed W' hW'), continuous_toFun := ⋯ }) P)), CategoryTheory.IsIso θ ∧ CategoryTheory.CategoryStruct.comp ((E.localResolution bed W hW).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (E.toSpaceMap bed W hW), continuous_toFun := ⋯ }) P)) (E.toSpaceMap bed W hW) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp θ ((E'.localResolution bed W' hW').ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (E'.toSpaceMap bed W' hW'), continuous_toFun := ⋯ }) P))) (E'.toSpaceMap bed W' hW') ∧ ∀ (s : (E.localResolution bed W hW).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (E.toSpaceMap bed W hW), continuous_toFun := ⋯ }) P) ⟶ (E'.localResolution bed W' hW').restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (E'.toSpaceMap bed W' hW'), continuous_toFun := ⋯ }) P)), CategoryTheory.IsIso s → CategoryTheory.CategoryStruct.comp ((E.localResolution bed W hW).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (E.toSpaceMap bed W hW), continuous_toFun := ⋯ }) P)) (E.toSpaceMap bed W hW) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s ((E'.localResolution bed W' hW').ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (E'.toSpaceMap bed W' hW'), continuous_toFun := ⋯ }) P))) (E'.toSpaceMap bed W' hW') → s = θ

The local transition at a point for two embeddings E, E' of two pieces, in the PAIR form (LocalEmbeddingData.exists_localTransition is its instance) — for z in an open O' of the common base open, a cover member P ∋ z, P ≤ O', carrying the UNIQUE isomorphism over X between the parts of the two local resolutions over P (exists_transitionData_pair + exists_transition_over_pair).

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

The local transition at a point — for z in an open O' of the common base open of the pieces i, j, a cover member P ∋ z, P ≤ O', carrying the UNIQUE isomorphism over X between the parts of the two local resolutions over P (exists_transitionData + exists_transition_over).

theorem Hironaka.Manifold.LocalEmbeddingData.transition_unique {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) (i j : D.ι) (O : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (hO : O ≤ D.pieceDom i (W i) ⊓ D.pieceDom j (W j)) (s s' : (D.pieceR bed W hW i).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.pieceToSpace bed i (W i) ⋯), continuous_toFun := ⋯ }) O) ⟶ (D.pieceR bed W hW j).restrictOpen ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.pieceToSpace bed j (W j) ⋯), continuous_toFun := ⋯ }) O)) (hs : CategoryTheory.IsIso s) (hs' : CategoryTheory.IsIso s') (hc : CategoryTheory.CategoryStruct.comp (((D.embedding i).localResolution bed (W i) ⋯).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.pieceToSpace bed i (W i) ⋯), continuous_toFun := ⋯ }) O)) (D.pieceToSpace bed i (W i) ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s ((D.pieceR bed W hW j).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.pieceToSpace bed j (W j) ⋯), continuous_toFun := ⋯ }) O))) (D.pieceToSpace bed j (W j) ⋯)) (hc' : CategoryTheory.CategoryStruct.comp (((D.embedding i).localResolution bed (W i) ⋯).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.pieceToSpace bed i (W i) ⋯), continuous_toFun := ⋯ }) O)) (D.pieceToSpace bed i (W i) ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp s' ((D.pieceR bed W hW j).ofRestrict ((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.pieceToSpace bed j (W j) ⋯), continuous_toFun := ⋯ }) O))) (D.pieceToSpace bed j (W j) ⋯)) : s = s'

The transition is unique (Kollár's "the required uniqueness", [Kol07, Theorem 36, proof]; with the independence as the hypothesis hind): two isomorphisms over X between the parts of two pieces over a common base open O agree — on every cover member P_z both restrict (restrictOver) to isomorphisms over X, hence to the unique local transition, and morphisms agreeing on a cover agree (hom_ext_of_cover).

theorem Hironaka.Manifold.LocalEmbeddingData.exists_transition {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (W : (i : D.ι) → TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (hW : ∀ (i : D.ι), IsCompact (closure ↑(W i))) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) (i j : D.ι) : ∃ (t : (D.pieceR bed W hW i).restrictOpen (D.pieceGlueOpens bed W hW i j) ⟶ (D.pieceR bed W hW j).restrictOpen (D.pieceGlueOpens bed W hW j i)), CategoryTheory.IsIso t ∧ CategoryTheory.CategoryStruct.comp ((D.pieceR bed W hW i).ofRestrict (D.pieceGlueOpens bed W hW i j)) (D.pieceToSpace bed i (W i) ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp t ((D.pieceR bed W hW j).ofRestrict (D.pieceGlueOpens bed W hW j i))) (D.pieceToSpace bed j (W j) ⋯)

The transition of two pieces (Włodarczyk's isomorphisms over the overlaps Ṽ_i ∩ Ṽ_j, [Wlo09, §4, (3)⇒(4)]; with the independence as the hypothesis hind) — an isomorphism over X between the parts of their local resolutions over the common base open: exists_isIso_over_of_cover glues the local transitions of the cover members P_z (exists_localTransition), with transition_unique as the uniqueness hypothesis, and the result is read onto the gluing opens pieceGlueOpens (the same opens, spelled through overOpens; restrictOpenIsoOfSetEq).