The blow-up of the origin restricted to the cusp

"The restriction of a smooth blow-up sequence need not be a smooth blow-up sequence" [Kol07, 30.2]. On the model of HironakaExamples/Sequence/CuspModel.lean (X = 𝔸²_k, Z = V(x, y), S = V(y² − x³)):

• isSmooth_seqOrigin: blowing up the origin is a smooth blow-up sequence; its center V(x, y) ≅ Spec k is smooth over k (smooth_origin_subschemeι: the subscheme is Spec (k[x, y]/(x, y)) and k → k[x, y]/(x, y) is an isomorphism, every polynomial being congruent to its constant term), the ambient 𝔸²_k being smooth over k (smooth_affineSpaceToSpec_two);
• not_smooth_cusp: the restricted sequence starts at S, which is not smooth over k. If it were, the local ring 𝒪_{S,0} = 𝒪_{𝔸²,0}/(y² − x³) would be regular; but 𝒪_{𝔸²,0} is regular, y² − x³ is a nonzero element of 𝔪² at the origin (x, y ∈ 𝔪), and the quotient of a regular local ring by a nonzero element of 𝔪² is never regular (HironakaExamples/Local/SingularQuotient.lean).

The predicate IsSmooth is Kollár's clause on the centers; the ambient clause of [Kol07, Notation 19], the smoothness of the stages, is the one that fails here.

theorem Hironaka.Sequence.Cusp.smooth_affineSpaceToSpec_two (k : Type u) [Field k] : AlgebraicGeometry.Smooth (AlgebraicGeometry.affineSpaceToSpec k 2)

The affine plane is smooth over k (of relative dimension 2).

theorem Hironaka.Sequence.Cusp.one_notMem_originIdeal (k : Type u) [Field k] : 1 ∉ originCenterIdeal k

1 ∉ (x, y).

theorem Hironaka.Sequence.Cusp.sub_C_constantCoeff_mem_originIdeal (k : Type u) [Field k] (p : MvPolynomial (Fin 2) k) : p - MvPolynomial.C (MvPolynomial.constantCoeff p) ∈ originCenterIdeal k

Every polynomial is congruent to its constant term modulo (x, y).

theorem Hironaka.Sequence.Cusp.bijective_mk_comp_algebraMap (k : Type u) [Field k] : Function.Bijective ⇑((Ideal.Quotient.mk (originCenterIdeal k)).comp (algebraMap k (MvPolynomial (Fin 2) k)))

The composite k → k[x, y] → k[x, y]/(x, y) is bijective.

theorem Hironaka.Sequence.Cusp.smooth_origin_subschemeι (k : Type u) [Field k] : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (originCenter k).subschemeι (AlgebraicGeometry.affineSpaceToSpec k 2))

The origin V(x, y) ⊂ 𝔸²_k is smooth over k: its subscheme is Spec (k[x, y]/(x, y)), and k → k[x, y]/(x, y) is an isomorphism.

theorem Hironaka.Sequence.Cusp.isSmooth_seqOrigin (k : Type u) [Field k] : (seqOrigin k).IsSmooth (AlgebraicGeometry.affineSpaceToSpec k 2)

Blowing up the origin of 𝔸²_k is a smooth blow-up sequence.

theorem Hironaka.Sequence.Cusp.cuspPoly_ne_zero (k : Type u) [Field k] : MvPolynomial.X 1 ^ 2 - MvPolynomial.X 0 ^ 3 ≠ 0

y² − x³ ≠ 0.

theorem Hironaka.Sequence.Cusp.not_smooth_cusp (k : Type u) [Field k] : ¬AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (cusp k).subschemeι (AlgebraicGeometry.affineSpaceToSpec k 2))

The cuspidal cubic is not smooth over k: the scheme at which the restricted sequence of [Kol07, 30.2] starts is singular.