Warning 63 on the model of Remark 33: Π is a smooth blow-up sequence of order ≥ 1

In [Kol07, Warning 63] the sequence Π (blow up the origin p of 𝔸³, then the birational transform C' of the z-axis C) is a smooth blow-up sequence of order ≥ 1 starting with (𝔸³, I_C, 1, ∅) in the sense of [Kol07, Definition 66]. By the recursion of Definition 66 (isOrderGeSeq_cons_iff) this is six clauses, treated here in turn:

• Smooth centers. p and C are coordinate subspaces of 𝔸³; V(x_0, …, x_{r-1}) ≅ Spec k[x_r, …, x_{n-1}] is smooth over k (the standard smoothness of polynomial algebras, transported along quotientCenterAlgEquiv). The second center C' lies over the z-chart of X_1 = B_p 𝔸³, where it is V(x', y') again (Cprime_comap_u_two, HironakaExamples/Sequence/Remark33Exceptional.lean) and is the unit ideal over the other two charts (Cprime_comap_u_of_lt): the single open piece V(C'|_{U_z}) → V(C') covers, and Smooth is Zariski-local at the source.
• Normal crossings. The empty family has snc with every smooth center (hasSncWith_empty_of_smooth). Its total transform (E_0) has snc with C': the only point of C' ∩ E_0 is the origin of the z-chart, where the chart coordinates x', y', z are a regular system of parameters (the étale-coordinate lemma at the origin of 𝔸³, transported along the stalk isomorphism of the chart) with E_0 = (z) and C' = (x', y'); at every other point of C' the divisor E_0 is absent and adapted parameters of the smooth C' suffice.
• Orders. ord_p I_C ≥ 1 since I_C ≤ p, and ord_{C'} C' ≥ 1 (leOrdAlong_one_of_le), the marked ideal at the second stage being C' itself (markedTransform_point_curve).

Together with not_isOrderGeSeq_seqCurvePoint (HironakaExamples/Sequence/Remark33Warning63.lean) this is the dichotomy of Warning 63: Π is a sequence of order ≥ 1 for (𝔸³, I_C, 1, ∅) and Σ is not, although Π = Σ as morphisms.

Coordinate subspaces of 𝔸ⁿ_k are smooth over k

theorem Hironaka.Sequence.smoothOfRelativeDimension_Spec_map_mk_comp_algebraMap (k : Type u) [Field k] (n r : ℕ) : AlgebraicGeometry.SmoothOfRelativeDimension (Nat.card { i : Fin n // ¬↑i < r }) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ((Ideal.Quotient.mk (AlgebraicGeometry.CoordinateSubspace.centerIdeal k n r)).comp (algebraMap k (MvPolynomial (Fin n) k)))))

k → k[x]/(x_0, …, x_{r-1}) is smooth of relative dimension n − r: the quotient is the polynomial algebra in the remaining variables (quotientCenterAlgEquiv and the standard smoothness of polynomial algebras).

theorem Hironaka.Sequence.smooth_Spec_map_mk_comp (k : Type u) [Field k] (n r : ℕ) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (AlgebraicGeometry.CoordinateSubspace.centerIdeal k n r)))) (AlgebraicGeometry.affineSpaceToSpec k n))

Spec (k[x]/(x_0, …, x_{r-1})) → Spec k is smooth.

theorem Hironaka.Sequence.smooth_coordinateSubspace_subschemeι (k : Type u) [Field k] (n r : ℕ) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.coordinateSubspace k n r).subschemeι (AlgebraicGeometry.affineSpaceToSpec k n))

The coordinate subspace V(x_0, …, x_{r-1}) ⊆ 𝔸ⁿ_k is smooth over k (the smoothness of the centers p and C).

theorem Hironaka.Sequence.smooth_subschemeι_comp_of_eq_coordinateSubspace (k : Type u) [Field k] {n r : ℕ} {J : (AlgebraicGeometry.Spec ↧(MvPolynomial (Fin n) k)).IdealSheafData} (hJ : J = AlgebraicGeometry.coordinateSubspace k n r) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp J.subschemeι (AlgebraicGeometry.affineSpaceToSpec k n))

