Step 2.1 never contains the component #
Step 2.1 of the proof of [Kol07, Theorem 103] (item 104, Step 2.1) runs the boundary-clearing
functor BD_{n,1,j} of [Kol07, Lemma 102] over the members E^j of the boundary in turn. Every
centre of the output of Lemma 102 is the push-forward of a centre on the strict transform of
E^j (the proof of [Kol07, Lemma 102]: the output is the push-forward along E^j ↪ X of the
run on E^j). A centre containing the strict transform c̃ of the component c = V(closure {η})
would therefore put c̃, hence its generic point, inside the strict transform of E^j; but the
generic point lies on no member of the boundary (GenericLift.notMem,
Hironaka.Resolution.Algebraic.Wlo05.EmbeddedGenericLift). Hence no centre of Step 2.1 contains
c̃, and the statement CP1 of the embedded desingularization
(Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) holds vacuously along it: the first
containing stage of the order reduction BO_{n,1} lies in Step 2.2. This observation is not in the
literature.
Three layers: the raw output rawSeq (not_centerContains_rawSeq, a strong induction on the
stage with the lifted generic point and
strictTransformSeq_le_center_pushforward_subschemeι); the functor of Lemma 102 at the mark 1
with the data bdData — the tuning parameter at the mark 1 is 1 and the empty blow-ups are
deleted (not_centerContains_bdData_seq, through exists_eraseIdx_eq and
centerContains_eraseEmpty_iff); and the iterated concatenation of Step 2.1
(not_centerContains_step21Seq, cp1For_step21Seq;
Hironaka.Resolution.Algebraic.OrderReduction.Step21BoundaryClearing). Used in
Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1Step2.
The raw output of Lemma 102 never contains c̃ (the proof of [Kol07, Lemma 102]): its
centres are push-forwards of centres on the strict transform of the member E^j, and the lifted
generic point of η lies on no member. Stated for any ideal sheaf I whose generic point η is
off the boundary; the centres of the sequence do not involve I.
The output of Lemma 102 never contains c̃ ([Kol07, Lemma 102] with the data bdData at
the mark 1), for any ideal sheaf I whose generic point η is off the boundary: the tuning
parameter at the mark 1 is 1, the value is rawSeq with its empty blow-ups deleted, and the
deletion preserves the stop rule (centerContains_eraseEmpty_iff).
The output of Lemma 102 with the data bdData at the mark 1 never contains c̃, for the
triple's own ideal (the proof of [Kol07, Lemma 102]).
Step 2.1 never contains c̃ ([Kol07, 104, Step 2.1]): by induction on the number of
passes, through the stop rule of the concatenation (centerContains_concat_iff_of_lt,
centerContains_concat_add_iff), each pass being the output of Lemma 102 on the induced triple
at the lifted generic point (not_centerContains_bdData_seq_of).
CP1 holds vacuously along Step 2.1.