Bierstone–Milman's Example 3.16: the saturation computed

[BM97, Example 3.16] blows up the origin of ℝ² for X = V(h), h = x⁴(x−1)² + y², and reads off in the chart x = u, y = uv the strict transform X' = V(u²(u−1)² + v²), with support {(0,0), (1,0)}, against the geometric strict transform X'' ([BM97, Remark 3.15]) with support {(1,0)}. The saturation lemma for K-analytic spaces, K = ℝ or ℂ (colonChain_locallyStationary, Hironaka.AnalyticSpace.Noether.Saturation), says the colon chain (J : I_F^k) of the total transform J by the exceptional ideal I_F is stationary near every point; this module computes that chain on the example, in the germ ring Conv 2 of the chart (the stalk of the structure sheaf at a point of the chart is Conv 2 through the Taylor isomorphism taylorEquivConv, with coordinates centred at the point):

• Chart 1 (x = u, y = uv; I_F = (u), h ∘ π = u² h₁, h₁ = u²(u−1)² + v²). At the point (0, c) of the exceptional divisor the centred equation is bm316Chart1 c = u²(u−1)² + (c + v)²; u is prime in the unique factorization domain Conv 2 and does not divide h₁, because the coefficient of v² in h₁ is 1 (coeff_bm316Chart1: h₁(0, v) = v² is not identically zero). Hence (u² h₁ : u^k) = (u^(2−k) h₁) for k ≤ 2 and = (h₁) for k ≥ 2 (colon_bm316Chart1_of_le_two, colon_bm316Chart1_of_two_le): the chain is stationary from N = 2 on, uniformly in c, and not before (colon_bm316Chart1_one_lt_two). The saturation is the ideal-theoretic strict transform (h₁).
• Chart 2 (x = u'v', y = v'; I_F = (v'), h ∘ π = v'² h₂, h₂ = u'⁴v'²(u'v'−1)² + 1). The computation is made at the origin of the chart only (bm316Chart2 is the series centred there): h₂ is a unit (constant coefficient 1, isUnit_bm316Chart2), so the saturation is the unit ideal at that point, again from N = 2 on (colon_bm316Chart2_of_two_le).
• Supports: the real zero set of h₁ is {(0,0), (1,0)} (zeroSet_bm316Chart1Fun); it meets F = {u = 0} in {(0,0)} (zeroSet_bm316Chart1Fun_inter_exceptional); the closure of its part off F is {(1,0)} (closure_zeroSet_bm316Chart1Fun_diff_exceptional). [BM97, Example 3.16] states that |X''| = {(1,0)}, strictly smaller than the support of X'; the identification of |X''| with this closure is the source's statement and is not verified here.

The two general colon computations (colon_span_pow_mul_of_le, colon_span_pow_mul_of_prime) are "(h₁) : u^j = (h₁) when h₁ and u are coprime", in Mathlib's vocabulary: u prime and u ∤ h give IsRelPrime h (u^j) (Irreducible.isRelPrime_iff_not_dvd), and a relatively prime divisor of a product divides the other factor (IsRelPrime.dvd_of_dvd_mul_right, in any DecompositionMonoid; a unique factorization domain is one). These are computations on concrete data; RealPlaneStrictTransform proves the same failure of the closure inclusion on the manifold-level blow-up.

theorem Hironaka.Examples.colon_span_pow_mul_of_le {R : Type u_1} [CommRing R] [IsDomain R] {u h : R} (hu : u ≠ 0) {m k : ℕ} (hk : k ≤ m) : Submodule.colon (Ideal.span {u ^ m * h}) ↑(Ideal.span {u} ^ k) = Ideal.span {u ^ (m - k) * h}

In a domain, for u ≠ 0 and k ≤ m, (u^m h : (u)^k) = (u^(m−k) h) — cancel u^k.

theorem Hironaka.Examples.colon_span_pow_mul_of_prime {R : Type u_1} [CommRing R] [IsDomain R] [DecompositionMonoid R] {u h : R} (hu : Prime u) (hh : ¬u ∣ h) {m k : ℕ} (hk : m ≤ k) : Submodule.colon (Ideal.span {u ^ m * h}) ↑(Ideal.span {u} ^ k) = Ideal.span {h}

For u prime with u ∤ h, (u^m h : (u)^k) = (h) for k ≥ m — cancel u^m, then h ∣ x u^(k−m) forces h ∣ x since h is relatively prime to every power of u.

noncomputable def Hironaka.Examples.bm316Chart1 (c : ℝ) : ↥(Analytic.Conv ℝ 2)

[BM97, Example 3.16], chart 1 (x = u, y = uv), at the point (0, c) of the exceptional divisor F = {u = 0}: the strict transform's equation h₁ = u²(u−1)² + v² in the coordinates centred at the point, u²(u−1)² + (c + v)², as a convergent series (u = convX 0, v = convX 1).

Equations

• Hironaka.Examples.bm316Chart1 c = Analytic.convX ℝ 0 ^ 2 * (Analytic.convX ℝ 0 - 1) ^ 2 + ((algebraMap ℝ ↥(Analytic.Conv ℝ 2)) c + Analytic.convX ℝ 1) ^ 2

