The local resolution map is an isomorphism over the simple locus

For an embedded desingularization functor bed (bed.IsEmbeddedDesing) and a piece of an analytic space (a closed subspace Y|_W of a relatively compact open W of an ambient manifold), the local resolution map P = σ^r|_{Ỹ} : Ỹ → Y|_W, the restriction of the composite blow-down to the final strict transform, is an isomorphism over the simple locus (Y|_W).regularLocus (Hom.IsIsoOver). This is clause (1) of Włodarczyk's resolution of analytic spaces Wlo09, Theorem 2.0.1, "res_Y : Ỹ → Y is an isomorphism over the nonsingular part of Y", deduced from clauses (2)–(3) of [Wlo09, Theorem 2.0.2] as in the proof of resolution from principalization in [Kol07, Theorem 27]; the algebraic counterpart is isIso_composite_restrict_of_centers_disjoint.

Proof. Clause (2) of the embedded desingularization says that no centre lies over a simple point: CentersOver (regSet)ᶜ (IsEmbeddedDesing.centersOver_compl_regSet). Along the sequence this gives, by induction on the stage: the exceptional divisors lie over (regSet)ᶜ (support_totalTransformSeq_subset_preimage_of_centersOver); off the exceptional family the germ map of the composite σ^i is bijective (germMap_stageMap_bijective_of_notMem_support, from the one-step statement IsBlowUp.germMap_bijective_of_notMem) and the strict transform is the pullback stalkwise (stalkIdeal_strictTransformSubspaceSeq_eq_map_of_notMem_support, from stalkIdeal_strictTransformSubspace_of_notMem_cosupport_of_hasLocalGenerators, the finite-type input discharged by saturationStalk_hasLocalGenerators); hence the whole preimage of regSet lies in Ỹ (preimage_subset_cosupport_strictTransformSubspaceSeq_of_centersOver). The composite σ^r is an analytic isomorphism over regSet (isAnalyticIsoOver_stageMap; cf. [Kol07, Theorem 35 (3)]), so P is bijective from P⁻¹(Reg) onto Reg; its stalk maps there are isomorphisms (isIso_map_stalkMap_of_bijective with fiberMap_bijective_of_stalkIdeal_eq_map); the criterion isIso_restrictTo_of_bijOn_of_bijective_stalkMap makes the restriction an isomorphism of analytic spaces, which is the predicate IsIsoOver through Hom.restrictSet_eq_restrictTo.

This is one of the clauses from which the resolution of analytic spaces is assembled in Hironaka/Manifold/Sequence/Restrict/.

theorem AnalyticManifold.FiniteSuccession.germMap_stageMap_bijective_of_notMem_support {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : Fin (S.length + 1)) {z : (S.stage i).carrier} (hz : z ∉ (S.totalTransformSeq i).support) : Function.Bijective ⇑(Manifold.germMap ⇑(S.stageMap i) ⋯ z)

Off the exceptional family the germ map of the composite σ^i : U_i → M is bijective: the composite of the germ maps of the blow-ups, each bijective off its exceptional divisor (IsBlowUp.germMap_bijective_of_notMem).

theorem AnalyticManifold.FiniteSuccession.stalkIdeal_strictTransformSubspaceSeq_eq_map_of_notMem_support {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (J : M.IdealSheaf) (i : Fin (S.length + 1)) {z : (S.stage i).carrier} (hz : z ∉ (S.totalTransformSeq i).support) : Manifold.IdealSheaf.stalkIdeal (S.strictTransformSubspaceSeq J i) z = Ideal.map (Manifold.germMap ⇑(S.stageMap i) ⋯ z) (Manifold.IdealSheaf.stalkIdeal J ((S.stageMap i) z))

Off the exceptional family the strict transform is the pullback, stalkwise: the stalk of Y_i at z is the image of the stalk of J at σ^i z under the germ map (stalkIdeal_strictTransformSubspace_of_notMem_cosupport_of_hasLocalGenerators iterated, the finite-type input by saturationStalk_hasLocalGenerators).

theorem AnalyticManifold.FiniteSuccession.support_totalTransformSeq_subset_preimage_of_centersOver {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {Z : Set M.carrier} (hZ : S.CentersOver Z) (i : Fin (S.length + 1)) : (S.totalTransformSeq i).support ⊆ ⇑(S.stageMap i) ⁻¹' Z

When every centre lies over Z, so does every exceptional divisor: a point of the new divisor maps into the centre, the rest is the induction hypothesis.

theorem AnalyticManifold.FiniteSuccession.preimage_subset_cosupport_strictTransformSubspaceSeq_of_centersOver {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (J : M.IdealSheaf) {Z : Set M.carrier} (hZ : S.CentersOver Zᶜ) (hZJ : Z ⊆ Manifold.IdealSheaf.support J) (i : Fin (S.length + 1)) : ⇑(S.stageMap i) ⁻¹' Z ⊆ Manifold.IdealSheaf.support (S.strictTransformSubspaceSeq J i)

Over a subset Z of the support of J missed by every centre, the strict transform contains the whole preimage of Z: off the exceptional family its stalk is the image of the stalk of J under a bijection, hence proper where the stalk of J is.

theorem Hironaka.Manifold.BEDanFamStar.IsEmbeddedDesing.centersOver_compl_regSet {𝕜 : Type} [RCLike 𝕜] {bed : BEDanFamStar 𝕜} (hbed : IsEmbeddedDesing 𝕜 bed) (n : ℕ) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : DomBEDan 𝕜 T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (((bed.fam n).fam T hT).seqOn U hU).toSuccession.CentersOver (T.pullback (M.inclusion U) ⋯).I.regSetᶜ

Clause (2) of IsEmbeddedDesing (clause (2) of [Wlo09, Theorem 2.0.2]) as CentersOver: every centre of every value lies over the complement of the simple locus regSet (T|U).I = ι '' regularLocus.

theorem Hironaka.Manifold.PieceEmbedding.localResolutionMap_isIsoOver_reg {𝕜 : 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)) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) : AnalyticSpace.Hom.IsIsoOver (E.localResolutionMap bed W hW) (E.restrictedIdeal W).toAnalyticSpace.regularLocus

The local resolution map P = σ^r|_{Ỹ} : Ỹ → Y|_W of the piece is an isomorphism over the simple locus (Y|_W).regularLocus (clause (1) of [Wlo09, Theorem 2.0.1] for the piece, from clauses (2)–(3) of [Wlo09, Theorem 2.0.2] as in the proof of [Kol07, Theorem 27]): over a simple point no centre lies (clause (2) of the embedded desingularization), so σ^r is an analytic isomorphism there, Ỹ is the pullback of Y there, and the induced morphism of closed subspaces is bijective with bijective stalk maps.