Clause (a) of Włodarczyk's Theorem 1.0.2: the modified run is a smooth blow-up sequence

The embedded desingularization sequence BED(X, I_Y, ∅) (Hironaka.Resolution.Algebraic.Wlo05.Embedded) is a concatenation of truncations of runs of BMO_1 on marked triples of mark 1: the run on the original triple, truncated before the absorbing blow-up, then the loop on the isolated triple — the induced triple at the truncation's end with its ideal enlarged to the colon by the absorbed components. Each run is a smooth blow-up sequence of order ≥ 1 for its own marked triple ([Kol07, Theorem 69 (1)], isOrderGeSeq_bmoOneRun); the truncation keeps that (isOrderGeSeq_take); the concatenation keeps it when the tail is one for the induced data (isOrderGeSeq_concat); and enlarging the ideal only lowers the order along the centres (isOrderGeSeq_of_le: the colon contains the ideal). Hence, by strong induction on the number of members, BED(X, I_Y, ∅) is a smooth blow-up sequence of order ≥ 1 starting with (X, I_Y, 1, ∅) (isOrderGeSeq_BED, in the sense of [Kol07, Definition 66]): every centre is smooth (BED_center_smooth), has simple normal crossings with the total transform of the boundary at its stage (BED_hasSncWith_center), and the total transforms are snc at every stage (BED_isSnc_totalTransformSeq, IsOrderGeSeq.isSnc_totalTransformSeq) — clause (a) of [Wlo05, Theorem 1.0.2] and the smoothness of the centres.

The three theorems take the hypotheses of the theorem — empty boundary, reduced Y — and are the forms used by Hironaka.Resolution.Algebraic.Wlo05.EmbeddedFunctorClauses.

theorem Hironaka.Resolution.isOrderGeSeq_bedAux {k : Type u} [Field k] [CharZero k] (N : ℕ) (T : MarkedTriple k) (hm : T.m = 1) (C : Finset T.X.left.IdealSheafData) : C.card = N → (bedAux T hm C).IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I 1 T.E

The loop is a smooth blow-up sequence of order ≥ 1 starting with (X, I, 1, E) ([Kol07, Definition 66]; [Kol07, Theorem 69 (1)]) — by strong induction on the number of members: the run truncated before the absorbing blow-up is one (isOrderGeSeq_take), the loop on the isolated triple is one for the induced data with the enlarged ideal (the induction hypothesis with isOrderGeSeq_of_le, the colon containing the ideal), and the concatenation is one (isOrderGeSeq_concat); without an absorption the loop is the run itself.

theorem Hironaka.Resolution.isOrderGeSeq_BED {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) : (BED T).IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I 1 T.E

The modified run BED(X, I_Y, ∅) is a smooth blow-up sequence of order ≥ 1 starting with (X, I_Y, 1, ∅) ([Wlo05, Theorem 1.0.2 (a)]; [Kol07, Definition 66]).

The three clauses

theorem Hironaka.Resolution.BED_center_smooth {k : Type u} [Field k] [CharZero k] (TX : AlgebraicGeometry.Triple k) (_hE : IsEmpty TX.E.ι) (i : Fin (BED TX).length) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp ((BED TX).center i).subschemeι (CategoryTheory.CategoryStruct.comp ((BED TX).stageMap i.castSucc) (TX.X.left ↘ AlgebraicGeometry.Spec ↧k)))

Every centre of BED(X, I_Y, ∅) is smooth over k — Włodarczyk's "blow-ups σᵢ of smooth centers C_{i−1}" [Wlo05, Theorem 1.0.2].

theorem Hironaka.Resolution.BED_isSnc_totalTransformSeq {k : Type u} [Field k] [CharZero k] (TX : AlgebraicGeometry.Triple k) (_hE : IsEmpty TX.E.ι) (i : Fin ((BED TX).length + 1)) : ((BED TX).totalTransformSeq TX.E i).IsSnc

The total transform of the boundary at every stage of BED(X, I_Y, ∅) is snc (IsOrderGeSeq.isSnc_totalTransformSeq) — the first part of clause (a) of [Wlo05, Theorem 1.0.2].

theorem Hironaka.Resolution.BED_hasSncWith_center {k : Type u} [Field k] [CharZero k] (TX : AlgebraicGeometry.Triple k) (_hE : IsEmpty TX.E.ι) (i : Fin (BED TX).length) : ((BED TX).totalTransformSeq TX.E i.castSucc).HasSncWith ((BED TX).center i)

Every centre has simple normal crossings with the total transform at its stage — the second part of clause (a) of [Wlo05, Theorem 1.0.2], "Cᵢ has simple normal crossings with Eᵢ".