Kollár's Example 106, the order-2 run continues: the blow-ups of q and of q'

In [Kol07, Example 106], after the blow-up of the origin the transform I₁ on the z-chart, I₁ = (x₁³z₁ − y₁², z₁(x₁⁴z₁ + x₁ − w₁³)), has order 2 at the origin q ∈ E₁ of that chart (HironakaExamples/MaximalContact/Example106Charts.lean), against Kollár's sentence "the order has dropped to 1", which holds on his x-chart only. This file follows the order-2 run two stages further, computed exactly in ℚ:

• blowing up q, the x₂-, y₂- and z₂-charts have no point of order 2, while on the w₂-chart I₂ = (x₂³z₂w₂² − y₂², z₂(x₂⁴z₂w₂⁴ + x₂ − w₂²)) has order exactly 2 at its origin q', its only ℚ-point of order 2, which lies on the strict transforms H₂ = (y₂) and H₂' = (y₂ − x₂²z₂w₂²) (y₂, y₂ − x₂²z₂w₂² ∈ MC(I₂));
• blowing up q', again only the w₃-chart has a point of order 2, its origin, for I₃ = (x₃³z₃w₃⁴ − y₃², z₃(x₃⁴z₃w₃⁸ + x₃ − w₃)), inside H₃ = (y₃) and H₃' = (y₃ − x₃²z₃w₃⁴).

So the order-2 run of Example 106 continues for at least three stages; its length is not computed here. The ℚ-point arguments read the value and the first partials of the generators at the point (vanish_of_mem_m4_sq).

The blow-up of q: the x₂-, y₂-, z₂-charts are empty

theorem Hironaka.Examples.Example106Stages.transform_example106_zx : (MvPolynomial.aeval ![MvPolynomial.X 0, MvPolynomial.X 1 * MvPolynomial.X 0, MvPolynomial.X 2 * MvPolynomial.X 0, MvPolynomial.X 3 * MvPolynomial.X 0]) (MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 - MvPolynomial.X 1 ^ 2) = MvPolynomial.X 0 ^ 2 * (MvPolynomial.X 0 ^ 2 * MvPolynomial.X 2 - MvPolynomial.X 1 ^ 2) ∧ (MvPolynomial.aeval ![MvPolynomial.X 0, MvPolynomial.X 1 * MvPolynomial.X 0, MvPolynomial.X 2 * MvPolynomial.X 0, MvPolynomial.X 3 * MvPolynomial.X 0]) (MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 3)) = MvPolynomial.X 0 ^ 2 * (MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 + 1 - MvPolynomial.X 3 ^ 3 * MvPolynomial.X 0 ^ 2))

The marked transforms of the generators of I₁ on the x₂-chart.

theorem Hironaka.Examples.Example106Stages.empty_example106_zx (a b c d : ℚ) : ¬Ideal.span {MvPolynomial.X 0 ^ 2 * MvPolynomial.X 2 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 + 1 - MvPolynomial.X 3 ^ 3 * MvPolynomial.X 0 ^ 2)} ≤ Ideal.span {MvPolynomial.X 0 - MvPolynomial.C a, MvPolynomial.X 1 - MvPolynomial.C b, MvPolynomial.X 2 - MvPolynomial.C c, MvPolynomial.X 3 - MvPolynomial.C d} ^ 2

No point of order 2 on the x₂-chart: ∂(x₂²z₂ − y₂²)/∂y₂ = −2y₂ and ∂/∂z₂ = x₂² force x₂ = y₂ = 0, and then ∂(z₂(x₂⁴z₂ + 1 − w₂³x₂²))/∂z₂ = 1.

