Kollár's Example 106, the first blow-up: the restriction to H and the four charts

[Kol07, Example 106]: I = (x³ − y², x⁴ + xz² − w³) ⊂ ℚ[x, y, z, w], m = 2, H = (y = 0) a hypersurface of maximal contact (y ∈ MC(I) = D(I), derivative_example106 in HironakaExamples/Balanced/Example106.lean), H' = (y − x²) a second one. Computed exactly in ℚ:

• I|_H = (x³, xz² − w³) in ℚ[x, z, w] has order 3 at the origin and D²(I|_H) = (x, z, w), as Kollár says;
• on the x-chart of the blow-up of the origin, I₁ = (x₁ − y₁², x₁(x₁ + z₁² − w₁³)), Kollár's display, has no point of order 2 (∂(x₁ − y₁²)/∂x₁ = 1), and I₁ + (x₁) = (x₁, y₁²), which gives Kollár's second centre (x₁ = y₁ = 0) of the order-1 run;
• the y- and w-charts have no point of order 2;
• on the z-chart, I₁ = (x₁³z₁ − y₁², z₁(x₁⁴z₁ + x₁ − w₁³)) has order exactly 2 at the origin q = [0:0:1:0] ∈ E₁, which is its only ℚ-point of order ≥ 2, and y₁, y₁ − x₁²z₁ ∈ MC(I₁). This corrects Kollár's sentence "the order has dropped to 1", which holds on the x-chart but not on the z-chart: the order-2 run of Example 106 continues at q (HironakaExamples/MaximalContact/Example106Stages.lean).

Tools: orders at a ℚ-point p are memberships in powers of 𝔪_p; from g ∈ 𝔪_p² the value and the first partials of g vanish at p (pderiv_mem_pow_of_mem_pow_succ, eval_eq_zero_of_mem_span), and the resulting rational equations are solved by cases.

theorem Hironaka.Examples.derivative_span_le_pow {σ : Type u_1} [Finite σ] {S : Set (MvPolynomial σ ℚ)} {N : Ideal (MvPolynomial σ ℚ)} {k : ℕ} (h : ∀ s ∈ S, s ∈ N ^ (k + 1)) : Ideal.derivative ℚ (Ideal.span S) ≤ N ^ k

D(⟨S⟩) ≤ 𝔪^k when every element of S lies in 𝔪^{k+1}: the generators stay, the partials drop one power (the Leibniz rule).

theorem Hironaka.Examples.derivativeIter_two_span_le_pow {σ : Type u_1} [Finite σ] {S : Set (MvPolynomial σ ℚ)} {N : Ideal (MvPolynomial σ ℚ)} {k : ℕ} (h : ∀ s ∈ S, s ∈ N ^ (k + 2)) : Ideal.derivativeIter ℚ 2 (Ideal.span S) ≤ N ^ k

D²(⟨S⟩) ≤ 𝔪^k when every element of S lies in 𝔪^{k+2}.

theorem Hironaka.Examples.pderiv_mem_derivative {σ : Type u_1} {J : Ideal (MvPolynomial σ ℚ)} (i : σ) {g : MvPolynomial σ ℚ} (hg : g ∈ J) : (MvPolynomial.pderiv i) g ∈ Ideal.derivative ℚ J

A partial derivative of a member of an ideal lies in its derivative ideal.

theorem Hironaka.Examples.eval_eq_zero_of_mem_m4 (a b c d : ℚ) {g : MvPolynomial (Fin 4) ℚ} (hg : g ∈ Ideal.span {MvPolynomial.X 0 - MvPolynomial.C a, MvPolynomial.X 1 - MvPolynomial.C b, MvPolynomial.X 2 - MvPolynomial.C c, MvPolynomial.X 3 - MvPolynomial.C d}) : (MvPolynomial.eval ![a, b, c, d]) g = 0

Members of 𝔪_p = (x − a, y − b, z − c, w − d) vanish at p = (a, b, c, d).

theorem Hironaka.Examples.vanish_of_mem_m4_sq (a b c d : ℚ) {g : MvPolynomial (Fin 4) ℚ} (hg : g ∈ Ideal.span {MvPolynomial.X 0 - MvPolynomial.C a, MvPolynomial.X 1 - MvPolynomial.C b, MvPolynomial.X 2 - MvPolynomial.C c, MvPolynomial.X 3 - MvPolynomial.C d} ^ 2) : (MvPolynomial.eval ![a, b, c, d]) g = 0 ∧ ∀ (i : Fin (Nat.succ 0).succ.succ.succ), (MvPolynomial.eval ![a, b, c, d]) ((MvPolynomial.pderiv i) g) = 0

