A counterexample to the formula (88.2) in Kollár's proof of Theorem 88 #

The proof of [Kol07, Theorem 88] rewrites the derivatives of a birational transform through the displayed formula (88.2), which rests on the identity ∂_{y_1}^j π_*^{-1}(I, m) = π_*^{-1}(∂_{x_1}^j I, m − j) for the chart coordinate y_1. Read for ideals, with ⟨∂^j J⟩ the ideal generated by the j-th partial derivatives of all elements of J, the equality is false, and so is the inclusion ⟨∂_{y_1}^j π_*^{-1}(I, m)⟩ ⊆ π_*^{-1}(D^j I, m − j). This file records the counterexample at m = 1; the conclusion (88.1) of the theorem is not affected in this example, where both sides of (88.1) are the unit ideal (not checked here).

What this library proves of Theorem 88 is its conclusion (88.1) under Kollár's hypotheses: for one blow-up in Hironaka/Resolution/Algebraic/Kol07/Theorem88BlowUp.lean (derivativeIter_markedTransform_eq_iSup) and along a smooth blow-up sequence of order ≥ m in Hironaka/Resolution/Algebraic/Kol07/Theorem88Sequence.lean (derivativeIter_markedTransformSeq_eq_iSup), with [Kol07, Corollary 89] in Hironaka/Resolution/Algebraic/Kol07/Corollary89.lean. The proof does not pass through (88.2): it computes on generators in the chart (Hironaka/Algebra/Local/TransformDerivIter.lean, Hironaka/Algebra/Local/TransformDerivNormalForm.lean, Hironaka/Algebra/Local/ChartLogDerivations.lean) with the supporting modules Hironaka/Scheme/IdealSheaf/Derivative/FlagCoords.lean, Hironaka/Scheme/IdealSheaf/Derivative/DualSpans.lean and Hironaka/Scheme/IdealSheaf/StalkLe.lean (flag coordinates, bases of derivations, and the stalk comparison for the sum over j ≤ s).

R = k[x_0, x_1, t], Z = (x_0, x_1), S = (x_0), I = (x_1² + t² x_1) (ord_Z I = 1), the chart of x_1 (x_0 = x_1 y_0, chart ring R' = k[y_0, x_1, t]): J = π_*^{-1}(I, 1) = (g) with g = x_1 + t², and π_*^{-1}(D I, 0) = (D I) R' = (x_1 g, 2 x_1 + t², t x_1) =: J_1.

In characteristic zero the ideal of all first partials contains the ideal itself: u = ∂(y u) − y ∂u for a derivation with ∂ y = 1 (mem_of_pderiv_eq_one). So the all-element inclusion ⟨∂_{y_0} J⟩ ⊆ J_1 would force J ⊆ J_1, i.e. g ∈ J_1.
g ∉ J_1 (transformElem_not_mem): the k-algebra map R' → k[t]/(t³), y_0 ↦ 0, x_1 ↦ −t²/2, t ↦ t, kills the three generators of J_1 and sends g to t²/2 ≠ 0.

Hence ⟨∂_{y_0} J⟩ ⊄ J_1, and a fortiori ⟨∂_{y_0} J⟩ ≠ J_1: both readings of (88.2) fail. The example is stated in the polynomial chart ring over ℚ; the localization at a point of the chart does not restore the inclusion (the test map factors through the local ring at the origin).

source