theorem Hironaka.Examples.Example106Stages.transform_example106_zy : (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 1, MvPolynomial.X 1, MvPolynomial.X 2 * MvPolynomial.X 1, MvPolynomial.X 3 * MvPolynomial.X 1]) (MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 - MvPolynomial.X 1 ^ 2) = MvPolynomial.X 1 ^ 2 * (MvPolynomial.X 0 ^ 3 * MvPolynomial.X 1 ^ 2 * MvPolynomial.X 2 - 1) ∧ (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 1, MvPolynomial.X 1, MvPolynomial.X 2 * MvPolynomial.X 1, MvPolynomial.X 3 * MvPolynomial.X 1]) (MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 3)) = MvPolynomial.X 1 ^ 2 * (MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 1 ^ 4 * MvPolynomial.X 2 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 3 * MvPolynomial.X 1 ^ 2))

The marked transforms on the y₂-chart.

theorem Hironaka.Examples.Example106Stages.empty_example106_zy (a b c d : ℚ) : ¬Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 1 ^ 2 * MvPolynomial.X 2 - 1, MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 1 ^ 4 * MvPolynomial.X 2 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 3 * MvPolynomial.X 1 ^ 2)} ≤ Ideal.span {MvPolynomial.X 0 - MvPolynomial.C a, MvPolynomial.X 1 - MvPolynomial.C b, MvPolynomial.X 2 - MvPolynomial.C c, MvPolynomial.X 3 - MvPolynomial.C d} ^ 2

No point of order 2 on the y₂-chart: x₂³y₂²z₂ = 1 and ∂/∂y₂ = 2x₂³y₂z₂ = 0 are incompatible.

theorem Hironaka.Examples.Example106Stages.transform_example106_zz : (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 2, MvPolynomial.X 1 * MvPolynomial.X 2, MvPolynomial.X 2, MvPolynomial.X 3 * MvPolynomial.X 2]) (MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 - MvPolynomial.X 1 ^ 2) = MvPolynomial.X 2 ^ 2 * (MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 ^ 2 - MvPolynomial.X 1 ^ 2) ∧ (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 2, MvPolynomial.X 1 * MvPolynomial.X 2, MvPolynomial.X 2, MvPolynomial.X 3 * MvPolynomial.X 2]) (MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 3)) = MvPolynomial.X 2 ^ 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 ^ 4 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 3 * MvPolynomial.X 2 ^ 2)

The marked transforms on the z₂-chart.

theorem Hironaka.Examples.Example106Stages.empty_example106_zz (a b c d : ℚ) : ¬Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 ^ 2 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 ^ 4 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 3 * MvPolynomial.X 2 ^ 2} ≤ Ideal.span {MvPolynomial.X 0 - MvPolynomial.C a, MvPolynomial.X 1 - MvPolynomial.C b, MvPolynomial.X 2 - MvPolynomial.C c, MvPolynomial.X 3 - MvPolynomial.C d} ^ 2

No point of order 2 on the z₂-chart: ∂(x₂⁴z₂⁴ + x₂ − w₂³z₂²)/∂x₂ = 4x₂³z₂⁴ + 1 and ∂(x₂³z₂² − y₂²)/∂z₂ = 2x₂³z₂ are incompatible.

The blow-up of q: the w₂-chart carries the point q' of order 2

theorem Hironaka.Examples.Example106Stages.transform_example106_zw : (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 3, MvPolynomial.X 1 * MvPolynomial.X 3, MvPolynomial.X 2 * MvPolynomial.X 3, MvPolynomial.X 3]) (MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 - MvPolynomial.X 1 ^ 2) = MvPolynomial.X 3 ^ 2 * (MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 2 - MvPolynomial.X 1 ^ 2) ∧ (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 3, MvPolynomial.X 1 * MvPolynomial.X 3, MvPolynomial.X 2 * MvPolynomial.X 3, MvPolynomial.X 3]) (MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 3)) = MvPolynomial.X 3 ^ 2 * (MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 2)) ∧ (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 3, MvPolynomial.X 1 * MvPolynomial.X 3, MvPolynomial.X 2 * MvPolynomial.X 3, MvPolynomial.X 3]) (MvPolynomial.X 1) = MvPolynomial.X 3 * MvPolynomial.X 1 ∧ (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 3, MvPolynomial.X 1 * MvPolynomial.X 3, MvPolynomial.X 2 * MvPolynomial.X 3, MvPolynomial.X 3]) (MvPolynomial.X 1 - MvPolynomial.X 0 ^ 2 * MvPolynomial.X 2) = MvPolynomial.X 3 * (MvPolynomial.X 1 - MvPolynomial.X 0 ^ 2 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 2)

