The cusp in the affine plane: a model for Kollár's warning on restriction

"The restriction of a smooth blow-up sequence need not be a smooth blow-up sequence" [Kol07, 30.2]. The example behind this sentence: with X = 𝔸², Z the origin and S the cuspidal cubic (y² = x³), blowing up the origin of the plane is a smooth blow-up sequence (its one center is the reduced point Spec k, smooth over k), but its restriction to S = V(y² − x³) is a blow-up sequence starting at a scheme that is not smooth over k, whereas a smooth blow-up sequence in Kollár's sense has a smooth ambient scheme at every stage [Kol07, Notation 19].

This module defines the model as named terms, in the pattern of HironakaExamples/Sequence/Remark33Model.lean:

• affine2 k = Spec k[x, y] with x = X 0, y = X 1;
• originCenter k = V(x, y) and cusp k = V(y² − x³) as ideal sheaves (specIdealSheaf);
• seqOrigin k : BlowUpSequence (affine2 k), the blow-up of the origin, of length 1.

The statements about them are proved in HironakaExamples/Sequence/CuspWitness.lean and HironakaExamples/Sequence/RestrictClosedImmersion.lean.

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Cusp.affine2 (k : Type u) [Field k] : AlgebraicGeometry.Scheme

The affine plane 𝔸²_k = Spec k[x, y], with x = X 0, y = X 1.

Equations

• Hironaka.Sequence.Cusp.affine2 k = AlgebraicGeometry.Spec ↧(MvPolynomial (Fin 2) k)

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Cusp.originCenterIdeal (k : Type u) [Field k] : Ideal (MvPolynomial (Fin 2) k)

The ideal (x, y) of the origin 0 ∈ 𝔸²_k.

Equations

• Hironaka.Sequence.Cusp.originCenterIdeal k = Ideal.span (Set.range MvPolynomial.X)

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Cusp.cuspIdeal (k : Type u) [Field k] : Ideal (MvPolynomial (Fin 2) k)

The ideal (y² − x³) of the cuspidal cubic.

Equations

• Hironaka.Sequence.Cusp.cuspIdeal k = Ideal.span {MvPolynomial.X 1 ^ 2 - MvPolynomial.X 0 ^ 3}

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Cusp.originCenter (k : Type u) [Field k] : (affine2 k).IdealSheafData

The origin Z = V(x, y) ⊂ 𝔸²_k as an ideal sheaf: the center of the blow-up.

Equations

• Hironaka.Sequence.Cusp.originCenter k = AlgebraicGeometry.specIdealSheaf (Hironaka.Sequence.Cusp.originCenterIdeal k)

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Cusp.cusp (k : Type u) [Field k] : (affine2 k).IdealSheafData

The cuspidal cubic S = V(y² − x³) ⊂ 𝔸²_k as an ideal sheaf: the closed subscheme to which the sequence is restricted.

Equations

• Hironaka.Sequence.Cusp.cusp k = AlgebraicGeometry.specIdealSheaf (Hironaka.Sequence.Cusp.cuspIdeal k)

noncomputable def Hironaka.Sequence.Cusp.seqOrigin (k : Type u) [Field k] : (affine2 k).BlowUpSequence

The blow-up sequence of length one blowing up the origin of the plane; the sequence of the example illustrating [Kol07, 30.2].

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Sequence.Cusp.length_seqOrigin (k : Type u) [Field k] : (seqOrigin k).length = 1

The sequence has one blow-up.