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

The push-forward j_* B of a blow-up sequence B of a closed subscheme S ⊆ X to X [Kol07, Definition 30.3] identifies the stage S_i of the given sequence with the strict transform inside X_i through an isomorphism e_i : S_i ≃ S_i'; the next blow-down S_{i+1} → S_i, composed with e_i, is then a blowing-up of S_i' along e_i(Z_i). This module proves the manifold statement behind that step: a blowing-up π : M' → M along Y in the sense of [BM88, Definition 4.1] (IsBlowUp) composed with a diffeomorphism g : M ≃ N of the base is a blowing-up of N along g '' Y (IsBlowUp.diffeomorph_comp). The adapted charts of g '' Y pull back along g to adapted charts of Y (transportChart along g⁻¹), a blow-up chart of π over φ ∘ g is a blow-up chart of g ∘ π over φ (IsBlowUpChart.diffeomorph_comp), and the remaining clauses transport by composition. Likewise a closed submanifold is carried to a closed submanifold by a diffeomorphism (IsClosedSubmanifold.image_diffeomorph). Not in the sources; the proofs are routine.

theorem Manifold.image_inter_source_eq_of_diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M N ⊤) (Y : Set M) : ↑g.toPartialDiffeomorphUniv.toPartialEquiv '' (Y ∩ g.toPartialDiffeomorphUniv.source) = ⇑g '' Y ∩ g.toPartialDiffeomorphUniv.target

The image of Y under a diffeomorphism, in the form the chart transport transportChart expects.

theorem Manifold.symm_image_image_inter_source_eq_of_diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M N ⊤) (Y : Set M) : ↑g.toPartialDiffeomorphUniv.symm.toPartialEquiv '' (⇑g '' Y ∩ g.toPartialDiffeomorphUniv.symm.source) = Y ∩ g.toPartialDiffeomorphUniv.symm.target

The preimage of g '' Y under a diffeomorphism, in the form the chart transport transportChart expects.

theorem Manifold.IsClosedSubmanifold.image_diffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M N ⊤) : IsClosedSubmanifold ψ (⇑g '' Y) c

A closed submanifold is carried to a closed submanifold by a diffeomorphism: the adapted charts of g '' Y are those of Y transported along g⁻¹.

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

A blow-up chart of π over the pull-back φ ∘ g of a chart φ of N is a blow-up chart of g ∘ π over φ.

theorem Manifold.IsBlowUp.diffeomorph_comp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (h : IsBlowUp ψ Y c π) (g : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M N ⊤) : IsBlowUp ψ (⇑g '' Y) c (⇑g ∘ π)

A blowing-up of M along Y composed with a diffeomorphism g : M ≃ N of the base is a blowing-up of N along g '' Y.