The marked transforms on the w₂-chart and the strict transforms of H₁, H₁'.

theorem Hironaka.Examples.Example106Stages.ord_zero_example106_zw : Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 2 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 2)} ≤ Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1, MvPolynomial.X 2, MvPolynomial.X 3} ^ 2 ∧ ¬Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 2 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 2)} ≤ Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1, MvPolynomial.X 2, MvPolynomial.X 3} ^ 3

I₂ has order exactly 2 at its origin q'.

theorem Hironaka.Examples.Example106Stages.cosupport_example106_zw (a b c d : ℚ) (h : Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 2 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 2)} ≤ Ideal.span {MvPolynomial.X 0 - MvPolynomial.C a, MvPolynomial.X 1 - MvPolynomial.C b, MvPolynomial.X 2 - MvPolynomial.C c, MvPolynomial.X 3 - MvPolynomial.C d} ^ 2) : a = 0 ∧ b = 0 ∧ c = 0 ∧ d = 0

Every ℚ-point of order ≥ 2 on the w₂-chart is its origin: ∂/∂y₂ = −2y₂, ∂(x₂³z₂w₂² − y₂²)/∂z₂ = x₂³w₂², and the partials of the second generator finish the two cases x₂ = 0, w₂ = 0.

theorem Hironaka.Examples.Example106Stages.mem_derivative_example106_zw_H : MvPolynomial.X 1 ∈ Ideal.derivative ℚ (Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 2 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 2)})

q' ∈ H₂: y₂ ∈ MC(I₂).

theorem Hironaka.Examples.Example106Stages.mem_derivative_example106_zw_H' : MvPolynomial.X 1 - MvPolynomial.X 0 ^ 2 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 2 ∈ Ideal.derivative ℚ (Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 2 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 2)})

q' ∈ H₂': y₂ − x₂²z₂w₂² ∈ MC(I₂), with ∂(x₂³z₂w₂² − y₂²)/∂x₂ = 3x₂²z₂w₂².

The blow-up of q': three empty charts and the w₃-chart

theorem Hironaka.Examples.Example106Stages.transform_example106_zwx : (MvPolynomial.aeval ![MvPolynomial.X 0, MvPolynomial.X 1 * MvPolynomial.X 0, MvPolynomial.X 2 * MvPolynomial.X 0, MvPolynomial.X 3 * MvPolynomial.X 0]) (MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 2 - MvPolynomial.X 1 ^ 2) = MvPolynomial.X 0 ^ 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 2 - MvPolynomial.X 1 ^ 2) ∧ (MvPolynomial.aeval ![MvPolynomial.X 0, MvPolynomial.X 1 * MvPolynomial.X 0, MvPolynomial.X 2 * MvPolynomial.X 0, MvPolynomial.X 3 * MvPolynomial.X 0]) (MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 2)) = MvPolynomial.X 0 ^ 2 * (MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 8 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 + 1 - MvPolynomial.X 3 ^ 2 * MvPolynomial.X 0))

The marked transforms of the generators of I₂ on the x₃-chart.

theorem Hironaka.Examples.Example106Stages.empty_example106_zwx (a b c d : ℚ) : ¬Ideal.span {MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 2 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 8 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 + 1 - MvPolynomial.X 3 ^ 2 * MvPolynomial.X 0)} ≤ Ideal.span {MvPolynomial.X 0 - MvPolynomial.C a, MvPolynomial.X 1 - MvPolynomial.C b, MvPolynomial.X 2 - MvPolynomial.C c, MvPolynomial.X 3 - MvPolynomial.C d} ^ 2