V(J) → Spec k is smooth for every J equal to a coordinate subspace (the shape in which the restrictions of C' to the charts arise).

The birational transform C' is smooth over k

instance Hironaka.Sequence.isOpenImmersion_subschemeMap_Cprime (k : Type u) [Field k] (e₀ : (Remark33.Zs k).blowUp ≅ Remark33.M k) : AlgebraicGeometry.IsOpenImmersion (((Remark33.Cprime k).comap (Remark33.u k e₀ 2)).subschemeMap (Remark33.Cprime k) (Remark33.u k e₀ 2) ⋯)

The piece of V(C') over the z-chart is an open immersion (isOpenImmersion_subschemeMap_of_comap).

theorem Hironaka.Sequence.exists_u_two_eq_of_mem_support (k : Type u) [Field k] (e₀ : (Remark33.Zs k).blowUp ≅ Remark33.M k) (he₀ : CategoryTheory.CategoryStruct.comp e₀.hom (Remark33.πm k) = (Remark33.Zs k).blowUpπ) {y : ↥(Remark33.Zs k).blowUp} (hy : y ∈ (Remark33.Cprime k).support) : ∃ (w : ↥(AlgebraicGeometry.Spec ↧(MvPolynomial (Fin 3) k))), (Remark33.u k e₀ 2) w = y

Every point of V(C') lies over the z-chart: C' is the unit ideal over the other two.

theorem Hironaka.Sequence.exists_subschemeMap_Cprime_eq (k : Type u) [Field k] (e₀ : (Remark33.Zs k).blowUp ≅ Remark33.M k) (he₀ : CategoryTheory.CategoryStruct.comp e₀.hom (Remark33.πm k) = (Remark33.Zs k).blowUpπ) (x : ↥(Remark33.Cprime k).subscheme) : ∃ (y : ↥((Remark33.Cprime k).comap (Remark33.u k e₀ 2)).subscheme), (((Remark33.Cprime k).comap (Remark33.u k e₀ 2)).subschemeMap (Remark33.Cprime k) (Remark33.u k e₀ 2) ⋯) y = x

The piece over the z-chart covers V(C') (the pullback square of the closed immersions).

theorem Hironaka.Sequence.u_two_π_comp_structure (k : Type u) [Field k] (e₀ : (Remark33.Zs k).blowUp ≅ Remark33.M k) (he₀ : CategoryTheory.CategoryStruct.comp e₀.hom (Remark33.πm k) = (Remark33.Zs k).blowUpπ) : CategoryTheory.CategoryStruct.comp (Remark33.u k e₀ 2) (CategoryTheory.CategoryStruct.comp (Remark33.Zs k).blowUpπ (AlgebraicGeometry.affineSpaceToSpec k 3)) = AlgebraicGeometry.affineSpaceToSpec k 3

The chart U_z → X_1 → 𝔸³ → Spec k is the structure map of Spec k[x', y', z].

theorem Hironaka.Sequence.smooth_Cprime_subschemeι (k : Type u) [Field k] (e₀ : (Remark33.Zs k).blowUp ≅ Remark33.M k) (he₀ : CategoryTheory.CategoryStruct.comp e₀.hom (Remark33.πm k) = (Remark33.Zs k).blowUpπ) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (Remark33.Cprime k).subschemeι (CategoryTheory.CategoryStruct.comp (Remark33.Zs k).blowUpπ (AlgebraicGeometry.affineSpaceToSpec k 3)))

The smoothness of the second center: the birational transform C' of the z-axis is smooth over k.

Stalks and supports of the ideal sheaves of ideals on Spec R

theorem Hironaka.Sequence.stalkIdeal_specIdealSheaf_germ {R : Type u} [CommRing R] (J : Ideal R) (y : ↥(AlgebraicGeometry.Spec ↧R)) : (AlgebraicGeometry.specIdealSheaf J).stalkIdeal y = Ideal.map ((CommRingCat.Hom.hom ((AlgebraicGeometry.Spec ↧R).presheaf.germ ⊤ y trivial)).comp (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧R).inv)) J

AlgebraicGeometry.stalkIdeal_specIdealSheaf (the stalk of the ideal sheaf of J at y is J 𝒪_{Spec R, y}, spelled with Mathlib's toStalk) in the spelling of the germs of global sections: toStalk R y = toOpen R ⊤ ≫ germ and (ΓSpecIso R).inv = toOpen R ⊤ definitionally.

The normal crossings of E_0 with C'

theorem Hironaka.Sequence.exists_regularSystem_origin (k : Type u) [Field k] : ∃ (m : ℕ) (z : Fin m → ↑((Remark33.affine3 k).presheaf.stalk (AlgebraicGeometry.origin k 3))), (Ideal.span (Set.range z) = IsLocalRing.maximalIdeal ↑((Remark33.affine3 k).presheaf.stalk (AlgebraicGeometry.origin k 3)) ∧ ↑m = ringKrullDim ↑((Remark33.affine3 k).presheaf.stalk (AlgebraicGeometry.origin k 3))) ∧ ∃ (σ : Fin 3 → Fin m), Function.Injective σ ∧ ∀ (c : Fin 3), z (σ c) = (CommRingCat.Hom.hom ((Remark33.affine3 k).presheaf.germ ⊤ (AlgebraicGeometry.origin k 3) trivial)) ((CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.ΓSpecIso ↧(MvPolynomial (Fin 3) k)).inv) (MvPolynomial.X c))

The étale-coordinate lemma (exists_span_eq_maximalIdeal_of_etale_coordinates) at the origin of 𝔸³, on the stalk: a regular system of parameters of 𝒪_{𝔸³,0} containing the germs of x, y, z.

theorem Hironaka.Sequence.eq_origin_of_mem_support (k : Type u) [Field k] (e₀ : (Remark33.Zs k).blowUp ≅ Remark33.M k) (he₀ : CategoryTheory.CategoryStruct.comp e₀.hom (Remark33.πm k) = (Remark33.Zs k).blowUpπ) {w : ↥(Remark33.affine3 k)} (hC : (Remark33.u k e₀ 2) w ∈ (Remark33.Cprime k).support) (hE : (Remark33.u k e₀ 2) w ∈ (Remark33.Ezero k).support) : w = AlgebraicGeometry.origin k 3

The only point of C' ∩ E_0 is the origin of the z-chart.

theorem Hironaka.Sequence.exists_isSncAt_origin (k : Type u) [Field k] (e₀ : (Remark33.Zs k).blowUp ≅ Remark33.M k) (he₀ : CategoryTheory.CategoryStruct.comp e₀.hom (Remark33.πm k) = (Remark33.Zs k).blowUpπ) : ∃ (n : ℕ) (z : Fin n → ↑((Remark33.Zs k).blowUp.presheaf.stalk ((Remark33.u k e₀ 2) (AlgebraicGeometry.origin k 3)))), ((AlgebraicGeometry.Scheme.DivisorFamily.empty (Remark33.affine3 k)).totalTransform (Remark33.Zs k)).IsSncAt ((Remark33.u k e₀ 2) (AlgebraicGeometry.origin k 3)) z ∧ ∃ (s : Finset (Fin n)), (Remark33.Cprime k).stalkIdeal ((Remark33.u k e₀ 2) (AlgebraicGeometry.origin k 3)) = Ideal.span (z '' ↑s)

At the origin a₀ of the z-chart the chart coordinates x', y', z (the regular system of parameters of 𝒪_{𝔸³,0} transported along the chart) exhibit E_0 = (z) and C' = (x', y').

theorem Hironaka.Sequence.hasSncWith_totalTransform_empty_Cprime (k : Type u) [Field k] (e₀ : (Remark33.Zs k).blowUp ≅ Remark33.M k) (he₀ : CategoryTheory.CategoryStruct.comp e₀.hom (Remark33.πm k) = (Remark33.Zs k).blowUpπ) : ((AlgebraicGeometry.Scheme.DivisorFamily.empty (Remark33.affine3 k)).totalTransform (Remark33.Zs k)).HasSncWith (Remark33.Cprime k)

The normal crossings at the second stage: the total transform (E_0) of the empty family has simple normal crossings with the center C'.

Π is a smooth blow-up sequence of order ≥ 1

theorem Hironaka.Sequence.markedTransform_Zs_Ys (k : Type u) [Field k] : (Remark33.Ys k).markedTransform (Remark33.Zs k) 1 = Remark33.Cprime k

The marked transform of C under the point blow-up is C' (markedTransform_point_curve for the coordinate subspaces).

theorem Hironaka.Sequence.isOrderGeSeq_Cprime (k : Type u) [Field k] : (AlgebraicGeometry.Scheme.BlowUpSequence.cons (Remark33.affine3 k) (Remark33.Zs k) (AlgebraicGeometry.Scheme.BlowUpSequence.cons (Remark33.Zs k).blowUp (Remark33.Cprime k) (AlgebraicGeometry.Scheme.BlowUpSequence.nil (Remark33.Cprime k).blowUp))).IsOrderGeSeq (AlgebraicGeometry.affineSpaceToSpec k 3) (Remark33.Ys k) 1 (AlgebraicGeometry.Scheme.DivisorFamily.empty (Remark33.affine3 k))

Π is a smooth blow-up sequence of order ≥ 1 starting with (𝔸³, I_C, 1, ∅), stated for the coordinate subspaces Zs and Ys.

theorem Hironaka.Sequence.isOrderGeSeq_aux (k : Type u) [Field k] {p C : (Remark33.affine3 k).IdealSheafData} (hp : p = Remark33.Zs k) (hC : C = Remark33.Ys k) : (AlgebraicGeometry.Scheme.BlowUpSequence.cons (Remark33.affine3 k) p (AlgebraicGeometry.Scheme.BlowUpSequence.cons p.blowUp (C.strictTransform p) (AlgebraicGeometry.Scheme.BlowUpSequence.nil (C.strictTransform p).blowUp))).IsOrderGeSeq (AlgebraicGeometry.affineSpaceToSpec k 3) C 1 (AlgebraicGeometry.Scheme.DivisorFamily.empty (Remark33.affine3 k))

The same for centers given by equations (the shape of seqPointCurve).

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

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