An embedded desingularization has proper simple normal crossings

Clause (3) of BEDanFamStar.IsEmbeddedDesing is proper: for an embedded desingularization functor bed with bed.IsEmbeddedDesing, the final strict transform Ỹ of every value has, at every point of its cosupport, a chart adapted to Ỹ which is a simple-normal-crossing chart of the final exceptional family E_r in which no component's coordinate is one of the coordinates of Ỹ (BEDanFamStar.IsProperSnc, Hironaka/Resolution/Analytic/Wlo09/ProperSnc.lean; the coordinate description of [Kol07, Definition 24], with the transversality of the output of the proof of [Wlo09, Theorem 7.4.1]).

Proof. Clause (3) gives the adapted simple-normal-crossing chart φ with the coordinates σ of Ỹ and the components' coordinates cidx. If a component E^j through the point had cidx j = σ i, then on φ.source every point of Ỹ (where z_{σ i} = 0) would lie on E^j (where z_{cidx j} = 0), so Ỹ ∩ φ.source ⊆ E_r, and the point would not be a limit of points of Ỹ off E_r. But Ỹ is non-singular (the first conjunct of clause (3)), so every point of its cosupport is a regular point of the closed subspace (mem_reg_toAnalyticSpace_iff), and the density theorem mem_closure_cosupport_strictTransformSubspaceSeq_diff_support_of_isRegular (Hironaka/Resolution/Analytic/Wlo09/StrictTransformDensity.lean) makes it such a limit. The pointwise step is IsSncChartAt.cidx_notMem_range_of_mem_closure_diff. Not in the sources in this form.

The dot-notation name BEDanFamStar.IsEmbeddedDesing.isProperSnc is the form in which the resolution of analytic spaces invokes it (hbed.isProperSnc).

theorem Manifold.HypersurfaceFamily.IsSncChartAt.cidx_notMem_range_of_mem_closure_diff {𝕜 : 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) {Z : Set M} {s : ℕ} {σ : Fin s ↪ Fin n} (hφ : IsAdaptedChart ψ Z φ σ) (ha : a ∈ closure (Z \ F.support)) (j : { j : F.ι // a ∈ F.hyp j }) : c j ∉ Set.range ⇑σ

The pointwise step: a simple-normal-crossing chart of F at a whose chart is adapted to Z is proper (cidx j ∉ range σ) as soon as a is a limit of points of Z off F; a component through a with cidx j = σ i would contain Z ∩ φ.source.

theorem Hironaka.Manifold.BEDanFamStar.IsEmbeddedDesing.isProperSnc {𝕜 : Type} [RCLike 𝕜] {bed : BEDanFamStar 𝕜} (hbed : IsEmbeddedDesing 𝕜 bed) : IsProperSnc 𝕜 bed

An embedded desingularization has proper simple normal crossings: clause (3) gives the adapted simple-normal-crossing chart at every point of the final strict transform Ỹ; Ỹ is non-singular, so the point is regular and the density theorem mem_closure_cosupport_strictTransformSubspaceSeq_diff_support_of_isRegular makes it a limit of points of Ỹ off E_r; IsSncChartAt.cidx_notMem_range_of_mem_closure_diff gives the proper conjunct.