Lemma 61: the maximal order does not increase under a blow-up of maximal order #
[Kol07, Lemma 61]: for a smooth blow-up π : B_Z X → X with ord_Z I = max-ord I = m, the marked
transform π_*^{-1}(I, m) has order at most m at every point q of B_Z X
(ord_controlledTransform_le), hence max-ord π_*^{-1}(I, m) ≤ max-ord I
(maxOrd_controlledTransform_le); in Kollár's unmarked form the transform is the weak transform
(maxOrd_weakTransform_le, Hironaka/Scheme/IdealSheaf/Order/ExceptionalOrder.lean).
Why. Off the exceptional divisor π is an isomorphism and the marked transform contains I^*,
so ord_q ≤ ord_{π q} I ≤ max-ord I (ord_controlledTransform_le_of_notMem, with
ord_comap_of_isOpenImmersion of Hironaka/Scheme/IdealSheaf/Order/Invariance.lean). At q ∈ F
over z ∈ Z: ord_z I = m (m = ord_Z I ≤ ord_z I ≤ max-ord I = m,
Hironaka/Scheme/IdealSheaf/Order/Specialization.lean), I_z ≤ Z_z^m
(Hironaka/Scheme/IdealSheaf/Order/Exceptional.lean), and 𝒪_{B,q} is the localization of the
chart ring 𝒪_{X,z}[y_i/y_ρ] (Hironaka/Algebra/Local/ChartRing.lean) at a prime 𝔮 of the fibre
(exists_stalk_equiv_localization_chart, Hironaka/Scheme/Smooth/LocalBlowUpChart.lean). The
identity F^m · π_*^{-1}(I, m) = I^* read on stalks says (y_ρ)^m · T_q = I_z 𝒪_{B,q}, so for f ∈ I_z of order m the transform f/y_ρ^m lies in T_q (y_ρ is a nonzerodivisor of the domain
𝒪_{B,q}), and its order is ≤ m by the local Lemma 61 at every prime of the fibre
(ordElem_algebraMap_transformElem_le, Hironaka/Algebra/Local/ChartFibre.lean). Kollár's proof
treats the origins of the charts and reaches every point of the exceptional divisor by a linear
change of coordinates; the argument at the non-rational points of the fibre is the library's own.
Used for the orders along centres in a blow-up sequence
(Hironaka/Scheme/BlowUpSequence/OrderAlongCenter.lean,
Hironaka/Scheme/BlowUpSequence/CentersCosupport.lean,
Hironaka/Scheme/BlowUpSequence/SmoothCenter.lean,
Hironaka/Scheme/BlowUpSequence/TransformDerivative.lean).
Off the exceptional divisor: π is an isomorphism over X ∖ Z, and the marked transform
contains I^*, so its order at q is at most ord_{π q} I.
The stalk of the exceptional divisor F = Z·𝒪_B at a point q of the fibre, in the chart data
of exists_stalk_equiv_localization_chart: it is the principal ideal (π^♯ y_ρ), since each
generator π^♯ y_i (i ≤ ρ) is π^♯ y_ρ times (y_i/y_ρ) read back through e. (The
equivalence e is used only through e.toRingHom: applying it directly makes the unifier work
through the localization's ring instances and exceeds the heartbeat limit.)
In the chart data at q: if π^♯ f lies in the stalk of F^m · T, then
π^♯ f = (π^♯ y_ρ)^m · t for some t in the stalk of T.
The equation (π^♯ y_ρ)^m · t = π^♯ f read through e: y_ρ^m · e t = f in R'_𝔮.
Cancelling y_ρ^m in the domain R'_𝔮: y_ρ^m · e t = f forces e t = f/y_ρ^m.
In the chart data at q, if π^♯ f lies in the stalk of F^m · T, then the transform
f/y_ρ^m of f ∈ P^m lies in the stalk of T transported to the chart ring's localization.
On the exceptional divisor: through the chart at q (exists_stalk_equiv_localization_chart),
F^m · π_*^{-1}(I, m) = I^* (Hironaka/Scheme/IdealSheaf/Order/ExceptionalOrder.lean) and the
local Lemma 61 at every prime of the fibre (ordElem_algebraMap_transformElem_le).
[Kol07, Lemma 61] pointwise: if ord_Z I = max-ord I = m, the marked transform
π_*^{-1}(I, m) has order at most m at every point of B_Z X.
[Kol07, Lemma 61]: max-ord π_*^{-1}(I, m) ≤ max-ord I when ord_Z I = max-ord I = m.
[Kol07, Lemma 61] in its unmarked form: the weak transform is the marked transform with mark
ord_Z I (weakTransformAlong_eq).