Order ≥ 2 at p: the value and the four partial derivatives vanish at p.

theorem Hironaka.Examples.eval_pderiv_pderiv_eq_zero_of_mem_m0_cube {g : MvPolynomial (Fin 4) ℚ} (hg : g ∈ Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1, MvPolynomial.X 2, MvPolynomial.X 3} ^ 3) (i j : Fin 4) : (MvPolynomial.eval ![0, 0, 0, 0]) ((MvPolynomial.pderiv j) ((MvPolynomial.pderiv i) g)) = 0

Order ≥ 3 at the origin excluded by a nonzero second partial: if g ∈ 𝔪₀³ then every second partial derivative of g vanishes at 0.

theorem Hironaka.Examples.x_mem_m0_fin4 : MvPolynomial.X 0 ∈ Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1, MvPolynomial.X 2, MvPolynomial.X 3}

x ∈ (x, y, z, w) in ℚ[x, y, z, w].

theorem Hironaka.Examples.y_mem_m0_fin4 : MvPolynomial.X 1 ∈ Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1, MvPolynomial.X 2, MvPolynomial.X 3}

y ∈ (x, y, z, w).

theorem Hironaka.Examples.z_mem_m0_fin4 : MvPolynomial.X 2 ∈ Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1, MvPolynomial.X 2, MvPolynomial.X 3}

z ∈ (x, y, z, w).

theorem Hironaka.Examples.w_mem_m0_fin4 : MvPolynomial.X 3 ∈ Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1, MvPolynomial.X 2, MvPolynomial.X 3}

w ∈ (x, y, z, w).

The restriction to H = (y = 0)

theorem Hironaka.Examples.Example106Charts.map_example106_H : Ideal.map (MvPolynomial.aeval ![MvPolynomial.X 0, 0, MvPolynomial.X 1, MvPolynomial.X 2]) (Ideal.span {MvPolynomial.X 0 ^ 3 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 0 ^ 4 + MvPolynomial.X 0 * MvPolynomial.X 2 ^ 2 - MvPolynomial.X 3 ^ 3}) = Ideal.span {MvPolynomial.X 0 ^ 3, MvPolynomial.X 0 * MvPolynomial.X 1 ^ 2 - MvPolynomial.X 2 ^ 3}

Kollár's "I|_H = (x³, xz² − w³)": the image of I under y ↦ 0.

theorem Hironaka.Examples.Example106Charts.ord_zero_map_example106_H : Ideal.span {MvPolynomial.X 0 ^ 3, MvPolynomial.X 0 * MvPolynomial.X 1 ^ 2 - MvPolynomial.X 2 ^ 3} ≤ Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1, MvPolynomial.X 2} ^ 3 ∧ ¬Ideal.span {MvPolynomial.X 0 ^ 3, MvPolynomial.X 0 * MvPolynomial.X 1 ^ 2 - MvPolynomial.X 2 ^ 3} ≤ Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1, MvPolynomial.X 2} ^ 4

Kollár's "I|_H has order 3": order exactly 3 at the origin of ℚ[x, z, w].

theorem Hironaka.Examples.Example106Charts.derivativeIter_map_example106_H : Ideal.derivativeIter ℚ 2 (Ideal.span {MvPolynomial.X 0 ^ 3, MvPolynomial.X 0 * MvPolynomial.X 1 ^ 2 - MvPolynomial.X 2 ^ 3}) = Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1, MvPolynomial.X 2}

Kollár's "MC(I|_H) = (x, z, w)": D²(I|_H) = (x, z, w).

The x-chart

theorem Hironaka.Examples.Example106Charts.transform_example106_x : (MvPolynomial.aeval ![MvPolynomial.X 0, MvPolynomial.X 1 * MvPolynomial.X 0, MvPolynomial.X 2 * MvPolynomial.X 0, MvPolynomial.X 3 * MvPolynomial.X 0]) (MvPolynomial.X 0 ^ 3 - MvPolynomial.X 1 ^ 2) = MvPolynomial.X 0 ^ 2 * (MvPolynomial.X 0 - MvPolynomial.X 1 ^ 2) ∧ (MvPolynomial.aeval ![MvPolynomial.X 0, MvPolynomial.X 1 * MvPolynomial.X 0, MvPolynomial.X 2 * MvPolynomial.X 0, MvPolynomial.X 3 * MvPolynomial.X 0]) (MvPolynomial.X 0 ^ 4 + MvPolynomial.X 0 * MvPolynomial.X 2 ^ 2 - MvPolynomial.X 3 ^ 3) = MvPolynomial.X 0 ^ 2 * (MvPolynomial.X 0 * (MvPolynomial.X 0 + MvPolynomial.X 2 ^ 2 - MvPolynomial.X 3 ^ 3)) ∧ (MvPolynomial.aeval ![MvPolynomial.X 0, MvPolynomial.X 1 * MvPolynomial.X 0, MvPolynomial.X 2 * MvPolynomial.X 0, MvPolynomial.X 3 * MvPolynomial.X 0]) (MvPolynomial.X 1) = MvPolynomial.X 0 * MvPolynomial.X 1 ∧ (MvPolynomial.aeval ![MvPolynomial.X 0, MvPolynomial.X 1 * MvPolynomial.X 0, MvPolynomial.X 2 * MvPolynomial.X 0, MvPolynomial.X 3 * MvPolynomial.X 0]) (MvPolynomial.X 1 - MvPolynomial.X 0 ^ 2) = MvPolynomial.X 0 * (MvPolynomial.X 1 - MvPolynomial.X 0)

