The resolution is an isomorphism over the simple points

Clause (2) of exists_functorial_resolution (ResolutionAssembly.lean): the map Π_X : R(X) → X is an isomorphism over the simple locus X.regularLocus — clause (2) of Hironaka's resolution problem [Hir64, Introduction], [Kol07, Theorem 45(2)], [Wlo09, Theorem 2.0.1(1)]. Read on the pieces: over each piece, localResolutionMap_isIsoOver_reg (Hironaka/Resolution/Analytic/Wlo09/IsoOverReg.lean; the local resolution Ỹ → Sp(W)/𝓘|W is an isomorphism over the simple points, the centres being disjoint from them, [Wlo09, Theorem 2.0.2(2)]) after the open immersion Sp(W)/𝓘|W → X onto the base open domOpens W, which carries the simple locus to the simple locus (isIsoOver_toSpaceMap_reg); on a glued space the descended map is an isomorphism over X.regularLocus ∩ ⋃ dom i when every piece map is (isIsoOver_descMap_inter_iUnion, Hironaka/Resolution/Analytic/Kol07Thm45/Glue/OverIsoReg.lean); then over the exhaustion.

The independence of the local resolution enters as the hypothesis hind (discharged in GluingProperties.lean). Not in the sources beyond the statements cited; bookkeeping.

theorem Hironaka.Manifold.PieceEmbedding.isIsoOver_toSpaceMap_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.toSpaceMap bed W hW) (X.regularLocus ∩ ↑(E.domOpens W))

The piece map Ỹ → X is an isomorphism over the simple points of its base open ([Wlo09, Theorem 2.0.2(2)]; Kollár's g⁻¹(Sing X̄) = Z_j ∩ Ex_tot, [Kol07, Theorem 27, proof]): toSpaceMap = Π ≫ q with q the open immersion of Sp(W)/𝓘|W onto domOpens W (pieceOverIncl on points); q is an isomorphism over X.regularLocus ∩ domOpens W (isIsoOver_of_isOpenImmersion), and q⁻¹(X.regularLocus ∩ domOpens W) is the simple locus of Sp(W)/𝓘|W (mem_reg_iff_of_isOpenImmersion), over which Π is an isomorphism (localResolutionMap_isIsoOver_reg); IsIsoOver.comp.

theorem Hironaka.Manifold.LocalEmbeddingData.isIsoOver_resolutionOnFullMap_reg {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (hU : IsOpen U) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) : AnalyticSpace.Hom.IsIsoOver (D.resolutionOnFullMap bed) (X.regularLocus ∩ U)

The descended map of the glued space is an isomorphism over the simple points of the OPEN U ([Wlo09, §4, (3)⇒(4)]) — the pieces' base opens cover U (closure_inner_subset_pieceDom, subset_iUnion_inner), each piece map is an isomorphism over X.regularLocus ∩ pieceDom i (isIsoOver_toSpaceMap_reg), so the descended map is one over X.regularLocus ∩ ⋃ pieceDom i (isIsoOver_descMap_inter_iUnion) and hence over the open subset X.regularLocus ∩ U (IsIsoOver.mono); the map resolutionOnFullMap unfolds to the chosen datum's descended map.

theorem Hironaka.Manifold.LocalEmbeddingData.isIsoOver_resolutionOnToSpace_reg {𝕜 : Type} [RCLike 𝕜] {X : AnalyticSpace 𝕜} {U : Set ↑↑X.toPresheafedSpace} (D : LocalEmbeddingData 𝕜 X U) (bed : BEDanFamStar 𝕜) (hU : IsOpen U) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) (hind : LocalResolutionIndependentOn X bed) : AnalyticSpace.Hom.IsIsoOver (D.resolutionOnToSpace bed) (X.regularLocus ∩ U)

The same on the space resolutionOn over the OPEN U: Π_U read into X is the open immersion Ũ → Ṿ followed by the descended map (restrictTo_comp_ofRestrict); the first is an isomorphism over Π⁻¹(X.regularLocus ∩ U) ⊆ Π⁻¹U (isIsoOver_of_isOpenImmersion), the second over X.regularLocus ∩ U (isIsoOver_resolutionOnFullMap_reg); IsIsoOver.comp.

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

Π_X is an isomorphism over the simple locus X.regularLocus ([Hir64, Introduction], clause (2) of the resolution problem; [Kol07, Theorem 45(2)]; [Wlo09, Theorem 2.0.1(1)]), for a reduced X, with the independence of the local resolution as hind — over each member U_n of the exhaustion the map Π_{U_n} is an isomorphism over X.regularLocus ∩ U_n (isIsoOver_resolutionOnToSpace_reg), the members cover X, and the descended map of the exhaustion gluing is an isomorphism over X.regularLocus ∩ ⋃ U_n = X.regularLocus (isIsoOver_descMap_inter_iUnion); the map bed.resolutionMap X unfolds to the chosen datum's descended map (resolutionPair_eq_of_glues).