The exceptional sub-family with the transform of a hypersurface is snc everywhere

Along a smooth blow-up sequence of order m whose centers lie in the transforms of H (smooth divisors), the selected members of E_r together with H_r are snc at every point, provided the selected members of E with H are (isSncOn_univ_subfamily_append_of_forall_le_center, by induction along the sequence). Kollár states this along the cosupport of I_r [Kol07, 104, Step 2.1]; the cosupport serves only to exclude the not-yet-cleared original members, so with nothing selected at the start the induction runs on the whole space. Its base case is H alone, a smooth divisor on a smooth scheme, snc everywhere (isSnc_append_empty_of_isSmoothDivisor); its step uses the smoothness and normal crossing conditions of [Kol07, Definition 66] at the center, the pointwise snc data on the exceptional divisor and the local isomorphism off it. The selected members at the end are the exceptional ones, those that are not birational transforms of original members (originalIdx): exceptionalFamily. So F_r + H_r is snc everywhere (isSnc_exceptionalFamily_append). This is what makes (X_r, I_r, F_r + H_r) a triple in the sense of [Kol07, Notation 64] when the maximal contact case of the proof of Theorem 103 restricts to the hypersurface [Kol07, 104, Step 2.2]: Kollár's "H + E is also a simple normal crossing divisor" holds for the exceptional sub-family.

noncomputable def AlgebraicGeometry.Scheme.BlowUpSequence.exceptionalFamily {X : Scheme} (S : X.BlowUpSequence) (E : X.DivisorFamily) : (S.stage (Fin.last S.length)).DivisorFamily

The exceptional sub-family of the total transform of E at the end of a sequence: the members that are not the birational transform of an original member (originalIdx). It is the family F_r for which "H_r + F_r is a simple normal crossing divisor" holds in the maximal contact case of the proof of Theorem 103 [Kol07, 104, Step 2.2].

Equations

• S.exceptionalFamily E = (S.totalTransformSeq E (Fin.last S.length)).subfamily fun (b : (S.totalTransformSeq E (Fin.last S.length)).ι) => ∀ (a : E.ι), b ≠ S.originalIdx E (Fin.last S.length) a

theorem Hironaka.Sequence.exceptionalFamily_component {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (E : X.DivisorFamily) (b : (S.exceptionalFamily E).ι) : (S.exceptionalFamily E).component b = (S.totalTransformSeq E (Fin.last S.length)).component ↑b

theorem Hironaka.Sequence.isSncOn_univ_subfamily_append_of_forall_le_center {k : Type u} [Field k] [CharZero k] (n : ℕ) {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (S : X.BlowUpSequence) {J : X.IdealSheafData} {E : X.DivisorFamily} {m : ℕ} : S.IsOrderSeq f J E m → ∀ (H : X.IdealSheafData), (∀ (i : Fin (S.length + 1)), AlgebraicGeometry.IsSmoothDivisor (S.strictTransformSeq H i)) → (∀ (i : Fin S.length), S.strictTransformSeq H i.castSucc ≤ S.center i) → ∀ (p : E.ι → Prop), ((E.subfamily p).append H).IsSncOn Set.univ → (((S.totalTransformSeq E (Fin.last S.length)).subfamily fun (i : (S.totalTransformSeq E (Fin.last S.length)).ι) => ∀ (a : E.ι), i = S.originalIdx E (Fin.last S.length) a → p a).append (S.strictTransformSeq H (Fin.last S.length))).IsSncOn Set.univ

The global form of the snc induction of [Kol07, 104, Step 2.1]: along a smooth blow-up sequence of order m all of whose centers lie in the transforms of a divisor H with smooth transforms, the selected members of the total transform together with the transform of H are snc at every point, provided the selected members of E with H are.

theorem Hironaka.Sequence.isSnc_exceptionalFamily_append {k : Type u} [Field k] [CharZero k] (n : ℕ) {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (S : X.BlowUpSequence) {J : X.IdealSheafData} {E : X.DivisorFamily} {m : ℕ} (hS : S.IsOrderSeq f J E m) (hE : E.IsSnc) (H : X.IdealSheafData) (hH : AlgebraicGeometry.IsSmoothDivisor H) (hHs : ∀ (i : Fin (S.length + 1)), AlgebraicGeometry.IsSmoothDivisor (S.strictTransformSeq H i)) (hcen : ∀ (i : Fin S.length), S.strictTransformSeq H i.castSucc ≤ S.center i) : ((S.exceptionalFamily E).append (S.strictTransformSeq H (Fin.last S.length))).IsSnc

"H + E is also a simple normal crossing divisor" [Kol07, 104, Step 2.2], for the exceptional sub-family: along a smooth blow-up sequence of order m starting with an snc family E, whose centers lie in the transforms of a smooth divisor H with smooth transforms, the exceptional sub-family of E_r together with H_r is a simple normal crossing family.