Going up: lifting simple normal crossings from a submanifold

The converse of the trace lemma hasSncWith_traceFamily, the normal-crossings ingredient of Kollár's Corollary 85 [Kol07, Corollary 85]: for S ⊆ M a closed submanifold and F a simple normal crossing family having simple normal crossings with S properly (E + S is a simple normal crossing divisor and no component contains S), a closed submanifold Z' ⊆ S having simple normal crossings with the trace F|_S in S has, read in M, simple normal crossings with F in the sense of [Kol07, Definition 24].

At a point a' of Z': the proper simple-normal-crossing chart φ of F adapted to S (its component coordinates off the S-block), the chart χ of S adapted to Z', which is a simple-normal-crossing chart of the trace, and the extended chart φ ≫ₕ extendComplE ψ σ₁ (χ₀⁻¹ ≫ₕ χ) of M (isAdaptedChart_extendComplE: the S-equations of φ, the Z'-coordinates of χ). Its component coordinates are the trace's component coordinates read through χ: a component E_j of F through a' is, in φ, the hyperplane {z_{c_j} = 0} with c_j off the S-block, so its equation depends only on the complementary coordinates and E_j is the pull-back of its trace under the projection to S, which χ straightens. Not in the sources in this form; the algebraic counterpart is hasSncWith_append_of_comap_of_isClosedImmersion.

theorem Hironaka.Manifold.hasSncWith_of_hasSncWith_traceFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (F : Manifold.HypersurfaceFamily M) (_hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hFS : Manifold.HypersurfaceFamily.HasSncWithProper ψ F S s) {Z' : Set hS.toAnalyticManifold.carrier} {c' : ℕ} (_hZ' : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z' c') (hZF : Manifold.HypersurfaceFamily.HasSncWith (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (hS.traceFamily F) Z' c') : Manifold.HypersurfaceFamily.HasSncWith ψ F (hS.imageVal Z') (c' + s)

Lifting simple normal crossings from a submanifold, the converse of hasSncWith_traceFamily (the normal-crossings step in the proof of [Kol07, Corollary 85]): for S ⊆ M a closed submanifold and F a simple normal crossing family having simple normal crossings with S properly (HasSncWithProper: E + S is a simple normal crossing divisor), a closed submanifold Z' ⊆ S having simple normal crossings with the trace F|_S in S has, read in M, simple normal crossings with F [Kol07, Definition 24]: the adapted coordinates of Z' on S extended by the equations of S, the component equations kept (the chart extension extendComplE). The hypotheses _hF (F is a simple normal crossing family) and _hZ' (Z' is a closed submanifold) are present because they describe the setting of [Kol07, Corollary 85] in which the lemma is applied, the boundary being a simple normal crossing divisor and Z' a centre; the proof does not need them, because hFS and hZF already provide at every point the adapted charts of S and of Z' which are simple-normal-crossing charts of F and of F|_S, and these are all it extends.