Gluing the local resolutions of the pieces over a relatively compact open

Włodarczyk glues the canonical desingularizations of the germs of an open cover: for a cover of a compact set Z by opens V_i ⊂ W_i ⊂ U_i with V̄_i ⊂ W_i and W̄_i ⊂ U_i compact, the desingularization of the germ at W̄_i determines the desingularization Ṽ_i → V_i, the embeddings Y_{Z_i ∩ Z_j} → Y_{Z_i} lift to embeddings of the desingularizations, and Ṽ is the manifold obtained by gluing the Ṽ_i along the Ṽ_i ∩ Ṽ_j, with des_V : Ṽ → V bimeromorphic and proper [Wlo09, §4, (3)⇒(4)]; the desingularization of a whole space is then assembled from the restrictions des_i⁻¹(U_i) → U_i [Wlo09, §4.3]. Kollár glues the resolutions of the members of an affine cover through the commutation with smooth surjections ([Kol07, Theorem 36, proof] and [Kol07, Proposition 37]). For local embedding data D : LocalEmbeddingData 𝕜 X U and an embedded desingularization functor bed : BEDanFamStar 𝕜:

• PieceEmbedding.domOpens E W: the base open of a piece embedding over an ambient open W — the points of the piece whose ambient point lies in W (Włodarczyk's W_i, read in X); PieceEmbedding.toSpaceMap E bed W hW: the local resolution's map to X (localResolutionToPiece followed by the open immersion of the piece), landing in domOpens; LocalEmbeddingData.pieceDom D i W and LocalEmbeddingData.pieceToSpace D bed i W hW are the two at the i-th piece;
• LocalEmbeddingData.ResolutionGluing D bed: the gluing datum — the chosen ambient opens W_i with compact closures containing the ambient points of closure (inner i), and a GlueOver of the local resolutions localResolution (D.embedding i) bed (W i) _ over X along the overlaps pieceDom i ∩ pieceDom j (the transitions are the unique isomorphisms between the local resolutions of two pieces restricted to the overlap, the cocycle identity follows from the same uniqueness, and the glued space is Hausdorff by the closed-graph criterion); its existence under hbed : bed.IsEmbeddedDesing is proved in GluingProperties.lean (resolutionGluesOn_of_isEmbeddedDesing, through PieceGlueDatum.lean), the proposition being LocalEmbeddingData.ResolutionGluesOn D bed := Nonempty (ResolutionGluing D bed) (the analytic counterpart of Hironaka.Resolution.BRDescends);
• LocalEmbeddingData.resolutionOnFullPair D bed: the glued space with its descended map to X when a gluing datum exists (chosen), the pair ⟨X, 𝟙 X⟩ otherwise (a fallback value, never taken under hbed, as the nil X of Hironaka.Resolution.Algebraic.Kol07.Thm36.BR) — the sigma pair keeps the map's type uniform across the two branches; resolutionOnFull/resolutionOnFullMap its components (des_V : Ṽ → V, over the union of the pieceDom);
• LocalEmbeddingData.resolutionOn D bed, the glued space restricted over U, and LocalEmbeddingData.resolutionOnMap D bed : resolutionOn D bed ⟶ X.restrictSet U — Włodarczyk's Ũ_i := des_i⁻¹(U_i) → U_i [Wlo09, §4.3]; resolutionOnToSpace the same map into X. The unfolding lemmas resolutionOnFullPair_eq_of_glues / _of_not_glues, resolutionOnFull_eq_of_glues / _of_not_glues record the two branches.

The gluing locus is pieceDom i ⊓ pieceDom j — the parts of the two pieces OVER W_i, W_j (range_localResolutionToPiece_subset) — the transcription of Włodarczyk's V_i ⊂ W_i ⊂ U_i, matching the overlap embPreimage W₁ ∩ embPreimage W₂ on which two local resolutions of one piece are compared. hbed binds no definition: membership in the class is a hypothesis of the theorems, never of a definition.

def Hironaka.Manifold.PieceEmbedding.domOpens {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) : TopologicalSpace.Opens ↑↑X.toPresheafedSpace

The base open of a piece embedding over the ambient open W: the points of X in the piece whose ambient point lies in W (embPreimage pushed into X): the open W_i of Włodarczyk's cover V_i ⊂ W_i ⊂ U_i [Wlo09, §4, (3)⇒(4)].

Equations

• E.domOpens W = { carrier := Subtype.val '' E.embPreimage W, is_open' := ⋯ }

theorem Hironaka.Manifold.PieceEmbedding.mem_domOpens {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier} {x : ↑↑X.toPresheafedSpace} : x ∈ E.domOpens W ↔ ∃ y ∈ E.embPreimage W, ↑y = x

Membership in the base open: the image in X of a point of the piece over W.

theorem Hironaka.Manifold.PieceEmbedding.domOpens_mono {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) {Q W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier} (h : Q ≤ W) : E.domOpens Q ≤ E.domOpens W

The base open is monotone in the ambient open.

noncomputable def Hironaka.Manifold.PieceEmbedding.toSpaceMap {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (bed : BEDanFamStar 𝕜) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW : IsCompact (closure ↑W)) : (E.localResolution bed W hW).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace

The local resolution's map to X: Π (localResolutionToPiece) followed by the open immersion of the piece: Włodarczyk's desingularization Ṽ_i → V_i ⊆ Y [Wlo09, §4, (3)⇒(4)].

Equations

• E.toSpaceMap bed W hW = CategoryTheory.CategoryStruct.comp (E.localResolutionToPiece bed W hW) (X.ofRestrict (X.openOf V))

theorem Hironaka.Manifold.PieceEmbedding.range_toFun_toSpaceMap_subset {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (bed : BEDanFamStar 𝕜) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) (hW : IsCompact (closure ↑W)) : Set.range (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (E.toSpaceMap bed W hW)) ⊆ ↑(E.domOpens W)

The map to X lands in the base open (range_localResolutionToPiece_subset).

@[reducible, inline]

abbrev Hironaka.Manifold.LocalEmbeddingData.pieceDom {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (i : D.ι) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) : TopologicalSpace.Opens ↑↑X.toPresheafedSpace

The base open of the i-th piece over the ambient open W: domOpens of the i-th embedding (the open W_i of Włodarczyk's cover V_i ⊂ W_i ⊂ U_i [Wlo09, §4, (3)⇒(4)]).

Equations

• D.pieceDom i W = (D.embedding i).domOpens W

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.LocalEmbeddingData.pieceToSpace {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (i : D.ι) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (hW : IsCompact (closure ↑W)) : ((D.embedding i).localResolution bed W hW).toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace

The piece map to X: toSpaceMap of the i-th embedding (Włodarczyk's desingularization Ṽ_i → V_i of V_i ⊂ U_i, read into Y [Wlo09, §4, (3)⇒(4)]).

Equations

• D.pieceToSpace bed i W hW = (D.embedding i).toSpaceMap bed W hW

structure Hironaka.Manifold.LocalEmbeddingData.ResolutionGluing {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) : Type u

A gluing datum for the local resolutions of the pieces of D — the ambient opens W_i ⋐ G_i over which the pieces are resolved, containing the ambient points of closure (inner i) (Włodarczyk's V̄_i ⊂ W_i), and the gluing data over X (GlueOver) of the local resolutions localResolution (D.embedding i) bed (W i) _ along the overlaps pieceDom i ∩ pieceDom j, with a Hausdorff glued space (the gluing of the Ṽ_i in [Wlo09, §4, (3)⇒(4)]).

• W (i : D.ι) : TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier

  The relatively compact ambient opens over which the pieces are resolved.

• isCompact_closure_W (i : D.ι) : IsCompact (closure ↑(self.W i))
• closure_inner_subset_pieceDom (i : D.ι) : closure (D.inner i) ⊆ ↑(D.pieceDom i (self.W i))

  V̄_i ⊂ W_i: the inner opens lie over the chosen ambient opens [Wlo09, §4, (3)⇒(4)].

• glue : X.GlueOver (fun (i : D.ι) => (D.embedding i).localResolution bed (self.W i) ⋯) (fun (i : D.ι) => D.pieceToSpace bed i (self.W i) ⋯) fun (i : D.ι) => D.pieceDom i (self.W i)

  The gluing over X of the local resolutions along the overlaps of their base opens.

@[reducible, inline]

abbrev Hironaka.Manifold.LocalEmbeddingData.ResolutionGluesOn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) : Prop

A gluing datum exists (the analytic counterpart of Hironaka.Resolution.BRDescends); its proof under hbed : bed.IsEmbeddedDesing is resolutionGluesOn_of_isEmbeddedDesing (GluingProperties.lean).

Equations

• D.ResolutionGluesOn bed = Nonempty (D.ResolutionGluing bed)

noncomputable def Hironaka.Manifold.LocalEmbeddingData.resolutionOnFullPair {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) : (R : AnalyticSpace 𝕜) × (R ⟶ X)

The glued space with its descended map to X, over the union of the base opens (Włodarczyk's Ṽ with des_V : Ṽ → V [Wlo09, §4, (3)⇒(4)]) — the glued analytic space of a chosen gluing datum when one exists, the pair ⟨X, 𝟙 X⟩ otherwise (a fallback value, never taken under hbed, as the nil X of Hironaka.Resolution.Algebraic.Kol07.Thm36.BR).

Equations

• D.resolutionOnFullPair bed = if h : D.ResolutionGluesOn bed then ⟨(Nonempty.some h).glue.gluedOver, (Nonempty.some h).glue.descMap⟩ else ⟨X, CategoryTheory.CategoryStruct.id X⟩

noncomputable def Hironaka.Manifold.LocalEmbeddingData.resolutionOnFull {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) : AnalyticSpace 𝕜

The glued space over the union of the base opens (Włodarczyk's Ṽ).

Equations

• D.resolutionOnFull bed = (D.resolutionOnFullPair bed).fst

noncomputable def Hironaka.Manifold.LocalEmbeddingData.resolutionOnFullMap {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) : D.resolutionOnFull bed ⟶ X

The descended map des_V : Ṽ → V ⊆ X into X.

Equations

• D.resolutionOnFullMap bed = (D.resolutionOnFullPair bed).snd

noncomputable def Hironaka.Manifold.LocalEmbeddingData.resolutionOn {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) : AnalyticSpace 𝕜

The resolution over U, resolutionOn D bed — the glued space of the local resolutions of the pieces of D, restricted over U (Włodarczyk's Ũ_i := des_i⁻¹(U_i) [Wlo09, §4.3]).

Equations

• D.resolutionOn bed = (D.resolutionOnFull bed).restrictSet (↑(D.resolutionOnFullMap bed) ⁻¹' U)

noncomputable def Hironaka.Manifold.LocalEmbeddingData.resolutionOnMap {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) : D.resolutionOn bed ⟶ X.restrictSet U

The resolution map over U, Π_U = resolutionOnMap D bed : resolutionOn D bed → X|U (Włodarczyk's restriction Ũ_i := des_i⁻¹(U_i) → U_i [Wlo09, §4.3]).

Equations

• D.resolutionOnMap bed = AnalyticSpace.Hom.restrictSet (D.resolutionOnFullMap bed) U

noncomputable def Hironaka.Manifold.LocalEmbeddingData.resolutionOnToSpace {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) : D.resolutionOn bed ⟶ X

The resolution map read into X: Π_U followed by the open immersion X|U → X (the map of one member of the exhaustion by relatively compact opens from which the resolution of the whole space is glued).

Equations

• D.resolutionOnToSpace bed = CategoryTheory.CategoryStruct.comp (D.resolutionOnMap bed) (X.ofRestrict (X.openOf U))

Unfolding lemmas

theorem Hironaka.Manifold.LocalEmbeddingData.resolutionOnFullPair_eq_of_glues {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (h : D.ResolutionGluesOn bed) : D.resolutionOnFullPair bed = ⟨(Nonempty.some h).glue.gluedOver, (Nonempty.some h).glue.descMap⟩

With a gluing datum, the pair is the chosen datum's glued space and map.

theorem Hironaka.Manifold.LocalEmbeddingData.resolutionOnFullPair_eq_of_not_glues {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (h : ¬D.ResolutionGluesOn bed) : D.resolutionOnFullPair bed = ⟨X, CategoryTheory.CategoryStruct.id X⟩

Without a gluing datum, the pair is ⟨X, 𝟙 X⟩ (a branch never taken under hbed).

theorem Hironaka.Manifold.LocalEmbeddingData.resolutionOnFull_eq_of_glues {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (h : D.ResolutionGluesOn bed) : D.resolutionOnFull bed = (Nonempty.some h).glue.gluedOver

With a gluing datum, resolutionOnFull is the chosen datum's glued space.

theorem Hironaka.Manifold.LocalEmbeddingData.resolutionOnFull_eq_of_not_glues {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (h : ¬D.ResolutionGluesOn bed) : D.resolutionOnFull bed = X

Without a gluing datum, resolutionOnFull is X.

theorem Hironaka.Manifold.LocalEmbeddingData.resolutionOnFullMap_heq_of_not_glues {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (h : ¬D.ResolutionGluesOn bed) : D.resolutionOnFullMap bed ≍ CategoryTheory.CategoryStruct.id X

Without a gluing datum, the descended map is (heterogeneously) the identity.