The restriction of an snc family to a smooth subscheme it has simple normal crossings with #
[Kol07, Definition 24], the last sentence: "If E does not contain Z, then E|_Z is again a
simple normal crossing divisor on Z." hasSncWith_comap_of_isClosedImmersion of
Hironaka.Scheme.Snc.RestrictHypersurface is the case of a smooth divisor H that is itself a
member of the family; isSnc_restrictedFamily of
Hironaka.Resolution.Algebraic.BoundaryClearing.Restriction restricts E − E^j to E^j. Clause
(3) of [Kol07, Theorem 36] for the affine resolution
(Hironaka.Resolution.Algebraic.Kol07.Thm36.SncPreimageSingular; the proof of [Kol07, Theorem 27]:
"g⁻¹(Sing X̄) = Z_j ∩ Ex_tot(π_0 ⋯ π_{j−1}) is a simple normal crossing divisor on Z_j") needs
the general case: the total exceptional divisor Ex_tot(π_0 ⋯ π_{j−1}) has simple normal crossings
with the smooth centre Z_j (Theorem 35 (1)) and no component of it contains the strict transform
X̄_j = Z_j^η, so its restriction to X̄_j — a subscheme of codimension ≥ 2 in general — is snc.
In snc coordinates z at a point x ∈ Z with Z_x = (z_l : l ∈ s), the images of the z_j, j ∉ s, are a regular system of parameters of 𝒪_{Z,x} = 𝒪_{X,x}/(z_s)
(Hironaka.Scheme.Snc.ParameterSubset, through the surjective stalk map of the closed immersion),
and every component E^i = (z_{c(i)}) through x has c(i) ∉ s exactly when E^i does not
contain Z near x (span_singleton_le_span_image_iff).
isSncAt_comap_of_hasSncWith: the pointwise statement at every point ofZ = V(ker g).isSnc_comap_of_hasSncWith:E|_Zis snc whenZis smooth overk.stalkIdeal_eq_of_isOpenImmersion_inclusion,HasSncWith.of_isOpenImmersion_inclusion: whenV(T) ⊆ V(Z)is an open subscheme (the identification of the strict transformX̄_jwith the componentZ_j^ηof the centre through the generic point), the two ideals have the same stalks alongV(T), soEhas snc withTas soon as it has snc withZ.not_stalkIdeal_le_of_isGenericPoint_notMem: the hypothesishnotfrom the generic point — a componentDwhose stalk atx ∈ V(T)is contained in that ofTcontainsV(T)nearx, hence contains the generic point of the irreducibleV(T)(stalkIdeal_specializesofHironaka.Scheme.IdealSheaf.Order.Constructible).
Sources: [Kol07, Definition 24; Theorem 27 (the proof); Theorem 36].
The last sentence of [Kol07, Definition 24], pointwise: for a closed immersion g : Y ⟶ X with
image Z = V(ker g) having simple normal crossings with E, such that no component of E contains
Z near any point of Z (hnot, stalkwise), the family E|_Z = E.comap g has snc coordinates at
every point of Y: the images of the snc coordinates of X not among those cutting out Z.
The last sentence of [Kol07, Definition 24]: for a closed immersion g : Y ⟶ X with Y smooth
over k and image Z = V(ker g) having simple normal crossings with E, if no component of E
contains Z near any of its points, then E|_Z = E.comap g is a simple normal crossing family on
Y.
Transport along the identification X̄_j = Z_j^η #
Along an open-immersion inclusion V(T) ⊆ V(Z) of closed subschemes, the ideals Z ≤ T have
the same stalk at every point of V(T): the stalk map of T.subschemeι = inclusion ≫ Z.subschemeι
factors through the isomorphism of stalks of the open immersion, so its kernel T_x
(ker_stalkMap_of_isClosedImmersion) is the kernel Z_x of the stalk map of Z.subschemeι.
The proof of [Kol07, Theorem 27] read on the identification X̄_j = Z_j^η: if E has simple
normal crossings with Z and V(T) ⊆ V(Z) is an open subscheme (Z ≤ T, the inclusion an open
immersion), then E has simple normal crossings with T — the snc coordinates at a point of V(T)
cut out V(Z), which is V(T) there.
The hypothesis hnot of isSncAt_comap_of_hasSncWith from a generalisation: if a point
η ∈ V(T) generalises x and η ∉ V(D), then D_x ⊄ T_x — otherwise
D_η = D_x 𝒪_η ⊆ T_x 𝒪_η = T_η ≠ (1) (stalkIdeal_specializes), i.e. η ∈ V(D). For a reducible
V(T), η is the generic point of an irreducible component of V(T) through x.
The hypothesis hnot of isSncAt_comap_of_hasSncWith from the generic point: if V(T) is
irreducible with generic point η ∉ V(D), then at no point x ∈ V(T) is D_x ⊆ T_x
(not_stalkIdeal_le_of_specializes_notMem at the generalisation η ⤳ x).