Transition laws of the blow-up charts

The function-level properties of the local model of the blowing-up with centre a coordinate subspace [BM88, Definition 4.1], in block form. The chart maps π_i = blowUpChartMap σ i and the transition maps T_ik = blowUpTransition σ i k satisfy π_k ∘ T_ik = π_i, T_ki ∘ T_ik = id and the cocycle law T_kl ∘ T_ik = T_il on the transition domains {u_{σ k} ≠ 0}, which are open; the transition maps are analytic there (they are rational in the coordinates) and the chart maps are polynomial. The chart map π_i is injective off the hyperplane {u_{σ i} = 0}, with the analytic inverse blowUpChartInv σ i, π_i u lies on the centre exactly when u_{σ i} = 0, and π_i fixes the centre pointwise (BlowUpGlue.blowUpChartMap_of_mem_center). For a compact set C, the set of points u of chart i with π_i u ∈ C and all ratio coordinates of norm at most one is compact, and every point of the chart is carried by a transition into such a box, the box of the chart of a block coordinate of maximal norm; this is the estimate behind the properness of the blow-down map of the glued blowing-up (Hironaka.Manifold.BlowUp.GluedTopology). The file ends with the two charts and the transition of the blowing-up of the plane at the origin, computed explicitly.

The transition formula, the cocycle law and the compactness estimate are not stated in the source; they are elementary verifications in coordinates.

Case analysis on a coordinate index

theorem Manifold.exists_eq_or_forall_ne {n c : ℕ} (σ : Fin c ↪ Fin n) (j : Fin n) : (∃ (l : Fin c), σ l = j) ∨ ∀ (l : Fin c), σ l ≠ j

Every index j is a block index σ l or off the block.

theorem Manifold.BlowUpGlue.blowUpChartMap_of_mem_center {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} {σ : Fin c ↪ Fin n} {i : Fin c} {x : Fin n → 𝕜} (hx : x ∈ blowUpCenter σ) : blowUpChartMap σ i x = x

π_i fixes the centre pointwise.

Compatibility of the chart maps with the transitions: π_k ∘ T_ik = π_i

theorem Manifold.blowUpChartMap_blowUpTransition {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i k : Fin c} (u : Fin n → 𝕜) (hu : u ∈ blowUpTransitionDomain σ i k) : blowUpChartMap σ k (blowUpTransition σ i k u) = blowUpChartMap σ i u

Inverse and cocycle laws, openness and analyticity

theorem Manifold.blowUpTransition_mem_domain {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i k : Fin c} (u : Fin n → 𝕜) (hu : u ∈ blowUpTransitionDomain σ i k) : blowUpTransition σ i k u ∈ blowUpTransitionDomain σ k i

theorem Manifold.blowUpTransition_blowUpTransition {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i k : Fin c} (u : Fin n → 𝕜) (hu : u ∈ blowUpTransitionDomain σ i k) : blowUpTransition σ k i (blowUpTransition σ i k u) = u

The inverse law T_ki ∘ T_ik = id on the transition domain.

theorem Manifold.blowUpTransition_cocycle {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i k l : Fin c} (u : Fin n → 𝕜) (hk : u ∈ blowUpTransitionDomain σ i k) (hl : u ∈ blowUpTransitionDomain σ i l) : blowUpTransition σ i k u ∈ blowUpTransitionDomain σ k l ∧ blowUpTransition σ k l (blowUpTransition σ i k u) = blowUpTransition σ i l u

The cocycle law T_kl ∘ T_ik = T_il where both sides are defined.

theorem Manifold.isOpen_blowUpTransitionDomain {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i k : Fin c} : IsOpen (blowUpTransitionDomain σ i k)

The transition domain is open.

