The lifting lemma: chart changes lift to the blow-up charts

Conditions (1) and (2) of [BM88, Definition 4.1] determine the blowing-up uniquely up to an isomorphism commuting with the blow-down map. This rests on lifting a centre-preserving analytic isomorphism g between open subsets of 𝕜ⁿ to the blow-up charts, the analytic heart of the construction of the blowing-up of a manifold and of its uniqueness. This file proves that lifting lemma in coordinates.

• Coordinate division on an open set. For F analytic on an open set N and vanishing on the hyperplane {x_k = 0}, the canonical quotient coordQuot k F (F x / x_k off the hyperplane, ∂_k F x on it) is analytic on N with F = x_k · coordQuot k F. This is coordinate division on a polydisc at the origin (exists_eq_mul_coord_of_vanish) translated to each point of the hyperplane, the quotient being canonical.
• The direction vector. g_normal(π_i u) = u_{σ i} · D(u), where D_k is the canonical quotient by u_{σ i} of the normal components of g ∘ π_i. The vector D(u) is nonzero: off the exceptional hyperplane because g preserves the centre; on it because D(u) = Dg(π_i u) d with d = ∂_{u_{σ i}} π_i(u) a vector with d_{σ i} = 1, and a centre-preserving isomorphism has a derivative mapping the tangent space of the centre onto itself (tangency of Dg and Dg⁻¹, chain rule).
• The lift. Where D_k ≠ 0, G(v) = (v_{σ i} D_k(v); D_l(v)/D_k(v); g(π_i v)_off) is analytic and π_k ∘ G = g ∘ π_i; two continuous lifts through the same chart agree, by continuity from the dense set {u_{σ i} ≠ 0} where π_k is injective.
• Two block embeddings. The source chart's centre is {x_σ = 0} and the target chart's is {x_τ = 0} for two embeddings σ, τ : Fin c ↪ Fin n of the same codimension: the situation of two adapted charts of the same submanifold, whose coordinate blocks need not occupy the same slots.
• Congruence, the identity and the cocycle for the direction quotients (liftDir_congr, liftDir_self_of_eqOn_id, liftDir_of_eqOn_id, liftDir_comp), all by the same density argument, and the identification of the lift of the identity with the transition map T_ik (liftMap_eq_blowUpTransition).

These are the inputs of the gluing of the blow-up charts into the blown-up manifold (Hironaka.Manifold.BlowUp.Atlas and the modules gluing the atlas). The lifting lemma is not proved in the source; the argument above is elementary.

Coordinate division on an open set

