Blow-up charts of the local model

Let 𝕜 be ℝ or ℂ. The blowing-up of an open neighbourhood V of 0 in 𝕜^m with centre {0} is covered by the charts V'_i = {ξ_i ≠ 0}, i = 1, …, m, with coordinates x_ii = x_i and x_ij = ξ_j / ξ_i for j ≠ i [BM88, Definition 4.1]; blowUpChartMap σ i is the chart map π_i in block form on 𝕜^n, the centre being the coordinate subspace {x_{σ k} = 0} cut out by an embedding σ : Fin c ↪ Fin n (the block need not consist of consecutive coordinates) and the coordinates off the block being carried along unchanged. This file adds the rest of the chart data of the local model and the pointwise unfoldings:

• blowUpChartMap_apply_scaling, blowUpChartMap_apply_ratio, blowUpChartMap_apply_off: slot σ i is the scaling variable, the block slots σ k with k ≠ i are multiplied by it, the coordinates off the block pass through;
• blowUpCenter σ is the centre {x_{σ k} = 0};
• blowUpTransition σ i k is the transition map from chart i to chart k: u'_{σ k} = u_{σ i} u_{σ k}, u'_{σ i} = 1 / u_{σ k}, u'_{σ j} = u_{σ j} / u_{σ k} for j ≠ i, k, the identity off the block (in the coordinates of the source, x_{kj} = ξ_j / ξ_k = x_{ij} / x_{ik}); its domain blowUpTransitionDomain σ i k is {u_{σ k} ≠ 0}, the whole space when i = k;
• blowUpChartInv σ i is the inverse of π_i off the hyperplane {x_{σ i} = 0}.

The identity π_k ∘ T_ik = π_i, the inverse and cocycle laws, analyticity and the compactness estimate are proved in Hironaka.Manifold.BlowUp.Transition.

def Manifold.blowUpCenter {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) : Set (Fin n → 𝕜)

The centre of the blow-up in block form: the coordinate subspace {x_{σ k} = 0}.

Equations

• Manifold.blowUpCenter σ = {x : Fin n → 𝕜 | ∀ (k : Fin c), x (σ k) = 0}

noncomputable def Manifold.blowUpTransition {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i k : Fin c) : (Fin n → 𝕜) → Fin n → 𝕜

The transition map from blow-up chart i to blow-up chart k, defined where u_{σ k} ≠ 0 (and the identity for i = k); in the coordinates of [BM88, Definition 4.1] it is x_{kj} = ξ_j / ξ_k = x_{ij} / x_{ik}.

Equations

• One or more equations did not get rendered due to their size.

def Manifold.blowUpTransitionDomain {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i k : Fin c) : Set (Fin n → 𝕜)

The domain of the transition map from chart i to chart k: {u_{σ k} ≠ 0} (the whole space for i = k).

Equations

• Manifold.blowUpTransitionDomain σ i k = if i = k then Set.univ else {u : Fin n → 𝕜 | u (σ k) ≠ 0}

@[simp]

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

theorem Manifold.blowUpChartMap_apply_ratio {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i k : Fin c} (u : Fin n → 𝕜) (hk : k ≠ i) : blowUpChartMap σ i u (σ k) = u (σ i) * u (σ k)

theorem Manifold.blowUpChartMap_apply_off {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i : Fin c} (u : Fin n → 𝕜) {j : Fin n} (hj : ∀ (k : Fin c), σ k ≠ j) : blowUpChartMap σ i u j = u j

theorem Manifold.blowUpTransition_self {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) : blowUpTransition σ i i = id

theorem Manifold.blowUpTransition_apply_k {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i k : Fin c} (u : Fin n → 𝕜) (hik : i ≠ k) : blowUpTransition σ i k u (σ k) = u (σ i) * u (σ k)

theorem Manifold.blowUpTransition_apply_i {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i k : Fin c} (u : Fin n → 𝕜) (hik : i ≠ k) : blowUpTransition σ i k u (σ i) = (u (σ k))⁻¹

theorem Manifold.blowUpTransition_apply_block {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i k : Fin c} (u : Fin n → 𝕜) (hik : i ≠ k) {l : Fin c} (hli : l ≠ i) (hlk : l ≠ k) : blowUpTransition σ i k u (σ l) = u (σ l) / u (σ k)

theorem Manifold.blowUpTransition_apply_off {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i k : Fin c} (u : Fin n → 𝕜) (hik : i ≠ k) {j : Fin n} (hj : ∀ (l : Fin c), σ l ≠ j) : blowUpTransition σ i k u j = u j

theorem Manifold.mem_blowUpTransitionDomain {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i k : Fin c} (u : Fin n → 𝕜) (hik : i ≠ k) : u ∈ blowUpTransitionDomain σ i k ↔ u (σ k) ≠ 0

theorem Manifold.blowUpTransitionDomain_self {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) : blowUpTransitionDomain σ i i = Set.univ

noncomputable def Manifold.blowUpChartInv {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) : (Fin n → 𝕜) → Fin n → 𝕜

The inverse of the chart map π_i off the hyperplane {x_{σ i} = 0}: u_{σ i} = x_{σ i}, u_{σ k} = x_{σ k} / x_{σ i} for k ≠ i, and the identity off the block (the coordinates x_ij = ξ_j / ξ_i of [BM88, Definition 4.1]).

Equations

• Manifold.blowUpChartInv σ i x j = if ∃ (k : Fin c), k ≠ i ∧ σ k = j then x j / x (σ i) else x j

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

theorem Manifold.blowUpChartInv_apply_ratio {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i k : Fin c} (x : Fin n → 𝕜) (hk : k ≠ i) : blowUpChartInv σ i x (σ k) = x (σ k) / x (σ i)

theorem Manifold.blowUpChartInv_apply_off {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i : Fin c} (x : Fin n → 𝕜) {j : Fin n} (hj : ∀ (k : Fin c), σ k ≠ j) : blowUpChartInv σ i x j = x j