Deleting empty blow-ups commutes with pull-back and push-forward, up to a final deletion

eraseEmpty_pullback deletes empty blow-ups before or after a surjective local analytic isomorphism with the same result. Along a non-surjective local isomorphism the pull-back may create new empty centres (a nonempty centre with empty preimage), so both sides must be cleaned at the end:

• BlowUpSequence.eraseEmpty_pullback_eraseEmpty: (L.eraseEmpty.pullback h hh).eraseEmpty = (L.pullback h hh).eraseEmpty for every local analytic isomorphism h ([Kol07, 34.1]);
• BlowUpSequence.eraseEmpty_pushforward_eraseEmpty: ((L.eraseEmpty).pushforward hS).eraseEmpty = (L.pushforward hS).eraseEmpty ([Kol07, Definition 30, 30.3]): the push-forward of an empty centre is empty, and the push-forward from the next stage is, along the isomorphism of the empty blowing-up, the push-forward from the given stage (pushforwardAux_pullback with the identification of the empty blowing-up with its base, IsPullbackStage for the empty centre).

The counterpart for schemes is AlgebraicGeometry.eraseEmpty_pullback_eraseEmpty' of Hironaka.Scheme.BlowUpSequence.EraseEmptyTransport. These are used for the non-surjective bullet of [Kol07, 34.1] for the functors built by descent.

Pull-back

theorem AnalyticManifold.BlowUpSequence.eraseEmpty_pullback_eraseEmpty {𝕜 : 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) : (L.eraseEmpty.pullback h hh).eraseEmpty = (L.pullback h hh).eraseEmpty

[Kol07, 34.1] along any local analytic isomorphism h: deleting the empty blow-ups of L and then pulling back, or pulling back first, give the same list after a final deletion of empty blow-ups — a nonempty centre may have an empty preimage, which the final deletion removes. The counterpart for schemes is AlgebraicGeometry.eraseEmpty_pullback_eraseEmpty', the same statement for blow-up sequences of schemes.

Push-forward

theorem AnalyticManifold.BlowUpSequence.imageVal_image_eq_empty_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {Tᵢ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : Manifold.PushforwardStage ψ s Tᵢ) (Z : Set Tᵢ.carrier) : ⋯.imageVal (⇑P.iso '' Z) = ∅ ↔ Z = ∅

The pushed-forward centre is empty iff the centre is.

theorem AnalyticManifold.BlowUpSequence.isPullbackStage_emptyBlowUp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {Tᵢ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : Manifold.PushforwardStage ψ s Tᵢ) {Z : Set Tᵢ.carrier} {c : ℕ} (hZ : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) (hZ₀ : Z = ∅) : (P.blowUpStep hZ ⋯).IsPullbackStage P (emptyBlowUpDiffeomorph ⋯ ⋯).symm.toAnalyticMap (emptyBlowUpDiffeomorph hZ hZ₀).symm.toAnalyticMap

The identification of the blowing-up along an empty pushed-forward centre with the stage.

theorem AnalyticManifold.BlowUpSequence.eraseEmpty_pushforwardAux_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {Tᵢ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : Manifold.PushforwardStage ψ s Tᵢ) (L : BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Tᵢ) : (pushforwardAux P L.eraseEmpty).eraseEmpty = (pushforwardAux P L).eraseEmpty

[Kol07, Definition 30, 30.3] with 34.1: the push-forward of a list with its empty blow-ups deleted has, after a final deletion, the empty blow-ups of the push-forward deleted — by induction through pushforwardAux, the empty first centre pushing forward to an empty centre and the push-forward from the next stage being the push-forward from the given stage along the isomorphism of the empty blowing-up (pushforwardAux_pullback).

theorem AnalyticManifold.BlowUpSequence.eraseEmpty_pushforward_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S s) (L : BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) hS.toAnalyticManifold) : (pushforward hS L.eraseEmpty).eraseEmpty = (pushforward hS L).eraseEmpty

Deleting empty blow-ups commutes with the push-forward along a closed submanifold ([Kol07, Definition 30, 30.3]) up to a final deletion: ((L.eraseEmpty).pushforward hS).eraseEmpty = (L.pushforward hS).eraseEmpty.