The order of an ideal along a smooth center of any shape #
The divisibility F^m ∣ π^* I, the exceptional order of π^* I and Kollár's Lemma 61 are proved
elsewhere in this library for an integral center Z of pure codimension, working at the generic
point of Z (Hironaka/Scheme/IdealSheaf/Order/Lemma61.lean,
Hironaka/Scheme/IdealSheaf/Order/ExceptionalOrder.lean). A center of [Kol07, Definition 66] may
have several components; this module runs the same arguments at the generic point of the component
through each point of the center, for a center that is merely smooth. The order of an ideal along a
reducible Z is understood at every generic point of Z, as in [Kol07, Definition 47].
The component through a point. At z ∈ Z the stalk Z_z is prime (𝒪_{X,z}/Z_z ≅ 𝒪_{Z,z} is
regular, so a domain). On an affine U ∋ z the prime p = Z_z ∩ Γ(U) has a point η ∈ U; η lies
in Z, specializes to z, and is a generic point of Z (no proper generization inside Z: a
prime q ⊆ p containing Z(U) becomes Z_z in 𝒪_{X,z}, so q = p). The stalk 𝒪_{X,η} is the
localization of 𝒪_{X,z} at Z_z, whence ord_{Z_z} I_z = ord_η I and Z_η = 𝔪_η
(exists_genericPoint_of_isPrime_stalkIdeal). Every generic point of Z in the sense of
Closeds.genericPoints arises this way from any point of its component.
The main results are weakTransform_eq_markedTransform_of_smooth (the birational transform of
[Kol07, 58] is the marked transform of [Kol07, Definition 60] when ord_Z I = m along every
component of Z) and maxOrd_controlledTransform_le_of_smooth ([Kol07, Lemma 61] for a smooth
center of any shape). They enter the transforms of triples and Remark 67
(Hironaka/Scheme/BlowUpSequence/Triple.lean, Remark67.lean).
The generic point of the component of the center through a point #
For z ∈ Z with Z_z prime: the generic point η of the component of Z through z (the
point of the prime Z_z ∩ Γ(U) of an affine U ∋ z) is a generic point of Z, specializes to
z, has Z_η = 𝔪_η, and ord_{Z_z} I_z = ord_η I for every I: the order along a center
[Kol07, Definition 47] read at the component through z. Not in the sources; the point-set
topology behind the arguments below.
A smooth center: containment in the powers of the center, the exceptional order, Lemma 61 #
The stalk of a smooth center at a point of the center is prime (𝒪_{X,z}/Z_z is regular).
Under a point of the blow-up the center's stalk is nonzero (it contains a member of a regular system of parameters).
Stalkwise, for a smooth center of any shape: if ord_Z I ≥ m along every component and
Z_z ≠ 0, then I_z ⊆ Z_z^m; the order along Z_z is the order at the generic point of the
component through z, and for a prime generated by part of a regular system of parameters an
ideal of order ≥ m along it lies in its m-th power.
On the blow-up of a smooth center of any shape: π^* I ⊆ F^m when ord_Z I ≥ m along every
component; at points over the center by stalkIdeal_le_pow_of_leOrdAlong, off it trivially.
F^m ∣ π^* I when ord_Z I ≥ m along every component of a smooth center: "the number
ord_Z I equals the multiplicity of π^* I along the exceptional divisor" [Kol07, Definition 47],
the inequality ≥.
At a generic point η of a smooth center Z of any shape over which the blow-up has points
(Z_η ≠ 0), ord_η I = m forbids F^{m+1} ∣ π^* I: the multiplicity of π^* I along the
exceptional divisor is at most ord_Z I [Kol07, Definition 47]. The argument is run on the chart
of the local blow-up at η, where Z_η = 𝔪_η: an element of I_η of order exactly m is not
in the (m+1)-st power of the center's ideal in the chart ring.
For a smooth center of any shape with ord_Z I = m along every component, the birational
transform of [Kol07, 58, (58.1)] is the marked transform π_*^{-1}(I, m) of
[Kol07, Definition 60]: the exceptional order of π^* I is m when the blow-up has a point over
the center, and when it has none the exceptional divisor is 𝒪 and both transforms are
π^* I.
[Kol07, Lemma 61] for a smooth center of any shape: if ord_Z I = m along every component
and max-ord I = m, the marked transform π_*^{-1}(I, m) has order at most m at every point
of B_Z X. The proof is Kollár's computation in the chart at each point over the center (an
element of order m of I_z has a transform of order ≤ m), the order at the center's point
being pinned by the generic point of its component; off the center the blow-up is an
isomorphism.
[Kol07, Lemma 61] in its global form: max-ord π_*^{-1}(I, m) ≤ m when
ord_Z I = max-ord I = m along a smooth center of any shape.