No point of order 2 on the x₃-chart: ∂(x₃⁴z₃w₃² − y₃²)/∂z₃ = x₃⁴w₃² forces x₃ = 0 or w₃ = 0, and then ∂(z₃(x₃⁸z₃w₃⁴ + 1 − w₃²x₃))/∂z₃ = 1.

theorem Hironaka.Examples.Example106Stages.transform_example106_zwy : (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 1, MvPolynomial.X 1, MvPolynomial.X 2 * MvPolynomial.X 1, MvPolynomial.X 3 * MvPolynomial.X 1]) (MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 2 - MvPolynomial.X 1 ^ 2) = MvPolynomial.X 1 ^ 2 * (MvPolynomial.X 0 ^ 3 * MvPolynomial.X 1 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 2 - 1) ∧ (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 1, MvPolynomial.X 1, MvPolynomial.X 2 * MvPolynomial.X 1, MvPolynomial.X 3 * MvPolynomial.X 1]) (MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 2)) = MvPolynomial.X 1 ^ 2 * (MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 1 ^ 8 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 2 * MvPolynomial.X 1))

The marked transforms on the y₃-chart.

theorem Hironaka.Examples.Example106Stages.empty_example106_zwy (a b c d : ℚ) : ¬Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 1 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 2 - 1, MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 1 ^ 8 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 2 * MvPolynomial.X 1)} ≤ Ideal.span {MvPolynomial.X 0 - MvPolynomial.C a, MvPolynomial.X 1 - MvPolynomial.C b, MvPolynomial.X 2 - MvPolynomial.C c, MvPolynomial.X 3 - MvPolynomial.C d} ^ 2

No point of order 2 on the y₃-chart: x₃³y₃⁴z₃w₃² = 1 and ∂/∂y₃ = 4x₃³y₃³z₃w₃² = 0 are incompatible.

theorem Hironaka.Examples.Example106Stages.transform_example106_zwz : (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 2, MvPolynomial.X 1 * MvPolynomial.X 2, MvPolynomial.X 2, MvPolynomial.X 3 * MvPolynomial.X 2]) (MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 2 - MvPolynomial.X 1 ^ 2) = MvPolynomial.X 2 ^ 2 * (MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 ^ 4 * MvPolynomial.X 3 ^ 2 - MvPolynomial.X 1 ^ 2) ∧ (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 2, MvPolynomial.X 1 * MvPolynomial.X 2, MvPolynomial.X 2, MvPolynomial.X 3 * MvPolynomial.X 2]) (MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 2)) = MvPolynomial.X 2 ^ 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 ^ 8 * MvPolynomial.X 3 ^ 4 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 2 * MvPolynomial.X 2)

The marked transforms on the z₃-chart.

theorem Hironaka.Examples.Example106Stages.empty_example106_zwz (a b c d : ℚ) : ¬Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 ^ 4 * MvPolynomial.X 3 ^ 2 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 ^ 8 * MvPolynomial.X 3 ^ 4 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 2 * MvPolynomial.X 2} ≤ Ideal.span {MvPolynomial.X 0 - MvPolynomial.C a, MvPolynomial.X 1 - MvPolynomial.C b, MvPolynomial.X 2 - MvPolynomial.C c, MvPolynomial.X 3 - MvPolynomial.C d} ^ 2

No point of order 2 on the z₃-chart: ∂(x₃⁴z₃⁸w₃⁴ + x₃ − w₃²z₃)/∂x₃ = 4x₃³z₃⁸w₃⁴ + 1 and ∂(x₃³z₃⁴w₃² − y₃²)/∂z₃ = 4x₃³z₃³w₃² are incompatible.

