The exceptional order of the total transform is ord_Z I

[Kol07, Definition 47]: ord_Z I "equals the multiplicity of π^* I along the exceptional divisor"; [Kol07, Definition 60]: the birational transform π_*^{-1}(I, m) for m ≤ ord_Z I, whose vanishing order along Z is "m less than the vanishing order of I along Z"; [Hau14, §6]: f^* = h^k f^s with k maximal, "the value of k is the order of f^* along E", and [Hau14, Definition 6.8], the controlled transform I^* = I_E^c · I^!.

• Sharpness, globally: if ord_Z I = m exactly then F^{m+1} ∤ I^* (not_pow_succ_dvd_comap). The proof pulls the inequality I^* ≤ F^{m+1} back along the local blow-up at the generic point η, the base change of B_Z X along Spec 𝒪_{X,η} → X (exists_isPullback_fromSpecStalk, Hironaka/Scheme/Smooth/LocalBlowUp.lean), whose centre is the maximal ideal 𝔪_η = Z_η (the centre is integral, so its local ring at η is a field), and then to the chart of the last coordinate y_ρ of a regular system of parameters (affineBlowUp.chart, affineBlowUp.chart_π and the specIdealSheaf calculus of Hironaka/Scheme/BlowUp/AffineBlowUp/Universal): on the chart ring R' = 𝒪_{X,η}[𝔪_η/y_ρ] it reads I_η R' ≤ (y_ρ)^{m+1}, which the local computation of Hironaka/Algebra/Local/ChartGenericFibre.lean (Kollár's expansion y_ρ^{-m} f(y₁ y_ρ, …) in the proof of [Kol07, Lemma 61]) refutes for an f ∈ I_η of order m. Only the contravariant pull-back of ideal sheaves along the base change is used, no isomorphism of stalks. That 𝒪_{X,η} is not a field, Z not being a component, comes from the dimension formula dim 𝒪_{X,η} + trdeg_k κ(η) = n on X and on Z (Scheme.ringKrullDim_stalk_add_trdeg_residueField_of_smoothOfRelativeDimension of Hironaka/Algebra/RegularSmooth/SchemeForms.lean; ringKrullDim_stalk_ne_zero).
• The exceptional order sup {c : F^c ∣ I^*} (exceptionalOrderAlong) is ord_Z I (exceptionalOrderAlong_eq_ord), from Hironaka/Scheme/IdealSheaf/Order/Exceptional.lean and the sharpness.
• For m ≤ ord_Z I, F^m · π_*^{-1}(I, m) = I^* (pow_mul_controlledTransformAlong), for m = ord_Z I the birational transform is the weak transform (weakTransformAlong_eq), and F^c ∣ π_*^{-1}(I, m) ⟺ c + m ≤ ord_Z I (pow_dvd_controlledTransformAlong_iff): the exceptional order drops by m.

Used for the order along a centre in a blow-up sequence (Hironaka/Scheme/BlowUpSequence/OrderAlongCenter.lean).

theorem AlgebraicGeometry.subschemeι_genericPoint_eq {X : Scheme} (Z : X.IdealSheafData) [IsIntegral Z.subscheme] {η : ↥X} (hη : IsGenericPoint η ↑Z.support) : Z.subschemeι (genericPoint ↥Z.subscheme) = η

The generic point of the subscheme of an integral center maps to the generic point of its support.

theorem AlgebraicGeometry.stalkIdeal_eq_maximalIdeal_of_isGenericPoint {X : Scheme} (Z : X.IdealSheafData) [IsIntegral Z.subscheme] {η : ↥X} (hη : IsGenericPoint η ↑Z.support) : Z.stalkIdeal η = IsLocalRing.maximalIdeal ↑(X.presheaf.stalk η)

At the generic point of an integral center the ideal of the center is the maximal ideal: the local ring of Z at its generic point is a field (Mathlib's function field).

theorem AlgebraicGeometry.ringKrullDim_stalk_ne_zero {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n r : ℕ) [SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [SmoothOfRelativeDimension (n - r) (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (hr : 1 ≤ r) (hrn : r ≤ n) {η : ↥X} (hη : IsGenericPoint η ↑Z.support) : ringKrullDim ↑(X.presheaf.stalk η) ≠ 0

Z is not a component of X: the local ring of X at the generic point of Z is not a field (the dimension formula on X and on Z: dim 𝒪_{X,η} = n − trdeg κ(η) = n − (n − r) = r ≥ 1).

theorem AlgebraicGeometry.not_pow_succ_dvd_comap {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n r : ℕ) [SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [SmoothOfRelativeDimension (n - r) (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (hr : 1 ≤ r) (hrn : r ≤ n) (I : X.IdealSheafData) {η : ↥X} (hη : IsGenericPoint η ↑Z.support) (m : ℕ) (hm : I.ord η = ↑m) : ¬Z.comap Z.blowUpπ ^ (m + 1) ∣ I.comap Z.blowUpπ

Sharpness (the expansion in the proof of [Kol07, Lemma 61]; [Hau14, §6], k maximal): if ord_Z I = m exactly then F^{m+1} does not divide I^*.

theorem AlgebraicGeometry.exceptionalOrderAlong_eq_ord {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n r : ℕ) [SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [SmoothOfRelativeDimension (n - r) (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (hr : 1 ≤ r) (hrn : r ≤ n) (I : X.IdealSheafData) {η : ↥X} (hη : IsGenericPoint η ↑Z.support) (hI : I.ord η ≠ ⊤) : ↑(exceptionalOrderAlong Z.blowUpπ (Z.comap Z.blowUpπ) I) = I.ord η

[Kol07, Definition 47]; [Hau14, §6]: the exceptional order of I^* — the largest c with F^c ∣ I^* — is ord_Z I, for I_η ≠ 0.

theorem AlgebraicGeometry.pow_mul_controlledTransformAlong {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n r : ℕ) [SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [SmoothOfRelativeDimension (n - r) (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (hr : 1 ≤ r) (hrn : r ≤ n) (I : X.IdealSheafData) {η : ↥X} (hη : IsGenericPoint η ↑Z.support) (m : ℕ) (hm : ↑m ≤ I.ord η) : Z.comap Z.blowUpπ ^ m * I.controlledTransformAlong Z.blowUpπ (Z.comap Z.blowUpπ) m = I.comap Z.blowUpπ

[Kol07, (60.1)]; [Hau14, Definition 6.8]: for m ≤ ord_Z I, F^m · π_*^{-1}(I, m) = I^*.

theorem AlgebraicGeometry.weakTransformAlong_eq {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n r : ℕ) [SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [SmoothOfRelativeDimension (n - r) (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (hr : 1 ≤ r) (hrn : r ≤ n) (I : X.IdealSheafData) {η : ↥X} (hη : IsGenericPoint η ↑Z.support) (m : ℕ) (hm : I.ord η = ↑m) : I.weakTransformAlong Z.blowUpπ (Z.comap Z.blowUpπ) = I.controlledTransformAlong Z.blowUpπ (Z.comap Z.blowUpπ) m

[Kol07, Definition 60]; [Hau14, Definition 6.8]: for m = ord_Z I the birational transform is the weak transform.

theorem AlgebraicGeometry.pow_dvd_controlledTransformAlong_iff {X : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n r : ℕ) [SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [SmoothOfRelativeDimension (n - r) (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (hr : 1 ≤ r) (hrn : r ≤ n) (I : X.IdealSheafData) {η : ↥X} (hη : IsGenericPoint η ↑Z.support) (m : ℕ) (hm : ↑m ≤ I.ord η) (c : ℕ) : Z.comap Z.blowUpπ ^ c ∣ I.controlledTransformAlong Z.blowUpπ (Z.comap Z.blowUpπ) m ↔ ↑(c + m) ≤ I.ord η

[Kol07, Definition 60], "m less": for m ≤ ord_Z I, F^c divides π_*^{-1}(I, m) exactly when c + m ≤ ord_Z I.