Bierstone–Milman's Example 3.16: the strict transform exceeds the closure

[BM97, Example 3.16]: for X = V(x⁴(x−1)² + y²) in the real plane, blown up at the origin, the ideal-theoretic strict transform X' has a point over the origin that does not lie in the closure of π⁻¹(|X| ∖ {0}) — the inclusion of the closure in the strict transform, which holds in general, is strict over ℝ. [BM97, Example 3.16] concludes that the geometric strict transform X'' of [BM97, Remark 3.15], the smallest closed subspace of π⁻¹(X) containing π⁻¹(X) ∖ π⁻¹(0), has |X''| = {(1, 0)} and differs from X'; this file verifies the closure statement, not the identification of |X''| with the closure. In the blow-up chart x = u, y = uv the pulled-back equation is u²·(u²(u−1)² + v²): the exceptional divisor {u = 0} is divided out once with multiplicity two, and the strict transform V(u²(u−1)² + v²) meets the exceptional divisor at the point p = (0, 0) of the x-axis direction, while |X| ∖ {0} ⊆ {(1, 0)} lifts into the single point (1, 0) of the chart. The argument:

• dvd_of_mul_pow_eq_mul_of_prime: in a domain, a u^k = b g with u prime and u ∤ g forces g ∣ a — the saturation of (u² g') by (u) lies in (g');
• not_dvd_coord_of_ne: two distinct coordinate germs vanishing at a point do not divide one another (in the Taylor series X_j is not a multiple of X_i) — hence u ∤ g';
• isAdaptedChart_origin, blowUpChartMap_zero, germ_bm316Section, bm316Ideal_cosupport_diff_subset (|X| ∖ {0} ⊆ {(1, 0)}, a real sum of squares);
• exists_mem_strictTransform_notMem_closure_bm316_of_blowUp: the witness p = Φ⁻¹(0) for the blow-up chart Φ of index 0 over the identity chart; π p = 0; the stalk of X' at p is the saturation (of finite type by saturationStalk_hasLocalGenerators), the exceptional stalk is (u), the total transform's stalk is (u²·g') (the chart formulas germMap_coord_self, germMap_coord_of_ne), u is prime (prime_coord_of_eq_zero), so the saturation lies in (g') with g'(p) = 0: p ∈ |X'|; and closure (π⁻¹(|X| ∖ {0})) ⊆ π⁻¹{(1, 0)} misses p.

The saturation of a principal ideal by a prime is [BM97, Proposition 3.13] in this case; the same example is computed in the ring of convergent power series in HironakaExamples/Saturation.lean.

theorem Hironaka.Manifold.dvd_of_mul_pow_eq_mul_of_prime {R : Type u_1} [CommRing R] [IsDomain R] {u g : R} (hu : Prime u) (hg : ¬u ∣ g) (k : ℕ) (a b : R) : a * u ^ k = b * g → g ∣ a

In a domain, if u is prime and u ∤ g, then a u^k = b g forces g ∣ a — the core of the saturation computation ([BM97, Proposition 3.13] for a principal ideal).

theorem Hironaka.Manifold.not_dvd_coord_of_ne {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {b : M} (hb : b ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {i j : Fin n} (h0 : ψ (↑φ b) i = 0) (h0' : ψ (↑φ b) j = 0) (hij : i ≠ j) : ¬Manifold.coord E ψ φ hφ hb i ∣ Manifold.coord E ψ φ hφ hb j

Two distinct coordinate germs vanishing at b do not divide one another — in the Taylor series X_j is not a multiple of X_i (its coefficient at X_j is 1, while every coefficient of X_i · w at a monomial without X_i vanishes).

theorem Hironaka.Manifold.isAdaptedChart_origin : Manifold.IsAdaptedChart (ContinuousLinearEquiv.refl ℝ (Fin 2 → ℝ)) {0} (chartAt (Fin 2 → ℝ) 0) (Function.Embedding.refl (Fin 2))

The identity chart of the plane is adapted to the origin, with both coordinates vanishing: the computation of the exists_adaptedChart field of isClosedSubmanifold_origin (RealPlane), repeated as a standalone statement.

theorem Hironaka.Manifold.blowUpChartMap_zero (σ : Fin 2 ↪ Fin 2) (i : Fin 2) : Manifold.blowUpChartMap σ i 0 = 0

The blow-up chart map of the plane sends 0 to 0.

theorem Hironaka.Manifold.germ_bm316Section (x : realPlane.carrier) : (CategoryTheory.ConcreteCategory.hom ((Manifold.structureSheaf ℝ (Fin 2 → ℝ) realPlane.carrier).presheaf.germ planeChart x ⋯)) bm316Section = Manifold.coord (Fin 2 → ℝ) (ContinuousLinearEquiv.refl ℝ (Fin 2 → ℝ)) (chartAt (Fin 2 → ℝ) 0) ⋯ ⋯ 0 ^ 4 * (Manifold.coord (Fin 2 → ℝ) (ContinuousLinearEquiv.refl ℝ (Fin 2 → ℝ)) (chartAt (Fin 2 → ℝ) 0) ⋯ ⋯ 0 - 1) ^ 2 + Manifold.coord (Fin 2 → ℝ) (ContinuousLinearEquiv.refl ℝ (Fin 2 → ℝ)) (chartAt (Fin 2 → ℝ) 0) ⋯ ⋯ 1 ^ 2

The germ of x⁴(x−1)² + y² at x in the coordinate germs of the identity chart.

theorem Hironaka.Manifold.bm316Ideal_cosupport_diff_subset : Manifold.IdealSheaf.support bm316Ideal \ {0} ⊆ {fun (i : Fin 2) => if i = 0 then 1 else 0}

[BM97, Example 3.16]: the support of V(x⁴(x−1)² + y²) off the origin lies in {(1, 0)} — a real sum of two squares vanishes iff both do.

theorem Hironaka.Manifold.exists_mem_strictTransform_notMem_closure_bm316_of_blowUp : ∃ p ∈ (Manifold.strictTransformSubspace isClosedSubmanifold_origin ⋯ bm316Ideal).support, p ∉ closure (⇑(Manifold.blowUpπ (ContinuousLinearEquiv.refl ℝ (Fin 2 → ℝ)) isClosedSubmanifold_origin) ⁻¹' (Manifold.IdealSheaf.support bm316Ideal \ {0}))

[BM97, Example 3.16]: the strict transform of V(x⁴(x−1)² + y²) ⊆ ℝ² under the blow-up of the plane at the origin has a point over the origin outside the closure of π⁻¹(|X| ∖ {0}). The point is the x-axis direction p = Φ⁻¹(0) in the blow-up chart Φ of index 0: there the total transform is (u²·g') with g' = u²(u−1)² + v², the exceptional ideal is (u), and the saturation lies in (g'), a proper ideal; the closure of π⁻¹(|X| ∖ {0}) ⊆ π⁻¹{(1, 0)} misses p since π p = 0.