The composite sequence on S = E^j and going up #
The proof of [Kol07, Lemma 102], third and fourth paragraphs: by the going-up theorem
[Kol07, Theorem 84], every blow-up sequence of order ≥ m starting with
(S, I_0|_S, m, (E − E^j)|_S) corresponds to a blow-up sequence of order m starting with
(X_0, I_0, E − E^j); since S = E^j, every blow-up center is a smooth subvariety of the
birational transform of E^j; and the output is BMO_{n−1,m}(S, I_0|_S, m, (E − E^j)|_S) pushed
forward ([Kol07, 30.3]) and composed on the right with the first blow-up π_{-1}.
The first step on S. Z_{-1}|_S, Z_{-1} viewed on S = E^j, pushes forward to Z_{-1}
(since Z_{-1} ⊆ E^j), is smooth over k (it is Z_{-1} itself, smooth by Center.lean), and
I|_S has order ≥ m along it (the order of I is ≥ m on Z_{-1} and does not drop under
restriction). Its exceptional divisor on X_S = blowUp S (Z_{-1}|_S) is empty: through the closed
immersion τ = blowUpMap ι Z_{-1} onto the birational transform of E^j, a point of X_S lies
over a point of E^j off Z_{-1} (Transform.lean describes that birational transform as the
saturation (E^j : Z_{-1}^∞)), so the pulled-back ideal of Z_{-1} is the unit ideal everywhere.
The restricted marked triple's fields are what its definition says (restrictedTriple_X/I/m/E),
its ideal is Kollár's I_0|_S (markedTransform_centerS_eq, the degenerate analogue of
[Kol07, Lemma 62]), and its old
members are the members of E_0 − E^j restricted along τ.
Going up, and the Warning in [Kol07, 104]. Theorem 84 as printed needs a D-balanced ideal,
which I_0 need not be; Kollár's reading is that the consequences of Theorem 84 hold for any
sequence of blow-ups of order m starting from the D-balanced I. So the composite sequence ON
S, first center Z_{-1}|_S, then B's sequence on the restricted marked triple, is a smooth
blow-up sequence of order ≥ m starting with (S, I|_S, m, (E − E^j)|_S)
(isOrderGeSeq_cons_centerS; [Kol07, Definition 66] step by step: the three facts about
Z_{-1}|_S, then B's own order condition, whose data are exactly the induced marked triple after
the first step), and the going-up theorem (Hironaka/Resolution/Algebraic/Kol07/GoingUp.lean) for
the D-balanced I on X with S = E^j and E − E^j gives that its push-forward rawSeq is a
smooth blow-up sequence of order m starting with (X, I, E − E^j) (isOrderSeq_rawSeq_erase).
The push-forward is π_{-1} followed by τ_* B(…) (rawSeq_eq, take_one_rawSeq: its first
center is Z_{-1} by map_centerS), so Definition 66 after one step gives Kollár's sentence: τ_* B(…) is a smooth blow-up sequence of order m starting with (X_0, I_0, E_0 − E^j)
(isOrderSeq_pushforward_restricted).
Bookkeeping for the output. Every center of rawSeq lies in the birational transform of E^j
at its stage (strictTransformSeq_le_center_pushforward_subschemeι), and only the first blow-up
π_{-1} can be empty: B returns no empty blow-ups and pushing a center forward along a closed
immersion preserves that.
Used by Output.lean, and outside this directory by the embedded-resolution modules
Hironaka/Resolution/Algebraic/Wlo05/EmbeddedNilCaseA.lean,
Hironaka/Resolution/Algebraic/Wlo05/EmbeddedCP1Step22Core.lean and
Hironaka/Resolution/Algebraic/Wlo05/EmbeddedCP3Raw.lean.
The push-forward of Z_{-1}|_S to X is Z_{-1}: the first center of the pushed-forward
composite sequence is the center of π_{-1} (map_comap_of_ker_le; Z_{-1} ⊆ E^j by
Basic.lean).
Z_{-1}|_S is smooth over k ([Kol07, Definition 65]; [Kol07, Notation 19]): as a closed
subscheme of S it is Z_{-1}, which is smooth (Center.lean).
I|_S has order ≥ m along Z_{-1}|_S (the order condition of [Kol07, Definition 65] for the
marked triple): the order of I is ≥ m on Z_{-1} (Basic.lean) and does not decrease under
restriction.
The exceptional divisor of Z_{-1}|_S on X_S is empty: X_S maps by τ onto the birational
transform of E^j, whose points lie over E^j off Z_{-1} (the saturation description of
Transform.lean), so the pulled-back ideal of Z_{-1} is the unit ideal at every point of
X_S.
The scheme of the restricted marked triple is X_S = blowUp S (Z_{-1}|_S), Kollár's S = E^j
on X_0 (the proof of [Kol07, Lemma 102]).
The ideal of the restricted marked triple is the marked transform of I|_S with control m
along Z_{-1}|_S.
The mark of the restricted marked triple is m.
The family of the restricted marked triple is the total transform of (E − E^j)|_S along
Z_{-1}|_S (Kollár's E_S := (E − E^j)|_S).
The ideal of the restricted marked triple is the restriction of I_0 = (π_{-1})^{-1}_* I along
τ = blowUpMap ι Z_{-1}, Kollár's I_0|_S (markedTransform_centerS_eq, the degenerate analogue
of [Kol07, Lemma 62]; [Kol07, Remark 67]).
The old members of the restricted family are the restrictions along τ of the members of
E_0 − E^j, the birational transforms of the members of E other than E^j
(strictTransform_comap_blowUpMap_of_hasSncWith, with (E − E^j) + E^j = E having snc with
Z_{-1} by Center.lean).
The composite sequence on S, first center Z_{-1}|_S, then the output of B on the
restricted marked triple, is a smooth blow-up sequence of order ≥ m starting with
(S, I|_S, m, (E − E^j)|_S) (the proof of [Kol07, Lemma 102] read through the Warning in
[Kol07, 104]): [Kol07, Definition 66] step by step (isOrderGeSeq_cons_iff), the three facts about
Z_{-1}|_S, then B's own order condition on the induced marked triple.
The output before the deletion of empty blow-ups is the push-forward ([Kol07, 30.3]) of the
composite sequence: first the blow-up of X along (Z_{-1}|_S).map ι, then tailSeq = τ_* B(…)
(pushforward_cons).
The first blow-up of the output is π_{-1} (Kollár composes "on the right with our first
blow-up π_{-1}", the proof of [Kol07, Lemma 102]): its center is (Z_{-1}|_S).map ι = Z_{-1}.
The output is a smooth blow-up sequence of order m starting with (X, I, E − E^j): the
going-up theorem [Kol07, Theorem 84] applied, per the Warning in [Kol07, 104], to the composite
sequence from the D-balanced I, with S = E^j (a smooth divisor) and (E − E^j) + E^j = E snc
(Hironaka/Resolution/Algebraic/Kol07/GoingUp.lean).
The tail of the output, τ_* B(S, I_0|_S, m, E_S), is a smooth blow-up sequence of order m
starting with (X_0, I_0, E_0 − E^j), where X_0 is the blow-up of X along
(Z_{-1}|_S).map ι = Z_{-1} (Kollár's "blow-up sequence of order m starting with
(X_0, I_0, E − E^j)", the proof of [Kol07, Lemma 102]): [Kol07, Definition 66] after the first
step (isOrderSeq_cons_iff).
Each center of the output lies in the birational transform of E^j at its stage (Kollár's
"every blow-up center is a smooth subvariety" of that birational transform, the proof of
[Kol07, Lemma 102]): strictTransformSeq_le_center_pushforward_subschemeι.
Only the first blow-up of the output can be empty: B returns no empty blow-ups ([Kol07, 32]
for BMO), and pushing a center forward along a closed immersion preserves nonemptiness
(comap_map).