Kollár's Example 106 for the order-reduction functor: the affine space and its origin

[Kol07, Example 106] follows the principalization of the ideal I = (x³ − y², x⁴ + xz² − w³) of a subvariety X ⊂ 𝔸⁴: ord I = 2, H = (y = 0) is a hypersurface of maximal contact, and the first blow-up is that of the origin. This module and HironakaExamples/OrderReduction/Example106BlowUp.lean, Example106Length.lean follow the order-reduction functor BO_{4,2} of [Kol07, Theorem 103] on the triple (𝔸⁴_ℚ, I, ∅). The statements are about any smooth blow-up sequence with the three properties of the functor's values, an order-2 sequence ([Kol07, Definition 66]), no empty centre ([Kol07, 32]) and final maximal order < 2 (clause (1) of Theorem 103), through the cosupport forcing of HironakaExamples/Sequence/CosuppForcing.lean: at each stage the next centre is supported at the order-2 locus of the current ideal. The computations are made at every scheme point of 𝔸⁴_ℚ = Spec ℚ[x, y, z, w], not only at its ℚ-points. This module treats the first stage:

• the cosupport {p : ord_p I ≥ 2} is the origin alone (two_le_ord_iff): by the derivative criterion c ≤ ord_p I ⟺ D^{c−1}(I) ⊆ 𝔭 ([Kol07, Lemma 74 (3)]) and D(I) = (x², y, z², xz, w²) (HironakaExamples/Balanced/Example106.lean), a prime containing D(I) contains every coordinate;
• max-ord I ≤ 2 at every point (maxOrd_le_two): D²(I) = (1), since ∂y/∂y = 1;
• the reduced origin is the ideal sheaf of (x, y, z, w) (vanishingIdeal_singleton_origin): the maximal ideal is prime, hence radical, with support the origin;
• the forcing applied (exists_eq_cons_specIdealSheaf_m0): every order-2 sequence for (I, ∅) on 𝔸⁴_ℚ with no empty centre and final maximal order < 2 begins with the blow-up of the origin, Kollár's "thus the first step is to blow up the origin in 𝔸⁴";
• the inputs making (𝔸⁴_ℚ, I, ∅) a triple (isNonzeroEverywhere_I106, the smoothness of 𝔸⁴_ℚ → Spec ℚ; the normal crossings of the empty boundary are Hironaka/Scheme/Snc/EmptyFamily.lean);
• Kollár's closing sentences as printed (strictTransform_meets_plane_ideal; see also [Kol07, Warning 23]): in the x-chart the strict transform X₁ = (x₁ − y₁², x₁ + z₁² − w₁³) meets the plane (x₁ = y₁ = 0) in the cuspidal curve (x₁ = y₁ = z₁² − w₁³ = 0).

The worked example is completed in HironakaExamples/KollarExample106Run.lean, where these facts are applied to the sequence produced by the functor Hironaka.BO.data 4 2.

The origin

theorem Hironaka.Examples.Example106BO.m0_eq_origin_asIdeal : Example106.m0 = (AlgebraicGeometry.origin ℚ 4).asIdeal

The ideal 𝔪₀ = (x, y, z, w) is the prime ideal of the origin of 𝔸⁴_ℚ.

theorem Hironaka.Examples.Example106BO.isClosed_singleton_origin : IsClosed {AlgebraicGeometry.origin ℚ 4}

The origin is a closed point of 𝔸⁴_ℚ: its prime ideal is maximal.

The cosupport of (I, 2) and the max-order

theorem Hironaka.Examples.Example106BO.two_le_ord_iff (p : ↥(AlgebraicGeometry.Spec ↧(MvPolynomial (Fin 4) ℚ))) : ↑2 ≤ (AlgebraicGeometry.specIdealSheaf Example106.I106).ord p ↔ p = AlgebraicGeometry.origin ℚ 4

At every scheme point p of 𝔸⁴_ℚ, ord_p I ≥ 2 iff p is the origin ([Kol07, Example 106]: "ord I = 2 … the first step is to blow up the origin"): the derivative criterion of [Kol07, Lemma 74 (3)] with D(I) = (x², y, z², xz, w²); a prime containing x², y, z², w² contains the four coordinates.

theorem Hironaka.Examples.Example106BO.maxOrd_le_two : (AlgebraicGeometry.specIdealSheaf Example106.I106).maxOrd ≤ ↑2

max-ord I ≤ 2 on 𝔸⁴_ℚ at every scheme point ([Kol07, Example 106]: "ord I = 2"): D²(I) = (1), because y ∈ D(I) and ∂y/∂y = 1, so no prime contains D²(I).

