Lemma 102: lifting simple normal crossings from a hypersurface with the hypersurface appended

In the proof of [Kol07, Lemma 102], the going-up theorem [Kol07, Theorem 84] turns a blow-up sequence of order ≥ m for (S, I_0|_S, m, (E - E^j)|_S) into one of order m for (X_0, I_0, E - E^j); then, S being E^j, "every blow-up center is a smooth subvariety" of the transform of E^j, so that one has in fact a blow-up sequence of order m starting with (X_0, I_0, E). This module proves the second sentence (not in the sources beyond that remark): the boundary E on X_0 is the pulled-back E - E^j together with the transform S of E^j, and a centre lying in S with simple normal crossings with the trace of the boundary on S has simple normal crossings with the boundary together with S.

• HypersurfaceFamily.idealSheaf_eq_of_support_eq — the reduced ideal sheaf of a family depends only on its support.
• hasSncWith_append_of_hasSncWith_traceFamily — for a closed hypersurface S and a family F having simple normal crossings with S properly, a closed submanifold Z' of S having simple normal crossings with the trace F|_S has, read in the ambient manifold, simple normal crossings with F + S: the chart of S adapted to Z' is extended by the coordinate of S, which keeps the coordinate of S.
• hasOnlyNormalCrossingsWith_idealSheaf_append_of_traceFamily — the same in terms of ideal sheaves: the reduced ideal sheaf of F + S has only normal crossings with the ideal sheaf of Z.

These are used in BDCor85.lean to obtain [Kol07, Corollary 85] with the hypersurface in the boundary.

theorem Manifold.HypersurfaceFamily.idealSheaf_eq_of_support_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F F' : HypersurfaceFamily M} (h : F.support = F'.support) : F.idealSheaf = F'.idealSheaf

The reduced ideal sheaf of a family of hypersurfaces depends only on the support of the family.

theorem Hironaka.Manifold.hasSncWith_append_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} (hS : Manifold.IsClosedSubmanifold ψ S 1) (F : Manifold.HypersurfaceFamily M) (_hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hFS : Manifold.HypersurfaceFamily.HasSncWithProper ψ F S 1) {Z' : Set hS.toAnalyticManifold.carrier} {c' : ℕ} (_hZ' : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) Z' c') (hZF : Manifold.HypersurfaceFamily.HasSncWith (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) (hS.traceFamily F) Z' c') : Manifold.HypersurfaceFamily.HasSncWith ψ (F.append S) (hS.imageVal Z') (c' + 1)

Lifting simple normal crossings from a hypersurface with the hypersurface appended (the proof of [Kol07, Lemma 102]: S being E^j, "every blow-up center is a smooth subvariety" of the transform of E^j, so that one has a blow-up sequence of order m starting with (X_0, I_0, E)): for a closed hypersurface S and a family F with simple normal crossings having simple normal crossings with S properly, a closed submanifold Z' of S (regarded as a manifold) having simple normal crossings with the trace F|_S has, read in the ambient manifold, simple normal crossings with F + S. The chart of S adapted to Z' and to the trace is extended to the ambient manifold along the chart of F adapted to S, and the extension keeps the coordinate of S.

theorem Hironaka.Manifold.hasOnlyNormalCrossingsWith_idealSheaf_append_of_traceFamily {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {X : AnalyticManifold 𝕜 E} {S : Set X.carrier} (hS : Manifold.IsClosedSubmanifold ψ S 1) (F : Manifold.HypersurfaceFamily X.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hFS : Manifold.HypersurfaceFamily.HasSncWithProper ψ F S 1) {Z : Set X.carrier} {c : ℕ} (hZ : Manifold.IsClosedSubmanifold ψ Z c) (hZS : Z ⊆ S) (h : AnalyticManifold.IdealSheaf.HasOnlyNormalCrossingsWith (hS.traceFamily F).idealSheaf ⋯.idealSheaf) : AnalyticManifold.IdealSheaf.HasOnlyNormalCrossingsWith (F.append S).idealSheaf hZ.idealSheaf

The ideal-sheaf form of hasSncWith_append_of_hasSncWith_traceFamily: for a closed submanifold Z ⊆ S of a closed hypersurface S whose trace on S has only normal crossings with the reduced ideal sheaf of the trace F|_S, the ideal sheaf of Z has only normal crossings with the reduced ideal sheaf of F + S, by the dictionary between simple normal crossings of families and normal crossings of reduced ideal sheaves on both sides.