Theorem 76 for a single smooth blow-up: the birational transform of derivatives #
[Kol07, Theorem 76] for one blow-up π : B_Z X → X of a smooth k-scheme along a smooth center
Z, in characteristic zero: for a marked ideal (I, m) with ord_Z I ≥ m and j ≤ m,
π_*^{-1}(D^j(I), m − j) ⊆ D^j(π_*^{-1}(I, m)), with D the derivative ideal sheaf of
[Kol07, Definition 73] and π_*^{-1}(·, ·) the marked transform of [Kol07, Definition 60]. Kollár
derives it from the chart formulas of [Kol07, 75]; the proof here follows the derivation-theoretic
argument of [Wlo05, Lemma 2.6.3]. The statement along a sequence is in
Hironaka/Scheme/BlowUpSequence/DerivativeSequence.lean.
Order bookkeeping. ord_Z I ≥ m gives ord_Z D^j(I) ≥ m − j at every generic point of Z
([Kol07, Lemma 74 (3)], le_ord_iff_le_ord_derivativeIter), hence, for a smooth center,
F^{m−j} ∣ π^* D^j(I) (pow_dvd_comap_of_leOrdAlong): the marked transform
π_*^{-1}(D^j(I), m − j) is defined in Kollár's sense.
The case j = 1. The inclusion π_*^{-1}(D(I), m) ⊆ D(π_*^{-1}(I, m+1)) is checked on stalks
(Scheme.IdealSheafData.le_of_stalkIdeal_le). Off the exceptional divisor π is an isomorphism
(isIso_stalkMap_π_of_notMem_support), the stalks of both transforms are π^* of the stalks of
D(I) and I (F_q = 𝒪, the colon by the unit ideal is trivial), the stalk of D(I) is
D_k(I_z) (stalkIdeal_derivative), and D_k commutes with a k-algebra isomorphism
(Ideal.derivative_map_ringEquiv). Over a point z ∈ Z the stalk 𝒪_{B,q} is the localization
R'_𝔮 of the chart ring R' = 𝒪_{X,z}[yᵢ/y_ρ] at a prime of the fibre, compatibly with π^♯
(exists_stalk_equiv_localization_chart_of_smooth), the exceptional stalk is (π^♯ y_ρ)
(stalkIdeal_comap_eq_span_of_chart) and I_z ⊆ P^{m+1} for P = Z_z = (y₀, …, y_ρ)
(stalkIdeal_le_pow_of_leOrdAlong). The stalk of a marked transform is the colon
(K_z 𝒪_{B,q} : (π^♯ y_ρ)^c), and through the isomorphism e with R'_𝔮 it is the localization
of the chart transform transformIdeal:
e(t) · y_ρ^m ∈ D_k(I_z) R'_𝔮 = y_ρ^m · π_*^{-1}(D_k(I_z), m) R'_𝔮 and y_ρ is a nonzerodivisor,
so e(t) lies in the localization of π_*^{-1}(D_k(I_z), m) ⊆ D_k(π_*^{-1}(I_z, m+1)) (the
ring-level inclusion transformIdeal_derivative_le, the argument of [Wlo05, Lemma 2.6.3]), which
lies in D_k of the localization (derivative_map_le), i.e. in D_k(e(T_q)) for the stalk T_q
of π_*^{-1}(I, m+1); transporting back along e gives t ∈ D_k(T_q). The k-algebra
structures are those of f and π ≫ f on the stalks (stalkAlgebra), and e respects them
(stalkMap_comp_algebraMap_stalkAlgebra).
All j. Induction on j: the case j = 1 for (D^j(I), m − j), defined by the order
bookkeeping, then monotonicity of D and D(D^j(I)) = D^{j+1}(I).
Derivative ideals and ring isomorphisms #
Conjugation of a k-derivation by a ring isomorphism respecting the k-structures.
Equations
- Derivation.congrRingEquiv e hk D = { toFun := fun (b : B) => e (D (e.symm b)), map_add' := ⋯, map_smul' := ⋯, map_one_eq_zero' := ⋯, leibniz' := ⋯ }
Instances For
The derivative ideal is transported by a ring isomorphism respecting the k-structures:
D(J) B = D(J B) — derivations are conjugated along e.
Order bookkeeping #
[Kol07, Lemma 74 (3)]: if ord_Z I ≥ m along every component and j ≤ m, then
ord_Z D^j(I) ≥ m − j.
For a smooth center with ord_Z I ≥ m and j ≤ m, F^{m−j} divides π^* D^j(I): the marked
transform π_*^{-1}(D^j(I), m − j) of [Kol07, Definition 73 (73.3)] is defined in the sense of
[Kol07, Definition 60].
The stalks of a marked transform #
Off the exceptional divisor the stalk of π_*^{-1}(K, c) is π^*(K_{π q}) (the exceptional
stalk is the unit ideal).
Over the center, in the chart data at q (exists_stalk_equiv_localization_chart_of_smooth),
the stalk of π_*^{-1}(K, c) is the colon (π^*(K_z) : (π^♯ y_ρ)^c).
One blow-up, j = 1: the two kinds of points of B_Z X #
The k-algebra structure of 𝒪_{B,q} through π ≫ f is π^♯ of the structure of 𝒪_{X,πq}
through f (stalkMap_comp_algebraMap_stalkAlgebra), pointwise.
Off the exceptional divisor: π is an isomorphism there, so the stalks of both transforms are
π^* of the stalks on X, and D_k is transported by the ring isomorphism π^♯.
Over the center, through the chart description of the stalk at q: the ring-level inclusion
transformIdeal_derivative_le, localized at the prime 𝔮 of the fibre and transported along
e.
[Kol07, Theorem 76] for j = 1 and one blow-up: for a smooth blow-up with ord_Z I ≥ m + 1
along every component of the center, π_*^{-1}(D(I), m) ⊆ D(π_*^{-1}(I, m + 1)).
One blow-up, all j #
[Kol07, Theorem 76] for one blow-up, by induction on j (compare [Wlo05, Lemma 2.6.3]): for
a smooth blow-up with ord_Z I ≥ m and j ≤ m, π_*^{-1}(D^j(I), m − j) ⊆ D^j(π_*^{-1}(I, m)).