Functoriality and injectivity of the pull-back of lists of centres

The pull-back h^* B of a blow-up sequence is functorial in the smooth morphism h [Kol07, Definition 30, 30.1], and a surjective h determines B from h^* B; this is the uniqueness of [Kol07, Proposition 37]: pull-back along a surjective g is injective, so g^* B̄'(X) = B(X') = g^* B̄(X) forces B̄'(X) = B̄(X), and "hence the existence is a local question" [Kol07, 34]. On lists of centres:

• BlowUpSequence.liftStep_unique: a continuous map over h between the chosen blowings-up is the lift liftStep (uniqueness of lifts: two continuous maps over h agree off the exceptional divisor, which is dense, eqOn_of_comp_eq_of_dense);
• pullback_congr, pullback_id, pullback_comp (the lift of the identity is the identity, the lift of a composite is the composite of the lifts);
• noEmptyCenters_pullback_of_surjective, eraseEmpty_pullback_of_surjective (the lift of a surjective local isomorphism is surjective, surjective_blowUpLift, so preimages of nonempty centres are nonempty);
• pullback_injective_of_surjective (centres are recovered as images under the surjective lifts), eq_of_pullback_openCover.

The last two groups are proved in Hironaka.Manifold.FiniteSuccession.Functor.PullbackInj and Hironaka.Manifold.FiniteSuccession.Functor.PullbackCover.

theorem AnalyticManifold.BlowUpSequence.liftStep_unique {𝕜 : 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) {G : (Manifold.blowUp ψ₀ ⋯).carrier → (Manifold.blowUp ψ₀ hY).carrier} (hG : Continuous G) (hcomm : ∀ (q : (Manifold.blowUp ψ₀ ⋯).carrier), (Manifold.blowUpπ ψ₀ hY) (G q) = h ((Manifold.blowUpπ ψ₀ ⋯) q)) : G = ⇑(liftStep h hh hY)

Uniqueness of lifts ([Kol07, Definition 30, 30.1]): a continuous map between the chosen blowings-up over the local analytic isomorphism h is the lift liftStep h hh hY — the two agree off the exceptional divisor, where the blow-down is injective, and that set is dense.

theorem AnalyticManifold.BlowUpSequence.isLocalDiffeomorph_comp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N P : AnalyticManifold 𝕜 E} {h : AnalyticMap N M} (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {k : AnalyticMap P N} (hk : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑k) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(ContMDiffMap.comp h k)

Local analytic isomorphisms compose (Mathlib's IsLocalDiffeomorphAt.comp, pointwise).

theorem AnalyticManifold.BlowUpSequence.pullback_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) {f g : AnalyticMap N M} (hfg : f = g) (hf : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑f) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) : L.pullback f hf = L.pullback g hg

theorem AnalyticManifold.BlowUpSequence.isLocalDiffeomorph_id {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (M : AnalyticManifold 𝕜 E) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑ContMDiffMap.id

The identity is a local analytic isomorphism (Diffeomorph.refl).

theorem AnalyticManifold.BlowUpSequence.liftStep_id {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) : liftStep ContMDiffMap.id ⋯ hY = ContMDiffMap.id

The lift of the identity is the identity.

@[simp]

theorem AnalyticManifold.BlowUpSequence.pullback_id {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) : L.pullback ContMDiffMap.id ⋯ = L

[Kol07, Definition 30, 30.1] (pullback_id): the pull-back along the identity is the identity.

theorem AnalyticManifold.BlowUpSequence.liftStep_comp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N P : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (k : AnalyticMap P N) (hk : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑k) {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) : liftStep (ContMDiffMap.comp h k) ⋯ hY = ContMDiffMap.comp (liftStep h hh hY) (liftStep k hk ⋯)

The lift of a composite is the composite of the lifts (uniqueness of lifts).

theorem AnalyticManifold.BlowUpSequence.pullback_comp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N P : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (k : AnalyticMap P N) (hk : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑k) : (L.pullback h hh).pullback k hk = L.pullback (ContMDiffMap.comp h k) ⋯

[Kol07, Definition 30, 30.1] (pullback_comp): the pull-back along a composite is the composite of the pull-backs.