Tuning of ideals: the converse direction of Theorem 100

Kollár's first tuning theorem [Kol07, Theorem 100] says that for I^s ⊆ J ⊆ W_{ms}(I) a smooth blow-up sequence is of order ≥ m for (X, I, m) iff it is of order ≥ ms for (X, J, ms). This module proves the converse direction (a sequence of order ≥ ms for (X, J, ms) is of order ≥ m for (X, I, m)), which uses only I^s ⊆ J; the boundary E is carried along.

• Powers under the marked transform. With π_*^{-1}(I, m) = (π^* I : F^m) (the colon form of the marked transform of [Kol07, Definition 60]), (π^* I : F^m)^s · F^{ms} = ((π^* I : F^m) · F^m)^s ⊆ (π^* I)^s = π^*(I^s), so π_*^{-1}(I, m)^s ⊆ π_*^{-1}(I^s, ms) for every I, m, s (pow_markedTransform_le). When F^m ∣ π^* I (Kollár's m ≤ ord_D I) the colon is an honest quotient, F^m · (π^* I : F^m) = π^* I, so F^{ms} · π_*^{-1}(I, m)^s = π^*(I^s), and the uniqueness of the quotient by the invertible F^{ms} gives equality (markedTransform_pow). Along a sequence, I^s ⊆ J propagates to I_i^s ⊆ J_i at every stage by induction, the step being the one-blow-up inclusion followed by the monotonicity of the marked transform in its ideal (pow_markedTransformSeq_le, Kollár's I_{r−1}^s ⊆ J_{r−1}); on a sequence of order ≥ m for (X, I, m, E) every F_{i+1}^m ∣ π_i^* I_i, so the equality propagates too (markedTransformSeq_pow, Kollár's I_{r−1}^s = (Π_{r−1})_*^{-1} I^s).
• The order at the center. At a point η of a scheme smooth over a field k of characteristic zero the stalk 𝒪_{X,η} is a regular local ring containing ℚ, so the order is multiplicative on its elements and ord_η (I^s) = s · ord_η I (ord_pow). Hence ord_Z J ≥ ms and I^s ⊆ J give s · ord_η I = ord_η (I^s) ≥ ord_η J ≥ ms at every generic point η of Z (the order is antitone in the ideal, [Kol07, Definition 59 (1)]), and cancelling s ≥ 1 in ℕ∞ gives ord_Z I ≥ m (leOrdAlong_of_pow_le).
• The direction assembled. For a sequence of order ≥ ms for (X, J, ms, E): the smoothness and normal crossing clauses of [Kol07, Definition 66] do not mention the ideal, and at every stage I_i^s ⊆ J_i turns ord_{Z_i} J_i ≥ ms into ord_{Z_i} I_i ≥ m, the stage X_i being smooth over k of the same relative dimension, so the sequence is of order ≥ m for (X, I, m, E) (tuning_mpr). Kollár's induction on the length of the sequence is the induction inside pow_markedTransformSeq_le; the order clauses are then read off stage by stage.

Powers under the marked transform

theorem Hironaka.Sequence.pow_markedTransform_le {X : AlgebraicGeometry.Scheme} (D I : X.IdealSheafData) (m s : ℕ) : I.markedTransform D m ^ s ≤ (I ^ s).markedTransform D (m * s)

π_*^{-1}(I, m)^s ⊆ π_*^{-1}(I^s, ms) (the proof of the converse in [Kol07, Theorem 100]), since (π^* I : F^m)^s · F^{ms} = ((π^* I : F^m) · F^m)^s ⊆ (π^* I)^s = π^*(I^s).

theorem Hironaka.Sequence.markedTransform_pow {X : AlgebraicGeometry.Scheme} (D I : X.IdealSheafData) (m s : ℕ) (h : D.exceptionalDivisor ^ m ∣ I.comap D.blowUpπ) : (I ^ s).markedTransform D (m * s) = I.markedTransform D m ^ s

When F^m ∣ π^* I (Kollár's m ≤ ord_D I, under which [Kol07, Definition 60] defines π_*^{-1}(I, m)), π_*^{-1}(I^s, ms) = π_*^{-1}(I, m)^s: indeed F^{ms} · π_*^{-1}(I, m)^s = (F^m · π_*^{-1}(I, m))^s = π^*(I^s), and the quotient by the invertible F^{ms} is unique.

theorem Hironaka.Sequence.pow_markedTransformSeq_le {X : AlgebraicGeometry.Scheme} (I J : X.IdealSheafData) (m s : ℕ) (S : X.BlowUpSequence) (hIJ : I ^ s ≤ J) (i : Fin (S.length + 1)) : S.markedTransformSeq I m i ^ s ≤ S.markedTransformSeq J (m * s) i

"Since I^s ⊂ J, we know that I_{r−1}^s ⊂ J_{r−1}" (the proof of the converse in [Kol07, Theorem 100]): by induction on the sequence, the step being the one-blow-up inclusion pow_markedTransform_le followed by the monotonicity of the marked transform in its ideal (markedTransform_mono).

theorem Hironaka.Sequence.markedTransformSeq_pow {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 (I ^ s) (m * s) i = S.markedTransformSeq I m i ^ s

I_{r−1}^s = (Π_{r−1})_*^{-1} I^s (the proof of the converse in [Kol07, Theorem 100]): along a smooth blow-up sequence of order ≥ m starting with (X, I, m, E), every F_{i+1}^m ∣ π_i^* I_i (pow_dvd_comap_of_leOrdAlong at each stage), so the one-blow-up equality markedTransform_pow propagates by induction on the sequence.

The order at the center

theorem Hironaka.Sequence.ord_pow {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (I : X.IdealSheafData) (s : ℕ) (hs : 1 ≤ s) (η : ↥X) : (I ^ s).ord η = ↑s * I.ord η

At every point η of a scheme smooth over a field of characteristic zero, ord_η (I^s) = s · ord_η I for s ≥ 1 (the pointwise form of cosupp(I, m) = cosupp(I^c, mc), [Kol07, Definition 59 (3)]). The stalk 𝒪_{X,η} is a regular local ring (isRegularLocalRing_stalk) containing ℚ (f.stalkAlgebraRat η), so the order is multiplicative on its elements (ordElem_mul_of_algebraRat) and ord_pow_of_ordElem_mul applies to the stalk ideal I_η, whose s-th power is the stalk of I^s.

theorem Hironaka.Sequence.leOrdAlong_of_pow_le {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (I J : X.IdealSheafData) (m s : ℕ) (Z : TopologicalSpace.Closeds ↥X) (hs : 1 ≤ s) (hIJ : I ^ s ≤ J) (hJ : J.LeOrdAlong Z ↑(m * s)) : I.LeOrdAlong Z ↑m

"If ord_Z J_{r−1} ≥ ms, then ord_Z I_{r−1} ≥ m" (the proof of the converse in [Kol07, Theorem 100]): at each generic point η of Z, ms ≤ ord_η J ≤ ord_η (I^s) = s · ord_η I (the order is antitone in the ideal, ord_anti, for the middle step), and s ≥ 1 cancels in ℕ∞.

The direction assembled

theorem Hironaka.Sequence.tuning_mpr {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 : ℕ) (hs : 1 ≤ s) (hIJ : I ^ s ≤ J) (h : S.IsOrderGeSeq f J (m * s) E) : S.IsOrderGeSeq f I m E

The converse direction of [Kol07, Theorem 100]: a smooth blow-up sequence of order ≥ ms for (X, J, ms, E) with I^s ⊆ J, s ≥ 1, is of order ≥ m for (X, I, m, E). The smoothness and normal crossing clauses of Definition 66 are inherited, and at every stage i the order clause ord_{Z_i} I_i ≥ m follows from I_i^s ⊆ J_i (pow_markedTransformSeq_le) and ord_{Z_i} J_i ≥ ms (leOrdAlong_of_pow_le), the stage X_i being smooth of relative dimension n over k (IsSmooth.smoothOfRelativeDimension_stageMap).