The order along a smooth centre and the exceptional divisor

[Kol07, Definition 47], last paragraph: "the number ord_Z I equals the multiplicity of π^* I along the exceptional divisor of the blow-up"; [Kol07, Definition 60] assumes m ≤ ord_Z I; [Hau14, Definition 6.8]: for c at most the order d of I along the centre, "I^* has order ≥ c along E".

For a smooth irreducible centre Z with generic point η and m ≤ ord_Z I = ord_η I, every section of I lies in Z^m near Z, I ≤ Z ^ m as ideal sheaves (le_pow_of_le_ord), and hence F^m ∣ I^* on the blow-up (exceptionalDivisor_pow_dvd_comap_of_le_ord). Kollár's argument reads I_η ⊆ 𝔪_η^m = (x₁, …, x_r)^m 𝒪_{X,η} at the generic point and propagates to the points of Z; here the propagation is Pᵐ R_P ∩ R = Pᵐ (the symbolic power equals the ordinary power for a prime P = Z_z generated by part of a regular system of parameters, le_ordAlong_chartCenter_iff of Hironaka/Algebra/Local/SymbolicPower.lean) applied at every point z of Z, through the identification of 𝒪_{X,η} with the localization of 𝒪_{X,z} at Z_z (ordAlong_stalkIdeal_eq_ord_stalkIdeal: on an affine open U ∋ z both stalks are localizations of Γ(U), Mathlib's IsAffineOpen.isLocalization_stalk, and Z_z ∩ Γ(U) = Z(U) is the prime of η, Z being integral). Integrality of the centre: Z is irreducible (the generic point) and its stalks are regular (smooth over k), so reduced (isIntegral_subscheme_of_smooth, via isIntegral_subscheme_of_isRegularLocalRing_stalk of Hironaka/Scheme/BlowUp/Transform/WeakTransform.lean).

Used for the order along centres and the strict transforms of components (Hironaka/Scheme/BlowUpSequence/OrderAlongCenter.lean, Hironaka/Scheme/BlowUpSequence/StrictTransformIntegral.lean, Hironaka/Resolution/Algebraic/MarkedOrderReduction/SplitOrder.lean, Hironaka/Resolution/Algebraic/Snc/ComponentStalks.lean) and for the sharpness F^{m+1} ∤ I^* (Hironaka/Scheme/IdealSheaf/Order/ExceptionalOrder.lean).

Integrality of an irreducible smooth center

theorem AlgebraicGeometry.irreducibleSpace_subscheme_of_isGenericPoint {X : Scheme} (Z : X.IdealSheafData) {η : ↥X} (hη : IsGenericPoint η ↑Z.support) : IrreducibleSpace ↥Z.subscheme

The subscheme of an ideal sheaf whose support has a generic point is irreducible.

theorem AlgebraicGeometry.isIntegral_subscheme_of_smooth {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) (Z : X.IdealSheafData) [Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] {η : ↥X} (hη : IsGenericPoint η ↑Z.support) : IsIntegral Z.subscheme

A centre smooth over k with a generic point is integral.

The order along the center at a point equals the order at the generic point

theorem AlgebraicGeometry.isPrime_stalkIdeal_of_mem_support {X : Scheme} (Z : X.IdealSheafData) [IsIntegral Z.subscheme] {z : ↥X} (hz : z ∈ Z.support) : (Z.stalkIdeal z).IsPrime

For an integral center, the stalk of its ideal sheaf at a point of the center is prime.

theorem AlgebraicGeometry.ordAlong_stalkIdeal_eq_ord_stalkIdeal {X : Scheme} (Z I : X.IdealSheafData) [IsIntegral Z.subscheme] {η z : ↥X} (hη : IsGenericPoint η ↑Z.support) (hz : z ∈ Z.support) [hP : (Z.stalkIdeal z).IsPrime] : IsLocalRing.ordAlong (Z.stalkIdeal z) (I.stalkIdeal z) = IsLocalRing.ord (I.stalkIdeal η)

The propagation from the generic point: at a point z of an integral centre Z with generic point η, the order of I_z along the prime Z_z — the order in the localization (𝒪_{X,z})_{Z_z} = 𝒪_{X,η} — is ord_η I.

theorem AlgebraicGeometry.le_pow_of_le_ordAlong_of_eq_chartCenter {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (x : Fin n → R) (hx : IsLocalRing.maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (r : Fin n) (P : Ideal R) [P.IsPrime] (hP : P = IsLocalRing.chartCenter x r) (I : Ideal R) (m : ℕ) (h : ↑m ≤ IsLocalRing.ordAlong P I) : I ≤ P ^ m

le_ordAlong_chartCenter_iff of Hironaka/Algebra/Local/SymbolicPower.lean transported along an identification of the prime with a chartCenter: m ≤ ord_P I gives I ≤ P^m.

The order along the centre bounds the exceptional multiplicity from below

theorem AlgebraicGeometry.le_pow_of_le_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) (m : ℕ) (hm : ↑m ≤ I.ord η) : I ≤ Z ^ m

If m ≤ ord_Z I then I ≤ Z^m (the hypothesis of [Kol07, Definition 60]; the argument at every point of Z is the library's own).

theorem AlgebraicGeometry.exceptionalDivisor_pow_dvd_comap_of_le_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) (m : ℕ) (hm : ↑m ≤ I.ord η) : Z.comap Z.blowUpπ ^ m ∣ I.comap Z.blowUpπ

[Kol07, Definition 47]; [Hau14, Definition 6.8]: if m ≤ ord_Z I then F^m divides the total transform I^* — F = Z·𝒪_B being invertible, I^* ≤ F^m suffices.