Kollár's Example 52.2: I + D(I)² for the double point I = (xy − zⁿ)

[Kol07, Example 52.2] starts with the double point ideal I = (xy − zⁿ): restricting to S = (x = 0) gives an n-fold line, and blowing up this line "is not an order 2 blow-up for I"; the ideal I + D(I)² = (xy, x², y², xz^{n−1}, yz^{n−1}, zⁿ) is D-balanced, and its restriction to (x = 0) is (y², yz^{n−1}, zⁿ).

In ℚ[x, y, z] with x = X 0, y = X 1, z = X 2 and 2 ≤ n:

• D(I) = (x, y, z^{n−1}) — the partial derivatives of xy − zⁿ are y, x, −n z^{n−1} (derivative_example52);
• I + D(I)² = (xy, x², y², xz^{n−1}, yz^{n−1}, zⁿ) (example52_eq): zⁿ = xy − (xy − zⁿ) and z^{2n−2} = z^{n−2} · zⁿ;
• D(I + D(I)²) ⊆ (x, y, z^{n−1}) and (x, y, z^{n−1})² ⊆ I + D(I)², so I + D(I)² is D-balanced with respect to 2 (isDBalanced_example52);
• the image under x ↦ 0, y ↦ y, z ↦ z is (y², yz^{n−1}, zⁿ) (map_example52).

@[reducible, inline]

noncomputable abbrev Hironaka.Balanced.example52 (n : ℕ) : Ideal (MvPolynomial (Fin 3) ℚ)

The double point ideal I = (xy − zⁿ) of Example 52.2.

Equations

• Hironaka.Balanced.example52 n = Ideal.span {MvPolynomial.X 0 * MvPolynomial.X 1 - MvPolynomial.X 2 ^ n}

@[reducible, inline]

noncomputable abbrev Hironaka.Balanced.example52D (n : ℕ) : Ideal (MvPolynomial (Fin 3) ℚ)

The ideal (x, y, z^{n−1}) = D(I).

Equations

• Hironaka.Balanced.example52D n = Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1, MvPolynomial.X 2 ^ (n - 1)}

@[reducible, inline]

noncomputable abbrev Hironaka.Balanced.example52T (n : ℕ) : Ideal (MvPolynomial (Fin 3) ℚ)

Kollár's I + D(I)² = (xy, x², y², xz^{n−1}, yz^{n−1}, zⁿ).

Equations

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

theorem Hironaka.Balanced.x_mem_D (n : ℕ) : MvPolynomial.X 0 ∈ example52D n

theorem Hironaka.Balanced.y_mem_D (n : ℕ) : MvPolynomial.X 1 ∈ example52D n

theorem Hironaka.Balanced.z_pow_mem_D (n : ℕ) : MvPolynomial.X 2 ^ (n - 1) ∈ example52D n

theorem Hironaka.Balanced.pderiv_zero_gen (n : ℕ) : (MvPolynomial.pderiv 0) (MvPolynomial.X 0 * MvPolynomial.X 1 - MvPolynomial.X 2 ^ n) = MvPolynomial.X 1

theorem Hironaka.Balanced.pderiv_one_gen (n : ℕ) : (MvPolynomial.pderiv 1) (MvPolynomial.X 0 * MvPolynomial.X 1 - MvPolynomial.X 2 ^ n) = MvPolynomial.X 0

theorem Hironaka.Balanced.pderiv_two_gen (n : ℕ) : (MvPolynomial.pderiv 2) (MvPolynomial.X 0 * MvPolynomial.X 1 - MvPolynomial.X 2 ^ n) = -(↑n * MvPolynomial.X 2 ^ (n - 1))

theorem Hironaka.Balanced.derivative_example52 (n : ℕ) (hn : 2 ≤ n) : Ideal.derivative ℚ (example52 n) = example52D n

The derivative in [Kol07, Example 52.2]: D(xy − zⁿ) = (x, y, z^{n−1}) for 2 ≤ n (also [Kol07, Example 82]: "D(I) = (x, y, z^{n−1})").

theorem Hironaka.Balanced.D_sq_le_T (n : ℕ) (hn : 2 ≤ n) : example52D n ^ 2 ≤ example52T n

(x, y, z^{n−1})² ⊆ (xy, x², y², xz^{n−1}, yz^{n−1}, zⁿ) for 2 ≤ n (z^{2n−2} = z^{n−2} · zⁿ).

theorem Hironaka.Balanced.example52_eq (n : ℕ) (hn : 2 ≤ n) : example52 n ⊔ Ideal.derivative ℚ (example52 n) ^ 2 = example52T n

[Kol07, Example 52.2]: I + D(I)² = (xy, x², y², xz^{n−1}, yz^{n−1}, zⁿ) for 2 ≤ n.

theorem Hironaka.Balanced.derivative_T_le (n : ℕ) (hn : 2 ≤ n) : Ideal.derivative ℚ (example52T n) ≤ example52D n

D(I + D(I)²) ⊆ (x, y, z^{n−1}) for 2 ≤ n: D(I) = (x, y, z^{n−1}) and, by the Leibniz rule, D(M²) ⊆ D(M) M + M D(M) ⊆ M (derivative_mul_le).

theorem Hironaka.Balanced.isDBalanced_example52 (n : ℕ) (hn : 2 ≤ n) : Ideal.IsDBalanced ℚ (example52 n ⊔ Ideal.derivative ℚ (example52 n) ^ 2) 2

[Kol07, Example 52.2] ("I + D(I)² … is D-balanced"): with respect to the mark 2, for 2 ≤ n.

theorem Hironaka.Balanced.map_example52 (n : ℕ) (hn : 2 ≤ n) : Ideal.map (MvPolynomial.aeval ![0, MvPolynomial.X 0, MvPolynomial.X 1]) (example52 n ⊔ Ideal.derivative ℚ (example52 n) ^ 2) = Ideal.span {MvPolynomial.X 0 ^ 2, MvPolynomial.X 0 * MvPolynomial.X 1 ^ (n - 1), MvPolynomial.X 1 ^ n}

[Kol07, Example 52.2] ("If we restrict I + D(I)² to (x = 0), we get the ideal (y², yz^{n−1}, zⁿ)"): the image under x ↦ 0, y ↦ X 0, z ↦ X 1 onto ℚ[y, z], for 2 ≤ n.