Kollár's Example 106: the tuned ideal of I = (x³ − y², x⁴ + xz² − w³)

[Kol07, Example 106] considers the subvariety X ⊂ 𝔸⁴ defined by the ideal I = (x³ − y², x⁴ + xz² − w³) and notes that ord I = 2 and that "H = (y = 0) is a hypersurface of maximal contact". The tuning step of the order reduction on this example, computed exactly in ℚ[x, y, z, w]:

• D(I) = (x², y, z², xz, w²) — the partial derivatives of x³ − y² are 3x², −2y, 0, 0, those of x⁴ + xz² − w³ are 4x³ + z², 0, 2xz, −3w², and x³ ∈ (x²) (derivative_example106);
• I and the tuned ideal W(I) = I + D(I)² have order exactly 2 at the origin (ord_zero_example106, ord_zero_tuned_example106): I ⊆ 𝔪₀², D(I) ⊆ 𝔪₀, and y² ∉ 𝔪₀³;
• the order-2 locus V(D(I)) has the origin as its only ℚ-point (cosupport_example106), and it is also cosupp(W(I), 2) since D(W(I)) = D(I) (derivative_sup_derivative_sq);
• I itself is neither D-balanced nor MC-invariant with respect to 2 (not_isDBalanced_example106, not_mcInvariant_example106): y·y ∈ D(I)², but y² ∉ I — at the point (1, 1, 0, 1), a common zero of the generators, y² evaluates to 1.

The D-balance and MC-invariance of W(I) are the general facts isDBalanced_sup_derivative_sq and mcInvariant_sup_derivative_sq of HironakaExamples.Balanced.Tuned; no explicit generators of this W(I) are computed.

@[reducible, inline]

noncomputable abbrev Hironaka.Examples.Example106.I106 : Ideal (MvPolynomial (Fin 4) ℚ)

Kollár's I = (x³ − y², x⁴ + xz² − w³).

Equations

• Hironaka.Examples.Example106.I106 = 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}

@[reducible, inline]

noncomputable abbrev Hironaka.Examples.Example106.D106 : Ideal (MvPolynomial (Fin 4) ℚ)

D(I) = (x², y, z², xz, w²).

Equations

• Hironaka.Examples.Example106.D106 = Ideal.span {MvPolynomial.X 0 ^ 2, MvPolynomial.X 1, MvPolynomial.X 2 ^ 2, MvPolynomial.X 0 * MvPolynomial.X 2, MvPolynomial.X 3 ^ 2}

@[reducible, inline]

noncomputable abbrev Hironaka.Examples.Example106.m0 : Ideal (MvPolynomial (Fin 4) ℚ)

The maximal ideal of the origin, 𝔪₀ = (x, y, z, w).

Equations

• Hironaka.Examples.Example106.m0 = Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1, MvPolynomial.X 2, MvPolynomial.X 3}

theorem Hironaka.Examples.Example106.pderiv_zero_gen1 : (MvPolynomial.pderiv 0) (MvPolynomial.X 0 ^ 3 - MvPolynomial.X 1 ^ 2) = MvPolynomial.C 3 * MvPolynomial.X 0 ^ 2

theorem Hironaka.Examples.Example106.pderiv_one_gen1 : (MvPolynomial.pderiv 1) (MvPolynomial.X 0 ^ 3 - MvPolynomial.X 1 ^ 2) = -(MvPolynomial.C 2 * MvPolynomial.X 1)

theorem Hironaka.Examples.Example106.pderiv_two_gen1 : (MvPolynomial.pderiv 2) (MvPolynomial.X 0 ^ 3 - MvPolynomial.X 1 ^ 2) = 0

theorem Hironaka.Examples.Example106.pderiv_three_gen1 : (MvPolynomial.pderiv 3) (MvPolynomial.X 0 ^ 3 - MvPolynomial.X 1 ^ 2) = 0

theorem Hironaka.Examples.Example106.pderiv_zero_gen2 : (MvPolynomial.pderiv 0) (MvPolynomial.X 0 ^ 4 + MvPolynomial.X 0 * MvPolynomial.X 2 ^ 2 - MvPolynomial.X 3 ^ 3) = MvPolynomial.C 4 * MvPolynomial.X 0 ^ 3 + MvPolynomial.X 2 ^ 2

theorem Hironaka.Examples.Example106.pderiv_one_gen2 : (MvPolynomial.pderiv 1) (MvPolynomial.X 0 ^ 4 + MvPolynomial.X 0 * MvPolynomial.X 2 ^ 2 - MvPolynomial.X 3 ^ 3) = 0