theorem Hironaka.Examples.coeff_bm316Chart1 (c : ℝ) : (MvPowerSeries.coeff (Finsupp.single 1 2)) ↑(bm316Chart1 c) = 1

The coefficient of v² in bm316Chart1 c is 1: h₁(0, v) = v² is not identically zero near any v₀.

theorem Hironaka.Examples.bm316Chart1_ne_zero (c : ℝ) : bm316Chart1 c ≠ 0

h₁ ≠ 0 in Conv ℝ 2.

theorem Hironaka.Examples.not_convX_dvd_bm316Chart1 (c : ℝ) : ¬Analytic.convX ℝ 0 ∣ bm316Chart1 c

u ∤ h₁ in Conv ℝ 2: a multiple of u has no u-free monomial, but h₁ has v².

theorem Hironaka.Examples.colon_bm316Chart1_of_two_le (c : ℝ) {k : ℕ} (hk : 2 ≤ k) : Submodule.colon (Ideal.span {Analytic.convX ℝ 0 ^ 2 * bm316Chart1 c}) ↑(Ideal.span {Analytic.convX ℝ 0} ^ k) = Ideal.span {bm316Chart1 c}

Chart 1, k ≥ 2: (u² h₁ : u^k) = (h₁) at every point (0, c) of F — the saturation is the ideal-theoretic strict transform, with N = 2 uniformly.

theorem Hironaka.Examples.colon_bm316Chart1_of_le_two (c : ℝ) {k : ℕ} (hk : k ≤ 2) : Submodule.colon (Ideal.span {Analytic.convX ℝ 0 ^ 2 * bm316Chart1 c}) ↑(Ideal.span {Analytic.convX ℝ 0} ^ k) = Ideal.span {Analytic.convX ℝ 0 ^ (2 - k) * bm316Chart1 c}

Chart 1, k ≤ 2: (u² h₁ : u^k) = (u^(2−k) h₁).

theorem Hironaka.Examples.colon_bm316Chart1_one_lt_two (c : ℝ) : Submodule.colon (Ideal.span {Analytic.convX ℝ 0 ^ 2 * bm316Chart1 c}) ↑(Ideal.span {Analytic.convX ℝ 0} ^ 1) < Submodule.colon (Ideal.span {Analytic.convX ℝ 0 ^ 2 * bm316Chart1 c}) ↑(Ideal.span {Analytic.convX ℝ 0} ^ 2)

N = 2 is sharp: the colon by u is strictly smaller than the colon by u² (u is not a unit and h₁ ≠ 0).

noncomputable def Hironaka.Examples.bm316Chart2 : ↥(Analytic.Conv ℝ 2)

[BM97, Example 3.16], chart 2 (x = u'v', y = v'; u' = convX ℝ 0, v' = convX ℝ 1): the cofactor h₂ = u'⁴v'²(u'v'−1)² + 1 of v'² in h ∘ π.

Equations

• Hironaka.Examples.bm316Chart2 = Analytic.convX ℝ 0 ^ 4 * Analytic.convX ℝ 1 ^ 2 * (Analytic.convX ℝ 0 * Analytic.convX ℝ 1 - 1) ^ 2 + 1

theorem Hironaka.Examples.isUnit_bm316Chart2 : IsUnit bm316Chart2

h₂ is a unit of Conv ℝ 2 — its constant coefficient is 1. The series is centred at the origin of chart 2, so this is the statement at that one point of F.

theorem Hironaka.Examples.colon_bm316Chart2_of_two_le {k : ℕ} (hk : 2 ≤ k) : Submodule.colon (Ideal.span {Analytic.convX ℝ 1 ^ 2 * bm316Chart2}) ↑(Ideal.span {Analytic.convX ℝ 1} ^ k) = ⊤

Chart 2 at its origin, k ≥ 2: (v'² h₂ : v'^k) is the unit ideal — X' does not pass through the origin of this chart.

theorem Hironaka.Examples.zeroSet_bm316Chart1Fun : {p : Fin 2 → ℝ | p 0 ^ 2 * (p 0 - 1) ^ 2 + p 1 ^ 2 = 0} = {![0, 0], ![1, 0]}

[BM97, Example 3.16]: the real zero set of h₁ = u²(u−1)² + v² is {(0,0), (1,0)}.

theorem Hironaka.Examples.zeroSet_bm316Chart1Fun_inter_exceptional : {p : Fin 2 → ℝ | p 0 ^ 2 * (p 0 - 1) ^ 2 + p 1 ^ 2 = 0} ∩ {p : Fin 2 → ℝ | p 0 = 0} = {![0, 0]}

X' ∩ F = {(0,0)}, the one point of the support of X' on the exceptional divisor.

theorem Hironaka.Examples.closure_zeroSet_bm316Chart1Fun_diff_exceptional : closure ({p : Fin 2 → ℝ | p 0 ^ 2 * (p 0 - 1) ^ 2 + p 1 ^ 2 = 0} \ {p : Fin 2 → ℝ | p 0 = 0}) = {![1, 0]}

The closure of the zero set of h₁ off F is {(1,0)}. [BM97, Example 3.16] states that this is the support of the geometric strict transform X'', strictly smaller than the support {(0,0), (1,0)} of X'; that identification is the source's statement.