The preimage of the singular locus is the trace of the exceptional divisor

For an embedded desingularization functor bed (bed.IsEmbeddedDesing) and a piece Y|_W of an analytic space, the local resolution map Π = σ^r|_{Ỹ} : Ỹ → Y|_W satisfies Π⁻¹((Y|_W).singularLocus) = Ỹ ∩ |E_r| as subsets of Ỹ, and this set is a simple normal crossing divisor of the non-singular space Ỹ (IsSncDivisorSet). This is clause (2) of Włodarczyk's resolution of analytic spaces [Wlo09, Theorem 2.0.1], "the inverse image of the singular locus is a simple normal crossing divisor", deduced from clauses (2)–(3) of [Wlo09, Theorem 2.0.2] and the fact that the support of the exceptional divisor is the exceptional locus.

The set equality. A point of E_r lies over the image of a centre, which is not a simple point (clause (2), support_totalTransformSeq_subset_preimage_of_centersOver); off E_r the composite is a local isomorphism and Ỹ is the pullback of Y stalkwise (Hironaka/Resolution/Analytic/Wlo09/IsoOverReg.lean), so regularity of the quotient stalks transports (isRegularLocalRing_quotient_strictTransformSubspaceSeq_iff_of_notMem_support) and the non-singularity of Ỹ (clause (3)) makes the image simple.

The simple normal crossing divisor. At a point x of Ỹ, the proper form of clause (3) (IsEmbeddedDesing.isProperSnc, Hironaka/Resolution/Analytic/Wlo09/ProperSncOfEmbeddedDesing.lean) gives an adapted chart φ of Ỹ which is a simple-normal-crossing chart of E_r with the components' coordinates off the block of Ỹ. Shrunk to a neighbourhood meeting only the components through x (IsSnc.exists_isOpen_forall_mem_of_mem), the one chart serves every point of Ỹ ∩ φ.source (IsSncChartAt.of_forall_mem, IsSncChartAt.comap_transportChart): on the open submanifold U := φ.source, Ỹ ∩ U is a closed submanifold of codimension c whose ideal sheaf is Ỹ|_U (comap_inclusion_eq_idealSheaf_of_isRegularLocalRing_quotient, through the vanishing ideals), and the pulled-back family E_r|_U has proper simple normal crossings with it (hasSncWithProper_comap_inclusion_of_isSncChartAt), so its trace is a simple normal crossing divisor of the bundled submanifold (isSnc_traceFamily). The predicate follows (isSncDivisorSet_toAnalyticSpace_of_forall): Sp(Ỹ ∩ U) ≅ Sp(U)/𝓘 = Sp(U)/(Ỹ|_U) ≅ Ỹ|_U' (closedSubmanifoldIso, restrictOpen_quotient_iso), the image of the trace's support being the trace of |E_r|. This is the chart-wise simple normal crossings of [Kol07, Definition 24] read on the subspace.

Together with Hironaka/Resolution/Analytic/Wlo09/IsoOverReg.lean these are the clauses from which the resolution of analytic spaces is assembled in Hironaka/Manifold/Sequence/Restrict/.

theorem AnalyticManifold.FiniteSuccession.isRegularLocalRing_quotient_strictTransformSubspaceSeq_iff_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) : IsRegularLocalRing (↑((Manifold.structureSheaf 𝕜 E (S.stage i).carrier).presheaf.stalk z) ⧸ Manifold.IdealSheaf.stalkIdeal (S.strictTransformSubspaceSeq J i) z) ↔ IsRegularLocalRing (↑((Manifold.structureSheaf 𝕜 E M.carrier).presheaf.stalk ((S.stageMap i) z)) ⧸ Manifold.IdealSheaf.stalkIdeal J ((S.stageMap i) z))

Off the exceptional family, regularity of the quotient stalk of the strict transform is regularity of the quotient stalk of J at the image: the germ map of the composite is bijective there and carries the one stalk ideal onto the other.

theorem Manifold.HypersurfaceFamily.IsSnc.exists_isOpen_forall_mem_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} (hF : IsSnc ψ F) (a : M) : ∃ (V : Set M), IsOpen V ∧ a ∈ V ∧ ∀ (j : F.ι), ∀ x ∈ V, x ∈ F.hyp j → a ∈ F.hyp j

Near a point of a simple normal crossing divisor only the components through the point are met.

