Theorem 100, the direction ⟹: the transform of the tuning ideal under one blow-up

The proof of [Kol07, Theorem 100] shows, by induction along the sequence, that the marked transforms J_i of (J, ms) stay inside the tuning ideals W_{ms}(I_i) of the marked transforms of (I, m). This module is the one-blow-up step of that induction, the displayed chain of Kollár's proof for a single smooth blow-up π : B_Z X → X with ord_Z I ≥ m:

• The product rule (Kollár's product of marked ideals (I₁, m₁) · (I₂, m₂) := (I₁ I₂, m₁ + m₂), [Kol07, Definition 59], under the birational transform of marked ideals, [Kol07, Definition 60]): when F^a ∣ π^* K₁ and F^b ∣ π^* K₂, π_*^{-1}(K₁ K₂, a + b) = π_*^{-1}(K₁, a) · π_*^{-1}(K₂, b) — π^*(K₁ K₂) = F^a π_*^{-1}(K₁, a) · F^b π_*^{-1}(K₂, b) = F^{a+b} · (product) (pow_mul_colon_of_dvd), and the quotient by the invertible F^{a+b} is unique (colon_pow_eq_of_mul_eq) (markedTransform_mul); iterated over a finite product (markedTransform_finset_prod), with markedTransform_pow of Hironaka.Resolution.Algebraic.Kol07.Tuning for the powers.
• The sum rule for an arbitrary family (markedTransform_iSup_le of Hironaka.Sequence for an ℕ-indexed family, here for any index and as an equality): when every π^* K_i is divisible by F^c, π_*^{-1}(⨆ K_i, c) = ⨆ π_*^{-1}(K_i, c), because π^*(⨆ K_i) = ⨆ F^c T_i = F^c · ⨆ T_i (markedTransform_iSup_eq).
• The transform of the tuning ideal (Kollár's chain read as the inclusion ⊆): π_*^{-1}(W_s(I), s) ⊆ W_s(π_*^{-1}(I, m)). Every generating product P_e = ∏_j (D^j I)^{e_j} of weight wt(e) ≥ s has F^{wt(e)} ∣ π^* P_e ([Kol07, Corollary 77]: F^{m-j} ∣ π^* D^j I from ord_Z D^j I ≥ m − j), so π_*^{-1}(P_e, s) ⊆ π_*^{-1}(P_e, wt(e)) (the colon by the smaller power F^s is the smaller ideal, controlledTransformAlong_mono) = ∏_j π_*^{-1}(D^j I, m − j)^{e_j} (the product rule) ⊆ ∏_j D^j(π_*^{-1}(I, m))^{e_j} ([Kol07, Theorem 76] for one blow-up) ⊆ W_s(π_*^{-1}(I, m)); the sum rule assembles the summands (markedTransform_W_le).

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_finset_prod {X Y : Scheme} {ι : Type u_1} (s : Finset ι) (g : ι → X.IdealSheafData) (π : Y ⟶ X) : (∏ i ∈ s, g i).comap π = ∏ i ∈ s, (g i).comap π

The pull-back of a finite product of ideal sheaves is the product of the pull-backs (comap_mul iterated; the empty product is the unit ideal, comap_top).

The product rule for marked transforms

theorem Hironaka.Sequence.markedTransform_mul {X : AlgebraicGeometry.Scheme} (D K₁ K₂ : X.IdealSheafData) (a b : ℕ) (h₁ : D.exceptionalDivisor ^ a ∣ K₁.comap D.blowUpπ) (h₂ : D.exceptionalDivisor ^ b ∣ K₂.comap D.blowUpπ) : (K₁ * K₂).markedTransform D (a + b) = K₁.markedTransform D a * K₂.markedTransform D b

The product rule for marked transforms (Kollár's product of marked ideals, [Kol07, Definition 59], under the birational transform of [Kol07, Definition 60]): for marked ideals (K₁, a), (K₂, b) whose transforms are defined, F^a ∣ π^* K₁ and F^b ∣ π^* K₂, the marked transform of (K₁ K₂, a + b) is the product of the marked transforms: π^*(K₁ K₂) = π^* K₁ · π^* K₂ = F^a π_*^{-1}(K₁, a) · F^b π_*^{-1}(K₂, b), and the quotient by the invertible F^{a+b} is unique.

theorem Hironaka.Sequence.markedTransform_one {X : AlgebraicGeometry.Scheme} (D : X.IdealSheafData) : AlgebraicGeometry.Scheme.IdealSheafData.markedTransform 1 D 0 = 1

The marked transform of the unit ideal with the mark 0 is the unit ideal (the empty product of the product rule).

theorem Hironaka.Sequence.pow_sum_dvd_comap_finset_prod {X : AlgebraicGeometry.Scheme} (D : X.IdealSheafData) {ι : Type u_1} (s : Finset ι) (g : ι → X.IdealSheafData) (c : ι → ℕ) (h : ∀ i ∈ s, D.exceptionalDivisor ^ c i ∣ (g i).comap D.blowUpπ) : D.exceptionalDivisor ^ ∑ i ∈ s, c i ∣ (∏ i ∈ s, g i).comap D.blowUpπ

Definedness of the transform of a finite product: if F^{c_i} ∣ π^* g_i for every factor, then F^{∑ c_i} ∣ π^* ∏ g_i.

theorem Hironaka.Sequence.markedTransform_finset_prod {X : AlgebraicGeometry.Scheme} (D : X.IdealSheafData) {ι : Type u_1} (s : Finset ι) (g : ι → X.IdealSheafData) (c : ι → ℕ) (h : ∀ i ∈ s, D.exceptionalDivisor ^ c i ∣ (g i).comap D.blowUpπ) : (∏ i ∈ s, g i).markedTransform D (∑ i ∈ s, c i) = ∏ i ∈ s, (g i).markedTransform D (c i)

The product rule iterated (Kollár's ∏_j (D^j I, m − j)^{c_j} with the markings added): for marked ideals (g_i, c_i) whose transforms are defined, the marked transform of (∏ g_i, ∑ c_i) is the product of the marked transforms.

The sum rule for an arbitrary family

theorem Hironaka.Sequence.markedTransform_iSup_eq {X : AlgebraicGeometry.Scheme} (D : X.IdealSheafData) {ι : Sort u_1} (K : ι → X.IdealSheafData) (c : ℕ) (hK : ∀ (i : ι), D.exceptionalDivisor ^ c ∣ (K i).comap D.blowUpπ) : (⨆ (i : ι), K i).markedTransform D c = ⨆ (i : ι), (K i).markedTransform D c

The sum rule for marked transforms (markedTransform_iSup_le, for a family indexed by any Sort and as an equality): for marked ideals (K_i, c) of the same mark whose transforms are defined, the marked transform of the sum is the sum of the marked transforms: π^*(⨆ K_i) = ⨆ π^* K_i = ⨆ F^c π_*^{-1}(K_i, c) = F^c · ⨆ π_*^{-1}(K_i, c), and the quotient by the invertible F^c is unique.

The transform of the tuning ideal under one blow-up

theorem Hironaka.Sequence.markedTransform_W_le {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (I : X.IdealSheafData) (m s : ℕ) (hm : I.LeOrdAlong Z.support ↑m) : (AlgebraicGeometry.Scheme.IdealSheafData.W f I m s).markedTransform Z s ≤ AlgebraicGeometry.Scheme.IdealSheafData.W (CategoryTheory.CategoryStruct.comp Z.blowUpπ f) (I.markedTransform Z m) m s

The one-blow-up step of the proof of [Kol07, Theorem 100] (the displayed chain, read as the inclusion ⊆): for a smooth blow-up with ord_Z I ≥ m along every component of the centre, π_*^{-1}(W_s(I), s) ⊆ W_s(π_*^{-1}(I, m)). Each generating product P_e = ∏_j (D^j I)^{e_j} with wt(e) ≥ s has F^{wt(e)} ∣ π^* P_e ([Kol07, Corollary 77]: F^{m−j} ∣ π^* D^j I), so π_*^{-1}(P_e, s) ⊆ π_*^{-1}(P_e, wt(e)) (mark comparison) = ∏_j π_*^{-1}(D^j I, m − j)^{e_j} (the product rule) ⊆ ∏_j D^j(π_*^{-1}(I, m))^{e_j} ([Kol07, Theorem 76] for one blow-up) ⊆ W_s(π_*^{-1}(I, m)) (the definition of W); the sum rule assembles the summands.