CP3 through Step 1, and the Step 1 reduction along the tower #
Step 1 of the proof of [Kol07, Theorem 107] (item 111, Step 1): BMO_{n,1} on (X, I, 1, E)
runs rounds of BO_{n,d} on the nonmonomial part N(I) for d = max-ord N(I) descending to 1,
then Steps 2 and 3. Along a round of order d the ideal of the round is the weak transform of
N(I), which is the nonmonomial part of the marked transform of I at every stage
(Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Weak). For the statement CP3 of the embedded
desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative): at a point of a
centre of a round of order ≥ 2 no chain shape of the current ideal exists, since its nonmonomial
part would have order ≤ 1 there while the centre has order ≥ 2; the round of order 1 is
BO_{n,1} on the nonmonomial triple, and the classification for N(K) given by the hypothesis
CP3BOFor is one for K (centerClassifiedAt_of_nonmonomialPart, the fine split of Kol07,
Definition–Lemma 110 with top monomial 1, and stratumIn_of_stratumIn_zero). The loop is the
well-founded recursion step1 of
Hironaka.Resolution.Algebraic.MarkedOrderReduction.Step1NonmonomialPart (cp3For_concat); at the
mark 1 Step 2 is empty; Step 3 is cp3For_step3Seq
(Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Step3); the base of the tower and its Step 1
reduction follow (cp3BMOAt_zero, cp3BMOAt_succ_of_cp3BOAt; [Kol07, 70]). This argument is not in
the literature. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Tower.
A stratum in the coordinates with the zero exponents is a stratum for any exponents: the zero exponents force a positive level, where the top exponents do not enter.
The marked transform of the unit ideal is the unit ideal at every stage (by the definition of
the marked transform, π⁻¹_*(I, m) = 𝒪(mF) · π^* I).
The classification for the ideal from the classification for its nonmonomial part (the fine
split of [Kol07, Definition–Lemma 110] read as a transfer): a chain shape of K gives the same
shape with top monomial 1 of N(K) (stalkIdeal_nonmonomialPart_of_kShape,
stalkIdeal_nonmonomialPart_of_iShape), whose stratum is one for K.
The rounds of order ≥ 2 of Step 1 ([Kol07, 111, Step 1]): no point of their centres carries
a K- or I-shape of the current ideal, since the nonmonomial part has order ≤ 1 at such a point
(ord_le_one_of_stalkIdeal_eq_chainKIdeal, ord_le_one_of_stalkIdeal_eq_chainIdeal), it is the
ideal of the round (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Weak), and the centre of the
round has order ≥ 2 (notMem_of_leOrdAlong_two); CP3 holds vacuously.
The round of order 1 of Step 1 ([Kol07, 111, Step 1] at d = 1) is BO_{n,1} on the
nonmonomial triple; its classification (the hypothesis CP3BOFor) is for the marked transform of
N(I) = the weak transform ([Kol07, Remark 67]) = the nonmonomial part of the marked transform
of I (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Weak), and a classification for N(K) is
one for K (centerClassifiedAt_of_nonmonomialPart).
The induction behind cp3For_step1 ([Kol07, 111, Step 1], the loop on d = max-ord N(I)),
on a bound for the loop variable: a round of order ≥ 2, or the round of order 1, then the
rest of Step 1 on the induced marked triple (cp3For_concat).
CP3 along the whole Step 1 ([Kol07, 111, Step 1]; recursion on the order of the round,
cp3For_concat).
At the mark 1 Step 2 is empty ([Kol07, 111, Steps 1–2]): after Step 1 the nonmonomial part
is the unit ideal (roundOrder_afterStep1_lt), so the separation order is 0
(sepOrder_eq_zero_iff, step2_of_eq_zero).
CP3 along BMO_{n,1} from CP3 along BO_{n,1} ([Kol07, 111]): the three steps concatenated
(cp3For_concat; Step 2 empty, Step 3 by cp3For_step3Seq).
The base of the tower ([Kol07, 70]): in dimension 0 the ideal is the unit ideal
(Triple.I_eq_top_of_hasDimLE_zero), so the marked transforms are the unit ideal and no centre
of order ≥ 1 has a point.
The Step 1 reduction along the tower ([Kol07, 70, (70.2)]: (68) in dimension n gives (69) in
dimension n): CP3 for BMO_{n+1,1} from CP3 for BO_{n+1,1} (bmoRun is bmoSeq on the data
boOfBMO of the tower).