Kollár's Example 106 run through the order-reduction functor BO_{4,2} #
[Kol07, Example 106] follows the principalization of I = (x³ − y², x⁴ + xz² − w³) on 𝔸⁴.
This file checks the beginning of the run against the functor BO_{4,2} of [Kol07, Theorem 103]
(Hironaka.BO.data, assembled from arbitrary inductive data BMO_{≤ 3}) on the triple
(𝔸⁴_ℚ, I, ∅) of HironakaExamples/KollarExample106Triple.lean. The chart computations it
relies on are those of HironakaExamples/OrderReduction/Example106.lean, Example106BlowUp.lean
and Example106Length.lean, together with the general cosupport forcing of
HironakaExamples/Sequence/CosuppForcing.lean and the comparison of the blow-up of Spec R with
the affine blow-up in HironakaExamples/BlowUp/Glue/SpecIso.lean.
How the check is run. Nothing of the inductive input B is unfolded: BO_{4,2} is tested
through its three properties alone. Its sequence is a smooth blow-up sequence of order 2
(isOrderSeq), has no empty centre (noEmptyCenters, the convention [Kol07, 32]) and ends with
maximal order < 2 (maxOrd_lt, [Kol07, Theorem 103 (1)]). Under these the centres are forced:
the cosupport {ord ≥ 2} of the current ideal is a single closed point, every generic point of
the next centre has order 2 ([Kol07, Definition 66 (4)]), so the centre is supported at that
point; being smooth it is the reduced point. At stage 0 the cosupport of I is the origin
(HironakaExamples/Balanced/Example106.lean, at every scheme point); at stage 1 the transform
I₁ = π_*^{-1}(I, 2) of the marked ideal ([Kol07, Definition 60]), which is the weak transform
since ord_0 I = 2, is read on the four charts of the blow-up of the origin, where it is
(σ_j I : x_j²): on the x-chart ∂_{x₁}(x₁ − y₁²) = 1, so the order has dropped to 1 there,
as Kollár says; the y- and w-charts have no point of order 2; but on the z-chart the
cosupport is the origin q = [0:0:1:0] ∈ E₁, the intersection of E₁ with the strict transform
of the z-axis. At stages 2 and 3 the same computation on K_z = (x³z − y², z(x⁴z + x − w³))
and K_zw finds further points q', q'' of order 2
(HironakaExamples/MaximalContact/Example106Stages.lean), so the order-2 run has at least four
blow-ups.
Kollár's text, corrected. "The order has dropped to 1" holds on the x-chart but not on the
z-chart, so BO_{4,2} does not yet continue with (I₁, 1, E₁) as printed: it first blows up
q (secondCenter, four_le_length). The cuspidal curve (x₁ = y₁ = z₁² − w₁³ = 0) of Kollár's
last sentences is strictTransform_meets_plane_ideal in
HironakaExamples/OrderReduction/Example106.lean, an instance of [Kol07, Warning 23] (the strict
transform of a smooth X need not meet the exceptional divisor in a simple normal crossing
divisor).
The triple (𝔸⁴_ℚ, I, ∅) of [Kol07, Example 106] is well formed in the sense of
[Kol07, Notation 64]: 𝔸⁴_ℚ → Spec ℚ is affine (quasi-compact, separated), smooth of relative
dimension 4, hence locally of finite type; I ≠ 0 on the domain ℚ[x, y, z, w]
(isNonzeroEverywhere_I106); the empty boundary is a simple normal crossing divisor
(isSnc_empty_of_smooth).
Kollár's "ord I = 2": the triple lies in the class BOClass 4 2 of Theorem 103: 1 ≤ 2,
dim 𝔸⁴ = 4 ≤ 4, max-ord I ≤ 2 (maxOrd_le_two, at every scheme point).
"Thus the first step is to blow up the origin in 𝔸⁴" ([Kol07, Example 106]):
BO_{4,2}(𝔸⁴_ℚ, I, ∅) begins with the blow-up of the origin m₀ = (x, y, z, w), by the cosupport
forcing at stage 0 (exists_eq_cons_specIdealSheaf_m0) applied to the three properties of the
functor.
The correction to Kollár's continuation: the second blow-up of BO_{4,2}(𝔸⁴_ℚ, I, ∅) has a
centre supported at q = [0:0:1:0], the point where the strict transform of the z-axis meets
E₁, at which I₁ has order exactly 2 (secondCenter_of_axioms applied to the three
properties of the functor, rewritten along the first-stage identity).
The order-2 run of BO_{4,2}(𝔸⁴_ℚ, I, ∅) has at least four blow-ups, forced by the points
q, q', q'' of order 2 at the stages 1, 2, 3
(HironakaExamples/MaximalContact/Example106Stages.lean; four_le_length_of_axioms applied to the
three properties of the functor).