The derivative ideals along a blow-up sequence of order ≥ m #
For a smooth blow-up sequence of order ≥ m starting with (X, I, m) and j ≤ m, the marked
transforms J_i of (D^j(I), m − j) along the same sequence satisfy J_i ⊆ D^j(I_i) for every
i, and the sequence is of order ≥ m − j starting with (X, D^j(I), m − j)
[Kol07, Corollary 77]. Kollár's argument: J_i = (Π_i)_*^{-1}(D^j I, m − j) ⊂ D^j (Π_i)_*^{-1}(I, m) = D^j(I_i), the containment being his Theorem 76 for the composite, and ord_{Z_i} I_i ≥ m gives
ord_{Z_i} D^j(I_i) ≥ m − j since each derivative lowers the order by at most one. The proof here
is an induction on the stage: at each step Theorem 76 for one blowing-up
(markedTransform_iteratedDeriv_le) and the monotonicity of the marked transform in the ideal
sheaf (birationalTransform_mono; both marked transforms are defined because the order along the
centre is antitone in the ideal sheaf, le_ordAlongIdeal_of_le, and ord_{Z_i} D^j(I_i) ≥ m − j
by le_ordAlongIdeal_iteratedDeriv). The containment is also proved in a prefix-bounded form
(markedTransformSeq_iteratedDeriv_le_of_forall_lt) that needs the order clause only at the
steps before the stage considered.
Also here: the ideal sheaf of a closed submanifold does not depend on the chart ψ : E ≃ 𝕜ⁿ
carried by the submanifold predicate (IsClosedSubmanifold.idealSheaf_eq_of_chart), needed
because a sequence carries one chosen chart per step.
This is the step by which the maximal-contact theorem [Kol07, Theorem 80] passes from a sequence
of order m for I to a sequence of order ≥ 1 for D^{m−1}(I).
The order along a centre is antitone in the ideal sheaf: J ⊆ K gives
ord_D K ≤ ord_D J at every point (in the form the marked transforms use).
The ideal sheaf of a closed submanifold does not depend on the chart ψ of the submanifold
predicate: at a point of Y a germ lies in it iff its section vanishes on Y nearby
(germ_mem_stalkIdeal_idealSheaf_iff), and off Y it is the unit ideal. The same-set case of
IsClosedSubmanifold.idealSheaf_congr (module BlowUp.Transform.IdealSheafCongr), which carries
the proof.
The marked transform is monotone in the ideal sheaf (colon ideals are monotone in the numerator), for a mark that is legitimate for the larger ideal sheaf (hence for the smaller one too, the order along the centre being antitone).
The order clause of [Kol07, Corollary 77] at one stage: where J_i ⊆ D^j(I_i) holds and
ord_{Z_i} I_i ≥ m (the order clause (4′) at the step i alone), ord_{Z_i} J_i ≥ m − j, since
ord_{Z_i} D^j(I_i) ≥ m − j.
The order clause of [Kol07, Corollary 77] at one stage, for a sequence of order ≥ m
(le_ordAlong_iteratedDeriv_of_le_of_le_ordAlong with the order clause (4′) of h).
The containment J_i ⊂ D^j(I_i) of [Kol07, Corollary 77] in a prefix-bounded form: for
j ≤ m and a stage i, if the marked transforms of (I, m) have order ≥ m along the centres
of the steps before i (the order clause (4′) of [Kol07, Definition 66] on the prefix, with no
normal-crossings clause), the marked transform of (D^j(I), m − j) at stage i lies in the
j-th derivative ideal sheaf of the marked transform of (I, m). Induction on the stage with
Kollár's Theorem 76 for one blowing-up and the monotonicity of the marked transform; the step
i uses (4′) at step i only.
The containment J_i ⊂ D^j(I_i) for every i of [Kol07, Corollary 77]: along a smooth
blow-up sequence of order ≥ m starting with (M, I, m, E₀) and for j ≤ m, the marked
transforms of (D^j(I), m − j) lie in the j-th derivative ideal sheaves of the marked
transforms of (I, m), at every stage (markedTransformSeq_iteratedDeriv_le_of_forall_lt with
the order clause (4′) of h).
A smooth blow-up sequence of order ≥ m starting with (M, I, m, E₀) is a smooth blow-up
sequence of order ≥ m − j starting with (M, D^j(I), m − j, E₀) [Kol07, Corollary 77].