The tuning ideal under one blowing-up: orders along the centre and the transform

The order bookkeeping of the tuning theorem [Kol07, Theorem 100] on analytic manifolds, for one blowing-up π : M' → M with centre the closed submanifold Y:

• at the stalk, ord_x (J^s) = s · ord_x J for s ≥ 1 (IdealSheaf.ord_pow): the stalk 𝒪_{M,x} is a regular local ring containing ℚ, so the order is multiplicative on its elements (ordElem_mul_of_algebraRat, ord_pow_of_ordElem_mul); the finite-dimensional model space is the setting;
• the converse direction of the theorem ("if ord_Z J_{r−1} ≥ ms then ord_Z I_{r−1} ≥ m"): for s ≥ 1 and I^s ⊆ J, ord_Y J ≥ ms at a point of Y gives ord_Y I ≥ m there (le_ordAlong_of_pow_le). The order along Y is locally constant on Y and bounded by the pointwise order, so ms ≤ ord_y J ≤ ord_y (I^s) = s · ord_y I at the points y of Y near a, whence m ≤ ord_y I there, and the pointwise bound on Y near a gives the stalk containment I_a ⊆ I_{Y,a}^m (stalkIdeal_le_pow_of_eventually_le_ord);
• the direct direction (from ord_Z I_{r−1} ≥ m Kollár derives ord_Z D^j(I_{r−1}) ≥ m − j and hence ord_Z ∏_j D^j(I_{r−1}, m)^{c_j} ≥ ∑ (m − j) c_j ≥ ms): ord_Y I ≥ m at a point of Y gives ord_Y W_s(I) ≥ s there (le_ordAlong_tuning): each generating product of stalkIdeal_tuning has order ≥ wt(e) ≥ s along Y (le_ordAlongIdeal_iteratedDeriv for the factors, the product and power rules of Hironaka.Manifold.BlowUp.Transform.MarkedAlgebra), and the sum keeps it;
• the displayed chain of the proof for one blowing-up, read as the inclusion π_*^{-1}(W_s(I), s) ⊆ W_s(π_*^{-1}(I, m)) (birationalTransform_tuning_le): with W_s(I) = ∑_e P_e, P_e = ∏_j (D^j I)^{e_j} over the finite exponent set of tuning_eq_finset_sum, each P_e has m − j ≤ ord_Y D^j I on its factors, so π_*^{-1}(P_e, s) ⊆ π_*^{-1}(P_e, wt e) = ∏_j π_*^{-1}(D^j I, m − j)^{e_j} ⊆ ∏_j D^j(π_*^{-1}(I, m))^{e_j} ⊆ W_s(π_*^{-1}(I, m)) (the mark comparison, the product and power rules, the derivative rule markedTransform_iteratedDeriv_le of [Kol07, Theorem 76], and the definition of W_s), and the sum rule assembles the summands.

The counterparts for schemes are in Hironaka.Resolution.Algebraic.Kol07.Tuning and Hironaka.Resolution.Algebraic.Tuning.Transform.

theorem Manifold.IdealSheaf.ord_pow {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (J : IdealSheaf (structureSheaf 𝕜 E M)) {s : ℕ} (hs : 1 ≤ s) (x : M) : (J ^ s).ord x = ↑s * J.ord x

At every point x of a manifold modelled on a finite-dimensional space, ord_x (J^s) = s · ord_x J for s ≥ 1 — the stalk 𝒪_{M,x} is a regular local ring containing ℚ, so the order is multiplicative on its elements (ordElem_mul_of_algebraRat).

theorem Manifold.le_ordAlong_of_pow_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) {I J : IdealSheaf (structureSheaf 𝕜 E M)} {m s : ℕ} (hs : 1 ≤ s) (hIJ : I ^ s ≤ J) {a : M} (ha : a ∈ Y) (hJ : ↑(m * s) ≤ hY.idealSheaf.ordAlongIdeal J a) : ↑m ≤ hY.idealSheaf.ordAlongIdeal I a

For s ≥ 1 and I^s ⊆ J, ord_Y J ≥ ms at a point of Y gives ord_Y I ≥ m there.

theorem Manifold.le_ordAlong_tuning {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {Y : Set M} {c : ℕ} [FiniteDimensional 𝕜 E] (hY : IsClosedSubmanifold ψ Y c) (I : IdealSheaf (structureSheaf 𝕜 E M)) (m s : ℕ) {a : M} (ha : a ∈ Y) (hm : ↑m ≤ hY.idealSheaf.ordAlongIdeal I a) : ↑s ≤ hY.idealSheaf.ordAlongIdeal (I.tuning m s) a

ord_Y I ≥ m at a point of Y gives ord_Y W_s(I) ≥ s there — each generating product ∏_j (D^j I)^{e_j} with ∑ (m − j) e_j ≥ s has order ≥ s along Y (le_ordAlongIdeal_iteratedDeriv for the factors), and the sum keeps it.

The transform of the tuning ideal under one blowing-up

theorem Manifold.birationalTransform_tuning_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (I : IdealSheaf (structureSheaf 𝕜 E M)) (m s : ℕ) (hm : ∀ x ∈ Y, ↑m ≤ hY.idealSheaf.ordAlongIdeal I x) : (MarkedIdealSheaf.birationalTransform hY h { I := I.tuning m s, m := s }).I ≤ (MarkedIdealSheaf.birationalTransform hY h { I := I, m := m }).I.tuning m s

For a blowing-up π with centre Y and ord_Y I ≥ m at every point of Y, π_*^{-1}(W_s(I), s) ⊆ W_s(π_*^{-1}(I, m)): each generating product P_e = ∏_j (D^j I)^{e_j} with ∑ (m − j) e_j ≥ s has m − j ≤ ord_Y D^j I (le_ordAlongIdeal_iteratedDeriv), so π_*^{-1}(P_e, s) ⊆ π_*^{-1}(P_e, ∑ (m − j) e_j) = ∏_j π_*^{-1}(D^j I, m − j)^{e_j} ⊆ ∏_j D^j(π_*^{-1}(I, m))^{e_j} ⊆ W_s(π_*^{-1}(I, m)) (the mark comparison, the product and power rules, markedTransform_iteratedDeriv_le of [Kol07, Theorem 76], the definition of W_s), and the sum rule assembles the summands of tuning_eq_finset_sum.