theorem Hironaka.Examples.Example106Stages.transform_example106_zww : (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 3, MvPolynomial.X 1 * MvPolynomial.X 3, MvPolynomial.X 2 * MvPolynomial.X 3, MvPolynomial.X 3]) (MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 2 - MvPolynomial.X 1 ^ 2) = MvPolynomial.X 3 ^ 2 * (MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 - MvPolynomial.X 1 ^ 2) ∧ (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 3, MvPolynomial.X 1 * MvPolynomial.X 3, MvPolynomial.X 2 * MvPolynomial.X 3, MvPolynomial.X 3]) (MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 + MvPolynomial.X 0 - MvPolynomial.X 3 ^ 2)) = MvPolynomial.X 3 ^ 2 * (MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 8 + MvPolynomial.X 0 - MvPolynomial.X 3)) ∧ (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 3, MvPolynomial.X 1 * MvPolynomial.X 3, MvPolynomial.X 2 * MvPolynomial.X 3, MvPolynomial.X 3]) (MvPolynomial.X 1) = MvPolynomial.X 3 * MvPolynomial.X 1 ∧ (MvPolynomial.aeval ![MvPolynomial.X 0 * MvPolynomial.X 3, MvPolynomial.X 1 * MvPolynomial.X 3, MvPolynomial.X 2 * MvPolynomial.X 3, MvPolynomial.X 3]) (MvPolynomial.X 1 - MvPolynomial.X 0 ^ 2 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 2) = MvPolynomial.X 3 * (MvPolynomial.X 1 - MvPolynomial.X 0 ^ 2 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4)

The marked transforms on the w₃-chart and the strict transforms of H₂, H₂'.

theorem Hironaka.Examples.Example106Stages.ord_zero_example106_zww : Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 8 + MvPolynomial.X 0 - MvPolynomial.X 3)} ≤ Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1, MvPolynomial.X 2, MvPolynomial.X 3} ^ 2 ∧ ¬Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 8 + MvPolynomial.X 0 - MvPolynomial.X 3)} ≤ Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1, MvPolynomial.X 2, MvPolynomial.X 3} ^ 3

I₃ has order exactly 2 at its origin.

theorem Hironaka.Examples.Example106Stages.cosupport_example106_zww (a b c d : ℚ) (h : Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 8 + MvPolynomial.X 0 - MvPolynomial.X 3)} ≤ Ideal.span {MvPolynomial.X 0 - MvPolynomial.C a, MvPolynomial.X 1 - MvPolynomial.C b, MvPolynomial.X 2 - MvPolynomial.C c, MvPolynomial.X 3 - MvPolynomial.C d} ^ 2) : a = 0 ∧ b = 0 ∧ c = 0 ∧ d = 0

Every ℚ-point of order ≥ 2 on the w₃-chart is its origin: ∂(x₃³z₃w₃⁴ − y₃²)/∂z₃ = x₃³w₃⁴ splits the cases x₃ = 0 and w₃ = 0, which ∂(z₃(x₃⁴z₃w₃⁸ + x₃ − w₃))/∂x₃ = 4x₃³z₃²w₃⁸ + z₃ and ∂/∂z₃ = 2x₃⁴z₃w₃⁸ + x₃ − w₃ finish.

theorem Hironaka.Examples.Example106Stages.mem_derivative_example106_zww_H : MvPolynomial.X 1 ∈ Ideal.derivative ℚ (Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 8 + MvPolynomial.X 0 - MvPolynomial.X 3)})

The origin of the w₃-chart lies on H₃: y₃ ∈ MC(I₃).

theorem Hironaka.Examples.Example106Stages.mem_derivative_example106_zww_H' : MvPolynomial.X 1 - MvPolynomial.X 0 ^ 2 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 ∈ Ideal.derivative ℚ (Ideal.span {MvPolynomial.X 0 ^ 3 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 4 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 2 * (MvPolynomial.X 0 ^ 4 * MvPolynomial.X 2 * MvPolynomial.X 3 ^ 8 + MvPolynomial.X 0 - MvPolynomial.X 3)})

The origin of the w₃-chart lies on H₃': y₃ − x₃²z₃w₃⁴ ∈ MC(I₃).