Lists of centres are determined locally

The isomorphism of [Kol07, 34] is unique, so its existence is a local question, as the proof of [Kol07, Theorem 36] puts it ("(34.1) is a local property"). On lists of centres: two lists on M whose pull-backs along every member of a family of local analytic isomorphisms with covering ranges agree are equal (eq_of_pullback_cover; the form eq_of_pullback_openCover for a nonempty open cover by analytic open embeddings): the centres are recovered from their preimages, and the lifts of the family to the chosen blowing-up again have covering ranges (exists_liftStep_eq: a point over h b is in the range of the lift, by the lift of a local inverse of h at b, Hironaka.Manifold.BlowUp.Functor).

theorem AnalyticManifold.BlowUpSequence.exists_liftStep_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (p : (Manifold.blowUp ψ₀ hY).carrier) {b : N.carrier} (hb : h b = (Manifold.blowUpπ ψ₀ hY) p) : ∃ (q : (Manifold.blowUp ψ₀ ⋯).carrier), (liftStep h hh hY) q = p

A point of Bl_Y M over a point h b of the range of the local analytic isomorphism h is in the range of the lift of h (lift of a local inverse of h at b maps π'⁻¹(Φ.source) onto π⁻¹(Φ.target); the body of surjective_of_comm, without the surjectivity of h).

theorem AnalyticManifold.BlowUpSequence.eq_of_pullback_cover {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {σ : Type u} [Nonempty σ] {N : σ → AnalyticManifold 𝕜 E} (ι : (i : σ) → AnalyticMap (N i) M) (hι : ∀ (i : σ), IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(ι i)) : (∀ (x : M.carrier), ∃ (i : σ), x ∈ Set.range ⇑(ι i)) → ∀ (L L' : BlowUpSequence ψ₀ M), (∀ (i : σ), L.pullback (ι i) ⋯ = L'.pullback (ι i) ⋯) → L = L'

[Kol07, 34], the general form: two lists on M whose pull-backs along every member of a family of local analytic isomorphisms with covering ranges agree are equal.

theorem AnalyticManifold.BlowUpSequence.eq_of_pullback_openCover {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {σ : Type u} [Nonempty σ] {N : σ → AnalyticManifold 𝕜 E} (ι : (i : σ) → AnalyticMap (N i) M) (hι : ∀ (i : σ), Manifold.IsAnalyticOpenEmbedding (ι i)) (hcov : ⋃ (i : σ), Set.range ⇑(ι i) = Set.univ) {L L' : BlowUpSequence ψ₀ M} (h : ∀ (i : σ), L.pullback (ι i) ⋯ = L'.pullback (ι i) ⋯) : L = L'

[Kol07, 34] (eq_of_pullback_openCover): two lists on M that agree after pull-back to every member of a nonempty open cover by analytic open embeddings are equal.