The derivative ideal under one blow-up: the cusp x² + y³

For X = 𝔸², I = (x² + y³), m = 2, the blow-up of the origin and j = 1 (a plane-curve instance in the spirit of [Kol07, Example 11]): D(I) = (x, y²); in the chart x = x₁ y₁, y = y₁ of the blow-up, I₁ = π_*^{-1}(I, 2) = (x₁² + y₁), J₁ = π_*^{-1}(D(I), 1) = (x₁, y₁), and D(I₁) = (x₁² + y₁, x₁, 1) = (1); so J₁ ⊆ D(I₁), which is [Kol07, Theorem 76] (Π_*^{-1}(D^j(I, m)) ⊆ D^j Π_*^{-1}(I, m)) for one blow-up and j = 1, and the inclusion is strict.

The computation is done on the local model of the blow-up at the origin: R a regular local ℚ-algebra with a two-dimensional coordinate system c (x₀ = x, x₁ = y), the center P = chartCenter c.x 1 = (x₀, x₁), the chart ring R' = R[x₀/x₁] of the coordinate x₁ (y₀ = x₀/x₁ is Kollár's x₁, and x₁ his y₁), the coordinate derivative c.D on R and the derivative c.chartD 1 of the chart with respect to the transformed derivations ∂'ⱼ. The transform π_*^{-1}(x₀² + x₁³, 2) = y₀² + x₁ is transformElem_sq_add_cube.

theorem Hironaka.Local.Examples.DerivativeSequence.pderiv_zero_sq_add_cube {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] (c : IsLocalRing.RegularCoords R 2) : (c.pderiv 0) (c.x 0 ^ 2 + c.x 1 ^ 3) = 2 * c.x 0

∂₀(x₀² + x₁³) = 2 x₀.

theorem Hironaka.Local.Examples.DerivativeSequence.pderiv_one_sq_add_cube {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] (c : IsLocalRing.RegularCoords R 2) : (c.pderiv 1) (c.x 0 ^ 2 + c.x 1 ^ 3) = 3 * c.x 1 ^ 2

∂₁(x₀² + x₁³) = 3 x₁².

theorem Hironaka.Local.Examples.DerivativeSequence.pderiv_sq_add_cube_mem {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] (c : IsLocalRing.RegularCoords R 2) (i : Fin 2) : (c.pderiv i) (c.x 0 ^ 2 + c.x 1 ^ 3) ∈ Ideal.span {c.x 0, c.x 1 ^ 2}

∂ᵢ(x₀² + x₁³) ∈ (x₀, x₁²) for both coordinates.

theorem Hironaka.Local.Examples.DerivativeSequence.sq_add_cube_mem {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] (c : IsLocalRing.RegularCoords R 2) : c.x 0 ^ 2 + c.x 1 ^ 3 ∈ Ideal.span {c.x 0, c.x 1 ^ 2}

x₀² + x₁³ ∈ (x₀, x₁²).

theorem Hironaka.Local.Examples.DerivativeSequence.D_sq_add_cube {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] (c : IsLocalRing.RegularCoords R 2) : c.D (Ideal.span {c.x 0 ^ 2 + c.x 1 ^ 3}) = Ideal.span {c.x 0, c.x 1 ^ 2}

D(x² + y³) = (x, y²) (characteristic zero: 2 and 3 are units).

theorem Hironaka.Local.Examples.DerivativeSequence.x_zero_mem_chartCenter {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] (c : IsLocalRing.RegularCoords R 2) : c.x 0 ∈ IsLocalRing.chartCenter c.x 1

x₀ ∈ P and x₁² ∈ P.

theorem Hironaka.Local.Examples.DerivativeSequence.x_one_sq_mem_chartCenter {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] (c : IsLocalRing.RegularCoords R 2) : c.x 1 ^ 2 ∈ IsLocalRing.chartCenter c.x 1

theorem Hironaka.Local.Examples.DerivativeSequence.transformElem_x_zero {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] (c : IsLocalRing.RegularCoords R 2) : IsLocalRing.transformElem c.x 1 (c.x 0) ⋯ = IsLocalRing.chartYR c.x 1 0

π_*^{-1}(x₀, 1) = y₀.

theorem Hironaka.Local.Examples.DerivativeSequence.transformElem_x_one_sq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] (c : IsLocalRing.RegularCoords R 2) : IsLocalRing.transformElem c.x 1 (c.x 1 ^ 2) ⋯ = (algebraMap R ↥(IsLocalRing.chartRing c.x 1)) (c.x 1)

π_*^{-1}(x₁², 1) = x₁.

theorem Hironaka.Local.Examples.DerivativeSequence.transformIdeal_D_sq_add_cube {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] (c : IsLocalRing.RegularCoords R 2) : IsLocalRing.transformIdeal c.x 1 (Ideal.span {c.x 0, c.x 1 ^ 2}) 1 = Ideal.span {IsLocalRing.chartYR c.x 1 0, (algebraMap R ↥(IsLocalRing.chartRing c.x 1)) (c.x 1)}

J₁ = π_*^{-1}((x, y²), 1) = (x₁, y₁); in the model, (y₀, x₁).

theorem Hironaka.Local.Examples.DerivativeSequence.transformIdeal_sq_add_cube {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] (c : IsLocalRing.RegularCoords R 2) : IsLocalRing.transformIdeal c.x 1 (Ideal.span {c.x 0 ^ 2 + c.x 1 ^ 3}) 2 = Ideal.span {IsLocalRing.chartYR c.x 1 0 ^ 2 + (algebraMap R ↥(IsLocalRing.chartRing c.x 1)) (c.x 1)}

I₁ = π_*^{-1}((x² + y³), 2) = (x₁² + y₁); in the model, (y₀² + x₁).

theorem Hironaka.Local.Examples.DerivativeSequence.chartDerivRing_one_transform {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] (c : IsLocalRing.RegularCoords R 2) : (c.chartDerivRing 1 1) (IsLocalRing.chartYR c.x 1 0 ^ 2 + (algebraMap R ↥(IsLocalRing.chartRing c.x 1)) (c.x 1)) = 1

∂'₁(y₀² + x₁) = 1 in the chart ring.

theorem Hironaka.Local.Examples.DerivativeSequence.chartD_transform_sq_add_cube {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] (c : IsLocalRing.RegularCoords R 2) : c.chartD 1 (Ideal.span {IsLocalRing.chartYR c.x 1 0 ^ 2 + (algebraMap R ↥(IsLocalRing.chartRing c.x 1)) (c.x 1)}) = ⊤

D'(I₁) = (x₁² + y₁, x₁, 1) = (1).

theorem Hironaka.Local.Examples.DerivativeSequence.span_transform_ne_top {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] (c : IsLocalRing.RegularCoords R 2) : Ideal.span {IsLocalRing.chartYR c.x 1 0, (algebraMap R ↥(IsLocalRing.chartRing c.x 1)) (c.x 1)} ≠ ⊤

J₁ = (y₀, x₁) is a proper ideal: it lies in the origin of the chart.