The new ideal I_0

The proof of [Kol07, Lemma 102] continues: the blow-up π_{-1} of Z_{-1} is an isomorphism, but the order of I along the selected components E^{jk} drops by m, giving a new ideal sheaf I_0; since the order of I along E^{jk} was at most m, it is now 0, so cosupp(I_0, m) contains no irreducible component of E^j.

The transform. Z_{-1} is a smooth center with ord_{Z_{-1}} I = m (Center.lean), so Kollár's formula (58.1) for the birational transform ([Kol07, 58]) is the marked transform I_0 = (π^* I : F^m) (weakTransform_eq_markedTransform_of_smooth, Hironaka/Scheme/BlowUpSequence/OrderAlongCenter.lean), and F^m divides π^* I (pow_dvd_comap_of_leOrdAlong), so F^m · I_0 = π^* I (exceptionalDivisor_pow_mul_weakTransform).

Over Z_{-1}. At a point x of the exceptional divisor F (which is Z_{-1} under the isomorphism π), ord_x (F^m · I_0) ≥ m · ord_x F + ord_x I_0 ≥ m + ord_x I_0 (superadditivity of the order) while ord_x (π^* I) = ord_{π x} I ≤ max-ord I = m; hence ord_x I_0 = 0 (ord_weakTransform_eq_zero_of_mem_exceptional).

Off Z_{-1}. The birational transform of E^j is (E^j : Z_{-1}^∞) carried along the isomorphism (strictTransformAlong_of_isIso, Hironaka/Scheme/BlowUp/Transform/TransformIso.lean); its points are the points of E^j off Z_{-1} (on Z_{-1} the stalks of E^j and Z_{-1} agree and the saturation is the unit ideal; off Z_{-1} the saturation is E^j itself). A generic point η of the birational transform maps to a generic point of E^j which is NOT selected into Z_{-1} (exists_genericPoint_of_mem_genericPoints_strictTransform: a generic point of E^j specializing to π η lies off Z_{-1}, hence on the saturation, and η is maximal there). Since π^* I ⊆ I_0, ord_η I_0 ≤ ord_{π η} I < m (ord_weakTransform_lt_of_mem_genericPoints, no D-balancedness needed), and for D-balanced I the dichotomy of Basic.lean gives ord_{π η} I = 0, so ord_η I_0 = 0 (ord_weakTransform_eq_zero_of_mem_genericPoints); at such a generic point the stalk of I_0 is the unit ideal, so its restriction to the birational transform of E^j is nonzero on every irreducible component (isNonzeroEverywhere_comap_weakTransform, through isNonzeroEverywhere_iff_irreducibleComponents of Hironaka/Scheme/BlowUpSequence/InducedData.lean on the subscheme: the generic points of its irreducible components are the generic points of the closed set under the closed embedding). This last statement, the nonvanishing required of the ideal of a triple ([Kol07, Definition 31, (1)]), is not made explicit by Kollár. Used by Restriction.lean.

Kollár's formula (58.1)

theorem Hironaka.BD.exceptionalDivisor_pow_mul_weakTransform {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) (hmax : T.I.maxOrd = ↑m) : (Zminus1 T.I m (T.E.component j)).exceptionalDivisor ^ m * T.I.weakTransform (Zminus1 T.I m (T.E.component j)) = T.I.comap (Zminus1 T.I m (T.E.component j)).blowUpπ

