Remark 67: passing between the marked and the unmarked versions

[Kol07, Remark 67]: if max-ord I = m, then in any blow-up sequence of order ≥ m starting with (X, I, m, E) one has max-ord I_i ≤ m by Lemma 61, so every blow-up has order exactly m; deleting the mark therefore gives a blow-up sequence of order m starting with (X, I, E), "and the converse also holds".

One step. Along a smooth center D with ord_D I ≥ m at every generic point and max-ord I ≤ m, the order along D is exactly m (ord_η I ≤ max-ord I ≤ m), so the marked transform is the weak transform (weakTransform_eq_markedTransform_of_smooth), and its max-ord is again ≤ m: by [Kol07, Lemma 61] for a smooth center of any shape when D is nonempty (then some generic point exists and max-ord I = m exactly), and trivially when D = ∅ (the blow-up is an isomorphism and no point lies over the center, ord_controlledTransform_le_of_notMem).

Along the sequence. The invariant max-ord I_i ≤ m propagates by induction on the sequence with the one-step lemma; it gives ord_{Z_i} I_i = m at every stage, the stagewise equality of the marked and the unmarked induced ideals, and the equivalence of the two notions of a sequence for (X, I, E) with max-ord I = m. The converse direction needs no bound on max-ord: ord_{Z_i} I_i = m already makes the marked and unmarked transforms agree at every stage.

theorem AlgebraicGeometry.ordAlongEq_of_leOrdAlong_of_maxOrd_le {X : Scheme} (D I : X.IdealSheafData) {m : ℕ} (hI : I.maxOrd ≤ ↑m) (hord : I.LeOrdAlong D.support ↑m) : I.OrdAlongEq D.support ↑m

The order along a closed subscheme is exactly m when it is ≥ m and max-ord I ≤ m.

theorem AlgebraicGeometry.maxOrd_markedTransform_le {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (D I : X.IdealSheafData) {m : ℕ} (hD : Smooth (CategoryTheory.CategoryStruct.comp D.subschemeι f)) (hI : I.maxOrd ≤ ↑m) (hord : I.LeOrdAlong D.support ↑m) : (I.markedTransform D m).maxOrd ≤ ↑m

One step of [Kol07, Remark 67] ("max-ord I_i ≤ m by (61)"): along a smooth center of any shape with ord_D I ≥ m and max-ord I ≤ m, the marked transform has max-ord ≤ m.

theorem AlgebraicGeometry.maxOrd_markedTransformSeq_le {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] {I : X.IdealSheafData} {E : X.DivisorFamily} {m : ℕ} {S : X.BlowUpSequence} (hI : I.maxOrd ≤ ↑m) (h : S.IsOrderGeSeq f I m E) (i : Fin (S.length + 1)) : (S.markedTransformSeq I m i).maxOrd ≤ ↑m

The invariant of [Kol07, Remark 67] along the sequence: with max-ord I ≤ m, every induced marked ideal has max-ord ≤ m.

theorem AlgebraicGeometry.markedTransformSeq_eq_weakTransformSeq_of_maxOrd_le {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] {I : X.IdealSheafData} {E : X.DivisorFamily} {m : ℕ} {S : X.BlowUpSequence} (hI : I.maxOrd ≤ ↑m) (h : S.IsOrderGeSeq f I m E) (i : Fin (S.length + 1)) : S.markedTransformSeq I m i = S.weakTransformSeq I i

[Kol07, Remark 67] along the sequence: with max-ord I ≤ m, the marked and the unmarked induced ideals coincide at every stage.

theorem AlgebraicGeometry.IsOrderGeSeq.maxOrd_le {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] {I : X.IdealSheafData} {E : X.DivisorFamily} {m : ℕ} {S : X.BlowUpSequence} (hI : I.maxOrd = ↑m) (h : S.IsOrderGeSeq f I m E) (i : Fin (S.length + 1)) : (S.markedTransformSeq I m i).maxOrd ≤ ↑m

"max-ord I_i ≤ m by (61)" [Kol07, Remark 67]: along a sequence of order ≥ m for (X, I, m, E) with max-ord I = m, every induced marked ideal has max-ord ≤ m.

theorem AlgebraicGeometry.IsOrderGeSeq.ordAlongEq {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] {I : X.IdealSheafData} {E : X.DivisorFamily} {m : ℕ} {S : X.BlowUpSequence} (hI : I.maxOrd = ↑m) (h : S.IsOrderGeSeq f I m E) (i : Fin S.length) : (S.markedTransformSeq I m i.castSucc).OrdAlongEq (S.center i).support ↑m

"And so every blow-up has order = m" [Kol07, Remark 67]: along a sequence of order ≥ m for (X, I, m, E) with max-ord I = m, the order of I_i along every center is exactly m.

theorem AlgebraicGeometry.IsOrderGeSeq.markedTransformSeq_eq_weakTransformSeq {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] {I : X.IdealSheafData} {E : X.DivisorFamily} {m : ℕ} {S : X.BlowUpSequence} (hI : I.maxOrd = ↑m) (h : S.IsOrderGeSeq f I m E) (i : Fin (S.length + 1)) : S.markedTransformSeq I m i = S.weakTransformSeq I i

The marked and the unmarked transforms coincide at every stage of a sequence of order ≥ m for (X, I, m, E) with max-ord I = m [Kol07, Remark 67].

theorem AlgebraicGeometry.IsOrderSeq.markedTransformSeq_eq_weakTransformSeq {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] {I : X.IdealSheafData} {E : X.DivisorFamily} {m : ℕ} {S : X.BlowUpSequence} (h : S.IsOrderSeq f I E m) (i : Fin (S.length + 1)) : S.markedTransformSeq I m i = S.weakTransformSeq I i

"The converse also holds" [Kol07, Remark 67]: along a sequence of order m for (X, I, E) the marked transforms with mark m coincide with the unmarked ones.

theorem AlgebraicGeometry.isOrderGeSeq_iff_isOrderSeq {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] {I : X.IdealSheafData} {E : X.DivisorFamily} {m : ℕ} {S : X.BlowUpSequence} (hI : I.maxOrd = ↑m) : S.IsOrderGeSeq f I m E ↔ S.IsOrderSeq f I E m

For max-ord I = m, a smooth blow-up sequence is of order ≥ m for (X, I, m, E) iff it is of order m for (X, I, E) [Kol07, Remark 67].