The marked transforms on the x-chart.

theorem Hironaka.Examples.Example106Charts.empty_example106_x (a b c d : ℚ) : ¬Ideal.span {MvPolynomial.X 0 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 0 * (MvPolynomial.X 0 + MvPolynomial.X 2 ^ 2 - MvPolynomial.X 3 ^ 3)} ≤ Ideal.span {MvPolynomial.X 0 - MvPolynomial.C a, MvPolynomial.X 1 - MvPolynomial.C b, MvPolynomial.X 2 - MvPolynomial.C c, MvPolynomial.X 3 - MvPolynomial.C d} ^ 2

No point of order 2 on the x-chart: ∂(x₁ − y₁²)/∂x₁ = 1.

theorem Hironaka.Examples.Example106Charts.sup_example106_x_E : Ideal.span {MvPolynomial.X 0 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 0 * (MvPolynomial.X 0 + MvPolynomial.X 2 ^ 2 - MvPolynomial.X 3 ^ 3)} ⊔ Ideal.span {MvPolynomial.X 0} = Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1 ^ 2}

Kollár's "I₁|_{E₁} = (x₁, y₁²)": I₁ + (x₁) = (x₁, y₁²).

The y-chart

theorem Hironaka.Examples.Example106Charts.transform_example106_y : (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 1, MvPolynomial.X 1, MvPolynomial.X 2 * MvPolynomial.X 1, MvPolynomial.X 3 * MvPolynomial.X 1]) (MvPolynomial.X 0 ^ 3 - MvPolynomial.X 1 ^ 2) = MvPolynomial.X 1 ^ 2 * (MvPolynomial.X 0 ^ 3 * MvPolynomial.X 1 - 1) ∧ (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 1, MvPolynomial.X 1, MvPolynomial.X 2 * MvPolynomial.X 1, MvPolynomial.X 3 * MvPolynomial.X 1]) (MvPolynomial.X 0 ^ 4 + MvPolynomial.X 0 * MvPolynomial.X 2 ^ 2 - MvPolynomial.X 3 ^ 3) = MvPolynomial.X 1 ^ 2 * (MvPolynomial.X 1 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 1 + MvPolynomial.X 0 * MvPolynomial.X 2 ^ 2 - MvPolynomial.X 3 ^ 3))

The marked transforms on the y-chart.

theorem Hironaka.Examples.Example106Charts.empty_example106_y (a b c d : ℚ) : ¬Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 1 - 1, MvPolynomial.X 1 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 1 + MvPolynomial.X 0 * MvPolynomial.X 2 ^ 2 - MvPolynomial.X 3 ^ 3)} ≤ Ideal.span {MvPolynomial.X 0 - MvPolynomial.C a, MvPolynomial.X 1 - MvPolynomial.C b, MvPolynomial.X 2 - MvPolynomial.C c, MvPolynomial.X 3 - MvPolynomial.C d} ^ 2

No point of order 2 on the y-chart: x₁³y₁ − 1 and its x₁-partial 3x₁²y₁ cannot both vanish.

The z-chart: the point of order 2