For max-ord I = m, F^m · I_0 = π_{-1}^* I (Kollár's formula (58.1), [Kol07, 58], and its Warning on the trivial blow-up of a smooth divisor): I_0 is the marked transform with control m and F^m divides π^* I.

Over Z_{-1}

theorem Hironaka.BD.ord_weakTransform_eq_zero_of_mem_exceptional {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) (hmax : T.I.maxOrd = ↑m) {x : ↥(Zminus1 T.I m (T.E.component j)).blowUp} (hx : x ∈ (Zminus1 T.I m (T.E.component j)).exceptionalDivisor.support) : (T.I.weakTransform (Zminus1 T.I m (T.E.component j))).ord x = 0

For max-ord I = m, I_0 has order 0 at every point over Z_{-1} (m + ord_x I_0 ≤ ord_x (F^m · I_0) = ord_{π x} I ≤ m): the order along E^{jk} is "reduced by m" in the proof of [Kol07, Lemma 102].

Off Z_{-1}: the birational transform of E^j

theorem Hironaka.BD.mem_support_saturate_iff {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) (x : ↥T.X.left) : x ∈ ((T.E.component j).saturate (Zminus1 T.I m (T.E.component j))).support ↔ x ∈ (T.E.component j).support ∧ x ∉ (Zminus1 T.I m (T.E.component j)).support

The points of the saturation (E^j : Z_{-1}^∞) are the points of E^j off Z_{-1}: on Z_{-1} the stalks of E^j and Z_{-1} agree and the saturation is the unit ideal; off Z_{-1} the colon by the unit ideal does not change E^j.

theorem Hironaka.BD.strictTransform_eq_comap_saturate {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) : (T.E.component j).strictTransform (Zminus1 T.I m (T.E.component j)) = ((T.E.component j).saturate (Zminus1 T.I m (T.E.component j))).comap (Zminus1 T.I m (T.E.component j)).blowUpπ

The birational transform of E^j under the trivial blow-up is the saturation (E^j : Z_{-1}^∞) carried along the isomorphism π_{-1} (strictTransformAlong_of_isIso).

theorem Hironaka.BD.exists_genericPoint_of_mem_genericPoints_strictTransform {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) {η : ↥(Zminus1 T.I m (T.E.component j)).blowUp} (hη : η ∈ ((T.E.component j).strictTransform (Zminus1 T.I m (T.E.component j))).support.genericPoints) : (Zminus1 T.I m (T.E.component j)).blowUpπ η ∈ (T.E.component j).support.genericPoints ∧ ¬↑m ≤ T.I.ord ((Zminus1 T.I m (T.E.component j)).blowUpπ η)

A generic point of the birational transform of E^j maps under π_{-1} to a generic point of E^j that is NOT selected into Z_{-1}.

theorem Hironaka.BD.ord_weakTransform_lt_of_mem_genericPoints {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) (_hmax : T.I.maxOrd = ↑m) {η : ↥(Zminus1 T.I m (T.E.component j)).blowUp} (hη : η ∈ ((T.E.component j).strictTransform (Zminus1 T.I m (T.E.component j))).support.genericPoints) : (T.I.weakTransform (Zminus1 T.I m (T.E.component j))).ord η < ↑m

For max-ord I = m, no generic point of the birational transform of E^j lies in cosupp(I_0, m) ("cosupp(I_0, m) does not contain any irreducible component of E^j", the proof of [Kol07, Lemma 102]): π^* I ⊆ I_0 and π η is a non-selected generic point of E^j. Neither D-balancedness nor m ≥ 1 is needed.

theorem Hironaka.BD.ord_weakTransform_eq_zero_of_mem_genericPoints {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) (hI : AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m) (hmax : T.I.maxOrd = ↑m) {η : ↥(Zminus1 T.I m (T.E.component j)).blowUp} (hη : η ∈ ((T.E.component j).strictTransform (Zminus1 T.I m (T.E.component j))).support.genericPoints) : (T.I.weakTransform (Zminus1 T.I m (T.E.component j))).ord η = 0

For D-balanced I with max-ord I = m, I_0 has order 0 along every irreducible component of the birational transform of E^j (the dichotomy of Basic.lean: at a non-selected generic point ord I = 0).

theorem Hironaka.BD.isNonzeroEverywhere_comap_weakTransform {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (m : ℕ) (j : T.E.ι) (hI : AlgebraicGeometry.Scheme.IdealSheafData.IsDBalanced (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I m) (hmax : T.I.maxOrd = ↑m) : ((T.I.weakTransform (Zminus1 T.I m (T.E.component j))).comap ((T.E.component j).strictTransform (Zminus1 T.I m (T.E.component j))).subschemeι).IsNonzeroEverywhere

For D-balanced I with max-ord I = m, the restriction of I_0 to the birational transform of E^j is nonzero on every irreducible component (the requirement on the ideal of a triple, [Kol07, Definition 31, (1)]): at the generic point of each component the stalk of I_0 is the unit ideal.