Remark 33 on the affine model: the chart computations

[Kol07, Remark 33] blows up the origin p = V(x, y, z) of 𝔸³ and then the birational transform C' of the z-axis C = V(x, y). The one computation behind "it is easy to see that X_2 ≅ X_2'" is that the total transform of C under the point blow-up is the exceptional divisor times the birational transform, (x, y)·𝒪 = E_0 · C', i.e. that C passes through p with multiplicity one. On the three charts of the model blow-up B_p 𝔸³ (the chart of x_j is Spec k[x_0, x_1, x_2] with the substitution x_i ↦ x_i x_j for i ≠ j, [Hau14, Definition 4.12]) this is elementary commutative algebra, collected here:

• in the chart of z the ideal (x, y) becomes (xz, yz) = (z) · (x, y), the exceptional ideal is (z), and (x, y) is a prime ideal not containing z, so the (z)-saturation of (z)·(x, y) is (x, y) (colon_map_two_le);
• in the charts of x and of y the ideal (x, y) becomes (x, yx) = (x), resp. (y), the exceptional ideal itself, whose saturation is the unit ideal.

The sheaf-level consequences on the blow-up blowUp used throughout the library are drawn in HironakaExamples/Sequence/Remark33Iso.lean.

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Remark33.subst (k : Type u) [Field k] (j : Fin 3) : MvPolynomial (Fin 3) k →ₐ[k] MvPolynomial (Fin 3) k

The chart substitution of the x_j-chart of B_p 𝔸³ [Hau14, Definition 4.12]: x_i ↦ x_i x_j for i ≠ j, x_j ↦ x_j.

Equations

• Hironaka.Sequence.Remark33.subst k j = AlgebraicGeometry.affineBlowUpAlgebra.chartSubst k (AlgebraicGeometry.CoordinateSubspace.center 3 3) j

theorem Hironaka.Sequence.Remark33.subst_X (k : Type u) [Field k] (j i : Fin 3) : (subst k j) (MvPolynomial.X i) = if i ≠ j then MvPolynomial.X i * MvPolynomial.X j else MvPolynomial.X i

theorem Hironaka.Sequence.Remark33.map_centerIdeal_three_subst (k : Type u) [Field k] (j : Fin 3) : Ideal.map (subst k j) (AlgebraicGeometry.CoordinateSubspace.centerIdeal k 3 3) = Ideal.span {MvPolynomial.X j}

The origin's ideal (x, y, z) becomes (x_j) in the chart of x_j: the exceptional ideal.

theorem Hironaka.Sequence.Remark33.map_centerIdeal_two_subst_of_lt (k : Type u) [Field k] (j : Fin 3) (hj : ↑j < 2) : Ideal.map (subst k j) (AlgebraicGeometry.CoordinateSubspace.centerIdeal k 3 2) = Ideal.span {MvPolynomial.X j}

The z-axis' ideal (x, y) becomes (x_j) in the chart of x_j for j = x, y: the birational transform of C misses these charts.

theorem Hironaka.Sequence.Remark33.map_centerIdeal_two_subst_two (k : Type u) [Field k] : Ideal.map (subst k 2) (AlgebraicGeometry.CoordinateSubspace.centerIdeal k 3 2) = Ideal.span {MvPolynomial.X 2} * AlgebraicGeometry.CoordinateSubspace.centerIdeal k 3 2

The z-axis' ideal (x, y) becomes (xz, yz) = (z) · (x, y) in the chart of z.

theorem Hironaka.Sequence.Remark33.centerIdeal_two_eq_ker (k : Type u) [Field k] : AlgebraicGeometry.CoordinateSubspace.centerIdeal k 3 2 = RingHom.ker ↑(AlgebraicGeometry.CoordinateSubspace.killPred k fun (i : Fin 3) => 2 ≤ ↑i)

(x, y) is the kernel of killing the variables x and y (killPred).

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

(x, y) is a prime ideal of k[x, y, z]: the kernel of killing x and y.

theorem Hironaka.Sequence.Remark33.X_two_notMem_centerIdeal_two (k : Type u) [Field k] : MvPolynomial.X 2 ∉ AlgebraicGeometry.CoordinateSubspace.centerIdeal k 3 2

z ∉ (x, y).

@[reducible, inline]

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

The chart form of the total transform of C.

Equations

• Hironaka.Sequence.Remark33.totalChart k j = Ideal.map (Hironaka.Sequence.Remark33.subst k j) (AlgebraicGeometry.CoordinateSubspace.centerIdeal k 3 2)

@[reducible, inline]

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

The chart form of the exceptional ideal.

Equations

• Hironaka.Sequence.Remark33.excChart k j = Ideal.map (Hironaka.Sequence.Remark33.subst k j) (AlgebraicGeometry.CoordinateSubspace.centerIdeal k 3 3)

theorem Hironaka.Sequence.Remark33.colon_map_two_le (k : Type u) [Field k] : Submodule.colon (totalChart k 2) ↑(excChart k 2 ^ 2) ≤ Submodule.colon (totalChart k 2) ↑(excChart k 2)

The (z)-saturation of (z) · (x, y) stops at the first step: an element f with f z² ∈ (z)·(x, y) already has f z ∈ (z)·(x, y), because z is a nonzerodivisor and (x, y) is a prime ideal not containing z.

theorem Hironaka.Sequence.Remark33.colon_map_of_lt_le (k : Type u) [Field k] (j : Fin 3) (hj : ↑j < 2) : Submodule.colon (totalChart k j) ↑(excChart k j ^ 2) ≤ Submodule.colon (totalChart k j) ↑(excChart k j)

In the charts of x and y the total transform of C is the exceptional ideal, whose saturation is everything.

theorem Hironaka.Sequence.Remark33.colon_map_le (k : Type u) [Field k] (j : Fin 3) : Submodule.colon (totalChart k j) ↑(excChart k j ^ 2) ≤ Submodule.colon (totalChart k j) ↑(excChart k j)

The saturation of the total transform of C by the exceptional ideal stops at the first step on every chart of B_p 𝔸³ (the (z)-saturation on the chart of z, trivially on the others).