theorem Hironaka.Examples.Example106Charts.transform_example106_z : (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 2, MvPolynomial.X 1 * MvPolynomial.X 2, MvPolynomial.X 2, MvPolynomial.X 3 * MvPolynomial.X 2]) (MvPolynomial.X 0 ^ 3 - MvPolynomial.X 1 ^ 2) = MvPolynomial.X 2 ^ 2 * (MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 - MvPolynomial.X 1 ^ 2) ∧ (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 2, MvPolynomial.X 1 * MvPolynomial.X 2, MvPolynomial.X 2, MvPolynomial.X 3 * MvPolynomial.X 2]) (MvPolynomial.X 0 ^ 4 + MvPolynomial.X 0 * MvPolynomial.X 2 ^ 2 - MvPolynomial.X 3 ^ 3) = MvPolynomial.X 2 ^ 2 * (MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 3)) ∧ (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 2, MvPolynomial.X 1 * MvPolynomial.X 2, MvPolynomial.X 2, MvPolynomial.X 3 * MvPolynomial.X 2]) (MvPolynomial.X 1) = MvPolynomial.X 2 * MvPolynomial.X 1 ∧ (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 2, MvPolynomial.X 1 * MvPolynomial.X 2, MvPolynomial.X 2, MvPolynomial.X 3 * MvPolynomial.X 2]) (MvPolynomial.X 1 - MvPolynomial.X 0 ^ 2) = MvPolynomial.X 2 * (MvPolynomial.X 1 - MvPolynomial.X 0 ^ 2 * MvPolynomial.X 2)

The marked transforms on the z-chart and the strict transforms of H, H'.

theorem Hironaka.Examples.Example106Charts.ord_zero_example106_z : Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 3)} ≤ Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1, MvPolynomial.X 2, MvPolynomial.X 3} ^ 2 ∧ ¬Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 3)} ≤ Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1, MvPolynomial.X 2, MvPolynomial.X 3} ^ 3

ord_q I₁ = 2: I₁ has order exactly 2 at the origin of the z-chart.

theorem Hironaka.Examples.Example106Charts.cosupport_example106_z (a b c d : ℚ) (h : Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 3)} ≤ Ideal.span {MvPolynomial.X 0 - MvPolynomial.C a, MvPolynomial.X 1 - MvPolynomial.C b, MvPolynomial.X 2 - MvPolynomial.C c, MvPolynomial.X 3 - MvPolynomial.C d} ^ 2) : a = 0 ∧ b = 0 ∧ c = 0 ∧ d = 0

cosupp(I₁, 2) = {q}: the only ℚ-point of order ≥ 2 on the z-chart is its origin.

theorem Hironaka.Examples.Example106Charts.mem_derivative_example106_z_H : MvPolynomial.X 1 ∈ Ideal.derivative ℚ (Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 3)})

q ∈ H₁: y₁ ∈ MC(I₁) = D(I₁), from ∂(x₁³z₁ − y₁²)/∂y₁ = −2y₁.

theorem Hironaka.Examples.Example106Charts.mem_derivative_example106_z_H' : MvPolynomial.X 1 - MvPolynomial.X 0 ^ 2 * MvPolynomial.X 2 ∈ Ideal.derivative ℚ (Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 3)})

q ∈ H₁': y₁ − x₁²z₁ ∈ MC(I₁), with ∂(x₁³z₁ − y₁²)/∂x₁ = 3x₁²z₁.

The w-chart

theorem Hironaka.Examples.Example106Charts.transform_example106_w : (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 3, MvPolynomial.X 1 * MvPolynomial.X 3, MvPolynomial.X 2 * MvPolynomial.X 3, MvPolynomial.X 3]) (MvPolynomial.X 0 ^ 3 - MvPolynomial.X 1 ^ 2) = MvPolynomial.X 3 ^ 2 * (MvPolynomial.X 0 ^ 3 * MvPolynomial.X 3 - MvPolynomial.X 1 ^ 2) ∧ (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 3, MvPolynomial.X 1 * MvPolynomial.X 3, MvPolynomial.X 2 * MvPolynomial.X 3, MvPolynomial.X 3]) (MvPolynomial.X 0 ^ 4 + MvPolynomial.X 0 * MvPolynomial.X 2 ^ 2 - MvPolynomial.X 3 ^ 3) = MvPolynomial.X 3 ^ 2 * (MvPolynomial.X 3 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 3 + MvPolynomial.X 0 * MvPolynomial.X 2 ^ 2 - 1))

The marked transforms on the w-chart.

theorem Hironaka.Examples.Example106Charts.empty_example106_w (a b c d : ℚ) : ¬Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 3 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 3 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 3 + MvPolynomial.X 0 * MvPolynomial.X 2 ^ 2 - 1)} ≤ Ideal.span {MvPolynomial.X 0 - MvPolynomial.C a, MvPolynomial.X 1 - MvPolynomial.C b, MvPolynomial.X 2 - MvPolynomial.C c, MvPolynomial.X 3 - MvPolynomial.C d} ^ 2

No point of order 2 on the w-chart: at a point of order ≥ 2, ∂(x₁³w₁ − y₁²)/∂w₁ = x₁³ forces x₁ = 0, and then ∂(w₁(x₁⁴w₁ + x₁z₁² − 1))/∂w₁ = 2x₁⁴w₁ + x₁z₁² − 1 = −1.