Kollár's Example 86.1: the birational transform of a D-balanced ideal need not be D-balanced

[Kol07, 86]: interchanging (π₀)⁻¹_* and Dⁱ on the left-hand side of the inequality of [Kol07, Theorem 76] makes it go "the wrong way", and "in general the birational transform is not D-balanced". [Kol07, Example 86.1]: the ideal (x², xyᵐ, y^{m+1}) is D-balanced, but after blowing up the origin one of the charts gives (x₁², x₁y₁^{m−1}, y₁^{m−1}), which is not.

In ℚ[x, y] with x = X 0, y = X 1:

• D(x², xyᵐ, y^{m+1}) ⊆ (x, yᵐ): every generator and every partial derivative of a generator lies in (x, yᵐ), and (x, yᵐ)² ⊆ (x², xyᵐ, y^{m+1}) since y^{2m} = y^{m−1} · y^{m+1} (isDBalanced_example86, 1 ≤ m).
• The chart x = x₁ y₁, y = y₁ is the chart ring of ℚ[x, y] with pivot y and centre (x, y) (IsLocalRing.chartRing); the marked transform of ((x², xyᵐ, y^{m+1}), 2) there is (x₁², x₁y₁^{m−1}, y₁^{m−1}) (transformIdeal_example86), by the uniqueness y₁² · J = I R' of the transformed ideal (Hironaka.Algebra.Local.Transform).
• In ℚ[x₁, y₁], x₁ ∈ D(J) (from ∂_{x₁} x₁² = 2x₁) and y₁^{m−2} ∈ D(J) (from ∂_{y₁} y₁^{m−1} = (m−1) y₁^{m−2}), so x₁ y₁^{m−2} ∈ D(J)², but x₁ y₁^{m−2} ∉ J — no generator's exponent divides (1, m−2) (not_isDBalanced_example86, 2 ≤ m).

@[reducible, inline]

noncomputable abbrev Hironaka.Balanced.example86 (m : ℕ) : Ideal (MvPolynomial (Fin 2) ℚ)

The ideal I = (x², xyᵐ, y^{m+1}) of Example 86.1.

Equations

• Hironaka.Balanced.example86 m = Ideal.span {MvPolynomial.X 0 ^ 2, MvPolynomial.X 0 * MvPolynomial.X 1 ^ m, MvPolynomial.X 1 ^ (m + 1)}

@[reducible, inline]

noncomputable abbrev Hironaka.Balanced.example86Chart (m : ℕ) : Ideal (MvPolynomial (Fin 2) ℚ)

The chart ideal J = (x₁², x₁y₁^{m−1}, y₁^{m−1}) of Example 86.1, in ℚ[x₁, y₁].

Equations

• Hironaka.Balanced.example86Chart m = Ideal.span {MvPolynomial.X 0 ^ 2, MvPolynomial.X 0 * MvPolynomial.X 1 ^ (m - 1), MvPolynomial.X 1 ^ (m - 1)}

theorem Hironaka.Balanced.x_mem_span_pair (m : ℕ) : MvPolynomial.X 0 ∈ Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1 ^ m}

theorem Hironaka.Balanced.y_pow_mem_span_pair (m : ℕ) : MvPolynomial.X 1 ^ m ∈ Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1 ^ m}

theorem Hironaka.Balanced.derivative_example86_le (m : ℕ) : Ideal.derivative ℚ (example86 m) ≤ Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1 ^ m}

D(x², xyᵐ, y^{m+1}) ⊆ (x, yᵐ): every generator and every partial derivative of a generator lies in (x, yᵐ).

theorem Hironaka.Balanced.span_pair_sq_le_example86 (m : ℕ) (hm : 1 ≤ m) : Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1 ^ m} ^ 2 ≤ example86 m

(x, yᵐ)² ⊆ (x², xyᵐ, y^{m+1}) for 1 ≤ m (y^{2m} = y^{m-1} · y^{m+1}).

theorem Hironaka.Balanced.isDBalanced_example86 (m : ℕ) (hm : 1 ≤ m) : Ideal.IsDBalanced ℚ (example86 m) 2

