Theorem 76 and Corollary 77 along a smooth blow-up sequence #
[Kol07, Theorem 76 and Corollary 77] for a smooth blow-up sequence S of order ≥ m starting
with (X, I, m, E) and j ≤ m: with J_0 = D^j(I) and J_{i+1} = (π_i)_*^{-1}(J_i, m − j) (the
marked recursion started at the derivative ideal, S.markedTransformSeq (I.derivativeIter f j) (m - j)) one has J_i ⊆ D^j(I_i) at every stage, every (π_i)_*^{-1}(J_i, m − j) is defined
(F_{i+1}^{m−j} ∣ π_i^* J_i), and S is a smooth blow-up sequence of order ≥ m − j starting
with (X, D^j(I), m − j, E).
The joint induction. Kollár deduces Corollary 77 from Theorem 76, but the transform along the
sequence in Theorem 76 is only defined once the order inequality of Corollary 77 is known at each
stage; the two are therefore proved together, as in [Wlo05, Lemma 2.6.4]. Theorem 76's inclusion
is proved by induction on the sequence S: for nil, J_0 = D^j(I); for cons X D rest, the
first stage is the one-blow-up inclusion π_*^{-1}(D^j(I), m − j) ⊆ D^j(π_*^{-1}(I, m))
(markedTransform_derivativeIter_le, Hironaka/Scheme/BlowUpSequence/TransformDerivative.lean, on
B_D X, which is the stage after the first blow-up definitionally), the marked recursion is
monotone in its starting ideal (markedTransformSeq_mono), and the tail is a sequence of order ≥ m for the transformed data (isOrderGeSeq_cons_iff) to which the induction hypothesis applies. The
order inequality of Corollary 77 is then read off at every stage: ord_{Z_i} J_i ≥ ord_{Z_i} D^j(I_i) ≥ m − j (a smaller ideal has a larger order; [Kol07, Lemma 74 (3)]). The one-stage
inductive step is stated separately for one blow-up (derivSeq_step), and the stagewise
divisibility follows from Corollary 77 through pow_dvd_comap_of_leOrdAlong at each stage
(exceptionalAt_pow_dvd_comap_step_of_leOrdAlong, by induction on S, the eqToHom of the first
step disappearing after a case split on the tail).
Kollár's warning that the transform depends on the whole sequence [Kol07, Warning 63] is why the
statements are made for the recursion markedTransformSeq and not for the composite Π.
The marked recursion is monotone in its starting ideal #
The controlled transform is monotone in the ideal (the colon and the inverse image are).
Kollár's marked transform π_*^{-1}(J, c) is monotone in J.
The marked recursion along a sequence is monotone in its starting ideal (used in the proof of [Kol07, Corollary 77]).
The inductive step at one stage #
The inductive step of [Kol07, Corollary 77] (compare the proof of [Wlo05, Lemma 2.6.4]): for
one smooth blow-up with ord_Z I ≥ m and j ≤ m, an ideal J ⊆ D^j(I) has ord_Z J ≥ m − j and
π_*^{-1}(J, m − j) ⊆ D^j(π_*^{-1}(I, m)).
Theorem 76 and Corollary 77 along the sequence #
[Kol07, Theorem 76] along the sequence (compare [Wlo05, Lemma 2.6.4]): J_i ⊆ D^j(I_i) at
every stage of a smooth blow-up sequence of order ≥ m starting with (X, I, m, E), for j ≤ m.
Induction on the sequence: the first stage is the one-blow-up Theorem 76
(markedTransform_derivativeIter_le), the marked recursion is monotone in its starting ideal,
and the tail is a sequence of order ≥ m for the transformed data.
[Kol07, Corollary 77]: a smooth blow-up sequence of order ≥ m starting with (X, I, m, E)
is one of order ≥ m − j starting with (X, D^j(I), m − j, E): the smoothness and normal
crossing conditions do not mention the ideal, and ord_{Z_i} J_i ≥ m − j because
J_i ⊆ D^j(I_i) (markedTransformSeq_derivativeIter_le) and ord_{Z_i} D^j(I_i) ≥ m − j
(leOrdAlong_derivativeIter).
pow_dvd_comap_of_leOrdAlong at every stage of a smooth sequence: an ideal of order ≥ c
along the center Z_i has F_{i+1}^c ∣ π_i^* K. By induction on the sequence; at the first stage
of a cons the step is blowUpπ once the tail's constructor is known.
The marked transform (π_i)_*^{-1}(J_i, m − j) of the derivative sequence is defined at every
stage in the sense of [Kol07, Definition 60] (F_{i+1}^{m−j} divides π_i^* J_i), because
ord_{Z_i} J_i ≥ m − j ([Kol07, Corollary 77]).