Tuning of ideals, I: Kollár's Theorem 100

Kollár's Theorem 100 [Kol07, Theorem 100] (Tuning of ideals, I): for a smooth variety X, an ideal sheaf I with m = max-ord I, an integer s ≥ 1 and an ideal sheaf J with I^s ⊂ J ⊂ W_{ms}(I), a smooth blow-up sequence is of order ≥ m starting with (X, I, m) iff it is of order ≥ ms starting with (X, J, ms). Here the theorem is stated with a divisor family E carried along, as Corollary 101 needs it.

• tuning_iff pairs the two directions: ⟹ is tuning_mp of Hironaka.Resolution.Algebraic.Tuning.Sequence, which uses only J ⊂ W_{ms}(I); ⟸ is tuning_mpr of Hironaka.Resolution.Algebraic.Kol07.Tuning, which uses only s ≥ 1 and I^s ⊂ J.
• The two bounds of the hypothesis: J = I^s (tuning_iff_pow; the inclusions are I^s ⊆ I^s and I^s ⊆ W_{ms}(I), pow_le_W) and J = W_{ms}(I) (tuning_iff_W; I^s ⊆ W_{ms}(I) and W_{ms}(I) ⊆ W_{ms}(I)), the latter being the form in which the proof of [Kol07, Corollary 101] invokes Theorem 100.
• W_2(I) = I + D(I)^2 (W_two_eq), Kollár's W(I) [Kol07, (54.1)], which is W_{m!}(I) [Kol07, Aside 99.10], at m = 2: an exponent vector e : Fin 3 → ℕ has weight 2e₀ + e₁ ≥ 2 iff e₀ ≥ 1 (then I^{e₀} D(I)^{e₁} D²(I)^{e₂} ⊆ I) or e₀ = 0 and e₁ ≥ 2 (then it lies in D(I)^2); conversely I and D(I)^2 are the generating products of (1, 0, 0) and (0, 2, 0). The worked examples of Hironaka.Balanced compute this ideal for Kollár's Examples 11 and 106.

W_2(I) = I + D(I)²

theorem Hironaka.Sequence.W_two_eq {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (I : X.IdealSheafData) : AlgebraicGeometry.Scheme.IdealSheafData.W f I 2 2 = I ⊔ AlgebraicGeometry.Scheme.IdealSheafData.derivative f I ^ 2

W_2(I) = I + D(I)^2, Kollár's W(I) [Kol07, (54.1)] — which is W_{m!}(I) [Kol07, Aside 99.10] — at m = 2: an exponent vector (e₀, e₁, e₂) has weight 2e₀ + e₁ ≥ 2 iff e₀ ≥ 1 or e₁ ≥ 2.

Theorem 100

theorem Hironaka.Sequence.tuning_iff {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) [CharZero k] (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (S : X.BlowUpSequence) (I J : X.IdealSheafData) (E : X.DivisorFamily) (m s : ℕ) (hI : I.maxOrd = ↑m) (hs : 1 ≤ s) (hIJ : I ^ s ≤ J) (hJW : J ≤ AlgebraicGeometry.Scheme.IdealSheafData.W f I m (m * s)) : S.IsOrderGeSeq f I m E ↔ S.IsOrderGeSeq f J (m * s) E

Kollár's Theorem 100 [Kol07, Theorem 100]: for m = max-ord I, s ≥ 1 and I^s ⊂ J ⊂ W_{ms}(I), a smooth blow-up sequence is of order ≥ m starting with (X, I, m, E) iff it is of order ≥ ms starting with (X, J, ms, E); the two directions tuning_mp and tuning_mpr paired. The hypothesis m = max-ord I is part of Kollár's statement and is kept so that the theorem reads as printed and its uses in Corollary 101 supply it; the proof does not need it, because both directions (tuning_mp, tuning_mpr) are order estimates valid for every m, comparing the marked transforms of I^s ⊆ J ⊆ W_{ms}(I) along the sequence.

The two bounds

theorem Hironaka.Sequence.tuning_iff_pow {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 s : ℕ) (hI : I.maxOrd = ↑m) (hs : 1 ≤ s) : S.IsOrderGeSeq f I m E ↔ S.IsOrderGeSeq f (I ^ s) (m * s) E

Theorem 100 at the lower bound J = I^s: (X, I, m, E) and (X, I^s, ms, E) have the same smooth blow-up sequences of order ≥ m, respectively ≥ ms.

theorem Hironaka.Sequence.tuning_iff_W {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 s : ℕ) (hI : I.maxOrd = ↑m) (hs : 1 ≤ s) : S.IsOrderGeSeq f I m E ↔ S.IsOrderGeSeq f (AlgebraicGeometry.Scheme.IdealSheafData.W f I m (m * s)) (m * s) E

Theorem 100 at the upper bound J = W_{ms}(I), the form invoked in the proof of [Kol07, Corollary 101]: (X, I, m, E) and (X, W_{ms}(I), ms, E) have the same smooth blow-up sequences of order ≥ m, respectively ≥ ms.