theorem Manifold.analyticAt_pi_of_forall {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {f : (Fin n → 𝕜) → Fin n → 𝕜} {x : Fin n → 𝕜} (h : ∀ (j : Fin n), AnalyticAt 𝕜 (fun (v : Fin n → 𝕜) => f v j) x) : AnalyticAt 𝕜 f x

A map into Fin n → 𝕜 is analytic when its coordinates are.

theorem Manifold.exists_blowUpTransition_mem_box {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i : Fin c} (u : Fin n → 𝕜) : ∃ (k : Fin c), u ∈ blowUpTransitionDomain σ i k ∧ ∀ (l : Fin c), l ≠ k → ‖blowUpTransition σ i k u (σ l)‖ ≤ 1

Every point u of chart i, on the exceptional hyperplane or not, is carried by some transition T_ik into the box {‖u'_{σ l}‖ ≤ 1, l ≠ k} of chart k: k = i when all ratio coordinates have norm at most 1, otherwise k is the index of a ratio coordinate of maximal norm. Not in the sources; the boxes cover the exceptional divisor, which gives the properness of the blow-down map.

theorem Manifold.analyticAt_apply {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (j : Fin n) (x : Fin n → 𝕜) : AnalyticAt 𝕜 (fun (v : Fin n → 𝕜) => v j) x

The coordinate projections are analytic.

theorem Manifold.analyticOnNhd_blowUpTransition {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i k : Fin c} : AnalyticOnNhd 𝕜 (blowUpTransition σ i k) (blowUpTransitionDomain σ i k)

The transition map is analytic on its domain.

theorem Manifold.contDiff_blowUpChartMap {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i : Fin c} : ContDiff 𝕜 ⊤ (blowUpChartMap σ i)

The chart map π_i is analytic (it is polynomial in the coordinates).

The exceptional set and the inverse chart map

theorem Manifold.blowUpChartMap_mem_center_iff {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i : Fin c} (u : Fin n → 𝕜) : blowUpChartMap σ i u ∈ blowUpCenter σ ↔ u (σ i) = 0

theorem Manifold.blowUpChartMap_blowUpChartInv {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i : Fin c} (x : Fin n → 𝕜) (hx : x (σ i) ≠ 0) : blowUpChartMap σ i (blowUpChartInv σ i x) = x

π_i ∘ π_i⁻¹ = id off the hyperplane {x_{σ i} = 0}.

theorem Manifold.blowUpChartInv_blowUpChartMap {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i : Fin c} (u : Fin n → 𝕜) (hu : u (σ i) ≠ 0) : blowUpChartInv σ i (blowUpChartMap σ i u) = u

π_i⁻¹ ∘ π_i = id off the exceptional hyperplane {u_{σ i} = 0}.

theorem Manifold.blowUpChartMap_injOn {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i : Fin c} : Set.InjOn (blowUpChartMap σ i) {u : Fin n → 𝕜 | u (σ i) ≠ 0}

The chart map π_i is injective off the exceptional hyperplane {u_{σ i} = 0}.

theorem Manifold.analyticOnNhd_blowUpChartInv {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i : Fin c} : AnalyticOnNhd 𝕜 (blowUpChartInv σ i) {x : Fin n → 𝕜 | x (σ i) ≠ 0}

The inverse π_i⁻¹ is analytic off the hyperplane {x_{σ i} = 0}.

The compactness estimate

theorem Manifold.isCompact_blowUpChartMap_preimage_inter_box {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i : Fin c} {C : Set (Fin n → 𝕜)} (hC : IsCompact C) : IsCompact {u : Fin n → 𝕜 | blowUpChartMap σ i u ∈ C ∧ ∀ (k : Fin c), k ≠ i → ‖u (σ k)‖ ≤ 1}

theorem Manifold.exists_mem_box_of_ne_center {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (x : Fin n → 𝕜) (hx : x ∉ blowUpCenter σ) : ∃ (i : Fin c) (u : Fin n → 𝕜), blowUpChartMap σ i u = x ∧ ∀ (k : Fin c), k ≠ i → ‖u (σ k)‖ ≤ 1

A point x off the centre is π_i u for some i and some u with ‖u_{σ k}‖ ≤ 1 for all k ≠ i, namely for i the index of a block coordinate of x of maximal norm.

The blowing-up of the plane at the origin

theorem Manifold.blowUpChartMap_fin_two_zero {𝕜 : Type} [RCLike 𝕜] (a b : 𝕜) : blowUpChartMap (Function.Embedding.refl (Fin 2)) 0 ![a, b] = ![a, a * b]

theorem Manifold.blowUpChartMap_fin_two_one {𝕜 : Type} [RCLike 𝕜] (a b : 𝕜) : blowUpChartMap (Function.Embedding.refl (Fin 2)) 1 ![a, b] = ![b * a, b]

Chart 1 of the blowing-up of the plane at the origin: (s, t) ↦ (ts, t).

theorem Manifold.blowUpTransition_fin_two {𝕜 : Type} [RCLike 𝕜] (a b : 𝕜) : blowUpTransition (Function.Embedding.refl (Fin 2)) 0 1 ![a, b] = ![b⁻¹, a * b]

The transition from chart 0 to chart 1 of the blowing-up of the plane at the origin: (u, v) ↦ (1/v, uv) on v ≠ 0.