Step 2.1 of order reduction: the rounds and the disjointness from the boundary #
The j-th round of Step 2.1 of the proof of [Kol07, Theorem 103] ([Kol07, 104, Step 2.1])
applies the boundary-clearing functor of [Kol07, Lemma 102] to the induced triple and to the
transform of the j-th member, so that afterwards Π⁻¹_{r(j)*}(E^i) ∩ cosupp(I_{r(j)}, m) = ∅
for every i ≤ j. This module reads off the two branches of the definition of BO.step21Seq
(step21Seq_zero, step21Seq_succ_of_lt, step21Seq_succ_of_not_lt) and its two carried facts
(isOrderSeq_step21Seq, noEmptyCenters_step21Seq), and proves the disjointness by induction on
the number of rounds (disjoint_cosupp_step21). At round j, the disjointness for the new
member E^j is clause (1) of [Kol07, Lemma 102] for BD_{n,m,j} on the induced triple
(BDData.disjoint_cosupp), read on the original family through the positions of the total
transform (nth_totalTransformSeq_of_lt) and transported through the concatenation
(disjoint_cosupp_concat_iff); for the old members E^i, i < j, the disjointness at the end of
the previous round persists along the j-th round because every centre of a blow-up of order m
lies in the cosupport (disjoint_cosupp_strictTransformSeq_last_of_disjoint). After all
card E.ι rounds the birational transform of every member misses the cosupport
(disjoint_cosupp_step21_final), the first of the two conclusions Kollár records at the end of
Step 2.1.
The sequence after j + 1 rounds is the sequence after j rounds followed by BD_{n,m,j}
applied to the induced triple, for a position j of E ([Kol07, 104, Step 2.1]).
Every Step 2.1 sequence is a smooth blow-up sequence of order m starting with (X, I, E):
the first carried fact.
No Step 2.1 sequence has an empty blow-up ([Kol07, 32]): the second carried fact.
After j rounds, the birational transforms of the first j members of E are disjoint from
the cosupport of the final ideal ([Kol07, 104, Step 2.1]).
After all card E.ι rounds, the birational transform of every member of E misses the
cosupport of the final ideal: the first conclusion of [Kol07, 104, Step 2.1],
"Π^{-1}_{r(s)*} E is disjoint from cosupp(I_{r(s)}, m)".