The reduced origin

theorem Hironaka.Examples.Example106BO.support_specIdealSheaf_m0 : (AlgebraicGeometry.specIdealSheaf Example106.m0).support = { carrier := {AlgebraicGeometry.origin ℚ 4}, isClosed' := isClosed_singleton_origin }

The support of the ideal sheaf of 𝔪₀ is the origin.

theorem Hironaka.Examples.Example106BO.vanishingIdeal_singleton_origin : AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal { carrier := {AlgebraicGeometry.origin ℚ 4}, isClosed' := isClosed_singleton_origin } = AlgebraicGeometry.specIdealSheaf Example106.m0

The vanishing ideal sheaf of the origin is the ideal sheaf of 𝔪₀ = (x, y, z, w), the reduced origin: a prime ideal is radical.

The forcing applied to the first stage

theorem Hironaka.Examples.Example106BO.exists_eq_cons_specIdealSheaf_m0 (S : (AlgebraicGeometry.Spec ↧(MvPolynomial (Fin 4) ℚ)).BlowUpSequence) (E : (AlgebraicGeometry.Spec ↧(MvPolynomial (Fin 4) ℚ)).DivisorFamily) (hS : S.IsOrderSeq (AlgebraicGeometry.affineSpaceToSpec ℚ 4) (AlgebraicGeometry.specIdealSheaf Example106.I106) E 2) (hne : S.NoEmptyCenters) (hend : (S.weakTransformSeq (AlgebraicGeometry.specIdealSheaf Example106.I106) (Fin.last S.length)).maxOrd < ↑2) : ∃ (rest : (AlgebraicGeometry.specIdealSheaf Example106.m0).blowUp.BlowUpSequence), S = AlgebraicGeometry.Scheme.BlowUpSequence.cons (AlgebraicGeometry.Spec ↧(MvPolynomial (Fin 4) ℚ)) (AlgebraicGeometry.specIdealSheaf Example106.m0) rest

Every smooth blow-up sequence of order 2 for (𝔸⁴_ℚ, I, E) with no empty centre whose final weak transform has maximal order < 2 begins with the blow-up of the reduced origin ([Kol07, Example 106]: "thus the first step is to blow up the origin in 𝔸⁴"): the cosupport forcing of HironakaExamples/Sequence/CosuppForcing.lean at two_le_ord_iff.

Well-formedness inputs

theorem Hironaka.Examples.Example106BO.I106_ne_bot : Example106.I106 ≠ ⊥

I ≠ 0: the generator x³ − y² has coefficient 1 at x³.

theorem Hironaka.Examples.Example106BO.isNonzeroEverywhere_I106 : (AlgebraicGeometry.specIdealSheaf Example106.I106).IsNonzeroEverywhere

I is nonzero on every irreducible component of 𝔸⁴_ℚ ([Kol07, Notation 64 (2)]): its stalk at every point is the image of the nonzero ideal I under the injective localisation map of the domain ℚ[x, y, z, w].

theorem Hironaka.Examples.Example106BO.smoothOfRelativeDimension_affineSpaceToSpec : AlgebraicGeometry.SmoothOfRelativeDimension 4 (AlgebraicGeometry.affineSpaceToSpec ℚ 4)

𝔸⁴_ℚ → Spec ℚ is smooth of relative dimension 4.

theorem Hironaka.Examples.Example106BO.smooth_affineSpaceToSpec : AlgebraicGeometry.Smooth (AlgebraicGeometry.affineSpaceToSpec ℚ 4)

𝔸⁴_ℚ → Spec ℚ is smooth.

Kollár's closing sentences, as printed

theorem Hironaka.Examples.Example106BO.strictTransform_meets_plane_ideal : Ideal.span {MvPolynomial.X 0 - MvPolynomial.X 1 ^ 2, MvPolynomial.X 0 + MvPolynomial.X 2 ^ 2 - MvPolynomial.X 3 ^ 3} ⊔ Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1} = Ideal.span {MvPolynomial.X 0, MvPolynomial.X 1, MvPolynomial.X 2 ^ 2 - MvPolynomial.X 3 ^ 3}

Kollár's closing sentences as printed ([Kol07, Example 106]; see also [Kol07, Warning 23]): in the x-chart ℚ[x₁, y₁, z₁, w₁] (the variables X 0, …, X 3) the strict transform X₁ = (x₁ − y₁², x₁ + z₁² − w₁³) meets the plane (x₁ = y₁ = 0) in the cuspidal curve (x₁ = y₁ = z₁² − w₁³ = 0).