Warning 63 on the model of Remark 33: the transforms along Π and the order dichotomy

[Kol07, Warning 63] compares the marked transforms of (I_C, 1) along the two sequences of Remark 33 on 𝔸³_k: Π (blow up the origin p, then the birational transform C' of the z-axis C) and Σ (blow up C, then D = σ_0⁻¹(p)). HironakaExamples/Sequence/Warning63.lean computes the values along Σ (𝒪 at both stages); this module computes the values along Π and proves the dichotomy: Π is a smooth blow-up sequence of order ≥ 1 for (𝔸³, I_C, 1, ∅) and Σ is not, although Π = Σ as morphisms.

• The first transform along Π. (π_0)_*⁻¹(I_C, 1) = C': the marked transform is the colon (π_0^* I_C : E_0), and π_0^* I_C = E_0 · C' is the key identity of HironakaExamples/Sequence/Remark33Iso.lean (curve_comap_eq), so the colon is C' by the uniqueness clause of [Kol07, Definition 60] (eq_markedTransform_of_pow_mul_eq).
• The end value along Π is (π_1)_*⁻¹(C', 1) = (E_1 : E_1) = 𝒪 (markedTransform_self).
• Σ is not of order ≥ 1. Along Σ the second stage carries the marked ideal (σ_0)_*⁻¹(I_C, 1) = 𝒪, whose order along the center D is 0 < 1; D is nonempty because the origin of the model's x-chart of B_C 𝔸³ lies over p.
• Π is of order ≥ 1. The six clauses of Definition 66 for Π: the centers p and C' are smooth over k, the total transforms of the empty family have simple normal crossings with them, and the marked ideals I_C and C' have order ≥ 1 along p and C' (HironakaExamples/Sequence/Remark33OrderSeq.lean). Two general lemmas serve here and later: the empty family has snc with every smooth center (adapted parameters, exists_adaptedParameters_of_smooth), and ord_Z I ≥ 1 whenever I ≤ Z.

The two general lemmas (hasSncWith_empty_of_smooth, leOrdAlong_one_of_le) are in the library module Hironaka/Resolution/Algebraic/Kol07/Remark33Warning63.lean.

The values along Π

theorem Hironaka.Sequence.markedTransform_point_curve (k : Type u) [Field k] : (Remark33.curve k).markedTransform (Remark33.point k) 1 = (Remark33.curve k).strictTransform (Remark33.point k)

The first transform along Π in [Kol07, Warning 63]: (π_0)_*⁻¹(I_C, 1) = C', since π_0^* I_C = E_0 · C' (curve_comap_eq).

theorem Hironaka.Sequence.markedTransformSeq_seqPointCurve_one (k : Type u) [Field k] : (Remark33.seqPointCurve k).markedTransformSeq (Remark33.curve k) 1 ⟨1, ⋯⟩ = (Remark33.curve k).strictTransform (Remark33.point k)

theorem Hironaka.Sequence.markedTransformSeq_seqPointCurve (k : Type u) [Field k] : (Remark33.seqPointCurve k).markedTransformSeq (Remark33.curve k) 1 (Fin.last 2) = ⊤

The end value along Π in [Kol07, Warning 63] is the unit ideal, (π_1)_*⁻¹(C', 1) = (E_1 : E_1) = 𝒪.

The order dichotomy: Σ is not of order ≥ 1

theorem Hironaka.Sequence.mem_support_specIdealSheaf_iff {R : Type u} [CommRing R] (J : Ideal R) (y : ↥(AlgebraicGeometry.Spec ↧R)) : y ∈ (AlgebraicGeometry.specIdealSheaf J).support ↔ J ≤ y.asIdeal

A point 𝔭 of Spec R lies in the support of the ideal sheaf of J iff J ⊆ 𝔭.

theorem Hironaka.Sequence.mem_support_specIdealSheaf_of_le {R : Type u} [CommRing R] (J : Ideal R) (y : ↥(AlgebraicGeometry.Spec ↧R)) (hJ : J ≤ y.asIdeal) : y ∈ (AlgebraicGeometry.specIdealSheaf J).support

A point 𝔭 of Spec R lies in the support of the ideal sheaf of J when J ⊆ 𝔭.

theorem Hironaka.Sequence.exists_mem_support_comap_π_Zs (k : Type u) [Field k] : ∃ (z : ↥(Remark33.Ys k).blowUp), z ∈ ((Remark33.Zs k).comap (Remark33.Ys k).blowUpπ).support

D = σ_0⁻¹(p) is nonempty: the origin of the model's x-chart of B_C 𝔸³ lies over p (the chart substitution x ↦ x, y ↦ yx, z ↦ z sends (x, y, z) into the origin).

theorem Hironaka.Sequence.not_isOrderGeSeq_aux (k : Type u) [Field k] {p C : (AlgebraicGeometry.Spec ↧(MvPolynomial (Fin 3) k)).IdealSheafData} (hp : p = Remark33.Zs k) (hC : C = Remark33.Ys k) : ¬(AlgebraicGeometry.Scheme.BlowUpSequence.cons (AlgebraicGeometry.Spec ↧(MvPolynomial (Fin 3) k)) C (AlgebraicGeometry.Scheme.BlowUpSequence.cons C.blowUp (p.comap C.blowUpπ) (AlgebraicGeometry.Scheme.BlowUpSequence.nil (p.comap C.blowUpπ).blowUp))).IsOrderGeSeq (AlgebraicGeometry.affineSpaceToSpec k 3) C 1 (AlgebraicGeometry.Scheme.DivisorFamily.empty (AlgebraicGeometry.Spec ↧(MvPolynomial (Fin 3) k)))

Σ is not a sequence of order ≥ 1 for (𝔸³, I_C, 1, ∅) (stated for the coordinate subspaces): at its second stage the marked ideal is 𝒪 (markedTransform_self), whose order along the nonempty center D is 0 < 1.

theorem Hironaka.Sequence.not_isOrderGeSeq_seqCurvePoint (k : Type u) [Field k] : ¬(Remark33.seqCurvePoint k).IsOrderGeSeq (AlgebraicGeometry.affineSpaceToSpec k 3) (Remark33.curve k) 1 (AlgebraicGeometry.Scheme.DivisorFamily.empty (Remark33.affine3 k))

[Kol07, Warning 63]: Σ is not a smooth blow-up sequence of order ≥ 1 starting with (𝔸³, I_C, 1, ∅).