Transitions between the abstract blow-up charts

The blowing-up π : M' → M of a closed submanifold is characterised abstractly (IsBlowUp): over an adapted chart φ of the centre, blow-up charts Φ_i of every index exist (exists_chart) and cover π⁻¹(φ.source) (cover), each reading ψ ∘ φ ∘ π = π_i ∘ ψ ∘ Φ_i (comm) with the model chart domain as target (mem_target_iff). Nothing says directly which points of M' lie in which chart. This module derives the transition rule from the axioms — Kollár's proof of the uniqueness of blow-up sequences needs the two lifts f'(q), g'(q) to be read in one chart of Bl_Y M [Kol07, Theorem 97, proof]:

• IsBlowUpChart.mem_source_of_mem_transitionDomain: if p ∈ Φ_i.source and the chart coordinates ψ (Φ_i p) lie in the transition domain T_ik (u_{σ k} ≠ 0, or i = k), then p ∈ Φ_k.source and ψ (Φ_k p) = T_ik (ψ (Φ_i p)) — the abstract charts are glued by the transition maps of the model blow-up (blowUpTransition), the chart changes of Bierstone–Milman's description of the blowing-up [BM88, Definition 4.1].

The proof is the uniqueness of lifts (IsBlowUp.eqOn_of_comp_eq, from the density of the complement of the exceptional divisor): the candidate q ↦ Φ_k⁻¹(ψ⁻¹(T_ik(ψ(Φ_i q)))) is a continuous map over π on the open set of transverse points, so it is the identity there.

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

A point of the blow-up chart of index i whose coordinates lie in the transition domain T_ik (u_{σ k} ≠ 0, or i = k) lies in the blow-up chart of index k over the same adapted chart, with coordinates T_ik of the old ones (the chart changes of the blowing-up, [BM88, Definition 4.1]). By the uniqueness of lifts (IsBlowUp.eqOn_of_comp_eq).