The resolution is a locally finite ambient blow-up composite

Kollár's resolution functor is projective over every compact subset [Kol07, Theorem 45(4)]; Włodarczyk's res_{Y,M} factors locally into a sequence of blow-ups at smooth centres, the factorization (∗) of [Wlo09, Theorem 2.0.2]. Here: over every relatively compact open V ⊆ X the resolution map Π_X is the composite of a finite sequence of blow-ups of the disjoint union of the pieces' ambients, restricted to strict transforms (clause (4) of exists_functorial_resolution, ResolutionAssembly.lean). The steps: an exhaustion member Uₙ ⊇ closure V, the datum Dₙ over Uₙ with its gluing Γₙ, the factorization of AmbientLift.lean at the SHRUNK family Γₙ.W i ⊓ Aᵢ (Aᵢ the trace of Uₙ on the ambient — every open of a piece is the preimage of an open of its ambient under the closed embedding ambientPoint), so that the pieces lie inside Uₙ, and the transport ofIsoOver (Hironaka/Resolution/Analytic/Kol07Thm45/AmbientFactorizationTransport.lean) along the exhaustion glue's identification of the part of R(X) over Uₙ with resolutionOn Dₙ.

Not in the sources beyond the statements cited; bookkeeping.

theorem Hironaka.Manifold.PieceEmbedding.exists_opens_embPreimage_eq {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {X : AnalyticSpace 𝕜} {V : Set ↑↑X.toPresheafedSpace} (E : PieceEmbedding 𝕜 n X V) (O : Set ↑↑X.toPresheafedSpace) (hO : IsOpen O) : ∃ (A : TopologicalSpace.Opens (pieceAmbient 𝕜 E.G).carrier), E.embPreimage A = Subtype.val ⁻¹' O

Every open of the piece X|V is, through the closed embedding ambientPoint, the trace of an open of the ambient Gᵢ (IsInducing.isOpen_iff).

theorem Hironaka.Manifold.LocalEmbeddingData.pieceDom_inf_eq_inter {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (i : D.ι) (W A : TopologicalSpace.Opens (pieceAmbient 𝕜 (D.embedding i).G).carrier) (O : Set ↑↑X.toPresheafedSpace) (hA : (D.embedding i).embPreimage A = Subtype.val ⁻¹' O) : ↑(D.pieceDom i (W ⊓ A)) = ↑(D.pieceDom i W) ∩ O

Shrinking the ambient open to the trace of O shrinks the base open to O: pieceDom i (W ⊓ A) = pieceDom i W ∩ O when embPreimage A = val ⁻¹' O.

theorem Hironaka.Manifold.LocalEmbeddingData.exists_ambientBlowUpFactorization_resolutionOnFullMap_of_subset {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) (V O : Set ↑↑X.toPresheafedSpace) (hO : IsOpen O) (hVO : V ⊆ O) (hVU : V ⊆ U) : ∃ (F : AnalyticSpace.Hom.AmbientBlowUpFactorization (D.resolutionOnFullMap bed) V), ∀ (i : F.ι), F.piece i ⊆ O

The ambient blow-up factorization at any open V ⊆ U, with the pieces inside a prescribed open O ⊇ V ([Kol07, Theorem 45(4)]): the factorization of the glued space's map at the gluing datum with the shrunk family Γ.W i ⊓ Aᵢ (Aᵢ the trace of O), with the independence of the local resolution as hind.

theorem Hironaka.Manifold.BEDanFamStar.ExhaustionGluing.exists_closure_subset_U {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) (X : AnalyticSpace 𝕜) (Ξ : bed.ExhaustionGluing X) (V : Set ↑↑X.toPresheafedSpace) (hV : IsCompact (closure V)) : ∃ (n : ℕ), closure V ⊆ ↑(Ξ.U n)

A relatively compact open lies in some member of the exhaustion (IsCompact.elim_directed_cover on the increasing Uₙ).

theorem Hironaka.Manifold.BEDanFamStar.ExhaustionGluing.coe_openOf_preimage_U {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) (X : AnalyticSpace 𝕜) (Ξ : bed.ExhaustionGluing X) (n : ℕ) : ↑(Ξ.glue.gluedOver.openOf (AnalyticSpace.KLocallyRingedSpace.Hom.toFun Ξ.glue.descMap ⁻¹' ↑(Ξ.U n))) = ↑((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun Ξ.glue.descMap, continuous_toFun := ⋯ }) (Ξ.U n))

The two spellings of the part of R(X) over Uₙ. Internal.

theorem Hironaka.Manifold.BEDanFamStar.ExhaustionGluing.coe_comap_resolutionOnToSpace_U {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) (X : AnalyticSpace 𝕜) (Ξ : bed.ExhaustionGluing X) (n : ℕ) : ↑((TopologicalSpace.Opens.comap { toFun := AnalyticSpace.KLocallyRingedSpace.Hom.toFun ((Ξ.D n).resolutionOnToSpace bed), continuous_toFun := ⋯ }) (Ξ.U n)) = ↑⊤

The part of the piece resolutionOn Dₙ over Uₙ is the whole piece (range_subset). Internal.

noncomputable def Hironaka.Manifold.BEDanFamStar.ExhaustionGluing.resolutionOnIso {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) (X : AnalyticSpace 𝕜) (Ξ : bed.ExhaustionGluing X) (n : ℕ) : (Ξ.glue.gluedOver.restrictSet (AnalyticSpace.KLocallyRingedSpace.Hom.toFun Ξ.glue.descMap ⁻¹' ↑(Ξ.U n))).toKLocallyRingedSpace ≅ ((Ξ.D n).resolutionOn bed).toKLocallyRingedSpace

The part of R(X) over Uₙ IS resolutionOn (D n) bed: the exhaustion glue's partIso at Uₙ = dom n (the part of the piece over Uₙ is the whole piece, range_subset).

Equations

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

theorem Hironaka.Manifold.BEDanFamStar.ExhaustionGluing.resolutionOnMap_comp_resolutionOnIso {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) (X : AnalyticSpace 𝕜) (Ξ : bed.ExhaustionGluing X) (n : ℕ) : CategoryTheory.CategoryStruct.comp (resolutionOnIso bed X Ξ n).hom ((Ξ.D n).resolutionOnMap bed) = AnalyticSpace.Hom.restrictSet Ξ.glue.descMap ↑(Ξ.U n)

It lies over X|Uₙ: Π_{Uₙ} ∘ e = des|Uₙ (the hypothesis hcomm of the transport ofIsoOver).

theorem Hironaka.Manifold.BEDanFamStar.isLocallyFiniteAmbientBlowUpComposite_resolutionMap_of_independent {𝕜 : Type} [RCLike 𝕜] (bed : BEDanFamStar 𝕜) (X : AnalyticSpace 𝕜) (hX : X.IsReduced) (hbed : IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) : AnalyticSpace.Hom.IsLocallyFiniteAmbientBlowUpComposite (bed.resolutionMap X)

Π_X is a locally finite ambient blow-up composite (clause (4) of exists_functorial_resolution; [Kol07, Theorem 45(4)]; the local factorization (∗) of [Wlo09, Theorem 2.0.2]), with the independence of the local resolution as hind: over every relatively compact open V, the factorization of the glued space over the exhaustion member Uₙ ⊇ closure V with its pieces inside Uₙ, transported along the part identification (ofIsoOver).