Remark 33 on the affine model: the isomorphism of end results

[Kol07, Remark 33]: blowing up 𝔸³ at the origin p and then along the birational transform C' of the z-axis C, or first along C and then along D = σ_0⁻¹(p), gives isomorphic end results. "It is easy to see" made explicit:

• X_2' = B_D(B_C 𝔸³) is the blow-up of 𝔸³ along C · p (blowUp.exists_mulIso: blowing up the inverse image of p on B_C 𝔸³ is blowing up the product C · p on 𝔸³);
• X_2 = B_{C'}(B_p 𝔸³), and the total transform of C under the point blow-up is the exceptional divisor times the birational transform, C.comap π_0 = E_0 · C' (curve_comap_eq): C passes through p with multiplicity one. This is the one computation of the module; it is checked on the three charts of the model blow-up (HironakaExamples/Sequence/Remark33Charts.lean) and transported along the isomorphism of the blow-up blowUp with the model (exists_iso_blowUp_coordinateSubspace). So blowing up C' is blowing up C' · E_0 = C.comap π_0 (blowUp.exists_mul_isInvertible_iso: multiplying the center by an invertible ideal does not change the blow-up), which is the blow-up of 𝔸³ along p · C = C · p (blowUp.exists_mulIso again).

The chain of these isomorphisms over 𝔸³ is exists_iso_last.

The saturation. On the blow-up B of p, with exceptional ideal E, the birational transform of C is the E-saturation ⨆ i (I : Eⁱ) of the total transform I = C.comap π_0. Since C ⊆ p, I ⊆ E and I = E · (I : E); and the saturation stops after one step, (I : E²) = (I : E), because on the chart of z the ideal I is (z) · (x, y) with (x, y) a prime not containing z, while on the charts of x and y it is the exceptional ideal itself (colon_map_le). Hence ⨆ i (I : Eⁱ) = (I : E) and I = E · C'. The chartwise inequality is transported from the polynomial ring through the ring isomorphisms of the charts (comap_colon_of_isOpenImmersion, le_of_comap_le_of_iSup_eq_top).

The ring-level and sheaf-level helpers (colons along ring maps and open immersions, inequalities on covers) are in the library module Hironaka/Scheme/BlowUpSequence/Remark33Iso.lean.

The model: B_p 𝔸³ and its charts

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Remark33.Zs (k : Type u) [Field k] : (AlgebraicGeometry.Spec ↧(MvPolynomial (Fin 3) k)).IdealSheafData

The origin p = V(x, y, z) as a coordinate subspace (coordinateSubspace).

Equations

• Hironaka.Sequence.Remark33.Zs k = AlgebraicGeometry.coordinateSubspace k 3 3

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Remark33.Ys (k : Type u) [Field k] : (AlgebraicGeometry.Spec ↧(MvPolynomial (Fin 3) k)).IdealSheafData

The z-axis C = V(x, y) as a coordinate subspace (coordinateSubspace).

Equations

• Hironaka.Sequence.Remark33.Ys k = AlgebraicGeometry.coordinateSubspace k 3 2

@[reducible, inline]

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

The model blow-up B_p 𝔸³ (modelBlowUp).

Equations

• Hironaka.Sequence.Remark33.M k = AlgebraicGeometry.CoordinateSubspace.modelBlowUp k 3 3

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Remark33.πm (k : Type u) [Field k] : M k ⟶ AlgebraicGeometry.Spec ↧(MvPolynomial (Fin 3) k)

The projection of the model blow-up.

Equations

• Hironaka.Sequence.Remark33.πm k = AlgebraicGeometry.affineBlowUp.π (AlgebraicGeometry.CoordinateSubspace.centerIdeal k 3 3)

@[reducible, inline]

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

The exceptional ideal of the model blow-up.

Equations

• Hironaka.Sequence.Remark33.Em k = (Hironaka.Sequence.Remark33.Zs k).comap (Hironaka.Sequence.Remark33.πm k)

@[reducible, inline]

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

The total transform of C on the model blow-up.

Equations

• Hironaka.Sequence.Remark33.Im k = (Hironaka.Sequence.Remark33.Ys k).comap (Hironaka.Sequence.Remark33.πm k)

theorem Hironaka.Sequence.Remark33.Em_isInvertible (k : Type u) [Field k] : (Em k).IsInvertible

theorem Hironaka.Sequence.Remark33.centerIdeal_two_le (k : Type u) [Field k] : AlgebraicGeometry.CoordinateSubspace.centerIdeal k 3 2 ≤ AlgebraicGeometry.CoordinateSubspace.centerIdeal k 3 3

theorem Hironaka.Sequence.Remark33.Im_le_Em (k : Type u) [Field k] : Im k ≤ Em k

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Remark33.chart (k : Type u) [Field k] (j : Fin 3) : AlgebraicGeometry.Spec ↧(MvPolynomial (Fin 3) k) ⟶ M k

The chart of x_j.

Equations

• Hironaka.Sequence.Remark33.chart k j = AlgebraicGeometry.CoordinateSubspace.modelChart k 3 3 j ⋯

theorem Hironaka.Sequence.Remark33.iSup_opensRange_chart (k : Type u) [Field k] : ⨆ (j : Fin 3), AlgebraicGeometry.Scheme.Hom.opensRange (chart k j) = ⊤

theorem Hironaka.Sequence.Remark33.chart_πm (k : Type u) [Field k] (j : Fin 3) : CategoryTheory.CategoryStruct.comp (chart k j) (πm k) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (subst k j).toRingHom)

