Step 1 of order reduction: properties of the tuned triple

Step 1 of the proof of [Kol07, Theorem 103] replaces the ideal I of a triple (X, I, E) with max-ord I = m by the maximal coefficient ideal W(I) = W_s(I) of [Kol07, Corollary 101], which is D-balanced and MC-invariant and for which order reduction is equivalent to order reduction for I. This module states, for the tuned triple T.tuned m hm = (X, W_{s(m)}(I), E), what the sheaf-level theory of tuning (Hironaka/Resolution/Algebraic/Tuning/) gives:

• the scheme and the divisor are unchanged and the ideal is W_{s(m)}(I), definitionally (tuned_X, tuned_I, tuned_E, hasDimLE_tuned);
• for max-ord I = m ≥ 1, the tuned ideal has maximal order s(m), is D-balanced and MC-invariant with respect to s(m), and a smooth blow-up sequence is of order m for T iff it is of order s(m) for the tuned triple (maxOrd_tuned, isDBalanced_tuned, isMCInvariant_tuned, isOrderSeq_tuned_iff; [Kol07, Theorem 100 and Corollary 101]);
• clause (1) of Theorem 103 transfers back through the tuning: along a smooth blow-up sequence of order m for (X, I, E), the final transform of W_{s(m)}(I) has maximal order < s(m) iff that of I has maximal order < m (maxOrd_weakTransformSeq_lt_iff_tuned). Pointwise, ord_x I_r ≥ m iff ord_x W_r ≥ s(m) at the last stage; a supremum in ℕ∞ of orders is < s, for a natural number s ≥ 1, iff every order is < s (maxOrd_lt_iff_forall_ord_lt), so the two suprema are below their marks together;
• tuning commutes with the two functoriality inputs of clause (2), the pull-back of triples along a smooth morphism and the change of fields ([Kol07, 34.1–34.2]), because the maximal coefficient ideal commutes with smooth pull-back and with base change (isPullbackOf_tuned, isBaseChangeOf_tuned);
• clause (1) of BOData read pointwise and as cosupp(I_r, m) = ∅ (BOData.ord_weakTransformSeq_lt, BOData.cosupp_eq_empty), and the domain unfolded (boClass_iff);
• the order condition of [Kol07, Definition 66] for (X, I, E) at order m and for (X, J, E) at order m' share the smoothness and normal-crossings clauses, which are computed from the centres alone, so they are equivalent as soon as the order clauses ord_{Z_i} I_i = m and ord_{Z_i} J_i = m' are, stage by stage (isOrderSeq_iff_of_ordAlongEq_iff; the remark on E in the proof of Corollary 101).

theorem Hironaka.BOData.ord_weakTransformSeq_lt {k : Type u} [Field k] [CharZero k] {n m : ℕ} (B : BOData n m) (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BOClass n m T) (x : ↥(((B.functor k).seq T hT).stage (Fin.last ((B.functor k).seq T hT).length))) : (((B.functor k).seq T hT).weakTransformSeq T.I (Fin.last ((B.functor k).seq T hT).length)).ord x < ↑m

Clause (1) of [Kol07, Theorem 103] read pointwise: the final birational transform has order < m at every point, an order being at most the maximal order.

theorem Hironaka.BOData.cosupp_eq_empty {k : Type u} [Field k] [CharZero k] {n m : ℕ} (B : BOData n m) (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BOClass n m T) : {x : ↥(((B.functor k).seq T hT).stage (Fin.last ((B.functor k).seq T hT).length)) | ↑m ≤ (((B.functor k).seq T hT).weakTransformSeq T.I (Fin.last ((B.functor k).seq T hT).length)).ord x} = ∅

Clause (1) of [Kol07, Theorem 103] as the emptiness of the cosupport: no point of the final stage has order ≥ m, cosupp(I_r, m) = ∅.

theorem Hironaka.BO.boClass_iff {k : Type u} [Field k] (n m : ℕ) (T : AlgebraicGeometry.Triple k) : AlgebraicGeometry.Triple.BOClass n m T ↔ 1 ≤ m ∧ T.HasDimLE n ∧ T.I.maxOrd ≤ ↑m

The domain of BO_{n,m} unfolded: 1 ≤ m, dim X ≤ n and max-ord I ≤ m.

