Coordinate germs under the blow-down and the chart change

Three facts about the blowing-up π : Bl_Y M → M and its blow-up charts, used to show that a morphism into the blowing-up over a given map is determined by its chart coordinates (the uniqueness half of the universal property of the blowing-up):

• IsBlowUpChart.germMap_coord_off: in a blow-up chart of index i the pulled-back off-block coordinates are the off-block coordinates of the chart, z_j ∘ π = u_j (the chart formula of [BM88, Definition 4.1] in germ form; IsBlowUpChart.germMap_coord_self and IsBlowUpChart.germMap_coord_of_ne are the block cases z_{σ i} ∘ π = u_i, z_{σ k} ∘ π = u_i u_k).
• germMap_coord_transportChart: off the centre, where π agrees with a partial diffeomorphism Φ₀, the pulled-back coordinate germs of a chart φ of M are the coordinate germs of the transported chart φ ∘ Φ₀ = φ ∘ π of Bl_Y M (transportChart).
• IsBlowUp.mem_source_of_coord_ne_zero: a point of the blow-up chart Φₖ whose σ i-th coordinate is nonzero lies in the blow-up chart Φᵢ over the same adapted chart: the chart change Φᵢ⁻¹ ∘ T_{ki} ∘ Φₖ through the transition map of the local model is a continuous lift of π on that region, so it is the identity by the uniqueness of continuous lifts (IsBlowUp.eqOn_of_comp_eq).

These facts enter the comparison of the blowing-up of a manifold with the monoidal transformation of an analytic space (Hironaka.AnalyticSpace.MonoidalUnique) and the strict transform of smooth subspaces (Hironaka.Manifold.BlowUp.Transform.StrictSmooth).

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

z_j ∘ π = u_j for j off the block: the pullback of an off-centre coordinate of the adapted chart is the same coordinate of the blow-up chart (the chart formula of [BM88, Definition 4.1] in germ form).

theorem Manifold.germMap_coord_transportChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {p : M'} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] (hπ : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ π) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (Φ₀ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M' M ⊤) (hΦ₀ : Set.EqOn π (↑Φ₀.toPartialEquiv) Φ₀.source) (hp : p ∈ Φ₀.source) (hπp : π p ∈ φ.source) (j : Fin n) : (germMap π hπ p) (coord E ψ φ hφ hπp j) = coord E ψ (transportChart Φ₀.symm φ) ⋯ ⋯ j

The coordinate germs of a chart φ of M pulled back along a map π that agrees with a partial diffeomorphism Φ₀ : M' → M near p are the coordinate germs of the transported chart φ ∘ Φ₀ = φ ∘ π of M' (transportChart).

theorem Manifold.IsBlowUp.mem_source_of_same_index {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {c : ℕ} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} {p : M'} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {Y : Set M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) {Φk : OpenPartialHomeomorph M' E} (hΦk : IsBlowUpChart ψ π φ σ i Φk) (hΦi : IsBlowUpChart ψ π φ σ i Φ) (hp : p ∈ Φk.source) : p ∈ Φ.source

Two blow-up charts of the same index over the same adapted chart have the same source: Φ⁻¹ ∘ Φₖ is a continuous lift of π on Φₖ.source (IsBlowUpChart.blowDown_symm_apply), so it is the identity by the uniqueness of lifts (IsBlowUp.eqOn_of_comp_eq).

theorem Manifold.IsBlowUp.mem_source_of_coord_ne_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} {φ : OpenPartialHomeomorph M E} {c : ℕ} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} {p : M'} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {Y : Set M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) {k : Fin c} {Φk : OpenPartialHomeomorph M' E} (hΦk : IsBlowUpChart ψ π φ σ k Φk) (hΦi : IsBlowUpChart ψ π φ σ i Φ) (hp : p ∈ Φk.source) (hne : ψ (↑Φk p) (σ i) ≠ 0) : p ∈ Φ.source

A point of the blow-up chart Φₖ whose σ i-th coordinate is nonzero lies in the blow-up chart Φᵢ over the same adapted chart: the chart change through the transition map T_{ki} is a continuous lift of π on that region, hence the identity (IsBlowUp.eqOn_of_comp_eq).