theorem Hironaka.Sequence.Remark33.Im_comap_chart (k : Type u) [Field k] (j : Fin 3) : (Im k).comap (chart k j) = AlgebraicGeometry.specIdealSheaf (totalChart k j)

theorem Hironaka.Sequence.Remark33.Em_comap_chart (k : Type u) [Field k] (j : Fin 3) : (Em k).comap (chart k j) = AlgebraicGeometry.specIdealSheaf (excChart k j)

theorem Hironaka.Sequence.Remark33.excChart_isInvertible (k : Type u) [Field k] (j : Fin 3) : (AlgebraicGeometry.specIdealSheaf (excChart k j)).IsInvertible

theorem Hironaka.Sequence.Remark33.Im_colon_sq_le (k : Type u) [Field k] : (Im k).colon (Em k ^ 2) ≤ (Im k).colon (Em k)

The saturation stops after one step on the model: (I : E²) ≤ (I : E).

theorem Hironaka.Sequence.Remark33.Im_colon_pow_succ_le (k : Type u) [Field k] (i : ℕ) : (Im k).colon (Em k ^ (i + 1)) ≤ (Im k).colon (Em k)

theorem Hironaka.Sequence.Remark33.strictTransformAlong_πm_eq (k : Type u) [Field k] : (Ys k).strictTransformAlong (πm k) (Em k) = (Im k).colon (Em k)

On the model, the birational transform of C is (I : E).

theorem Hironaka.Sequence.Remark33.Em_mul_colon (k : Type u) [Field k] : Em k * (Im k).colon (Em k) = Im k

On the model: I = E · (I : E).

theorem Hironaka.Sequence.Remark33.Im_eq_Em_mul_strictTransform (k : Type u) [Field k] : Im k = Em k * (Ys k).strictTransformAlong (πm k) (Em k)

The key identity on the model: the total transform of C is the exceptional ideal times the birational transform.

Transport to the blow-up blowUp

theorem Hironaka.Sequence.Remark33.coordinateSubspace_comap_eq (k : Type u) [Field k] : (Ys k).comap (Zs k).blowUpπ = (Zs k).comap (Zs k).blowUpπ * (Ys k).strictTransformAlong (Zs k).blowUpπ ((Zs k).comap (Zs k).blowUpπ)

The key identity on blowUp (coordinateSubspace k 3 3), the blow-up of 𝔸³ at p.

theorem Hironaka.Sequence.Remark33.point_eq_coordinateSubspace (k : Type u) [Field k] : point k = Zs k

theorem Hironaka.Sequence.Remark33.curve_eq_coordinateSubspace (k : Type u) [Field k] : curve k = Ys k

theorem Hironaka.Sequence.Remark33.curve_comap_eq (k : Type u) [Field k] : (curve k).comap (point k).blowUpπ = (point k).exceptionalDivisor * (curve k).strictTransform (point k)

The total transform of C under the point blow-up is E_0 · C' (the one computation behind "it is easy to see" in [Kol07, Remark 33]), stated for the blow-up and strict transform used throughout the library.

The isomorphism of the end results

theorem Hironaka.Sequence.Remark33.exists_iso_last (k : Type u) [Field k] : ∃ (e : (seqPointCurve k).last ≅ (seqCurvePoint k).last), CategoryTheory.CategoryStruct.comp e.hom (seqCurvePoint k).composite = (seqPointCurve k).composite

X_2 ≅ X_2' over 𝔸³ [Kol07, Remark 33].