Example: the strict transform of a line under the blow-up of the plane at the origin

The blowing-up of the origin of 𝕜² in the local model (blowUpChartMap, blowUpCenter on Fin 2 → 𝕜, indices 0, 1) has two charts, (u, v) ↦ (u, uv) (index 0) and (s, t) ↦ (st, t) (index 1) — the charts V'_i = {ξ_i ≠ 0} of Bierstone–Milman's blowing-up [BM88, Definition 4.1]. The strict transform of the line E = {z₀ = 0} is {u₀ = 0} in the chart of index 1 and misses the chart of index 0 (Kollár: "only r − 1 of these can be written in the above form", [Kol07, Theorem 88, proof]); the exceptional divisor is {u_i = 0} in the chart of index i ([Kol07, Notation 19]: the exceptional divisor of a blow-up is the preimage of the centre). The identities are instances of the chart-level lemmas on strict transforms (strictTransform_inter_source_of_ne, strictTransform_inter_source_self) for the identity chart of the model, which is a blow-up chart over itself (isBlowUpChart_model), and of blowUpChartMap_mem_center_iff.

theorem Hironaka.Manifold.refl_mem_maximalAtlas_model {𝕜 : Type} [RCLike 𝕜] {n : ℕ} : OpenPartialHomeomorph.refl (Fin n → 𝕜) ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ (Fin n → 𝕜)

The identity chart of the model Fin n → 𝕜 lies in the maximal analytic atlas.

theorem Hironaka.Manifold.isAdaptedChart_model {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) : Manifold.IsAdaptedChart (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (Manifold.blowUpCenter σ) (OpenPartialHomeomorph.refl (Fin n → 𝕜)) σ

The identity chart of the model is adapted to the block centre blowUpCenter σ.

theorem Hironaka.Manifold.isBlowUpChart_model {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) : Manifold.IsBlowUpChart (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (Manifold.blowUpChartMap σ i) (OpenPartialHomeomorph.refl (Fin n → 𝕜)) σ i (OpenPartialHomeomorph.refl (Fin n → 𝕜))

The identity chart of the model is a blow-up chart of index i over the identity chart, for the blow-up chart map π_i itself.

theorem Hironaka.Manifold.strictTransformSet_fin_two_one {𝕜 : Type} [RCLike 𝕜] : Manifold.strictTransformSet (Manifold.blowUpChartMap (Function.Embedding.refl (Fin 2)) 1) (Manifold.blowUpCenter (Function.Embedding.refl (Fin 2))) {x : Fin 2 → 𝕜 | x 0 = 0} = {u : Fin 2 → 𝕜 | u 0 = 0}

In the chart of index 1, (s, t) ↦ (st, t), the strict transform of the line E = {z₀ = 0} is {u₀ = 0}.

theorem Hironaka.Manifold.strictTransformSet_fin_two_zero {𝕜 : Type} [RCLike 𝕜] : Manifold.strictTransformSet (Manifold.blowUpChartMap (Function.Embedding.refl (Fin 2)) 0) (Manifold.blowUpCenter (Function.Embedding.refl (Fin 2))) {x : Fin 2 → 𝕜 | x 0 = 0} = ∅

In the chart of index 0, (u, v) ↦ (u, uv), the strict transform of the line E = {z₀ = 0} is empty ([Kol07, Theorem 88, proof]).

theorem Hironaka.Manifold.preimage_center_fin_two {𝕜 : Type} [RCLike 𝕜] (i : Fin 2) : Manifold.blowUpChartMap (Function.Embedding.refl (Fin 2)) i ⁻¹' Manifold.blowUpCenter (Function.Embedding.refl (Fin 2)) = {u : Fin 2 → 𝕜 | u i = 0}

In the chart of index i the exceptional divisor is {u_i = 0} [Kol07, Notation 19].