The gluing datum of the local resolutions: the pieces and their ambient opens

Włodarczyk glues the canonical desingularizations of the local embeddings of an analytic space into a desingularization of the space [Wlo09, §4, (3)⇒(4)]. For local embedding data D : LocalEmbeddingData 𝕜 X U (inner opens V_i ⋐ U_i with compact closures, covering U), this module holds the piece-level notions of the proof that the local resolutions glue (ResolutionGluesOn, PieceGlue.lean; proved in PieceGlueDatum.lean as LocalEmbeddingData.resolutionGluesOn_of_isEmbeddedDesing_of_independent) that need no gluing yet:

• LocalEmbeddingData.pieceR D bed W hW i and pieceGlueOpens D bed W hW i j: the pieces Ỹ_i := localResolution (D.embedding i) bed (W i) _ of the gluing datum and their gluing opens (GlueOver.glueOpens, the points over the overlaps pieceDom i ⊓ pieceDom j);
• LocalResolutionIndependentOn X bed: the independence of the local resolution from the embedding, as a hypothesis — the conclusion of localResolution_independent_of_local (LocalResolutionIndependent.lean) for a fixed X, the input of the transitions between the pieces; discharged from IsEmbeddedDesing in GluingProperties.lean;
• LocalEmbeddingData.exists_W D i: the relatively compact ambient open W_i of the piece whose base open contains closure (inner i) (Włodarczyk's V̄_i ⊂ W_i) — the ambient image of the compact closure (inner i) (pulled into the piece along the closed embedding ambientPoint) is compact in the ambient G_i, and exists_opens_isCompact_closure_superset (the ambient being locally compact Hausdorff) gives W_i ⋐ G_i around it.

Not in the sources beyond Włodarczyk's construction; bookkeeping.

def Hironaka.Manifold.LocalResolutionIndependentOn {𝕜 : Type} [RCLike 𝕜] (X : AnalyticSpace 𝕜) (bed : BEDanFamStar 𝕜) : Prop

The independence of the local resolution from the embedding, as a hypothesis: for two piece embeddings E₁, E₂ of the same open V ⊆ X and relatively compact ambient opens W₁, W₂, the local resolutions restricted over embPreimage W₁ ∩ embPreimage W₂ are isomorphic over the piece by a UNIQUE isomorphism — the conclusion of localResolution_independent_of_local (LocalResolutionIndependent.lean) for a fixed X, with the functor bed outside the quantifier. The theorems of the gluing take this proposition as a hypothesis hind; localResolutionIndependentOn_of_isEmbeddedDesing (GluingProperties.lean) discharges it from IsEmbeddedDesing.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.LocalEmbeddingData.pieceR {𝕜 : 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))) (i : D.ι) : AnalyticSpace 𝕜

The pieces of the gluing datum — the local resolutions of the pieces of D over the chosen ambient opens (Włodarczyk's Ṽ_i, [Wlo09, §4, (3)⇒(4)]).

Equations

• D.pieceR bed W hW i = (D.embedding i).localResolution bed (W i) ⋯

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.LocalEmbeddingData.pieceGlueOpens {𝕜 : 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))) (i j : D.ι) : TopologicalSpace.Opens ↑↑(D.pieceR bed W hW i).toPresheafedSpace

The gluing opens of the pieces — the points of Ỹ_i over the overlap pieceDom i ⊓ pieceDom j of the base opens (GlueOver.glueOpens; [Wlo09, §4, (3)⇒(4)]).

Equations

• D.pieceGlueOpens bed W hW i j = AnalyticSpace.GlueOver.glueOpens X (D.pieceR bed W hW) (fun (i : D.ι) => D.pieceToSpace bed i (W i) ⋯) (fun (i : D.ι) => D.pieceDom i (W i)) i j

theorem Hironaka.Manifold.LocalEmbeddingData.exists_W {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (i : D.ι) : ∃ (W' : TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier), IsCompact (closure ↑W') ∧ closure (D.inner i) ⊆ ↑(D.pieceDom i W')

The ambient opens of the gluing datum (Włodarczyk's V̄_i ⊂ W_i, [Wlo09, §4, (3)⇒(4)]) — each inner closure lies over a relatively compact open of the piece's ambient: the ambient image of the compact closure (inner i) is compact (isClosedEmbedding_ambientPoint), and exists_opens_isCompact_closure_superset puts a relatively compact open around it in the locally compact Hausdorff ambient G_i.