The exceptional set is a simple normal crossings divisor set; the range of the resolution

Clause (3) of exists_functorial_resolution (ResolutionAssembly.lean) in its set form ([Wlo09, Theorem 2.0.1(2)]; [Kol07, Theorem 45(3)]): Π_X⁻¹(X.singularLocus) is a simple normal crossings divisor set of R(X). Over each piece, localResolutionMap_preimage_sing_eq_inter_exceptional (Hironaka/Resolution/Analytic/Wlo09/PreimageSing.lean) gives it for Π⁻¹((Sp(W)/𝓘|W).singularLocus), and the open immersion q of Sp(W)/𝓘|W onto its base open carries the singular locus to the singular locus (isSncDivisorSet_toSpaceMap_preimage_sing); the predicate is local on glued spaces (isSncDivisorSet_gluedOver_preimage, Hironaka/AnalyticSpace/Glue/OverSnc.lean) and restricts to the open subspaces Ũ_n = Ṿ_n|Π_n⁻¹U_n (IsSncDivisorSet.restrictOpen); then over the exhaustion.

The range conjunct of clause (4) of exists_functorial_resolution: range Π_X = closure X.regularLocus — for a real-analytic space the simple points need not be dense, so Π_X need not be surjective [Hir64, Introduction]. The range is closed (Π_X proper) and contains X.regularLocus (the restricted map onto X.regularLocus is onto, by clause (2)), and the complement of the divisor set Π_X⁻¹(X.singularLocus) is dense in R(X) (IsSncDivisorSet.dense_compl, Hironaka/AnalyticSpace/SncDivisorSetLocal.lean) and maps into X.regularLocus.

The independence of the local resolution enters as the hypothesis hind. Not in the sources beyond the statements cited; bookkeeping.

theorem Hironaka.Manifold.PieceEmbedding.exists_openImmersion_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)) : ∃ (q : (E.restrictedIdeal W).toAnalyticSpace.toKLocallyRingedSpace ⟶ X.toKLocallyRingedSpace), AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑q ∧ AnalyticSpace.KLocallyRingedSpace.Hom.toFun q = E.pieceOverIncl W ∧ E.toSpaceMap bed W hW = CategoryTheory.CategoryStruct.comp (E.localResolutionMap bed W hW) q

The open immersion q : Sp(W)/𝓘|W → X of the piece over W (pieceOverIncl 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, with toSpaceMap = Π ≫ q.

theorem Hironaka.Manifold.PieceEmbedding.isSncDivisorSet_toSpaceMap_preimage_sing {𝕜 : 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) : (E.localResolution bed W hW).IsSncDivisorSet (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (E.toSpaceMap bed W hW) ⁻¹' X.singularLocus)

The inverse image of the singular locus of X under the piece map Ỹ → X is a simple normal crossings divisor set ([Wlo09, Theorem 2.0.1(2)]): it is Π⁻¹((Sp(W)/𝓘|W).singularLocus) (localResolutionMap_preimage_sing_eq_inter_exceptional), the open immersion q carrying the singular locus to the singular locus (mem_reg_iff_of_isOpenImmersion).

theorem Hironaka.Manifold.LocalEmbeddingData.isSncDivisorSet_resolutionOnFullMap_preimage_sing {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) : (D.resolutionOnFull bed).IsSncDivisorSet (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resolutionOnFullMap bed) ⁻¹' X.singularLocus)

The same on the glued space of the pieces: the pieces' inverse images of the singular locus are simple normal crossings divisor sets (isSncDivisorSet_toSpaceMap_preimage_sing) and the predicate is local on the glued space (isSncDivisorSet_gluedOver_preimage); the map resolutionOnFullMap unfolds to the chosen datum's descended map.

theorem Hironaka.Manifold.LocalEmbeddingData.isSncDivisorSet_resolutionOnToSpace_preimage_sing {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) : (D.resolutionOn bed).IsSncDivisorSet (AnalyticSpace.KLocallyRingedSpace.Hom.toFun (D.resolutionOnToSpace bed) ⁻¹' X.singularLocus)

The same on the space resolutionOn over U: Ũ = Ṿ|Π⁻¹U is an open subspace of the glued space (IsSncDivisorSet.restrictOpen) and Π_U read into X is the open immersion followed by the descended map (restrictTo_comp_ofRestrict). No hU: the restriction lemma takes any openOf.

theorem Hironaka.Manifold.BEDanFamStar.resolution_isSncDivisorSet_preimage_sing_of_independent {𝕜 : Type} [RCLike 𝕜] (X : AnalyticSpace 𝕜) (hX : X.IsReduced) (bed : BEDanFamStar 𝕜) (hbed : IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) : (bed.resolution X).IsSncDivisorSet (↑(bed.resolutionMap X) ⁻¹' X.singularLocus)

Π_X⁻¹(X.singularLocus) is a simple normal crossings divisor set of R(X) (Wlo09, Theorem 2.0.1(2); [Kol07, Theorem 45(3)]), for a reduced X, with the independence of the local resolution as hind — over each member U_n of the exhaustion the inverse image of the singular locus under Π_{U_n} is a simple normal crossings divisor set (isSncDivisorSet_resolutionOnToSpace_preimage_sing) and the predicate is local on the glued space (isSncDivisorSet_gluedOver_preimage, resolutionPair_eq_of_glues).

theorem Hironaka.Manifold.BEDanFamStar.range_resolutionMap_eq_closure_reg_of_independent {𝕜 : Type} [RCLike 𝕜] (X : AnalyticSpace 𝕜) (hX : X.IsReduced) (bed : BEDanFamStar 𝕜) (hbed : IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) : Set.range ↑(bed.resolutionMap X) = closure X.regularLocus

range Π_X = closure X.regularLocus (for a real-analytic space the simple points need not be dense, [Hir64, Introduction]), for a reduced X, with the independence of the local resolution as hind — ⊇: the range is closed (Π_X proper, isProperMap_resolutionMap) and contains X.regularLocus (the restricted map Π_X⁻¹(X.regularLocus) → X.regularLocus is an isomorphism, hence onto, resolutionMap_isIsoOver_reg_of_independent); ⊆: the complement of the divisor set Π_X⁻¹(X.singularLocus) is dense in R(X) (IsSncDivisorSet.dense_compl) and Π_X maps it into X.regularLocus.