Step 2 of order reduction: the assembled sequence and the maximal-contact case #
Steps 1 and 2 of the proof of [Kol07, Theorem 103]: on a triple with a smooth hypersurface of
maximal contact, BO_{n,m}(X, I, E) is Step 2.1 followed by Step 2.2 on the tuned ideal
W_{s(m)}(I), and the empty sequence when max-ord I < m.
- Step 2 (
step2Seq = S₁.concat step22) is a smooth blow-up sequence of ordermfor(X, I, E)(isOrderSeq_concat, the second part being an order-msequence for the original boundary byisOrderSeq_step22_totalTransformSeq), without empty blow-ups (noEmptyCenters_concat), whose final ideal hasmax-ord < m(maxOrd_weakTransformSeq_concat_lastreduces it tomaxOrd_step22_lt); the deletion of empty blow-ups of [Kol07, 32] is the identity on it. BO^H_{n,m}(maxContactCase) is read back through the tuning of Step 1 (Hironaka.BD.isOrderSeq_iff_tuned,maxOrd_weakTransformSeq_lt_iff_tuned): a smooth blow-up sequence of ordermfor the original(X, I, E), without empty blow-ups, withmax-ord I_r < m(clause (1) of Theorem 103); below the mark the empty sequence, for which clause (1) ismax-ord I < mitself.
These are the fields of the local functor of Step 3
(Hironaka/Resolution/Algebraic/OrderReduction/Step3Globalization.lean).
Step 2 is Step 2.1 followed by Step 2.2 (definitional).
Step 2 is a smooth blow-up sequence of order m starting with (X, I, E) (Step 2 of the
proof of [Kol07, Theorem 103]): isOrderSeq_concat, Step 2.2 being an order-m sequence for the
original boundary E_r.
Step 2 has no empty blow-up ([Kol07, 32]).
The final ideal of Step 2 has max-ord < m (clause (1) of [Kol07, Theorem 103] for Step 2):
it is the final ideal of Step 2.2 up to the identification of the last stages.
Deleting the empty blow-ups of Step 2 changes nothing: there are none ([Kol07, 32]).
At the mark, BO^H_{n,m}(X, I, E) is Step 2 on the tuned triple (X, W_{s(m)}(I), E) at the
mark s(m), with H kept (retune_keeps_maxContact): Step 1 of the proof of
[Kol07, Theorem 103].
Below the mark, BO^H_{n,m}(X, I, E) is the empty sequence (the remark after
[Kol07, Theorem 68]).
BO^H_{n,m}(X, I, E) is a smooth blow-up sequence of order m starting with (X, I, E):
Step 2 on the tuned triple, read back through Hironaka.BD.isOrderSeq_iff_tuned
([Kol07, Corollary 101]), or the empty sequence.
BO^H_{n,m}(X, I, E) has no empty blow-up ([Kol07, 32]).
max-ord I_r < m at the end of BO^H_{n,m}(X, I, E) (clause (1) of [Kol07, Theorem 103]):
Step 2's max-ord < s(m) for the tuned ideal read back through
maxOrd_weakTransformSeq_lt_iff_tuned; below the mark, max-ord I < m itself.
Deleting the empty blow-ups of BO^H_{n,m}(X, I, E) changes nothing: there are none
([Kol07, 32]).