Hironaka's Corollary 3: simplification of an algebraic boundary

[Hir64, Corollary 3, p. 146], "the simplification of an algebraic boundary", stated by Hironaka as an immediate consequence of Main Theorem II: for a non-singular algebraic k-scheme X and a nowhere dense closed subscheme W, there is a finite succession of monoidal transformations with non-singular centres D_i lying over W (D_i ⊆ f̄_i⁻¹(W), where f̄_i = f_0 ∘ ⋯ ∘ f_{i-1}) such that X_r is non-singular and the associated reduced scheme red(f̄_r⁻¹(W)) is defined by an invertible sheaf of ideals and has only normal crossings ([Hir64, Definition 2] for the last notion). It is proved here from Kollár's principalization theorem [Kol07, Theorem 35] applied to the triple (X, I_W, ∅):

• the hypothesis: Hironaka's "nowhere dense" is topological, while a triple asks the ideal to be nonzero on every irreducible component (Kollár's "not zero on any irreducible component"); the bridge is isNonzeroEverywhere_of_isNowhereDense_support;
• clause (ii): the centres of BP with empty boundary are the centres of the order reduction BMO_1, which lie over V(I_W) (stageMap_mem_support_of_mem_center_BP);
• clause (i): the end result of a smooth blow-up sequence over k is smooth, hence regular (isRegular_of_smooth);
• clause (iii): clause (2) of [Kol07, Theorem 35] writes Π^* I_W = ∏ F_j^{a_j} with F a simple normal crossing family (BP_isIdealOfSncDivisor); its radical is the reduced union of the members with positive multiplicity (radical_prod_pow_eq_unionIdeal_subfamily), a simple normal crossing subfamily, whose reduced union has only normal crossings (IsSnc.isSncBoundary_unionIdeal) and is invertible (isInvertible_unionIdeal_of_isSnc).

Corollary 3

theorem Hironaka.Resolution.hironaka_corollary3 {k : Type u} [Field k] [CharZero k] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.QuasiCompact (X ↘ AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsSeparated (X ↘ AlgebraicGeometry.Spec ↧k)] (hN : ∃ (N : ℕ), AlgebraicGeometry.SmoothOfRelativeDimension N (X ↘ AlgebraicGeometry.Spec ↧k)) (W : X.IdealSheafData) (hW : IsNowhereDense ↑W.support) : ∃ (S : X.BlowUpSequence), (∀ (i : Fin S.length), AlgebraicGeometry.IsRegular (S.center i).subscheme) ∧ AlgebraicGeometry.IsRegular S.last ∧ (∀ (i : Fin S.length), ∀ x ∈ (S.center i).support, (S.stageMap i.castSucc) x ∈ W.support) ∧ (W.comap S.composite).radical.IsInvertible ∧ (W.comap S.composite).radical.IsSncBoundary

[Hir64, Corollary 3, p. 146]: for X smooth of a single relative dimension over k (Hironaka: X as in Main Theorem II, non-singular; its non-singularity follows from smoothness, and the restriction to one relative dimension is lifted in ComponentwiseCorollaries) and W a nowhere dense closed subscheme, a finite succession of monoidal transformations with non-singular centres such that (i) the end result is non-singular, (ii) every centre lies over W, and (iii) the reduced inverse image of W is defined by an invertible sheaf of ideals and has only normal crossings. Proved from Kollár's principalization theorem [Kol07, Theorem 35] on (X, I_W, ∅) rather than, as in Hironaka, from Main Theorem II.