theorem Manifold.HypersurfaceFamily.IsSncChartAt.of_forall_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} {φ : OpenPartialHomeomorph M E} {a : M} {c : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : IsSncChartAt ψ F φ a c) {b : M} (hb : b ∈ φ.source) (hsub : ∀ (j : F.ι), b ∈ F.hyp j → a ∈ F.hyp j) : IsSncChartAt ψ F φ b fun (j : { j : F.ι // b ∈ F.hyp j }) => c ⟨↑j, ⋯⟩

A simple-normal-crossing chart at a is a simple-normal-crossing chart at every point b of its source all of whose components pass through a, with the indices restricted.

theorem Manifold.HypersurfaceFamily.IsSncChartAt.comap_transportChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {F : HypersurfaceFamily M.carrier} (h : AnalyticMap N M) {Φ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤} {a : N.carrier} (haΦ : a ∈ Φ.source) (hΦ : Set.EqOn (⇑h) (↑Φ.toPartialEquiv) Φ.source) {φ : OpenPartialHomeomorph M.carrier E} {c : { j : F.ι // h a ∈ F.hyp j } → Fin n} (hc : IsSncChartAt ψ F φ (h a) c) : IsSncChartAt ψ (comap (⇑h) F) (transportChart Φ.symm φ) a fun (j : { j : (comap (⇑h) F).ι // a ∈ (comap (⇑h) F).hyp j }) => c ⟨↑j, ⋯⟩

A simple-normal-crossing chart of F at h a transports along a local inverse of h to a simple-normal-crossing chart of the inverse image F.comap h at a (the step inside isSnc_comap, made a lemma).

theorem Hironaka.Manifold.stalkIdeal_eq_vanishingStalk_cosupport_of_isRegularLocalRing_quotient {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {A : AnalyticManifold 𝕜 E} (J : A.IdealSheaf) (hns : ∀ a ∈ Manifold.IdealSheaf.support J, IsRegularLocalRing (↑((Manifold.structureSheaf 𝕜 E A.carrier).presheaf.stalk a) ⧸ Manifold.IdealSheaf.stalkIdeal J a)) (a : A.carrier) : Manifold.IdealSheaf.stalkIdeal J a = Manifold.vanishingStalk (Manifold.IdealSheaf.support J) a

An ideal sheaf with regular quotient stalks along its support is the reduced ideal of its support: its stalks are the vanishing ideals. At a support point the stalk is a coordinate ideal on an adapted chart (exists_adaptedChart_of_isRegularLocalRing_quotient), so the local Hadamard lemma applies; off the closed support both sides are the unit ideal.

theorem Hironaka.Manifold.comap_inclusion_eq_idealSheaf_of_isRegularLocalRing_quotient {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {A : AnalyticManifold 𝕜 E} (J : A.IdealSheaf) (hns : ∀ a ∈ Manifold.IdealSheaf.support J, IsRegularLocalRing (↑((Manifold.structureSheaf 𝕜 E A.carrier).presheaf.stalk a) ⧸ Manifold.IdealSheaf.stalkIdeal J a)) (U : TopologicalSpace.Opens A.carrier) {c : ℕ} (hS : Manifold.IsClosedSubmanifold ψ (⇑(A.inclusion U) ⁻¹' Manifold.IdealSheaf.support J) c) : Manifold.IdealSheaf.pullback ⇑(A.inclusion U) ⋯ J = hS.idealSheaf

On an open U on which the support of such a J is a closed submanifold, the inverse image of J is the ideal sheaf of that submanifold.

theorem Hironaka.Manifold.hasSncWithProper_comap_inclusion_of_isSncChartAt {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {A : AnalyticManifold 𝕜 (Fin n → 𝕜)} {F : Manifold.HypersurfaceFamily A.carrier} {Y : Set A.carrier} {c : ℕ} {φ : OpenPartialHomeomorph A.carrier (Fin n → 𝕜)} {σ : Fin c ↪ Fin n} {a : A.carrier} {cidx : { j : F.ι // a ∈ F.hyp j } → Fin n} (hφ : Manifold.IsAdaptedChart (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) Y φ σ) (hc : Manifold.HypersurfaceFamily.IsSncChartAt (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) F φ a cidx) (hproper : ∀ (j : { j : F.ι // a ∈ F.hyp j }), cidx j ∉ Set.range ⇑σ) (hsub : ∀ (j : F.ι), ∀ x ∈ φ.source, x ∈ F.hyp j → a ∈ F.hyp j) : Manifold.HypersurfaceFamily.HasSncWithProper (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (Manifold.HypersurfaceFamily.comap (⇑(A.inclusion { carrier := φ.source, is_open' := ⋯ })) F) (⇑(A.inclusion { carrier := φ.source, is_open' := ⋯ }) ⁻¹' Y) c

A proper adapted simple-normal-crossing chart at a point a of Y, whose source meets only the components through a, makes the inverse image of F on the open submanifold φ.source have proper simple normal crossings with the trace of Y there, with the one transported chart at every point.

theorem Hironaka.Manifold.isSncDivisorSet_toAnalyticSpace_of_forall {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {A : AnalyticManifold 𝕜 (Fin n → 𝕜)} (J : A.IdealSheaf) (Z : Set A.carrier) (h : ∀ x ∈ Manifold.IdealSheaf.support J, ∃ (U : TopologicalSpace.Opens A.carrier) (_ : x ∈ U) (c : ℕ) (hS : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (⇑(A.inclusion U) ⁻¹' Manifold.IdealSheaf.support J) c), Manifold.IdealSheaf.pullback ⇑(A.inclusion U) ⋯ J = hS.idealSheaf ∧ ∃ (F : Manifold.HypersurfaceFamily (A.restrict U).carrier), Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin (n - c) → 𝕜)) (hS.traceFamily F) ∧ F.support = ⇑(A.inclusion U) ⁻¹' Z) : J.toAnalyticSpace.IsSncDivisorSet ((fun (y : ↑↑J.toAnalyticSpace.toPresheafedSpace) => ↑J.toAnalyticSpaceι y) ⁻¹' Z)

The predicate IsSncDivisorSet for a closed subspace V(J) and the trace of an ambient set Z, from local data at every point of the support: an open U, the support a closed submanifold of U with J|_U its ideal sheaf, and a family on U whose trace is a simple normal crossing family with support the trace of Z. The comparison isomorphisms are Sp(Y) ≅ Sp(M)/𝓘_Y (closedSubmanifoldIso) and (X|_U)/(𝒥|_U) ≅ (X/𝒥)|_U (restrictOpen_quotient_iso).

theorem Hironaka.Manifold.PieceEmbedding.localResolutionMap_preimage_sing_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)) (hbed : BEDanFamStar.IsEmbeddedDesing 𝕜 bed) : ↑(E.localResolutionMap bed W hW) ⁻¹' (E.restrictedIdeal W).toAnalyticSpace.singularLocus = (fun (y : ↑↑((E.localResolutionSeq bed W hW).toSuccession.strictTransformSubspaceSeq (E.restrictedIdeal W) (Fin.last (E.localResolutionSeq bed W hW).toSuccession.length)).toAnalyticSpace.toPresheafedSpace) => ↑((E.localResolutionSeq bed W hW).toSuccession.strictTransformSubspaceSeq (E.restrictedIdeal W) (Fin.last (E.localResolutionSeq bed W hW).toSuccession.length)).toAnalyticSpaceι y) ⁻¹' ((E.localResolutionSeq bed W hW).toSuccession.totalTransformSeq (Fin.last (E.localResolutionSeq bed W hW).toSuccession.length)).support

The preimage of the singular locus under the local resolution map is the trace of the exceptional divisor: Π⁻¹((Y|_W).singularLocus) = Ỹ ∩ |E_r| as subsets of Ỹ (from clauses (2) and (3) of [Wlo09, Theorem 2.0.2]).

theorem Hironaka.Manifold.PieceEmbedding.localResolutionMap_preimage_sing_eq_inter_exceptional {𝕜 : 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.localResolutionMap bed W hW) ⁻¹' (E.restrictedIdeal W).toAnalyticSpace.singularLocus = (fun (y : ↑↑((E.localResolutionSeq bed W hW).toSuccession.strictTransformSubspaceSeq (E.restrictedIdeal W) (Fin.last (E.localResolutionSeq bed W hW).toSuccession.length)).toAnalyticSpace.toPresheafedSpace) => ↑((E.localResolutionSeq bed W hW).toSuccession.strictTransformSubspaceSeq (E.restrictedIdeal W) (Fin.last (E.localResolutionSeq bed W hW).toSuccession.length)).toAnalyticSpaceι y) ⁻¹' ((E.localResolutionSeq bed W hW).toSuccession.totalTransformSeq (Fin.last (E.localResolutionSeq bed W hW).toSuccession.length)).support ∧ (E.localResolution bed W hW).IsSncDivisorSet (↑(E.localResolutionMap bed W hW) ⁻¹' (E.restrictedIdeal W).toAnalyticSpace.singularLocus)

Clause (2) of [Wlo09, Theorem 2.0.1] for the local resolution map of a piece: the preimage of the singular locus is the trace of the exceptional divisor, and it is a simple normal crossing divisor of the non-singular space Ỹ.