Transport of a blowing-up along a diffeomorphism of the source

Kollár identifies the stage S_{i+1} := Bl_{Z_i ∩ S_i} S_i of a restricted blow-up sequence with the birational transform of S_i [Kol07, Definition 30.2]. Once the strict transform S' of a closed submanifold S under a blowing-up along Y ⊆ S is identified with the blowing-up of S along Y by a diffeomorphism g : S' → Bl_Y S over S, the restricted blow-down π|_{S'} = blowUpπ ∘ g is itself a blowing-up in the sense of [BM88, Definition 4.1] (IsBlowUp). This module proves the transport statement used there: the six clauses of IsBlowUp transport along a diffeomorphism of the source, analyticity, properness, the isomorphism off the centre and the bijection by composition, the blow-up charts by pre-composition with g (transportChart along g⁻¹, which keeps the target and the chart relations). Nothing here is specific to submanifolds. Not in the sources; the proof is routine.

theorem Manifold.IsBlowUpChart.comp_diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N] {π : M' → M} {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hΦ : IsBlowUpChart ψ π φ σ i Φ) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N M' ⊤) : IsBlowUpChart ψ (π ∘ ⇑g) φ σ i (transportChart g.toPartialDiffeomorphUniv.symm Φ)

A blow-up chart of π pre-composed with a diffeomorphism g : N → M' is a blow-up chart of π ∘ g over the same adapted chart, with the same target.

theorem Manifold.IsBlowUp.comp_diffeomorph {𝕜 : 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'] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N] [T2Space N] [SecondCountableTopology N] {π : M' → M} (h : IsBlowUp ψ Y c π) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N M' ⊤) : IsBlowUp ψ Y c (π ∘ ⇑g)

A blowing-up composed with a diffeomorphism of its source is a blowing-up with the same centre.