The reduction to a D-balanced ideal

The proof of [Kol07, Lemma 102] opens by replacing I with the tuned ideal W_{m!}(I), which is D-balanced, order reduction for (X, I, E) being equivalent to order reduction for (X, W_{m!}(I), E) by [Kol07, Corollary 101]. This library's tuning parameter is s(m) = tuningParam m (Hironaka/Algebra/Local/TuningParam.lean), and Corollary 101 at that parameter is tuning_iff_tuningParam (Hironaka/Resolution/Algebraic/Tuning/Parameter.lean), a statement about the MARKED sequences of [Kol07, Definition 66]: "of order ≥ m for (X, I, m, E)" iff "of order ≥ s(m) for (X, W_{s(m)}(I), s(m), E)". Lemma 102's functor is of order m (unmarked), and max-ord I = m: [Kol07, Remark 67] (isOrderGeSeq_iff_isOrderSeq, Hironaka/Scheme/BlowUpSequence/Remark67.lean) identifies the marked and the unmarked sequences on the left, and again on the right since max-ord W_{s(m)}(I) = s(m) (maxOrd_W, Hironaka/Resolution/Algebraic/Tuning/Corollary101.lean). That is isOrderSeq_iff_tuned.

"Order reduction … is equivalent": along such a sequence the cosupports agree stage by stage, cosupp(I_i, m) = cosupp(W_i, s(m)) (le_ord_weakTransformSeq_iff_tuned), by the two inclusions of the proof of [Kol07, Theorem 100]: W_i ⊆ W_{s}(I_i) (markedTransformSeq_W_le) together with ord_x I_i ≥ m ⟹ ord_x W_s(I_i) ≥ s (le_ord_W_of_le_ord, both in Hironaka/Resolution/Algebraic/Tuning/Sequence.lean) give ⟹; I_i^{s'} ⊆ W_i for s = m s' (pow_markedTransformSeq_le, from I^{s'} ⊆ W_{m s'}(I)) with ord_x (I_i^{s'}) = s' · ord_x I_i (ord_pow, both in Hironaka/Resolution/Algebraic/Kol07/Tuning.lean) gives ⟸. Remark 67 makes the marked transforms the weak ones on both sides. This transfers clause (1) of Lemma 102 from the tuned ideal to I (Assembly.lean, AssemblyTuned.lean).

Used also by OrderSeqAssignment.ofTunedClass, Hironaka/Resolution/Algebraic/OrderReduction/Tuned.lean, Hironaka/Resolution/Algebraic/OrderReduction/Step22Assembly.lean and Hironaka/Resolution/Algebraic/OrderReduction/Step22Cosupp.lean.

theorem Hironaka.BD.isOrderSeq_iff_tuned {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [CharZero k] (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (S : X.BlowUpSequence) (I : X.IdealSheafData) (E : X.DivisorFamily) (m : ℕ) (hI : I.maxOrd = ↑m) (hm : 1 ≤ m) : S.IsOrderSeq f I E m ↔ S.IsOrderSeq f (AlgebraicGeometry.Scheme.IdealSheafData.W f I m (IsLocalRing.tuningParam m)) E (IsLocalRing.tuningParam m)

For max-ord I = m ≥ 1, a smooth blow-up sequence is of order m starting with (X, I, E) iff it is of order s(m) starting with (X, W_{s(m)}(I), E) (the first paragraph of the proof of [Kol07, Lemma 102]; [Kol07, Corollary 101] at s(m), i.e. tuning_iff_tuningParam, with [Kol07, Remark 67] on both sides).

theorem Hironaka.BD.le_ord_weakTransformSeq_iff_tuned {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [CharZero k] (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (S : X.BlowUpSequence) (I : X.IdealSheafData) (E : X.DivisorFamily) (m : ℕ) (hI : I.maxOrd = ↑m) (hm : 1 ≤ m) (h : S.IsOrderSeq f I E m) (i : Fin (S.length + 1)) (x : ↥(S.stage i)) : ↑m ≤ (S.weakTransformSeq I i).ord x ↔ ↑(IsLocalRing.tuningParam m) ≤ (S.weakTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.W f I m (IsLocalRing.tuningParam m)) i).ord x

Along a smooth blow-up sequence of order m starting with (X, I, E), max-ord I = m ≥ 1, at every stage and point ord_x I_i ≥ m ⟺ ord_x W_i ≥ s(m): the inclusions I_i^{s'} ⊆ W_i ⊆ W_s(I_i) of the proof of [Kol07, Theorem 100].