A smooth Y gives the empty succession: the tools

For a smooth reduced Y the embedded desingularization sequence BED(X, I_Y, ∅) (Hironaka.Resolution.Algebraic.Wlo05.Embedded) is the empty succession — [Wlo05, 4.6]: at a smooth point of Y the invariant is already terminal. The theorem is bed_eq_nil_of_smooth (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedNilCore); this module holds the tools of its proof:

• the run of BMO_1 on the unit ideal is empty (bmoOneRun_eq_nil_of_maxOrd_lt_one, bmoOneRun_eq_nil_of_eq_top): a smooth blow-up sequence of order ≥ 1 without empty blow-ups for an ideal of maximal order < 1 is nil (eq_nil_of_isOrderGeSeq_of_maxOrd_lt), and [Kol07, Theorem 69 (1)] with the convention [Kol07, 32] gives both for the run;
• the stage-0 shapes of the loop: the truncation at 0 is the empty sequence (take_zero), and on a sequence written as cons X D rest the stop rule at stage 0 fires for the component vanishingIdeal (closure {η}) of a point η of the first centre D (centerContains_zero_of_mem_support): D ≤ vanishingIdeal (closure {η}) is closure {η} ⊆ supp D (the Galois connection le_support_iff_le_vanishingIdeal), so no reducedness of the centre is used;
• the loop through a round with an absorption at stage 0: the found index is 0 (find_eq_zero_of_hasAbsorptionAt_zero) and the loop's length is the length of the loop from the isolated triple (length_bedAux_of_hasAbsorptionAt_zero); at a round without an absorption on the unit ideal the loop is empty (length_bedAux_eq_zero_of_eq_top).

The invariant of the induction is in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedNilInvariant.

The run on the unit ideal

theorem Hironaka.Resolution.bmoOneRun_eq_nil_of_maxOrd_lt_one {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (hI : T.I.maxOrd < 1) : bmoOneRun T hm = AlgebraicGeometry.Scheme.BlowUpSequence.nil T.X.left

The run of BMO_1 on a marked triple whose ideal has maximal order < 1 is empty ([Kol07, Theorem 69 (1)] with the convention [Kol07, 32]): a smooth blow-up sequence of order ≥ 1 without empty blow-ups for such an ideal is nil (eq_nil_of_isOrderGeSeq_of_maxOrd_lt).

theorem Hironaka.Resolution.bmoOneRun_eq_nil_of_eq_top {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (hI : T.I = ⊤) : bmoOneRun T hm = AlgebraicGeometry.Scheme.BlowUpSequence.nil T.X.left

The run of BMO_1 on the unit ideal is empty (the terminal round of the loop, when nothing is left).

Stage 0 of a sequence

theorem Hironaka.Resolution.take_zero {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) : S.take 0 = AlgebraicGeometry.Scheme.BlowUpSequence.nil X

The truncation of a sequence at 0 is the empty sequence.

theorem Hironaka.Resolution.centerContains_zero_of_mem_support {X : AlgebraicGeometry.Scheme} (D : X.IdealSheafData) (rest : D.blowUp.BlowUpSequence) {η : ↥X} (hη : η ∈ D.support) : CenterContains (AlgebraicGeometry.Scheme.BlowUpSequence.cons X D rest) (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) 0

On a sequence starting with the blow-up of D, if a point η lies in the support of D, the first centre contains the closure of η — as ideals, D ≤ vanishingIdeal (closure {η}) — so the stop rule fires at stage 0 for the component vanishingIdeal (closure {η}) (CenterContains; the strict transform at stage 0 is the ideal itself).

theorem Hironaka.Resolution.hasAbsorptionAt_zero_of_mem_support {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) {D : T.X.left.IdealSheafData} {rest : D.blowUp.BlowUpSequence} (hrun : bmoOneRun T hm = AlgebraicGeometry.Scheme.BlowUpSequence.cons T.X.left D rest) {η : ↥T.X.left} (hη : η ∈ D.support) (hC : AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η}) ∈ C) : HasAbsorptionAt T hm C 0

The stop rule at stage 0 for the loop's component set, when the run starts with the blow-up of D, from a point η ∈ D whose component ideal is in the set.

theorem Hironaka.Resolution.find_eq_zero_of_hasAbsorptionAt_zero {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (h0 : HasAbsorptionAt T hm C 0) : Nat.find ⋯ = 0

With an absorption at stage 0, the loop's first index is 0.

theorem Hironaka.Resolution.isolatedTriple_m {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (n : ℕ) : (isolatedTriple T hm C n).m = 1

The isolated triple keeps the mark 1.

The length of the loop through a round

theorem Hironaka.Resolution.length_bedAux_of_hasAbsorptionAt_zero {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (h0 : HasAbsorptionAt T hm C 0) : (bedAux T hm C).length = (bedAux (isolatedTriple T hm C 0) ⋯ (remainingComponents T hm C 0)).length

At a round with an absorption at stage 0 the loop's length is the length of the loop from the isolated triple at stage 0 (the truncation at 0 is empty).

theorem Hironaka.Resolution.length_bedAux_eq_zero_of_eq_top {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) (h : ¬∃ (n : ℕ), HasAbsorptionAt T hm C n) (hI : T.I = ⊤) : (bedAux T hm C).length = 0

At a round without an absorption the loop is the run, whose length is 0 when the ideal is the unit ideal.