theorem Hironaka.Examples.Example106.pderiv_two_gen2 : (MvPolynomial.pderiv 2) (MvPolynomial.X 0 ^ 4 + MvPolynomial.X 0 * MvPolynomial.X 2 ^ 2 - MvPolynomial.X 3 ^ 3) = MvPolynomial.C 2 * (MvPolynomial.X 0 * MvPolynomial.X 2)

theorem Hironaka.Examples.Example106.pderiv_three_gen2 : (MvPolynomial.pderiv 3) (MvPolynomial.X 0 ^ 4 + MvPolynomial.X 0 * MvPolynomial.X 2 ^ 2 - MvPolynomial.X 3 ^ 3) = -(MvPolynomial.C 3 * MvPolynomial.X 3 ^ 2)

theorem Hironaka.Examples.Example106.x_sq_mem_D106 : MvPolynomial.X 0 ^ 2 ∈ D106

theorem Hironaka.Examples.Example106.y_mem_D106 : MvPolynomial.X 1 ∈ D106

theorem Hironaka.Examples.Example106.z_sq_mem_D106 : MvPolynomial.X 2 ^ 2 ∈ D106

theorem Hironaka.Examples.Example106.xz_mem_D106 : MvPolynomial.X 0 * MvPolynomial.X 2 ∈ D106

theorem Hironaka.Examples.Example106.w_sq_mem_D106 : MvPolynomial.X 3 ^ 2 ∈ D106

theorem Hironaka.Examples.Example106.derivative_example106 : Ideal.derivative ℚ I106 = D106

D(x³ − y², x⁴ + xz² − w³) = (x², y, z², xz, w²).

theorem Hironaka.Examples.Example106.x_mem_m0_ex106 : MvPolynomial.X 0 ∈ m0

theorem Hironaka.Examples.Example106.y_mem_m0_ex106 : MvPolynomial.X 1 ∈ m0

theorem Hironaka.Examples.Example106.z_mem_m0_ex106 : MvPolynomial.X 2 ∈ m0

theorem Hironaka.Examples.Example106.w_mem_m0_ex106 : MvPolynomial.X 3 ∈ m0

theorem Hironaka.Examples.Example106.y_sq_notMem_m0_cube : MvPolynomial.X 1 ^ 2 ∉ m0 ^ 3

y² ∉ 𝔪₀³: differentiate twice in y and evaluate at the origin.

theorem Hironaka.Examples.Example106.I106_le_m0_sq : I106 ≤ m0 ^ 2

I ⊆ 𝔪₀².

theorem Hironaka.Examples.Example106.y_sq_mem_tuned : MvPolynomial.X 1 ^ 2 ∈ I106 ⊔ Ideal.derivative ℚ I106 ^ 2

y² ∈ I + D(I)².

theorem Hironaka.Examples.Example106.ord_zero_example106 : I106 ≤ m0 ^ 2 ∧ ¬I106 ≤ m0 ^ 3

Kollár's "ord I = 2": I has order exactly 2 at the origin — y² ≡ x³ modulo I and y² ∉ 𝔪₀³.

theorem Hironaka.Examples.Example106.D106_le_m0 : D106 ≤ m0

D(I) ⊆ 𝔪₀.

theorem Hironaka.Examples.Example106.ord_zero_tuned_example106 : I106 ⊔ Ideal.derivative ℚ I106 ^ 2 ≤ m0 ^ 2 ∧ ¬I106 ⊔ Ideal.derivative ℚ I106 ^ 2 ≤ m0 ^ 3

The tuned ideal W(I) = I + D(I)² has order exactly 2 at the origin.

theorem Hironaka.Examples.Example106.cosupport_example106 (a b c d : ℚ) (h : ∀ g ∈ Ideal.derivative ℚ I106, (MvPolynomial.eval ![a, b, c, d]) g = 0) : a = 0 ∧ b = 0 ∧ c = 0 ∧ d = 0

cosupp(I, 2) = V(D(I)) has the origin as its only ℚ-point.

theorem Hironaka.Examples.Example106.y_sq_notMem_I106 : MvPolynomial.X 1 ^ 2 ∉ I106

y² ∉ I: at (1, 1, 0, 1), a common zero of x³ − y² and x⁴ + xz² − w³, y² evaluates to 1.

theorem Hironaka.Examples.Example106.not_isDBalanced_example106 : ¬Ideal.IsDBalanced ℚ I106 2

I is not D-balanced with respect to 2.

theorem Hironaka.Examples.Example106.not_mcInvariant_example106 : ¬Ideal.derivative ℚ I106 * Ideal.derivative ℚ I106 ≤ I106

I is not MC-invariant with respect to 2.