The marked transform of a smaller ideal is contained in the birational transform

In the proof of Theorem 107, "if ord N(I) ≥ m, we can apply order reduction (68) to N(I), until its order drops below m" [Kol07, 111, Step 1]: a round of order reduction for the nonmonomial part N(I) at d = max-ord N(I) ≥ m is a sequence of order d ≥ m for N(I), hence of order ≥ m for (I, m), since ord_Z I ≥ ord_Z N(I). At the later stages of the round the center Z_i has ord_{Z_i} J_i = d for the birational transform J_i of J = N(I), and the marked transform I_i of (I, m) must have ord_{Z_i} I_i ≥ m; this module supplies the per-stage inclusion I_i ⊆ J_i. One step is π^{-1}_*(I, m) = (π^* I : F^m) ⊆ (π^* J : F^m) ⊆ (π^* J : F^d) = π^{-1}_* J for I ⊆ J, m ≤ d = ord_Z J (the colon is monotone in the ideal and antitone in the divisor; the birational transform of J is its marked transform at the exact order d, weakTransform_eq_markedTransform_of_smooth), and ord_{Z_i} I_i ≥ ord_{Z_i} J_i = d ≥ m follows because the order is antitone in the ideal.

• markedTransform_le_weakTransform_of_le: one blow-up.
• markedTransformSeq_le_weakTransformSeq_of_le: along a smooth blow-up sequence of order d for J, at every stage.
• isOrderGeSeq_of_isOrderSeq_of_le: a smooth blow-up sequence of order d ≥ m for (X, J, E) is a smooth blow-up sequence of order ≥ m for (X, I, m, E) whenever I ⊆ J (same centers, same boundaries).

theorem AlgebraicGeometry.markedTransform_le_weakTransform_of_le {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] {I J : X.IdealSheafData} {m d : ℕ} (hmd : m ≤ d) (D : X.IdealSheafData) [Smooth (CategoryTheory.CategoryStruct.comp D.subschemeι f)] (hord : J.OrdAlongEq D.support ↑d) (hIJ : I ≤ J) : I.markedTransform D m ≤ J.weakTransform D

For I ⊆ J, m ≤ d and a smooth center D with ord_D J = d, the marked transform π^{-1}_*(I, m) = (π^* I : F^m) of [Kol07, Definition 60] is contained in the birational transform π^{-1}_* J = (π^* J : F^d) of [Kol07, 58].

theorem AlgebraicGeometry.markedTransformSeq_le_weakTransformSeq_of_le {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] {I J : X.IdealSheafData} {E : X.DivisorFamily} {m d : ℕ} (hmd : m ≤ d) {S : X.BlowUpSequence} (hS : S.IsOrderSeq f J E d) (hIJ : I ≤ J) (i : Fin (S.length + 1)) : S.markedTransformSeq I m i ≤ S.weakTransformSeq J i

Along a smooth blow-up sequence of order d ≥ m for (X, J, E), the marked transforms of (I, m) are contained in the birational transforms of J at every stage whenever I ⊆ J; the per-stage form of "ord_Z I ≥ ord_Z N(I)" in [Kol07, 111, Step 1].

theorem AlgebraicGeometry.isOrderGeSeq_of_isOrderSeq_of_le {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] {I J : X.IdealSheafData} {E : X.DivisorFamily} {m d : ℕ} (hmd : m ≤ d) {S : X.BlowUpSequence} (hS : S.IsOrderSeq f J E d) (hIJ : I ≤ J) : S.IsOrderGeSeq f I m E

A smooth blow-up sequence of order d ≥ m for (X, J, E) is a smooth blow-up sequence of order ≥ m for (X, I, m, E) whenever I ⊆ J: the same centers, smooth and with simple normal crossings with the same boundaries, and ord_{Z_i} I_i ≥ ord_{Z_i} J_i = d ≥ m at every stage by the per-stage inclusion. This is how the order reduction of N(I) in [Kol07, 111, Step 1] is a sequence of order ≥ m for (I, m).