theorem Hironaka.BO.tuned_X {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (hm : 1 ≤ m) : (T.tuned m hm).X.left = T.X.left

The tuned triple has the same underlying scheme.

theorem Hironaka.BO.tuned_I {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (hm : 1 ≤ m) : (T.tuned m hm).I = AlgebraicGeometry.Scheme.IdealSheafData.W (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m (IsLocalRing.tuningParam m)

The ideal of the tuned triple is the maximal coefficient ideal W_{s(m)}(I).

theorem Hironaka.BO.tuned_E {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (hm : 1 ≤ m) : (T.tuned m hm).E = T.E

The tuned triple has the same boundary divisor.

theorem Hironaka.BO.hasDimLE_tuned {k : Type u} [Field k] {T : AlgebraicGeometry.Triple k} {n : ℕ} (h : T.HasDimLE n) (m : ℕ) (hm : 1 ≤ m) : (T.tuned m hm).HasDimLE n

The tuned triple of a triple with dim X ≤ n has dim X ≤ n, the scheme being unchanged.

theorem Hironaka.BO.maxOrd_tuned {k : Type u} [Field k] [CharZero k] {T : AlgebraicGeometry.Triple k} {m : ℕ} (hI : T.I.maxOrd = ↑m) (hm : 1 ≤ m) : (T.tuned m hm).I.maxOrd = ↑(IsLocalRing.tuningParam m)

For max-ord I = m ≥ 1 the tuned ideal has maximal order s(m) ([Kol07, Theorem 54.2 (i)] for the exponent m!; maxOrd_W for an arbitrary exponent).

theorem Hironaka.BO.isDBalanced_tuned {k : Type u} [Field k] [CharZero k] {T : AlgebraicGeometry.Triple k} {m : ℕ} (hI : T.I.maxOrd = ↑m) (hm : 1 ≤ m) : AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced (T.X.left ↘ AlgebraicGeometry.Spec ↧k) (T.tuned m hm).I (IsLocalRing.tuningParam m)

For max-ord I = m ≥ 1 the tuned ideal is D-balanced with respect to s(m) ([Kol07, Corollary 101]).

theorem Hironaka.BO.isMCInvariant_tuned {k : Type u} [Field k] [CharZero k] {T : AlgebraicGeometry.Triple k} {m : ℕ} (hI : T.I.maxOrd = ↑m) (hm : 1 ≤ m) : AlgebraicGeometry.Scheme.IdealSheafData.IsMCInvariant (T.X.left ↘ AlgebraicGeometry.Spec ↧k) (T.tuned m hm).I (IsLocalRing.tuningParam m)

For max-ord I = m ≥ 1 the tuned ideal is MC-invariant with respect to s(m) ([Kol07, Corollary 101]).

theorem Hironaka.BO.isOrderSeq_tuned_iff {k : Type u} [Field k] [CharZero k] {T : AlgebraicGeometry.Triple k} (S : T.X.left.BlowUpSequence) {m : ℕ} (hI : T.I.maxOrd = ↑m) (hm : 1 ≤ m) : S.IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.E m ↔ S.IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) (T.tuned m hm).I (T.tuned m hm).E (IsLocalRing.tuningParam m)

For max-ord I = m ≥ 1, a smooth blow-up sequence is of order m for T iff it is of order s(m) for the tuned triple ([Kol07, Corollary 101]).

theorem Hironaka.BO.maxOrd_lt_iff_forall_ord_lt {X : AlgebraicGeometry.Scheme} (J : X.IdealSheafData) {s : ℕ} (hs : 1 ≤ s) : J.maxOrd < ↑s ↔ ∀ (x : ↥X), J.ord x < ↑s

For a natural number s ≥ 1, the maximal order of an ideal sheaf is < s iff its order at every point is < s: both say that every order is ≤ s − 1, and ℕ∞ has no limit point below a natural number. Not in the sources.

theorem Hironaka.BO.maxOrd_weakTransformSeq_lt_iff_tuned {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (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) : (S.weakTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.W f I m (IsLocalRing.tuningParam m)) (Fin.last S.length)).maxOrd < ↑(IsLocalRing.tuningParam m) ↔ (S.weakTransformSeq I (Fin.last S.length)).maxOrd < ↑m

Along a smooth blow-up sequence of order m for (X, I, E) with max-ord I = m ≥ 1, the final birational transform of the tuned ideal has maximal order < s(m) iff that of I has maximal order < m. Not in the sources; it carries clause (1) of [Kol07, Theorem 103] from the tuned triple back to (X, I, E). The pointwise statement is Hironaka.BD.le_ord_weakTransformSeq_iff_tuned at the last stage; the two suprema are compared through maxOrd_lt_iff_forall_ord_lt.

theorem Hironaka.BO.isPullbackOf_tuned {k : Type u} [Field k] {T T' : AlgebraicGeometry.Triple k} {g : T'.X.left ⟶ T.X.left} [AlgebraicGeometry.Smooth g] (h : T'.IsPullbackOf T g) (m : ℕ) (hm : 1 ≤ m) : (T'.tuned m hm).IsPullbackOf (T.tuned m hm) g

The tuned triple of a pull-back along a smooth morphism is the pull-back of the tuned triple: the maximal coefficient ideal commutes with smooth pull-back (W_comap_of_smooth), as the derivatives do. Used for [Kol07, 34.1].

theorem Hironaka.BO.isBaseChangeOf_tuned {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] {T : AlgebraicGeometry.Triple k} {T' : AlgebraicGeometry.Triple L} {σ : k →+* L} {p : T'.X.left ⟶ T.X.left} (h : T'.IsBaseChangeOf T σ p) (m : ℕ) (hm : 1 ≤ m) : (T'.tuned m hm).IsBaseChangeOf (T.tuned m hm) σ p

The tuned triple of a change of fields is the change of fields of the tuned triple: the maximal coefficient ideal commutes with base change along a field extension (W_comap_of_isPullback_specMap). Used for [Kol07, 34.2].

theorem Hironaka.BO.isOrderSeq_iff_of_ordAlongEq_iff {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (f : X ⟶ AlgebraicGeometry.Spec ↧k) (I J : X.IdealSheafData) (E : X.DivisorFamily) (m m' : ℕ) (h : ∀ (i : Fin S.length), (S.weakTransformSeq I i.castSucc).OrdAlongEq (S.center i).support ↑m ↔ (S.weakTransformSeq J i.castSucc).OrdAlongEq (S.center i).support ↑m') : S.IsOrderSeq f I E m ↔ S.IsOrderSeq f J E m'

The order condition of [Kol07, Definition 66] across a change of ideal: the smoothness and normal-crossings clauses depend only on the centres, so the conditions for (I, m) and (J, m') are equivalent once the order clauses are, stage by stage. This is the remark on the role of E in the proof of [Kol07, Corollary 101]: adding E "poses the same restriction" on both.