Włodarczyk's embedded desingularization sequence `BED` #

The sequence of blow-ups of Włodarczyk's embedded desingularization theorem with smooth centres [Wlo05, Theorem 1.0.2], in the strengthened form of Bravo–Villamayor [Wlo05, Theorem 4.7.1]: for a reduced closed subscheme Y = ⋃ Yᵢ of a smooth variety X, a sequence of blow-ups in smooth centres after which the strict transforms Ỹᵢ of the components are smooth and disjoint, and the full transform of I_Y is its monomial part times I_Ỹ. Włodarczyk's proof runs the canonical resolution of the marked ideal (X, I_Y, ∅, 1) [Wlo05, 4.6] with a modification: the procedure is run until "the strict transform of one of the components Yᵢ is the center"; at that moment, by the Claim of the proof of Theorem 4.7.1, the controlled transform of (I_Y, 1) agrees with I_Ỹᵢ near Ỹᵢ; these strict transforms are isolated, the procedure continues "ignoring these isolated components", and at the end any components not meeting the strict transforms are principalized.

Kollár's blow-up sequence functors expose neither Włodarczyk's invariant nor his "moment", so the modification is transcribed as an outer loop around the order reduction functor BMO_1 of [Kol07, Theorem 69] (Hironaka.Stage.BMO_m): run BMO_1 on the marked triple; at the first stage whose centre contains the strict transform of one of the components not yet isolated, truncate the run before that blow-up, replace the ideal by its colon by the reduced ideal of the absorbed strict transforms (the isolation), and restart on the modified marked triple with the remaining components. Włodarczyk's reordering of the monomial part (his Step 2b, which terminates by his invariant) is not transcribed; the stop rule alone is. Włodarczyk's Claim fails for this order of the steps (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedHypotheses), and the clauses of the theorem are instead proved from the local form of the ideal near an isolated component (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative and the modules EmbeddedCP*).

The construction #

bmoOneRun T hm — the run of BMO_1 on a marked triple T of mark 1; it is a smooth blow-up sequence of order ≥ 1 for T (isOrderGeSeq_bmoOneRun).
HasAbsorptionAt T hm C n — the stop rule: at stage n of the run the centre CONTAINS the strict transform of some member of the finite set C of (the strict transforms of) the components not yet isolated (CenterContains; Kollár's "some blow-up center must contain η_X" in the proof of [Kol07, Corollary 22]). Stage 0 is "before the first blow-up of the round".
stageTriple T hm n — the marked triple induced at stage n of the run truncated there (MarkedTriple.induced; a prefix of a sequence of order ≥ 1 is one). isolatedTriple T hm C n — that triple with its ideal replaced by the colon I_n : I_Γ, I_Γ the REDUCED ideal of the union of the absorbed strict transforms: I : I_Γ is 𝒪 near Γ where I = I_Γ, and I away from Γ; it is canonical, with no choice of a neighbourhood. remainingComponents T hm C n — the strict transforms of the other members of C at stage n. Both are the constructions isolatedAt and remainingAt for an arbitrary run and arbitrary absorbed and remaining families, at the truncated run.
bedAux T hm C — the loop: run BMO_1 on T; if some stage has an absorption, take the FIRST such stage n₀ (Nat.find), truncate the run BEFORE the absorbing blow-up (take n₀), isolate, and recurse on the isolated triple with the remaining components (well-founded on the number of remaining components, the absorbed set being nonempty); if no stage has one, the round is the whole run and the loop stops. The restart on the modified marked triple IS the definition: no stability property of Kollár's functors is assumed, and the exhaustiveness "every remaining component is eventually absorbed" ([Wlo05, 4.6]: otherwise the generic points would be transformed isomorphically) is a theorem about this object, not a clause of it.
BED T — Włodarczyk's embedded desingularization sequence of the triple T = (X, I_Y, E): the loop from the marked triple (X, I_Y, 1, E) with the components of V(I_Y) (their reduced ideals, componentIdeals). The theorem concerns E = ∅ and reduced Y; the definition needs neither.

Where the stop happens #

At mark 1 every absorption of a strict transform happens in the d = 1 round of Step 1 of [Kol07, Theorem 107] (Hironaka.Resolution.Algebraic.MarkedOrderReduction.Step1NonmonomialPart), inside Step 2.2 of [Kol07, Theorem 103] (the modules Hironaka.OrderReduction.Step22*: Lemma 102 at the position of the maximal-contact hypersurface), and at the bottom of the maximal-contact chain it is the opening trivial blow-up π_{-1} of [Kol07, Lemma 102] (Hironaka.BD.piMinusOne) of the hypersurface Ỹ_c ⊂ H_{r-1}, pushed forward through the chain. The strict transform of the absorbed component along that blow-up is EMPTY (strictTransformAlong saturates by the exceptional ideal, which is the component's own ideal), so the stop is what keeps Ỹ alive: Włodarczyk's termination in his Step 1ba is "no π_{-1} at a maximal-contact position", and the truncation before the absorbing blow-up is exactly that.

The clauses of [Wlo05, Theorem 1.0.2] for BED — smooth centres and the simple normal crossing clauses, the centres disjoint from the smooth points of Y, the final strict transform smooth and snc with the boundary, the fine form of the full transform, and the behaviour under smooth morphisms of the ambient — are proved in the modules Hironaka.Resolution.Algebraic.Wlo05.Embedded*, collected for the functor EDFunctor in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedFunctorClauses, and stated as the theorem AlgebraicGeometry.exists_functorial_embeddedDesingularization at the end of that module.

Włodarczyk's embedded desingularization sequence BED #

The construction #

Where the stop happens #

The run of BMO_1 on a marked triple of mark 1 #

One round: the stop rule, the truncated run, the isolated triple #

The loop #

The components of Y and the sequence BED #

Włodarczyk's embedded desingularization sequence `BED` #

The run of `BMO_1` on a marked triple of mark `1` #

The components of `Y` and the sequence `BED` #