Documentation

HironakaExamples.Balanced.Example11

Kollár's Example 11: the tuned ideal of `I = (x² + y³ − z⁶)` #

[Kol07, Example 11] resolves S := (x² + y³ − z⁶ = 0) ⊂ 𝔸³ through the hypersurface H := (x = 0) and the trace S ∩ H = (y³ − z⁶ = 0) ⊂ 𝔸², which has multiplicity 3 although "we came from a multiplicity 2 situation". The tuning step of the order reduction on this example, computed exactly in ℚ[x, y, z]:

D(I) = (x, y², z⁵) — the partial derivatives of x² + y³ − z⁶ are 2x, 3y², −6z⁵ (derivative_example11, by derivative_span_pderiv);
the tuned ideal W(I) = W_2(I) = I + D(I)² = (x², xy², xz⁵, y⁴, y²z⁵, y³z⁴, z⁶ − y³) (tuned_example11): the six products of x, y², z⁵ are generators except z¹⁰ = z⁴(z⁶ − y³) + y³z⁴, and conversely y³z⁴ = z⁴(x² + y³ − z⁶) − x²z⁴ + z¹⁰, z⁶ − y³ = x² − (x² + y³ − z⁶);
I and W(I) have order exactly 2 at the origin (ord_zero_example11, ord_zero_tuned_example11): both lie in 𝔪₀², and x² ∉ 𝔪₀³ (two partial derivatives and the evaluation at 0);
the order-2 locus V(D(I)) has the origin as its only ℚ-point (cosupport_example11), 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_example11, not_mcInvariant_example11): x·x ∈ D(I)², but x² ∉ I — at the point (1, 0, 1), a zero of x² + y³ − z⁶, x² evaluates to 1;
the restrictions of W(I) to H = (x = 0) and to H' = (x + y² = 0) — the images under x ↦ 0 and x ↦ −y² into ℚ[y, z] — are both (y⁴, y²z⁵, y³z⁴, z⁶ − y³) (map_tuned_example11_H, map_tuned_example11_H'), and that ideal's order-2 locus has the origin as its only ℚ-point (cosupport_tuned_example11_H: −3y² and 6z⁵ are among its partial derivatives).

@[reducible, inline]

noncomputable abbrev Hironaka.Examples.Example11.I11 :

Ideal (MvPolynomial (Fin 3) ℚ)

Kollár's I = (x² + y³ − z⁶).

Equations

Hironaka.Examples.Example11.I11 = Ideal.span {MvPolynomial.X 0 ^ 2 + MvPolynomial.X 1 ^ 3 - MvPolynomial.X 2 ^ 6}

Instances For

@[reducible, inline]

noncomputable abbrev Hironaka.Examples.Example11.D11 :

Ideal (MvPolynomial (Fin 3) ℚ)

D(I) = (x, y², z⁵).

Equations

Hironaka.Examples.Example11.D11 = Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1 ^ 2, MvPolynomial.X 2 ^ 5}

Instances For

@[reducible, inline]

noncomputable abbrev Hironaka.Examples.Example11.T11 :

Ideal (MvPolynomial (Fin 3) ℚ)

The tuned ideal W(I) = (x², xy², xz⁵, y⁴, y²z⁵, y³z⁴, z⁶ − y³).

Equations

One or more equations did not get rendered due to their size.

Instances For

@[reducible, inline]

noncomputable abbrev Hironaka.Examples.Example11.m0 :

Ideal (MvPolynomial (Fin 3) ℚ)

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

Equations

Hironaka.Examples.Example11.m0 = Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1, MvPolynomial.X 2}

Instances For

theorem Hironaka.Examples.Example11.pderiv_zero_ex11 :

(MvPolynomial.pderiv 0) (MvPolynomial.X 0 ^ 2 + MvPolynomial.X 1 ^ 3 - MvPolynomial.X 2 ^ 6) = MvPolynomial.C 2 * MvPolynomial.X 0

theorem Hironaka.Examples.Example11.pderiv_one_ex11 :

(MvPolynomial.pderiv 1) (MvPolynomial.X 0 ^ 2 + MvPolynomial.X 1 ^ 3 - MvPolynomial.X 2 ^ 6) = MvPolynomial.C 3 * MvPolynomial.X 1 ^ 2

theorem Hironaka.Examples.Example11.pderiv_two_ex11 :

(MvPolynomial.pderiv 2) (MvPolynomial.X 0 ^ 2 + MvPolynomial.X 1 ^ 3 - MvPolynomial.X 2 ^ 6) = -(MvPolynomial.C 6 * MvPolynomial.X 2 ^ 5)

theorem Hironaka.Examples.Example11.x_mem_D11 :

MvPolynomial.X 0 ∈ D11

theorem Hironaka.Examples.Example11.y_sq_mem_D11 :

MvPolynomial.X 1 ^ 2 ∈ D11

theorem Hironaka.Examples.Example11.z_five_mem_D11 :

MvPolynomial.X 2 ^ 5 ∈ D11

theorem Hironaka.Examples.Example11.derivative_example11 :

Ideal.derivative ℚ I11 = D11

D(x² + y³ − z⁶) = (x, y², z⁵).

theorem Hironaka.Examples.Example11.x_sq_mem_T11 :

