The blowing-up as a quadratic transformation in charts

Bierstone–Milman's axiom (3.8)(4) requires their category of spaces to be closed under blowing-up, and a blowing-up with smooth centre to be described locally as a quadratic transformation in regular coordinate charts: on the chart U'_i of π⁻¹(U), w' = w, z'_i = z_i, z'_j = z_j / z_i [BM97, (3.8)(4) and §3, "Blowing-up", pp. 26–27]. This file identifies the three descriptions of the blowing-up in the sources with the blowing-up IsBlowUp: the chart map blowUpChartMap σ i is the formula x_i = x_{ii}, x_j = x_{ii} x_{ij} of [BM88, Definition 4.1] by definition, and IsBlowUpChart.comm says that π reads as that map in a blow-up chart over an adapted chart of the centre; unfolding it gives z_i ∘ π = u_i, z_k ∘ π = u_i · u_k, w_j ∘ π = u_j, and off the exceptional divisor (where the scaling coordinate u_i is nonzero) the chart coordinates z'_j = z_j / z_i of Bierstone–Milman are blowUpChartInv σ i. Kollár's chart y_j = x_j / x_r (j < r), y_r = x_r, y_j = x_j (j > r) [Kol07, Definition 60, (60.2)] is the same map read in Kollár's ordering of the coordinates (a permutation τ). Finally every blowing-up is covered by such charts (IsBlowUp.cover), and exists_isBlowUp realizes the axiom: for every closed submanifold there is a blowing-up, described locally as a quadratic transformation.

theorem Manifold.blowUpChart_coord_scaling {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : IsBlowUpChart ψ π φ σ i Φ) {p : M'} (hp : p ∈ Φ.source) : ψ (↑φ (π p)) (σ i) = ψ (↑Φ p) (σ i)

The quadratic transformation, scaling coordinate: z_i ∘ π = u_i on the blow-up chart of index i (IsBlowUpChart.comm unfolded; [BM97, §3, "Blowing-up"], [BM88, Definition 4.1]).

theorem Manifold.blowUpChart_coord_ratio {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : IsBlowUpChart ψ π φ σ i Φ) {p : M'} (hp : p ∈ Φ.source) {k : Fin c} (hk : k ≠ i) : ψ (↑φ (π p)) (σ k) = ψ (↑Φ p) (σ i) * ψ (↑Φ p) (σ k)

The quadratic transformation, the other centre coordinates: z_k ∘ π = u_i · u_k for k ≠ i ([BM97, §3, "Blowing-up"], [BM88, Definition 4.1]).

theorem Manifold.blowUpChart_coord_off {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : IsBlowUpChart ψ π φ σ i Φ) {p : M'} (hp : p ∈ Φ.source) {j : Fin n} (hj : ∀ (k : Fin c), σ k ≠ j) : ψ (↑φ (π p)) j = ψ (↑Φ p) j

The quadratic transformation, the off-centre coordinates: w_j ∘ π = u_j for j outside the centre indices (w' = w in [BM97, §3, "Blowing-up"]).

theorem Manifold.IsBlowUpChart.coord_scaling_ne_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} [ChartedSpace E M] (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {p : M'} (hp : p ∈ Φ.source) (hpY : π p ∉ Y) : ψ (↑Φ p) (σ i) ≠ 0

Off the exceptional divisor the scaling coordinate of the blow-up chart is nonzero.

theorem Manifold.blowUpChart_coord_ratio_div {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} [ChartedSpace E M] (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {p : M'} (hp : p ∈ Φ.source) (hpY : π p ∉ Y) {k : Fin c} (hk : k ≠ i) : ψ (↑Φ p) (σ k) = ψ (↑φ (π p)) (σ k) / ψ (↑φ (π p)) (σ i)

Off the exceptional divisor the blow-up chart coordinates are the quotients z'_j = z_j / z_i of [BM97, §3, "Blowing-up"].

theorem Manifold.blowUpChart_eq_blowUpChartInv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} [ChartedSpace E M] (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {p : M'} (hp : p ∈ Φ.source) (hpY : π p ∉ Y) : ψ (↑Φ p) = blowUpChartInv σ i (ψ (↑φ (π p)))

Off the exceptional divisor the blow-up chart is the inverse quadratic transformation blowUpChartInv σ i of the adapted chart.

theorem Manifold.blowUpChartMap_eq_kollarChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} [ChartedSpace E M] (hφ : IsAdaptedChart ψ Y φ σ) (hΦ : IsBlowUpChart ψ π φ σ i Φ) {p : M'} (hp : p ∈ Φ.source) (hpY : π p ∉ Y) (r : Fin n) (τ : Fin n ≃ Fin n) (hτr : τ r = σ i) (hlt : ∀ (j : Fin n), j < r ↔ ∃ (k : Fin c), k ≠ i ∧ τ j = σ k) : (∀ j < r, ψ (↑Φ p) (τ j) = ψ (↑φ (π p)) (τ j) / ψ (↑φ (π p)) (τ r)) ∧ ψ (↑Φ p) (τ r) = ψ (↑φ (π p)) (τ r) ∧ ∀ (j : Fin n), r < j → ψ (↑Φ p) (τ j) = ψ (↑φ (π p)) (τ j)

In Kollár's ordering τ of the coordinates (τ r = σ i, the other centre indices before r) the blow-up chart coordinates are Kollár's y_j = x_j / x_r (j < r), y_r = x_r, y_j = x_j (j > r) [Kol07, Definition 60, (60.2)]: the chart U'_i of [BM97], the chart V'_i of [BM88] and Kollár's chart are the same map.

theorem Manifold.isBlowUp_quadraticTransformation {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] (h : IsBlowUp ψ Y c π) (hφ : IsAdaptedChart ψ Y φ σ) {p : M'} (hp : π p ∈ φ.source) : ∃ (i : Fin c) (Φ : OpenPartialHomeomorph M' E), IsBlowUpChart ψ π φ σ i Φ ∧ p ∈ Φ.source ∧ ∀ q ∈ Φ.source, ψ (↑φ (π q)) = blowUpChartMap σ i (ψ (↑Φ q))

A blowing-up with smooth centre is described locally as a quadratic transformation in regular coordinate charts [BM97, (3.8)(4)]: every point over an adapted chart of the centre lies in a blow-up chart of some index on which x ∘ π = blowUpChartMap σ i ∘ u (the clauses cover and comm of IsBlowUp).

theorem Manifold.exists_isBlowUp_quadraticTransformation {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : ∃ (M' : Type u) (x : TopologicalSpace M') (x_1 : ChartedSpace E M') (x_2 : IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M') (x_3 : T2Space M') (x_4 : SecondCountableTopology M') (π : M' → M), IsBlowUp ψ Y c π ∧ ∀ (φ : OpenPartialHomeomorph M E) (σ : Fin c ↪ Fin n), IsAdaptedChart ψ Y φ σ → ∀ (p : M'), π p ∈ φ.source → ∃ (i : Fin c) (Φ : OpenPartialHomeomorph M' E), IsBlowUpChart ψ π φ σ i Φ ∧ p ∈ Φ.source ∧ ∀ q ∈ Φ.source, ψ (↑φ (π q)) = blowUpChartMap σ i (ψ (↑Φ q))

The category of analytic manifolds is closed under blowing-up with smooth centre, and the blowing-up is described locally as a quadratic transformation in the adapted charts of the centre [BM97, (3.8)(4)]; the blowing-up is the one of exists_isBlowUp.