noncomputable def Manifold.coordQuot {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (k : Fin n) (F : (Fin n → 𝕜) → 𝕜) (x : Fin n → 𝕜) : 𝕜

The canonical quotient of F by the coordinate x_k: F x / x_k off the hyperplane {x_k = 0}, the partial derivative ∂_k F x on it.

Equations

• Manifold.coordQuot k F x = if x k = 0 then (fderiv 𝕜 F x) (Pi.single k 1) else F x / x k

theorem Manifold.coordQuot_of_ne {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (k : Fin n) (F : (Fin n → 𝕜) → 𝕜) {x : Fin n → 𝕜} (hx : x k ≠ 0) : coordQuot k F x = F x / x k

The quotient off the hyperplane is the literal quotient.

theorem Manifold.coordQuot_of_eq {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (k : Fin n) (F : (Fin n → 𝕜) → 𝕜) {x : Fin n → 𝕜} (hx : x k = 0) : coordQuot k F x = (fderiv 𝕜 F x) (Pi.single k 1)

The quotient on the hyperplane is the partial derivative.

theorem Manifold.mul_coordQuot {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (k : Fin n) (F : (Fin n → 𝕜) → 𝕜) {N : Set (Fin n → 𝕜)} (h0 : ∀ x ∈ N, x k = 0 → F x = 0) {x : Fin n → 𝕜} (hx : x ∈ N) : x k * coordQuot k F x = F x

x_k · coordQuot k F x = F x for F vanishing on the hyperplane.

theorem Manifold.eq_fderiv_of_eq_mul {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (k : Fin n) {G Q : (Fin n → 𝕜) → 𝕜} {U : Set (Fin n → 𝕜)} (hU : IsOpen U) (hQ : AnalyticOnNhd 𝕜 Q U) (h : ∀ y ∈ U, G y = y k * Q y) {y : Fin n → 𝕜} (hy : y ∈ U) (hyk : y k = 0) : (fderiv 𝕜 G y) (Pi.single k 1) = Q y

If G = x_k · Q on an open set with Q analytic, then Q is the partial derivative of G on the hyperplane.

theorem Manifold.analyticOnNhd_coordQuot {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (k : Fin n) (F : (Fin n → 𝕜) → 𝕜) {N : Set (Fin n → 𝕜)} (hN : IsOpen N) (hF : AnalyticOnNhd 𝕜 F N) (h0 : ∀ x ∈ N, x k = 0 → F x = 0) : AnalyticOnNhd 𝕜 (coordQuot k F) N

Coordinate division on an open set: the canonical quotient of an analytic function vanishing on the hyperplane {x_k = 0} is analytic. The division on a polydisc at the origin is translated to each point of the hyperplane.

Tangency and the chain rule for centre-preserving maps

theorem Manifold.fderiv_apply_mem_of_preserves_center {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ τ : Fin c ↪ Fin n) {h : (Fin n → 𝕜) → Fin n → 𝕜} {U : Set (Fin n → 𝕜)} (hU : IsOpen U) (hh : AnalyticOnNhd 𝕜 h U) (hpres : ∀ y ∈ U, y ∈ blowUpCenter σ → h y ∈ blowUpCenter τ) {x : Fin n → 𝕜} (hx : x ∈ U) (hxc : x ∈ blowUpCenter σ) {t : Fin n → 𝕜} (ht : ∀ (k : Fin c), t (σ k) = 0) (k : Fin c) : (fderiv 𝕜 h x) t (τ k) = 0

A map carrying the coordinate subspace {x_σ = 0} into {x_τ = 0} near x has a derivative mapping the tangent vectors of the first into those of the second.

theorem Manifold.fderiv_comp_fderiv_eq_id {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {g g' : (Fin n → 𝕜) → Fin n → 𝕜} {V₁ V₂ : Set (Fin n → 𝕜)} (hV₁ : IsOpen V₁) (hg : AnalyticOnNhd 𝕜 g V₁) (hg' : AnalyticOnNhd 𝕜 g' V₂) (hmaps : ∀ x ∈ V₁, g x ∈ V₂) (hgg' : ∀ x ∈ V₁, g' (g x) = x) {x : Fin n → 𝕜} (hx : x ∈ V₁) : fderiv 𝕜 g' (g x) ∘SL fderiv 𝕜 g x = ContinuousLinearMap.id 𝕜 (Fin n → 𝕜)

Chain rule for a two-sided inverse on an open set: Dg'(g x) ∘ Dg(x) = id.

The direction vector and the lift

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

The normal components of g ∘ π_i in the target block τ.

Equations

• Manifold.normalComp σ τ i g k u = g (Manifold.blowUpChartMap σ i u) (τ k)

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

The direction quotient D_k = (g ∘ π_i)_{τ k} / u_{σ i}, canonical across {u_{σ i} = 0}.

Equations

• Manifold.liftDir σ τ i g k = Manifold.coordQuot (σ i) (Manifold.normalComp σ τ i g k)

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

The lift of g from chart i (block σ) to chart k (block τ): u'_{τ k} = u_{σ i} D_k, u'_{τ l} = D_l / D_k, the coordinates off the block τ those of g ∘ π_i.

Equations

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

theorem Manifold.liftMap_apply_k {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} {σ τ : Fin c ↪ Fin n} {i : Fin c} {g : (Fin n → 𝕜) → Fin n → 𝕜} (k : Fin c) (v : Fin n → 𝕜) : liftMap σ τ i g k v (τ k) = v (σ i) * liftDir σ τ i g k v

The lift at the target scaling slot: u'_{τ k} = u_{σ i} D_k.

theorem Manifold.liftMap_apply_block {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} {σ τ : Fin c ↪ Fin n} {i : Fin c} {g : (Fin n → 𝕜) → Fin n → 𝕜} {k l : Fin c} (hlk : l ≠ k) (v : Fin n → 𝕜) : liftMap σ τ i g k v (τ l) = liftDir σ τ i g l v / liftDir σ τ i g k v

The lift at a target ratio slot: u'_{τ l} = D_l / D_k.

theorem Manifold.liftMap_apply_off {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} {σ τ : Fin c ↪ Fin n} {i : Fin c} {g : (Fin n → 𝕜) → Fin n → 𝕜} (k : Fin c) (v : Fin n → 𝕜) {j : Fin n} (hj : ∀ (l : Fin c), τ l ≠ j) : liftMap σ τ i g k v j = g (blowUpChartMap σ i v) j

The lift off the target block: the coordinates of g ∘ π_i.

theorem Manifold.normalComp_eq_zero {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} {σ τ : Fin c ↪ Fin n} {i : Fin c} {g : (Fin n → 𝕜) → Fin n → 𝕜} {V₁ : Set (Fin n → 𝕜)} (hc : ∀ x ∈ V₁, x ∈ blowUpCenter σ ↔ g x ∈ blowUpCenter τ) (k : Fin c) {u : Fin n → 𝕜} (hu : blowUpChartMap σ i u ∈ V₁) (h0 : u (σ i) = 0) : normalComp σ τ i g k u = 0

The normal components of g ∘ π_i vanish on {u_{σ i} = 0}.

theorem Manifold.analyticOnNhd_normalComp {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} {σ τ : Fin c ↪ Fin n} {i : Fin c} {g : (Fin n → 𝕜) → Fin n → 𝕜} {V₁ : Set (Fin n → 𝕜)} (hg : AnalyticOnNhd 𝕜 g V₁) (k : Fin c) : AnalyticOnNhd 𝕜 (normalComp σ τ i g k) (blowUpChartMap σ i ⁻¹' V₁)

The normal components of g ∘ π_i are analytic.

theorem Manifold.analyticOnNhd_liftDir {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} {σ τ : Fin c ↪ Fin n} {i : Fin c} {g : (Fin n → 𝕜) → Fin n → 𝕜} {V₁ : Set (Fin n → 𝕜)} (hV₁ : IsOpen V₁) (hg : AnalyticOnNhd 𝕜 g V₁) (hc : ∀ x ∈ V₁, x ∈ blowUpCenter σ ↔ g x ∈ blowUpCenter τ) (k : Fin c) : AnalyticOnNhd 𝕜 (liftDir σ τ i g k) (blowUpChartMap σ i ⁻¹' V₁)

The direction quotients are analytic on π_i⁻¹(V₁).

theorem Manifold.mul_liftDir {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} {σ τ : Fin c ↪ Fin n} {i : Fin c} {g : (Fin n → 𝕜) → Fin n → 𝕜} {V₁ : Set (Fin n → 𝕜)} (hc : ∀ x ∈ V₁, x ∈ blowUpCenter σ ↔ g x ∈ blowUpCenter τ) (k : Fin c) {u : Fin n → 𝕜} (hu : blowUpChartMap σ i u ∈ V₁) : u (σ i) * liftDir σ τ i g k u = g (blowUpChartMap σ i u) (τ k)

u_{σ i} · D_k(u) = (g ∘ π_i)(u)_{τ k}.

theorem Manifold.exists_liftDir_ne_zero {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} {σ τ : Fin c ↪ Fin n} {i : Fin c} {g : (Fin n → 𝕜) → Fin n → 𝕜} {V₁ V₂ : Set (Fin n → 𝕜)} (hV₁ : IsOpen V₁) (hg : AnalyticOnNhd 𝕜 g V₁) (hc : ∀ x ∈ V₁, x ∈ blowUpCenter σ ↔ g x ∈ blowUpCenter τ) (hV₂ : IsOpen V₂) {g' : (Fin n → 𝕜) → Fin n → 𝕜} (hg₁ : Set.BijOn g V₁ V₂) (hg' : AnalyticOnNhd 𝕜 g' V₂) (hgg' : ∀ x ∈ V₁, g' (g x) = x) {u : Fin n → 𝕜} (hu : blowUpChartMap σ i u ∈ V₁) : ∃ (k : Fin c), liftDir σ τ i g k u ≠ 0

The direction vector is nonzero: some D_k(u) ≠ 0.

theorem Manifold.blowUpChartMap_liftMap {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} {σ τ : Fin c ↪ Fin n} {i : Fin c} {g : (Fin n → 𝕜) → Fin n → 𝕜} {V₁ : Set (Fin n → 𝕜)} (hc : ∀ x ∈ V₁, x ∈ blowUpCenter σ ↔ g x ∈ blowUpCenter τ) (k : Fin c) {v : Fin n → 𝕜} (hv : blowUpChartMap σ i v ∈ V₁) (hk : liftDir σ τ i g k v ≠ 0) : blowUpChartMap τ k (liftMap σ τ i g k v) = g (blowUpChartMap σ i v)

The lift commutes with the blow-down: π_k ∘ G = g ∘ π_i where D_k ≠ 0.

theorem Manifold.analyticOnNhd_liftMap {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} {σ τ : Fin c ↪ Fin n} {i : Fin c} {g : (Fin n → 𝕜) → Fin n → 𝕜} {V₁ : Set (Fin n → 𝕜)} (hV₁ : IsOpen V₁) (hg : AnalyticOnNhd 𝕜 g V₁) (hc : ∀ x ∈ V₁, x ∈ blowUpCenter σ ↔ g x ∈ blowUpCenter τ) (k : Fin c) : AnalyticOnNhd 𝕜 (liftMap σ τ i g k) (blowUpChartMap σ i ⁻¹' V₁ ∩ {v : Fin n → 𝕜 | liftDir σ τ i g k v ≠ 0})

The lift is analytic where D_k ≠ 0.

theorem Manifold.exists_lift_blowUpChartMap {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} {σ τ : Fin c ↪ Fin n} {i : Fin c} {g : (Fin n → 𝕜) → Fin n → 𝕜} {V₁ V₂ : Set (Fin n → 𝕜)} (hV₁ : IsOpen V₁) (hg : AnalyticOnNhd 𝕜 g V₁) (hc : ∀ x ∈ V₁, x ∈ blowUpCenter σ ↔ g x ∈ blowUpCenter τ) (hV₂ : IsOpen V₂) {g' : (Fin n → 𝕜) → Fin n → 𝕜} (hg₁ : Set.BijOn g V₁ V₂) (hg' : AnalyticOnNhd 𝕜 g' V₂) (hgg' : ∀ x ∈ V₁, g' (g x) = x) {u : Fin n → 𝕜} (hu : blowUpChartMap σ i u ∈ V₁) : ∃ (k : Fin c) (N : Set (Fin n → 𝕜)) (G : (Fin n → 𝕜) → Fin n → 𝕜), IsOpen N ∧ u ∈ N ∧ AnalyticOnNhd 𝕜 G N ∧ ∀ v ∈ N, blowUpChartMap τ k (G v) = g (blowUpChartMap σ i v)

The lifting lemma, local form: every point of π_i⁻¹(V₁) has a neighbourhood on which g ∘ π_i factors analytically through some chart k of the target block. This is the analytic content of the uniqueness clause of [BM88, Definition 4.1].

Uniqueness of lifts by density

theorem Manifold.subset_closure_ne {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i : Fin c} {N : Set (Fin n → 𝕜)} (hN : IsOpen N) : N ⊆ closure {v : Fin n → 𝕜 | v ∈ N ∧ v (σ i) ≠ 0}

The complement of the exceptional hyperplane is dense in every open set: a point with v_{σ i} = 0 is a limit of points v + s e_{σ i}, s ≠ 0.

theorem Manifold.eqOn_of_lift_blowUpChartMap {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) {i k : Fin c} {τ : Fin c ↪ Fin n} {N : Set (Fin n → 𝕜)} (hN : IsOpen N) {g G₁ G₂ : (Fin n → 𝕜) → Fin n → 𝕜} (h₁ : ContinuousOn G₁ N) (h₂ : ContinuousOn G₂ N) (hG₁ : ∀ v ∈ N, blowUpChartMap τ k (G₁ v) = g (blowUpChartMap σ i v)) (hG₂ : ∀ v ∈ N, blowUpChartMap τ k (G₂ v) = g (blowUpChartMap σ i v)) (hinj : ∀ v ∈ N, v (σ i) ≠ 0 → g (blowUpChartMap σ i v) ∉ blowUpCenter τ) : Set.EqOn G₁ G₂ N

Uniqueness of the lift: two continuous lifts of g through chart k on an open set agree. They agree off the exceptional hyperplane, where π_k is injective (the lifts have G_v(τ k) ≠ 0 there because g carries the points off the centre off the centre), and the complement is dense.

Congruence, the identity and the cocycle for the direction quotients

theorem Manifold.liftDir_congr {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} {σ τ : Fin c ↪ Fin n} {i : Fin c} {g₁ g₂ : (Fin n → 𝕜) → Fin n → 𝕜} {V : Set (Fin n → 𝕜)} (hV : IsOpen V) (h : ∀ x ∈ V, g₁ x = g₂ x) (k : Fin c) {u : Fin n → 𝕜} (hu : blowUpChartMap σ i u ∈ V) : liftDir σ τ i g₁ k u = liftDir σ τ i g₂ k u

The direction quotients depend on g only near π_i u.

theorem Manifold.liftMap_congr {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} {σ τ : Fin c ↪ Fin n} {i : Fin c} {g₁ g₂ : (Fin n → 𝕜) → Fin n → 𝕜} {V : Set (Fin n → 𝕜)} (hV : IsOpen V) (h : ∀ x ∈ V, g₁ x = g₂ x) (k : Fin c) {v : Fin n → 𝕜} (hv : blowUpChartMap σ i v ∈ V) : liftMap σ τ i g₁ k v = liftMap σ τ i g₂ k v

The lift depends on g only near π_i v.

theorem Manifold.analyticOnNhd_of_eqOn_id {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {g : (Fin n → 𝕜) → Fin n → 𝕜} {V : Set (Fin n → 𝕜)} (hV : IsOpen V) (hid : ∀ x ∈ V, g x = x) : AnalyticOnNhd 𝕜 g V

A map equal to the identity on an open set is analytic there.

theorem Manifold.mem_center_iff_of_eqOn_id {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} {σ : Fin c ↪ Fin n} {g : (Fin n → 𝕜) → Fin n → 𝕜} {V : Set (Fin n → 𝕜)} (hid : ∀ x ∈ V, g x = x) (x : Fin n → 𝕜) : x ∈ V → (x ∈ blowUpCenter σ ↔ g x ∈ blowUpCenter σ)

A map equal to the identity on an open set preserves the centre there.

theorem Manifold.liftDir_self_of_eqOn_id {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} {σ : Fin c ↪ Fin n} {i : Fin c} {g : (Fin n → 𝕜) → Fin n → 𝕜} {V : Set (Fin n → 𝕜)} (hV : IsOpen V) (hid : ∀ x ∈ V, g x = x) {u : Fin n → 𝕜} (hu : blowUpChartMap σ i u ∈ V) : liftDir σ σ i g i u = 1

Where g is the identity, D_i = 1.

theorem Manifold.liftDir_of_eqOn_id {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} {σ : Fin c ↪ Fin n} {i : Fin c} {g : (Fin n → 𝕜) → Fin n → 𝕜} {V : Set (Fin n → 𝕜)} (hV : IsOpen V) (hid : ∀ x ∈ V, g x = x) {k : Fin c} (hk : k ≠ i) {u : Fin n → 𝕜} (hu : blowUpChartMap σ i u ∈ V) : liftDir σ σ i g k u = u (σ k)

Where g is the identity, D_k = u_{σ k} for k ≠ i.

theorem Manifold.liftMap_eq_blowUpTransition {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} {σ : Fin c ↪ Fin n} {i : Fin c} {g : (Fin n → 𝕜) → Fin n → 𝕜} {V : Set (Fin n → 𝕜)} (hV : IsOpen V) (hid : ∀ x ∈ V, g x = x) (k : Fin c) {u : Fin n → 𝕜} (hu : blowUpChartMap σ i u ∈ V) (hk : liftDir σ σ i g k u ≠ 0) : liftMap σ σ i g k u = blowUpTransition σ i k u

The lift of (a map equal to) the identity from chart i to chart k is the transition map T_ik of Hironaka.Manifold.BlowUp.Charts.

theorem Manifold.liftDir_comp {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} {σ τ ρ : Fin c ↪ Fin n} {i : Fin c} {g : (Fin n → 𝕜) → Fin n → 𝕜} {V : Set (Fin n → 𝕜)} {g' : (Fin n → 𝕜) → Fin n → 𝕜} {W : Set (Fin n → 𝕜)} (hV : IsOpen V) (hg : AnalyticOnNhd 𝕜 g V) (hc : ∀ x ∈ V, x ∈ blowUpCenter σ ↔ g x ∈ blowUpCenter τ) (hW : IsOpen W) (hg' : AnalyticOnNhd 𝕜 g' W) (hc' : ∀ x ∈ W, x ∈ blowUpCenter τ ↔ g' x ∈ blowUpCenter ρ) (hmaps : ∀ x ∈ V, g x ∈ W) (k l : Fin c) {u : Fin n → 𝕜} (hu : blowUpChartMap σ i u ∈ V) (hk : liftDir σ τ i g k u ≠ 0) : liftDir σ ρ i (g' ∘ g) l u = liftDir σ τ i g k u * liftDir τ ρ k g' l (liftMap σ τ i g k u)

The cocycle of the direction quotients: for g followed by g', D^{g' ∘ g}_l(u) = D^g_k(u) · D^{g'}_l(G_k u) with G_k the lift of g to chart k.