[Kol07, Example 86.1]: (x², xyᵐ, y^{m+1}) is D-balanced with respect to 2, for 1 ≤ m.

@[reducible, inline]

noncomputable abbrev Hironaka.Balanced.chart86 : Subalgebra (MvPolynomial (Fin 2) ℚ) (Localization.Away (MvPolynomial.X 1))

The chart ring of ℚ[x, y] with pivot y (the chart x = x₁ y₁, y = y₁ of the blow-up of the origin), IsLocalRing.chartRing.

Equations

• Hironaka.Balanced.chart86 = IsLocalRing.chartRing MvPolynomial.X 1

@[reducible, inline]

noncomputable abbrev Hironaka.Balanced.chartCoord : Fin 2 → ↥chart86

The coordinates x₁ = x / y, y₁ = y of the chart.

Equations

• Hironaka.Balanced.chartCoord = IsLocalRing.chartYR MvPolynomial.X 1

@[reducible, inline]

noncomputable abbrev Hironaka.Balanced.ybar : ↥chart86

The image ȳ of y in the chart ring.

Equations

• Hironaka.Balanced.ybar = (algebraMap (MvPolynomial (Fin 2) ℚ) ↥Hironaka.Balanced.chart86) (MvPolynomial.X 1)

theorem Hironaka.Balanced.chartCoord_one : chartCoord 1 = ybar

y₁ = y in the chart ring: the pivot coordinate is its own image.

theorem Hironaka.Balanced.algebraMap_x_eq : (algebraMap (MvPolynomial (Fin 2) ℚ) ↥chart86) (MvPolynomial.X 0) = ybar * chartCoord 0

x = y · x₁ in the chart ring.

theorem Hironaka.Balanced.transformIdeal_example86 (m : ℕ) (hm : 1 ≤ m) : IsLocalRing.transformIdeal MvPolynomial.X 1 (example86 m) 2 = Ideal.span {chartCoord 0 ^ 2, chartCoord 0 * chartCoord 1 ^ (m - 1), chartCoord 1 ^ (m - 1)}

[Kol07, Example 86.1] ("after blowing up the origin, one of the charts gives (x₁², x₁y₁^{m−1}, y₁^{m−1})"): in the chart of ℚ[x, y] with pivot y and centre (x, y), the marked transform of ((x², xyᵐ, y^{m+1}), 2) is (x₁², x₁y₁^{m−1}, y₁^{m−1}), for 1 ≤ m — by the uniqueness y₁² · J = I R' of the transformed ideal.

theorem Hironaka.Balanced.x_mem_derivative_example86Chart (m : ℕ) : MvPolynomial.X 0 ∈ Ideal.derivative ℚ (example86Chart m)

x₁ ∈ D(J), from ∂_{x₁} x₁² = 2 x₁.

theorem Hironaka.Balanced.y_pow_mem_derivative_example86Chart (m : ℕ) (hm : 2 ≤ m) : MvPolynomial.X 1 ^ (m - 2) ∈ Ideal.derivative ℚ (example86Chart m)

y₁^{m−2} ∈ D(J) for 2 ≤ m, from ∂_{y₁} y₁^{m−1} = (m−1) y₁^{m−2}.

theorem Hironaka.Balanced.not_mem_example86Chart (m : ℕ) (hm : 2 ≤ m) : MvPolynomial.X 0 * MvPolynomial.X 1 ^ (m - 2) ∉ example86Chart m

x₁ y₁^{m−2} ∉ (x₁², x₁y₁^{m−1}, y₁^{m−1}) for 2 ≤ m: no generator divides it.

theorem Hironaka.Balanced.not_isDBalanced_example86 (m : ℕ) (hm : 2 ≤ m) : ¬Ideal.IsDBalanced ℚ (example86Chart m) 2

[Kol07, Example 86.1] ("which is not D-balanced"; the remark of [Kol07, 86]): the chart ideal (x₁², x₁y₁^{m−1}, y₁^{m−1}) is not D-balanced with respect to 2, for 2 ≤ m.