Kollár's Remark 33 on the affine model: two blow-up sequences with the same end result

Kollár's genuine counterexample to "the end result determines the sequence" [Kol07, Remark 33]: for a smooth pointed curve p ∈ C in a smooth 3-fold X_0, blowing up p and then the birational transform of C gives Π : X_2 → X_1 = B_p X_0 → X_0 with exceptional divisors E_0, E_1 ⊂ X_2, while blowing up C and then the preimage D = σ_0⁻¹(p) gives Σ : X_2' → X_1' = B_C X_0 → X_0; the end results are isomorphic, X_2 ≅ X_2', and under this isomorphism E_1 corresponds to E_0' and E_0 to E_1'.

This module defines the two sequences on the affine model X_0 = 𝔸³_k = Spec k[x, y, z], C = V(x, y) (the z-axis) and p = V(x, y, z) (the origin), as terms of AlgebraicGeometry.Scheme.BlowUpSequence, so that the isomorphism of the end results, the matching of the exceptional divisors and the computations of Warning 63 can refer to them:

• seqPointCurve k: blow up p, then the birational (strict) transform of C in B_p 𝔸³;
• seqCurvePoint k: blow up C, then σ_0⁻¹(p), the inverse image ideal sheaf of p in B_C 𝔸³.

Both have length 2, and they are different terms because their first centers differ (seqPointCurve_ne_seqCurvePoint, from ne_of_center_zero_ne: z ∈ (x, y, z) but z ∉ (x, y), MvPolynomial.mem_ideal_span_X_image). The isomorphism X_2 ≅ X_2' of the end results is proved in HironakaExamples/Sequence/Remark33Iso.lean, and the matching of the exceptional divisors in HironakaExamples/Sequence/Remark33Exceptional.lean.

@[reducible, inline]

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

The affine 3-space 𝔸³_k = Spec k[x, y, z], with x = X 0, y = X 1, z = X 2.

Equations

• Hironaka.Sequence.Remark33.affine3 k = AlgebraicGeometry.Spec ↧(MvPolynomial (Fin 3) k)

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Remark33.pointIdeal (k : Type u) [Field k] : Ideal (MvPolynomial (Fin 3) k)

The ideal (x, y, z) of the origin p.

Equations

• Hironaka.Sequence.Remark33.pointIdeal k = Ideal.span (Set.range MvPolynomial.X)

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Remark33.curveIdeal (k : Type u) [Field k] : Ideal (MvPolynomial (Fin 3) k)

The ideal (x, y) of the z-axis C.

Equations

• Hironaka.Sequence.Remark33.curveIdeal k = Ideal.span (MvPolynomial.X '' {0, 1})

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Remark33.point (k : Type u) [Field k] : (affine3 k).IdealSheafData

The origin p = V(x, y, z) ⊂ 𝔸³_k as an ideal sheaf.

Equations

• Hironaka.Sequence.Remark33.point k = AlgebraicGeometry.specIdealSheaf (Hironaka.Sequence.Remark33.pointIdeal k)

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Remark33.curve (k : Type u) [Field k] : (affine3 k).IdealSheafData

The z-axis C = V(x, y) ⊂ 𝔸³_k as an ideal sheaf.

Equations

• Hironaka.Sequence.Remark33.curve k = AlgebraicGeometry.specIdealSheaf (Hironaka.Sequence.Remark33.curveIdeal k)

noncomputable def Hironaka.Sequence.Remark33.seqPointCurve (k : Type u) [Field k] : (affine3 k).BlowUpSequence

The first process of [Kol07, Remark 33]: blow up p, then the birational transform of C.

Equations

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

noncomputable def Hironaka.Sequence.Remark33.seqCurvePoint (k : Type u) [Field k] : (affine3 k).BlowUpSequence

The second process of [Kol07, Remark 33]: blow up C, then D = σ_0⁻¹(p).

Equations

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

theorem Hironaka.Sequence.Remark33.length_seqPointCurve (k : Type u) [Field k] : (seqPointCurve k).length = 2

theorem Hironaka.Sequence.Remark33.length_seqCurvePoint (k : Type u) [Field k] : (seqCurvePoint k).length = 2

theorem Hironaka.Sequence.Remark33.pointIdeal_ne_curveIdeal (k : Type u) [Field k] : pointIdeal k ≠ curveIdeal k

z ∈ (x, y, z) but z ∉ (x, y).

theorem Hironaka.Sequence.Remark33.point_ne_curve (k : Type u) [Field k] : point k ≠ curve k

theorem Hironaka.Sequence.Remark33.seqPointCurve_ne_seqCurvePoint (k : Type u) [Field k] : seqPointCurve k ≠ seqCurvePoint k

The two processes of [Kol07, Remark 33] are different sequences, their first centers being p and C.

The exceptional divisors on the two end results

Kollár writes E_0, E_1 ⊂ X_2 for the exceptional divisors of Π and E_0', E_1' ⊂ X_2' for those of Σ [Kol07, Remark 33]: E_1 (resp. E_1') is the exceptional divisor of the second blow-up, E_0 (resp. E_0') the birational (strict) transform under the second blow-up of the exceptional divisor of the first. All four are reduced divisors, given here by their ideal sheaves.

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Remark33.excSecondPointCurve (k : Type u) [Field k] : (seqPointCurve k).last.IdealSheafData

E_1 ⊂ X_2: the exceptional divisor of the second blow-up of Π (the blow-up of the birational transform of C).

Equations

• Hironaka.Sequence.Remark33.excSecondPointCurve k = (Hironaka.Sequence.Remark33.seqPointCurve k).exceptionalAt 1

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Remark33.excFirstTransformPointCurve (k : Type u) [Field k] : (seqPointCurve k).last.IdealSheafData

E_0 ⊂ X_2: the birational transform, under the second blow-up of Π, of the exceptional divisor of the first blow-up (the blow-up of p).

Equations

• Hironaka.Sequence.Remark33.excFirstTransformPointCurve k = ((Hironaka.Sequence.Remark33.seqPointCurve k).exceptionalAt 0).strictTransform ((Hironaka.Sequence.Remark33.seqPointCurve k).center 1)

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Remark33.excSecondCurvePoint (k : Type u) [Field k] : (seqCurvePoint k).last.IdealSheafData

E_1' ⊂ X_2': the exceptional divisor of the second blow-up of Σ (the blow-up of D = σ_0⁻¹(p)).

Equations

• Hironaka.Sequence.Remark33.excSecondCurvePoint k = (Hironaka.Sequence.Remark33.seqCurvePoint k).exceptionalAt 1

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Remark33.excFirstTransformCurvePoint (k : Type u) [Field k] : (seqCurvePoint k).last.IdealSheafData

E_0' ⊂ X_2': the birational transform, under the second blow-up of Σ, of the exceptional divisor of the first blow-up (the blow-up of C).

Equations

• Hironaka.Sequence.Remark33.excFirstTransformCurvePoint k = ((Hironaka.Sequence.Remark33.seqCurvePoint k).exceptionalAt 0).strictTransform ((Hironaka.Sequence.Remark33.seqCurvePoint k).center 1)