Simple normal crossings with an appended hypersurface along the center; sub-families

hasSncWith_append_of_le (Hironaka/Scheme/BlowUpSequence/RestrictDivisors.lean; Kol07, Definition 24 (4)) takes H + E to have simple normal crossings on the whole scheme but uses the data only at the points of the center Z. In the boundary-clearing step of the proof of Theorem 103 [Kol07, 104, Step 2.1] the family H_k + E_k has simple normal crossings only along the points of order ≥ m (the original members of E may meet H badly away from them), so this module gives the variant hasSncWith_append_of_le_on with the hypothesis in the along-a-set form IsSncOn Z.support (the same argument), and HasSncWith.subfamily: a center having simple normal crossings with E has simple normal crossings with every sub-family of E (restrict the injection of [Kol07, Definition 24 (3)]).

theorem AlgebraicGeometry.HasSncWith.subfamily {X : Scheme} {E : X.DivisorFamily} {Z : X.IdealSheafData} (h : E.HasSncWith Z) (p : E.ι → Prop) : (E.subfamily p).HasSncWith Z

A center having simple normal crossings with E has simple normal crossings with every sub-family of E: restrict the injection of [Kol07, Definition 24 (3)].

theorem AlgebraicGeometry.hasSncWith_append_of_le_on {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [Smooth f] {E : X.DivisorFamily} {J Z : X.IdealSheafData} (hE : (E.append J).IsSncOn ↑Z.support) (hZ : E.HasSncWith Z) (hle : J ≤ Z) : (E.append J).HasSncWith Z

hasSncWith_append_of_le with the hypothesis on E + J weakened to the points of the center: a center Z ⊆ V(J) having simple normal crossings with E, such that E + J has simple normal crossings at every point of Z, has simple normal crossings with E + J [Kol07, Definition 24 (4)]. The proof exchanges a coordinate of Z for the equation of J in 𝔪/𝔪², as in hasSncWith_append_of_le.