MvPolynomial.X 0 ^ 2 ∈ T11

theorem Hironaka.Examples.Example11.xy_sq_mem_T11 :

MvPolynomial.X 0 * MvPolynomial.X 1 ^ 2 ∈ T11

theorem Hironaka.Examples.Example11.xz_five_mem_T11 :

MvPolynomial.X 0 * MvPolynomial.X 2 ^ 5 ∈ T11

theorem Hironaka.Examples.Example11.y_four_mem_T11 :

MvPolynomial.X 1 ^ 4 ∈ T11

theorem Hironaka.Examples.Example11.y_sq_z_five_mem_T11 :

MvPolynomial.X 1 ^ 2 * MvPolynomial.X 2 ^ 5 ∈ T11

theorem Hironaka.Examples.Example11.y_cube_z_four_mem_T11 :

MvPolynomial.X 1 ^ 3 * MvPolynomial.X 2 ^ 4 ∈ T11

theorem Hironaka.Examples.Example11.z_six_sub_mem_T11 :

MvPolynomial.X 2 ^ 6 - MvPolynomial.X 1 ^ 3 ∈ T11

theorem Hironaka.Examples.Example11.z_ten_mem_T11 :

MvPolynomial.X 2 ^ 10 ∈ T11

z¹⁰ = z⁴(z⁶ − y³) + y³z⁴ ∈ W(I).

theorem Hironaka.Examples.Example11.D11_sq_le_T11 :

D11 ^ 2 ≤ T11

(x, y², z⁵)² ⊆ W(I).

theorem Hironaka.Examples.Example11.tuned_example11 :

I11 ⊔ Ideal.derivative ℚ I11 ^ 2 = T11

W(I) = I + D(I)² = (x², xy², xz⁵, y⁴, y²z⁵, y³z⁴, z⁶ − y³).

theorem Hironaka.Examples.Example11.x_sq_notMem_m0_cube :

MvPolynomial.X 0 ^ 2 ∉ m0 ^ 3

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

theorem Hironaka.Examples.Example11.ord_zero_example11 :

I11 ≤ m0 ^ 2 ∧ ¬I11 ≤ m0 ^ 3

I = (x² + y³ − z⁶) has order exactly 2 at the origin.

theorem Hironaka.Examples.Example11.T11_le_m0_sq :

W(I) ⊆ 𝔪₀²: every generator has degree ≥ 2.

theorem Hironaka.Examples.Example11.ord_zero_tuned_example11 :

T11 ≤ m0 ^ 2 ∧ ¬T11 ≤ m0 ^ 3

The tuned ideal W(I) has order exactly 2 at the origin.

theorem Hironaka.Examples.Example11.cosupport_example11 (a b c : ℚ) (h : ∀ g ∈ Ideal.derivative ℚ I11, (MvPolynomial.eval ![a, b, c]) g = 0) :

a = 0 ∧ b = 0 ∧ c = 0

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

theorem Hironaka.Examples.Example11.x_sq_notMem_I11 :

MvPolynomial.X 0 ^ 2 ∉ I11

x² ∉ I: at (1, 0, 1), a zero of x² + y³ − z⁶, x² evaluates to 1.

theorem Hironaka.Examples.Example11.not_isDBalanced_example11 :

¬Ideal.IsDBalanced ℚ I11 2

I is not D-balanced with respect to 2.

theorem Hironaka.Examples.Example11.not_mcInvariant_example11 :

¬Ideal.derivative ℚ I11 * Ideal.derivative ℚ I11 ≤ I11

I is not MC-invariant with respect to 2.

@[reducible, inline]

noncomputable abbrev Hironaka.Examples.Example11.TH11 :

Ideal (MvPolynomial (Fin 2) ℚ)

The common restriction (y⁴, y²z⁵, y³z⁴, z⁶ − y³) in ℚ[y, z] (y = X 0, z = X 1).

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Hironaka.Examples.Example11.map_tuned_example11_H :

Ideal.map (MvPolynomial.aeval ![0, MvPolynomial.X 0, MvPolynomial.X 1]) T11 = TH11

W(I)|_H for H = (x = 0) is (y⁴, y²z⁵, y³z⁴, z⁶ − y³).

theorem Hironaka.Examples.Example11.map_tuned_example11_H' :

Ideal.map (MvPolynomial.aeval ![-MvPolynomial.X 0 ^ 2, MvPolynomial.X 0, MvPolynomial.X 1]) T11 = TH11

W(I)|_{H'} for H' = (x + y² = 0) is the same ideal (y⁴, y²z⁵, y³z⁴, z⁶ − y³): x ↦ −y² sends x² ↦ y⁴, xy² ↦ −y⁴, xz⁵ ↦ −y²z⁵.

theorem Hironaka.Examples.Example11.cosupport_tuned_example11_H (b c : ℚ) (h : ∀ g ∈ Ideal.derivative ℚ TH11, (MvPolynomial.eval ![b, c]) g = 0) :

b = 0 ∧ c = 0

The order-2 locus of (y⁴, y²z⁵, y³z⁴, z⁶ − y³) has the origin as its only ℚ-point: −3y² and 6z⁵ are partial derivatives of z⁶ − y³.