A marked sequence of order ≥ m for an ideal of maximal order < m is empty

The marked analogue of eq_nil_of_isOrderSeq_of_maxOrd_lt: a smooth blow-up sequence of order ≥ m starting with (X, I, m, E) [Kol07, Definition 66] and without empty blow-ups [Kol07, 32] is the empty sequence when max-ord I < m. Its first center, being nonempty, contains a generic point of one of its components (Closeds.exists_mem_genericPoints_specializes), where the order of I is ≥ m by condition (4′) of Definition 66, above the maximal order. The closed-embedding clause of the order reduction functors uses this at m = 1 for the unit ideal: when the ideal J on the hypersurface is the unit ideal, both sides of the clause are the empty sequence.

theorem AlgebraicGeometry.eq_nil_of_isOrderGeSeq_of_maxOrd_lt {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) {S : X.BlowUpSequence} {I : X.IdealSheafData} {m : ℕ} {E : X.DivisorFamily} (hS : S.IsOrderGeSeq f I m E) (hne : S.NoEmptyCenters) (hI : I.maxOrd < ↑m) : S = Scheme.BlowUpSequence.nil X

A smooth blow-up sequence of order ≥ m without empty blow-ups, for an ideal of maximal order < m, is the empty sequence [Kol07, Definition 66 and 32].