The gluing datum of the local resolutions

Włodarczyk's gluing of the canonical desingularizations of the local embeddings [Wlo09, §4, (3)⇒(4)]: under hbed and the independence of the local resolution from the embedding (as the hypothesis LocalResolutionIndependentOn X bed), a gluing datum ResolutionGluing D bed exists — the relatively compact ambient opens W_i over the inner opens (exists_W), the transitions on the overlaps of the base opens (exists_transition), and GlueOver.exists_glueOver_of_transitions (Hironaka/AnalyticSpace/Glue/OverLemmas.lean), whose cocycle, t_id and Hausdorffness come from the UNIQUENESS of the transitions (transition_unique). This is the form of resolutionGluesOn_of_isEmbeddedDesing (GluingProperties.lean) with the independence as a hypothesis; that module discharges hind.

isProperMap_resolutionOnMap (Włodarczyk: des_V : Ṽ → V is proper, [Wlo09, §4, (3)⇒(4)]): the map Π_U : resolutionOn D bed → X|U is proper for an OPEN U. Over each base open pieceDom i (W i) the glued space is the local resolution Ỹ_i of the piece and the descended map is the piece map Π_i (GlueOver.isProperMap_restrictPreimage_descMap); Π_i : Ỹ_i → Sp(W)/𝓘|W is proper because it lies over the proper composite σ^r along the closed embedding of the strict transform (isProperMap_toFun_localResolutionMap), and Sp(W)/𝓘|W → X is an open immersion onto the base open (range_pieceOverIncl); the base opens cover U ⊆ ⋃ inner i (isProperMap_restrictPreimage_of_cover). Two remarks on the hypotheses: hU : IsOpen U is NECESSARY (for a non-open U the convention openOf makes Π_U the full map Ṽ → X, whose image is the open ⋃ pieceDom i), and the theorem takes no hypothesis on bed (without a gluing datum the pair is ⟨X, 𝟙 X⟩ and Π_U is the identity of X|U).

Kollár's counterpart is the gluing of the local resolutions by a formal property of blow-up sequence functors [Kol07, Theorem 36, proof]. Not in the sources beyond that; bookkeeping.

theorem Hironaka.Manifold.PieceEmbedding.isProperMap_toFun_localResolutionMap {𝕜 : 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)) : IsProperMap ↑(E.localResolutionMap bed W hW)

The local resolution map Π : Ỹ → Sp(W)/𝓘|W is proper (Włodarczyk's des proper, [Wlo09, §4, (3)⇒(4)]): ι_Y ∘ Π = Sp(σ^r) ∘ ι_Ỹ (localResolutionMap_comp_ι) with ι_Ỹ a closed embedding (isClosedEmbedding_toFun_toAnalyticSpaceι) and σ^r proper (isProperMap_stageMap), and ι_Y continuous injective (isProperMap_of_comp_of_inj).

theorem Hironaka.Manifold.PieceEmbedding.range_toFun_restrictedIdealHom {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (W : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier) : Set.range ↑(E.restrictedIdealHom W) = {z : ↑↑E.ideal.toAnalyticSpace.toPresheafedSpace | ↑E.ideal.toAnalyticSpaceι z ∈ W}

The range of the restriction-of-a-quotient map Sp(W)/𝓘|W → Sp(G)/𝓘 is the set of points over W: range_toFun_homOfPullbackEq at the open inclusion W ↪ G.

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

The open immersion of the piece over W into X, on points (Włodarczyk's Ṽ_i → V_i ⊆ Y, [Wlo09, §4, (3)⇒(4)]): the restriction-of-a-quotient map, the inverse of the embedding and the inclusion of the piece — the second factor of toSpaceMap = Π ≫ (Sp(W)/𝓘|W → X).

Equations

• E.pieceOverIncl W w = ↑(↑E.embInv (↑(E.restrictedIdealHom W) w))

theorem Hironaka.Manifold.PieceEmbedding.toFun_toSpaceMap_eq {𝕜 : 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)) (y : ↑↑(E.localResolution bed W hW).toPresheafedSpace) : AnalyticSpace.KLocallyRingedSpace.Hom.toFun (E.toSpaceMap bed W hW) y = E.pieceOverIncl W (↑(E.localResolutionMap bed W hW) y)

toSpaceMap on points is the open immersion of the piece over W after the local resolution map — the factorisation toSpaceMap = pieceOverIncl ∘ Π, rfl.

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

The open immersion of the piece over W is an open embedding on points: the three factors are open immersions (isOpenImmersion_restrictedIdealHom, isOpenImmersion_inv_emb, the inclusion of the open piece).

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

The open immersion of the piece over W lands onto the base open domOpens W: the points of the piece whose ambient point lies in W (range_toFun_restrictedIdealHom; embInv inverts the embedding).

theorem Hironaka.Manifold.PieceEmbedding.isProperMap_toSpaceMap_dom {𝕜 : 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)) : IsProperMap fun (y : ↑↑(E.localResolution bed W hW).toPresheafedSpace) => ⟨AnalyticSpace.KLocallyRingedSpace.Hom.toFun (E.toSpaceMap bed W hW) y, ⋯⟩

The piece map Ỹ → domOpens W onto its base open is proper (Włodarczyk's des_V proper on one piece, [Wlo09, §4, (3)⇒(4)]): Π : Ỹ → Sp(W)/𝓘|W is proper (isProperMap_toFun_localResolutionMap) and Sp(W)/𝓘|W → domOpens W is a homeomorphism (isOpenEmbedding_pieceOverIncl, range_pieceOverIncl).

theorem Hironaka.Manifold.LocalEmbeddingData.resolutionGluesOn_of_isEmbeddedDesing_of_independent {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) : D.ResolutionGluesOn bed

The local resolutions of the pieces of D glue ([Wlo09, §4, (3)⇒(4)]; Kol07, Theorem 36, proof) — resolutionGluesOn_of_isEmbeddedDesing (GluingProperties.lean) with the independence of the local resolution as the hypothesis hind: the ambient opens from exists_W, the transitions from exists_transition, the gluing datum from GlueOver.exists_glueOver_of_transitions with the uniqueness transition_unique supplying the cocycle, t_id and Hausdorffness.

theorem Hironaka.Manifold.LocalEmbeddingData.isProperMap_resolutionOnMap {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (hU : IsOpen U) : IsProperMap ↑(D.resolutionOnMap bed)

The map Π_U : resolutionOn D bed → X|U is proper for an open U (Włodarczyk's des_V : Ṽ → V proper, [Wlo09, §4, (3)⇒(4)]). With a gluing datum, over each base open pieceDom i (W i) the glued space is Ỹ_i and the descended map is the proper piece map Π_i (GlueOver.isProperMap_restrictPreimage_descMap_of_subset on the cover {pieceDom i (W i)} of U ⊆ ⋃ inner i); without one, the pair is ⟨X, 𝟙 X⟩ and Π_U is the identity of X|U. No hypothesis on bed is needed, and hU : IsOpen U is necessary.