Theorem 100, the direction ⟹: along a blow-up sequence

The direction of [Kol07, Theorem 100] proved first in Kollár's text: for J ⊂ W_{ms}(I), a smooth blow-up sequence of order ≥ m starting with (X, I, m) is a smooth blow-up sequence of order ≥ ms starting with (X, J, ms).

• Along the sequence ("we prove by induction on r"): at every stage i, (Π_i)_*^{-1}(W_s(I), s) ⊆ W_s(I_i) — induction on the succession, the step being the one-blow-up inclusion markedTransform_W_le (Hironaka.Resolution.Algebraic.Tuning.Transform) followed by the monotonicity of the marked recursion in its starting ideal (markedTransformSeq_mono), exactly as [Kol07, Theorem 76] is lifted along the sequence (markedTransformSeq_W_le); for J ⊆ W_s(I), J_i ⊆ W_s(I_i) by monotonicity (markedTransformSeq_le_W, Kollár's J_{r−1} ⊆ W_{ms}(I_{r−1})).
• The order estimate (Kollár: "ord_Z D^j(I_{r−1}) ≥ m − j" when ord_Z I_{r−1} ≥ m, so the product ∏_j D^j(I_{r−1}, m)^{c_j} has order ≥ ∑ (m − j) c_j ≥ ms along Z): at a point η with ord_η I ≥ m, every generating product ∏_j (D^j I)^{e_j} of W_s(I) has order ≥ ∑_j (m − j) e_j = wt(e) ≥ s — [Kol07, Lemma 74 (3)] at the stalk (le_ord_iff_le_ord_derivativeIter), the order of a power is at least the multiple (le_ord_pow), the order of a product at least the sum (le_ord_mul, iterated: sum_ord_le_ord_prod) — and an ideal all of whose generators have order ≥ s lies in 𝔪^s (le_ord_iff), so ord_η W_s(I) ≥ s (le_ord_W_of_le_ord); hence ord_Z I ≥ m gives ord_Z W_s(I) ≥ s at every generic point of the closed set Z (leOrdAlong_W). The computation is at the stalk of η with no coordinates: the generic points of a centre are not closed, and the coordinate bridge stalkIdeal_W needs spanning coordinates, which exist at closed points only.
• The direction assembled: the smoothness and normal-crossing clauses of [Kol07, Definition 66] do not mention the ideal; at every stage J_i ⊆ W_{ms}(I_i), ord_{Z_i} I_i ≥ m gives ord_{Z_i} W_{ms}(I_i) ≥ ms and so ord_{Z_i} J_i ≥ ms (the order is antitone in the ideal, [Kol07, Definition 59, (1)]) (tuning_mp).

theorem Hironaka.Local.sum_ord_le_ord_prod {R : Type u_1} [CommRing R] [IsLocalRing R] {ι : Type u_2} (s : Finset ι) (g : ι → Ideal R) : ∑ i ∈ s, IsLocalRing.ord (g i) ≤ IsLocalRing.ord (∏ i ∈ s, g i)

The order of a finite product of ideals is at least the sum of the orders (le_ord_mul iterated; the empty product is the unit ideal, of order 0).

The transform of the tuning ideal along the sequence

theorem Hironaka.Sequence.markedTransformSeq_W_le {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (S : X.BlowUpSequence) (I : X.IdealSheafData) (E : X.DivisorFamily) (m s : ℕ) (h : S.IsOrderGeSeq f I m E) (i : Fin (S.length + 1)) : S.markedTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.W f I m s) s i ≤ AlgebraicGeometry.Scheme.IdealSheafData.W (CategoryTheory.CategoryStruct.comp (S.stageMap i) f) (S.markedTransformSeq I m i) m s

Along a smooth blow-up sequence of order ≥ m starting with (X, I, m, E), at every stage i, (Π_i)_*^{-1}(W_s(I), s) ⊆ W_s(I_i) (the induction of the proof of [Kol07, Theorem 100]). Induction on the succession: the first stage is the one-blow-up inclusion markedTransform_W_le (the centre is smooth with ord_Z I ≥ m, by Definition 66), the marked recursion is monotone in its starting ideal, and the tail is a sequence of order ≥ m for the transformed data.

theorem Hironaka.Sequence.markedTransformSeq_le_W {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (S : X.BlowUpSequence) (I : X.IdealSheafData) (E : X.DivisorFamily) (m s : ℕ) (J : X.IdealSheafData) (hJW : J ≤ AlgebraicGeometry.Scheme.IdealSheafData.W f I m s) (h : S.IsOrderGeSeq f I m E) (i : Fin (S.length + 1)) : S.markedTransformSeq J s i ≤ AlgebraicGeometry.Scheme.IdealSheafData.W (CategoryTheory.CategoryStruct.comp (S.stageMap i) f) (S.markedTransformSeq I m i) m s

The inductive statement as Kollár writes it in the proof of [Kol07, Theorem 100] ("since J ⊂ W_{ms}(I), we know that J_{r−1} = (Π_{r−1})_*^{-1}(J, ms) ⊂ … = W_{ms}(I_{r−1})"): for J ⊆ W_s(I), J_i ⊆ W_s(I_i) at every stage — markedTransformSeq_W_le with the monotonicity of the marked recursion (markedTransformSeq_mono).

The order of the tuning ideal

theorem Hironaka.Sequence.le_ord_W_of_le_ord {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (I : X.IdealSheafData) (m s : ℕ) (η : ↥X) (hη : ↑m ≤ I.ord η) : ↑s ≤ (AlgebraicGeometry.Scheme.IdealSheafData.W f I m s).ord η

The order estimate of the proof of [Kol07, Theorem 100] at a point: if ord_η I ≥ m then ord_η W_s(I) ≥ s — every generating product ∏_j (D^j I)^{e_j} with wt(e) ≥ s has order ≥ ∑_j (m − j) e_j = wt(e), since ord_η D^j I ≥ m − j ([Kol07, Lemma 74 (3)] at the stalk, j < m; trivial for j = m), ord (K^c) ≥ c · ord K and ord (K₁ K₂) ≥ ord K₁ + ord K₂; and a supremum of ideals of order ≥ s has order ≥ s (it lies in 𝔪^s). No coordinates on the stalk are used.

theorem Hironaka.Sequence.leOrdAlong_W {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (I : X.IdealSheafData) (m s : ℕ) (Z : TopologicalSpace.Closeds ↥X) (hm : I.LeOrdAlong Z ↑m) : (AlgebraicGeometry.Scheme.IdealSheafData.W f I m s).LeOrdAlong Z ↑s

The order estimate of the proof of [Kol07, Theorem 100] along a closed set ("if ord_Z I_{r−1} ≥ m, then … ord_Z ∏_j D^j(I_{r−1}, m)^{c_j} ≥ ∑ (m − j) c_j ≥ ms"): for a closed Z, ord_Z I ≥ m implies ord_Z W_s(I) ≥ s, at every generic point of Z.

The direction assembled

theorem Hironaka.Sequence.tuning_mp {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (S : X.BlowUpSequence) (I J : X.IdealSheafData) (E : X.DivisorFamily) (m s : ℕ) (hJW : J ≤ AlgebraicGeometry.Scheme.IdealSheafData.W f I m (m * s)) (h : S.IsOrderGeSeq f I m E) : S.IsOrderGeSeq f J (m * s) E

[Kol07, Theorem 100], the direction ⟹: for J ⊆ W_{ms}(I), a smooth blow-up sequence of order ≥ m starting with (X, I, m, E) is a smooth blow-up sequence of order ≥ ms starting with (X, J, ms, E). The smoothness and normal-crossing clauses do not mention the ideal; at every stage J_i ⊆ W_{ms}(I_i), ord_{Z_i} I_i ≥ m gives ord_{Z_i} W_{ms}(I_i) ≥ ms and so ord_{Z_i} J_i ≥ ms (the order is antitone in the ideal).