Order ≥ m for a smaller marked ideal along the same sequence

In the proof of Theorem 107, order reduction for the monomial part M(I) is run where I = M(I), off the cosupport of the nonmonomial part [Kol07, 111, Steps 2 and 3]. In this library the geometric third step is run on X itself for the marked ideal (M(I), m), and its centers are read as centers for (I, m): the sequence is of order ≥ m for (I, m) because I ⊆ M(I) and the marked transform is monotone in the ideal (markedTransformSeq_mono), so at every center ord_{Z_i} I_i ≥ ord_{Z_i} M_i ≥ m (a smaller ideal has the larger cosupport, property (1) of the cosupport in [Kol07, Definition 59]). This is the marked analogue of isOrderGeSeq_of_isOrderSeq_of_le (Hironaka/Scheme/BlowUpSequence/MarkedLeWeak.lean: order d ≥ m for J unmarked, hence ≥ m for (I, m) marked); here both ideals are marked at the same m.

• isOrderGeSeq_of_le: a smooth blow-up sequence of order ≥ m for (X, J, m, E) is one for (X, I, m, E) whenever I ≤ J (same centers, same boundaries; no smoothness of X enters).

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

A smooth blow-up sequence of order ≥ m for (X, J, m, 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 ≥ m at every stage since Π^{-1}_{i *}(I, m) ⊆ Π^{-1}_{i *}(J, m) ("cosupp(I, m) ⊃ cosupp(J, m) for I ⊂ J", [Kol07, Definition 59]). The marked analogue of isOrderGeSeq_of_isOrderSeq_of_le; no smoothness of X is used beyond what IsOrderGeSeq f carries.