Deleting empty blow-ups commutes with pull-back along a surjective local isomorphism

The second bullet of [Kol07, 34.1] for the functor descended along a cover: the value of the globalised functor on an open embedding h is read after pull-back along the surjective cover g₂ of the source, and (h^* B(T)).eraseEmpty pulled back along g₂ must be (g₂^* h^* B(T)).eraseEmpty; so deleting empty blow-ups commutes with pull-back along a surjective local analytic isomorphism (eraseEmpty_pullback): a centre is empty iff its preimage under a surjection is, and the transport of the cleaned tail along the analytic isomorphism Bl_∅ M ≃ M of an empty blowing-up commutes with the pull-back because that transport is itself a pull-back. The latter is map_eq_pullback_symm: the transport of a list along a diffeomorphism φ : A ≃ B (BlowUpSequence.map, defined through IsClosedSubmanifold.image_diffeomorph and the lifts liftDiffeomorph) is its pull-back along φ⁻¹, the two lifts to the blowings-up being the same map over φ⁻¹ (liftStep_unique) once the centres φ(Y) and (φ⁻¹)⁻¹(Y) are identified (cons_congr_heq, heq_pullback_of_heq: the only place where two lists on the blowings-up of propositionally equal centres are compared, by substitution of the set).

Comparing lists on the blowings-up of propositionally equal centres

theorem AnalyticManifold.BlowUpSequence.cons_congr_heq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y₁ Y₂ : Set M.carrier} {c : ℕ} (e : Y₁ = Y₂) (h₁ : Manifold.IsClosedSubmanifold ψ₀ Y₁ c) (h₂ : Manifold.IsClosedSubmanifold ψ₀ Y₂ c) (r₁ : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ h₁)) (r₂ : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ h₂)) (hr : r₁ ≍ r₂) : cons h₁ r₁ = cons h₂ r₂

Two cons with propositionally equal centres and heterogeneously equal tails are equal.

theorem AnalyticManifold.BlowUpSequence.heq_pullback_of_heq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M A : AnalyticManifold 𝕜 E} {Y₁ Y₂ : Set M.carrier} {c : ℕ} (e : Y₁ = Y₂) (h₁ : Manifold.IsClosedSubmanifold ψ₀ Y₁ c) (h₂ : Manifold.IsClosedSubmanifold ψ₀ Y₂ c) (Z : BlowUpSequence ψ₀ A) (f₁ : AnalyticMap (Manifold.blowUp ψ₀ h₁) A) (f₂ : AnalyticMap (Manifold.blowUp ψ₀ h₂) A) (hf₁ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑f₁) (hf₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑f₂) (hf : f₁ ≍ f₂) : Z.pullback f₁ hf₁ ≍ Z.pullback f₂ hf₂

Pull-backs of a list along heterogeneously equal maps out of the blowings-up of propositionally equal centres are heterogeneously equal.

theorem AnalyticManifold.BlowUpSequence.heq_liftStep_of_forall {𝕜 : 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) {S : Set N.carrier} (hS : Manifold.IsClosedSubmanifold ψ₀ S c) (e : S = ⇑h ⁻¹' Y) (G : AnalyticMap (Manifold.blowUp ψ₀ hS) (Manifold.blowUp ψ₀ hY)) (hcomm : ∀ (q : (Manifold.blowUp ψ₀ hS).carrier), (Manifold.blowUpπ ψ₀ hY) (G q) = h ((Manifold.blowUpπ ψ₀ hS) q)) : G ≍ liftStep h hh hY

A map over h from the blowing-up of a centre equal to h⁻¹(Y) to the blowing-up of Y is the lift liftStep (liftStep_unique, up to the identification of the centres).

The transport along a diffeomorphism is a pull-back

@[reducible, inline]

abbrev Diffeomorph.toAnalyticMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {A B : AnalyticManifold 𝕜 E} (φ : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) A.carrier B.carrier ⊤) : AnalyticMap A B

The diffeomorphism φ : A ≃ B as an analytic map.

Equations

• φ.toAnalyticMap = ⟨⇑φ, ⋯⟩

theorem AnalyticManifold.BlowUpSequence.heq_liftDiffeomorph_symm {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {A B : AnalyticManifold 𝕜 E} (φ : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) A.carrier B.carrier ⊤) {Y : Set A.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) : (liftDiffeomorph φ hY).symm.toAnalyticMap ≍ liftStep φ.symm.toAnalyticMap ⋯ hY

The inverse of the lift of φ : A ≃ B to the blowings-up (liftDiffeomorph) is the pull-back lift of φ⁻¹, the centres φ(Y) and (φ⁻¹)⁻¹(Y) identified.

theorem AnalyticManifold.BlowUpSequence.map_eq_pullback_symm {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {A B : AnalyticManifold 𝕜 E} (Z : BlowUpSequence ψ₀ A) (φ : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) A.carrier B.carrier ⊤) : map φ Z = Z.pullback φ.symm.toAnalyticMap ⋯

The transport of a list along a diffeomorphism φ : A ≃ B (map) is its pull-back along φ⁻¹.

eraseEmpty commutes with surjective pull-back

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

[Kol07, 34.1] for a surjective local analytic isomorphism g: deleting the empty blow-ups commutes with the pull-back along g — a centre is empty iff its preimage is, and the transport of the cleaned tail along the isomorphism of an empty blowing-up is a pull-back (map_eq_pullback_symm), so the two sides are pull-backs of the cleaned tail along the two composites π⁻¹ ∘ g and g₁ ∘ π'⁻¹, equal by the lift identity π ∘ g₁ = g ∘ π'.