The cosupport of the tuned ideal

In Step 1 of the proof of [Kol07, Theorem 103], after tuning, W_s(I) is used as an unmarked ideal of maximal order s. The pointwise content, at every point x of a smooth variety and for m, s ≥ 1:

• ord_x I ≥ m ⟹ ord_x W_s(I) ≥ s (the order estimate le_ord_W_of_le_ord of Hironaka.Resolution.Algebraic.Tuning.Sequence), and
• ord_x I < m ⟹ W_s(I)_x = 𝒪_x: MC(I) = D^{m−1}(I) has order 0 at x ([Kol07, Lemma 74 (3)]; ord_MC_eq_zero), so MC(I)_x = 𝒪_x, and MC(I)^s ⊆ W_s(I) (MC_pow_le_W) (ord_W_eq_zero_of_ord_lt).

Hence s ≤ ord_x W_s(I) ⟺ m ≤ ord_x I (le_ord_W_iff): cosupp(W_s(I), s) = cosupp(I, m) (cosupp_W), and W_s(I) has order 0 or ≥ s everywhere, so its support, the unmarked cosupport, is the same set (support_W). No coordinates are used (the stalk bridge stalkIdeal_W needs spanning coordinates, which exist at closed points only); the statements hold for every I. At the parameters of Corollary 101 (s = r·lcm(2, …, m), m = max-ord I) support_W is also IsDBalanced.cosupp_eq_support of Hironaka.Resolution.Algebraic.Balanced.Order applied to isDBalanced_W.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ord_W_eq_zero_of_ord_lt {k : Type u} [Field k] [CharZero k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) (m s : ℕ) (hm : 1 ≤ m) {x : ↥X} (hx : I.ord x < ↑m) : (W f I m s).ord x = 0

Where I has order < m, the tuned ideal W_s(I) is the unit ideal: MC(I)_x = 𝒪_x by [Kol07, Lemma 74 (3)] and MC(I)^s ⊆ W_s(I) (compare [Kol07, Definition 83]).

theorem AlgebraicGeometry.Scheme.IdealSheafData.le_ord_W_iff {k : Type u} [Field k] [CharZero k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) (m s : ℕ) (hm : 1 ≤ m) (hs : 1 ≤ s) (x : ↥X) : ↑s ≤ (W f I m s).ord x ↔ ↑m ≤ I.ord x

For m, s ≥ 1, ord_x W_s(I) ≥ s iff ord_x I ≥ m.

theorem AlgebraicGeometry.Scheme.IdealSheafData.cosupp_W {k : Type u} [Field k] [CharZero k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) (m s : ℕ) (hm : 1 ≤ m) (hs : 1 ≤ s) : {x : ↥X | ↑s ≤ (W f I m s).ord x} = {x : ↥X | ↑m ≤ I.ord x}

cosupp(W_s(I), s) = cosupp(I, m) for m, s ≥ 1 (Step 1 of the proof of [Kol07, Theorem 103]).

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_W {k : Type u} [Field k] [CharZero k] {X : Scheme} (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) (m s : ℕ) (hm : 1 ≤ m) (hs : 1 ≤ s) : ↑(W f I m s).support = {x : ↥X | ↑m ≤ I.ord x}

The support of W_s(I) is cosupp(I, m): W_s(I) has order 0 or ≥ s at every point (the remark "cosupp(I, m) = cosupp I" of [Kol07, Definition 83] for the D-balanced W_s(I)). At s = r·lcm(2, …, m), m = max-ord I, this is also IsDBalanced.cosupp_eq_support for isDBalanced_W.