The restriction of an snc divisor to a transverse hypersurface

Kollár: "if E does not contain Z, then E|_Z is again a simple normal crossing divisor on Z" [Kol07, Definition 24], here for a smooth hypersurface H having simple normal crossings with F and containing no component of F near any point (near every point of H ∩ E^j there are points of H off E^j). At a ∈ H, a chart φ adapted to H (H = {z_{σ 0} = 0}) which is an snc chart of F (E^j = {z_{c j} = 0}) has c j ≠ σ 0 for every component through a — otherwise E^j would contain H on the chart — so the coordinates of the components through a are among the n − 1 coordinates that the induced chart φ|_H of the manifold H keeps (projCompl): E^j ∩ H = {w_{c' j} = 0} on φ|_H, with c' injective. The components of F|_H are the traces E^j ∩ H, closed hypersurfaces of H by the same charts, and the family stays locally finite (the preimage of a locally finite family under the continuous inclusion). This is the restriction of the boundary to a hypersurface of maximal contact (Hironaka/Resolution/Analytic/OrderReduction/Modified/StopRestrict.lean).

theorem Manifold.HypersurfaceFamily.IsSncChartAt.notMem_range_of_frequently {𝕜 : 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} {H : Set M} {φ : OpenPartialHomeomorph M E} {c : ℕ} {σ : Fin c ↪ Fin n} (hφ : IsAdaptedChart ψ H φ σ) {a : M} {cidx : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : IsSncChartAt ψ F φ a cidx) (j : { j : F.ι // a ∈ F.hyp j }) (hne : ∃ᶠ (x : M) in nhdsWithin a H, x ∉ F.hyp ↑j) : cidx j ∉ Set.range ⇑σ

In a chart adapted to H which is an snc chart of F at a ∈ H, a component through a near which H is not contained in the component has its coordinate off the block of H.

theorem Manifold.HypersurfaceFamily.IsSncChartAt.restrict_isSncChartAt {𝕜 : 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} {H : Set M} (hH : IsClosedSubmanifold ψ H 1) {φ : OpenPartialHomeomorph M E} {σ : Fin 1 ↪ Fin n} (hφ : IsAdaptedChart ψ H φ σ) {a : M} (ha : a ∈ H) {cidx : { j : F.ι // a ∈ F.hyp j } → Fin n} (hc : IsSncChartAt ψ F φ a cidx) (hne : ∀ (j : F.ι), a ∈ F.hyp j → ∃ᶠ (x : M) in nhdsWithin a H, x ∉ F.hyp j) : IsSncChartAt (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) (F.restrict H) (hφ.chartOn ha) ⟨a, ha⟩ fun (j : { j : (F.restrict H).ι // ⟨a, ha⟩ ∈ (F.restrict H).hyp j }) => (complEquiv σ) ⟨cidx ⟨↑j, ⋯⟩, ⋯⟩

For a ∈ H, a chart adapted to H which is an snc chart of F at a, and no component through a containing H near a, the induced chart of H (IsAdaptedChart.chartOn) is an snc chart of the restriction F|_H at a, with the indices of the components read in the complement of the block of H.

theorem Manifold.HypersurfaceFamily.isSnc_restrict {𝕜 : 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} {H : Set M} (hF : IsSnc ψ F) (hH : IsClosedSubmanifold ψ H 1) (hsnc : HasSncWith ψ F H 1) (hne : ∀ a ∈ H, ∀ (j : F.ι), a ∈ F.hyp j → ∃ᶠ (x : M) in nhdsWithin a H, x ∉ F.hyp j) : IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) (F.restrict H)

Kollár's "if E does not contain Z, then E|_Z is again a simple normal crossing divisor on Z" [Kol07, Definition 24]: if the snc divisor F has simple normal crossings with the smooth hypersurface H and no component of F contains H near any point, then F|_H is a simple normal crossings divisor on the manifold H.