Pull-back along surjective local analytic isomorphisms: empty centres and injectivity

A good blow-up sequence functor should commute with smooth surjections [Kol07, 34.1]: the pull-back along a surjective local analytic isomorphism of a list without empty centres has none (the centres are preimages of nonempty sets under surjective lifts, surjective_blowUpLift), so eraseEmpty changes nothing. The uniqueness of [Kol07, Proposition 37] (g^* B̄'(X) = B(X') = g^* B̄(X) forces B̄'(X) = B̄(X), by [Kol07, Definition 30, 30.1]): pull-back along a surjective local analytic isomorphism is injective on lists of centres (the centres are recovered as images, and the lifts are again surjective).

theorem AnalyticManifold.BlowUpSequence.surjective_liftStep {𝕜 : 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) (hs : Function.Surjective ⇑h) : Function.Surjective ⇑(liftStep h hh hY)

[Kol07, Definition 30, 30.1]: the lift of a surjective local analytic isomorphism is surjective (surjective_blowUpLift).

theorem AnalyticManifold.BlowUpSequence.noEmptyCenters_pullback_of_surjective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) : Function.Surjective ⇑h → L.NoEmptyCenters → (L.pullback h hh).NoEmptyCenters

The pull-back along a surjective local analytic isomorphism of a list without empty centres has no empty centre.

theorem AnalyticManifold.BlowUpSequence.eraseEmpty_pullback_of_surjective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (hL : L.NoEmptyCenters) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (hs : Function.Surjective ⇑h) : (L.pullback h hh).eraseEmpty = L.pullback h hh

[Kol07, 34.1] (eraseEmpty_pullback_of_surjective): deleting the empty blow-ups of the pull-back along a surjective local analytic isomorphism changes nothing.

theorem AnalyticManifold.BlowUpSequence.pullback_injective_of_surjective {𝕜 : 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) : Function.Surjective ⇑h → ∀ (L L' : BlowUpSequence ψ₀ M), L.pullback h hh = L'.pullback h hh → L = L'

[Kol07, Proposition 37]: pull-back along a surjective local analytic isomorphism is injective on lists of centres.