A blowing-up does not depend on the linear chart ψ

A finite succession carries one chosen linear chart ψ_i : E ≃ 𝕜^{n_i} per step (FiniteSuccession.chartAt, extracted from the monoidality witness of the step), while the restriction of a succession to a closed submanifold S ⊆ M [Kol07, Definition 30.2], given for one chart ψ, has to read every step's blowing-up in that chart. As for closed submanifolds (IsClosedSubmanifold.congr_chart), the notion "blowing-up along Y of codimension c" in the sense of [BM88, Definition 4.1] (IsBlowUp) does not depend on ψ: n = n' by dimension, and the linear automorphism L = ψ'⁻¹ ∘ ψ of E carries the adapted charts and the blow-up charts for ψ to those for ψ', with the same coordinate functions (IsBlowUp.congr_chart). Not in the sources; the proof is a routine transport of charts.

theorem Manifold.mem_image_clm_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : E ≃L[𝕜] F) (T : Set E) (w : F) : w ∈ ⇑e '' T ↔ e.symm w ∈ T

Membership in the image of a set under a continuous linear equivalence.

theorem Manifold.IsBlowUp.congr_chart {𝕜 : 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} {n' : ℕ} (ψ' : E ≃L[𝕜] Fin n' → 𝕜) (h : IsBlowUp ψ Y c π) : IsBlowUp ψ' Y c π

The notion "blowing-up along Y of codimension c" does not depend on the linear chart ψ : E ≃ 𝕜ⁿ: the adapted charts and the blow-up charts for ψ' are those for ψ composed with the linear automorphism ψ'⁻¹ ∘ ψ of E, with the same coordinate functions.