Documentation

Hironaka.Resolution.Analytic.Kol07Thm45.GluingProperties

The resolution of analytic spaces: the gluing and its global properties #

The theorems of the gluing of the local resolutions over an exhaustion and the properties of the glued resolution R(X) → X, in their final form: each is the corresponding theorem of the preceding modules with the independence of the local resolution from the embedding discharged by localResolution_independent_of_local (LocalResolutionIndependent.lean) at the local form localResolution_independent_local (LocalResolutionShear.lean) —

The sources are Kollár's Theorem 45 with its proof through Proposition 37 [Kol07, Theorem 45], [Kol07, Proposition 37], Włodarczyk's gluing over an open cover by relatively compact opens [Wlo09, §4.3], and the countability at infinity of an analytic space [Hir64, Ch. 0, §1, p. 120].

source
theorem Hironaka.Manifold.localResolutionIndependentOn_of_isEmbeddedDesing (𝕜 : Type) [RCLike 𝕜] (X : AnalyticSpace 𝕜) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) :
LocalResolutionIndependentOn X bed

The independence of the local resolution from the embedding, as the proposition LocalResolutionIndependentOn X bed that the gluing theorems take as their hypothesis hind — localResolution_independent_of_local (LocalResolutionIndependent.lean) at the local form localResolution_independent_local (LocalResolutionShear.lean).

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

The local resolutions of the pieces of a local embedding datum glue — resolutionGluesOn_of_isEmbeddedDesing_of_independent (PieceGlueDatum.lean) at the independence.

source
theorem Hironaka.Manifold.resolutionGlues_of_isEmbeddedDesing (𝕜 : Type) [RCLike 𝕜] (X : AnalyticSpace 𝕜) (hX : X.IsReduced) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) :
bed.ResolutionGlues X

The resolution glues along an exhaustion — resolutionGlues_of_isEmbeddedDesing_of_independent (PieceGlueIndep.lean) at the independence.

source
theorem Hironaka.Manifold.resolution_clauses_of_isEmbeddedDesing (𝕜 : Type) [RCLike 𝕜] (X : AnalyticSpace 𝕜) (hX : X.IsReduced) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) :
(bed.resolution X).IsNonsingular ∧ AnalyticSpace.Hom.IsIsoOver (bed.resolutionMap X) X.regularLocus ∧ (bed.resolution X).IsSncDivisorSet (↑(bed.resolutionMap X) ⁻¹' X.singularLocus) ∧ AnalyticSpace.Hom.IsLocallyFiniteAmbientBlowUpComposite (bed.resolutionMap X) ∧ ∀ (Y : AnalyticSpace 𝕜), Y.IsReduced → ∀ (U : Set ↑↑X.toPresheafedSpace) (V : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsOpen V → ∀ (φ : X.restrictSet U ⟶ Y.restrictSet V), CategoryTheory.IsIso φ → ∃ (ψ : (bed.resolution X).restrictSet (↑(bed.resolutionMap X) ⁻¹' U) ⟶ (bed.resolution Y).restrictSet (↑(bed.resolutionMap Y) ⁻¹' V)), CategoryTheory.IsIso ψ ∧ CategoryTheory.CategoryStruct.comp ψ (AnalyticSpace.Hom.restrictSet (bed.resolutionMap Y) V) = CategoryTheory.CategoryStruct.comp (AnalyticSpace.Hom.restrictSet (bed.resolutionMap X) U) φ

The five clauses of exists_functorial_resolution for R(X) → X — non-singularity, the isomorphism over X.regularLocus, the simple normal crossings divisor set over X.singularLocus, the locally finite ambient blow-up composite, the functoriality for isomorphisms of open subspaces — each the theorem of the preceding modules at the independence (for X, and for Y in clause (5)).

source
theorem Hironaka.Manifold.range_resolutionMap_eq_closure_reg (𝕜 : Type) [RCLike 𝕜] (X : AnalyticSpace 𝕜) (hX : X.IsReduced) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) :
Set.range ↑(bed.resolutionMap X) = closure X.regularLocus

The range of Π_X is the closure of the simple locus — range_resolutionMap_eq_closure_reg_of_independent (ResolutionSnc.lean) at the independence.

source
theorem Hironaka.Manifold.resolutionOn_indep (𝕜 : Type) [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U U' : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (D' : LocalEmbeddingData 𝕜 X U') (hU : IsOpen U) (hUU' : U ⊆ U') (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 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, in the U ⊆ U' form — resolutionOn_indep_of_independent (PieceGlueIndep.lean) at the independence.

source
theorem Hironaka.Manifold.resolutionOn_indep_self (𝕜 : Type) [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D D' : LocalEmbeddingData 𝕜 X U) (hU : IsOpen U) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) :
∃! ψ : D.resolutionOn bed ⟶ D'.resolutionOn bed, CategoryTheory.IsIso ψ ∧ CategoryTheory.CategoryStruct.comp ψ (D'.resolutionOnMap bed) = D.resolutionOnMap bed

The U' = U instance of resolutionOn_indep.

source
theorem Hironaka.Manifold.nonempty_ambientBlowUpFactorization_resolutionOnFullMap (𝕜 : Type) [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) :
Nonempty (AnalyticSpace.Hom.AmbientBlowUpFactorization (D.resolutionOnFullMap bed) U)

The ambient blow-up factorization of the glued space's map at U — nonempty_ambientBlowUpFactorization_resolutionOnFullMap_of_independent (AmbientLift.lean) at the independence.