Uniqueness of maps over the blow-down of a sequence of centres

A blow-up is an isomorphism off its centre, so a map into the blow-up is determined off the exceptional divisor by its composite with the blow-down. Along a whole sequence of centres L: two continuous maps into the last stage of L that agree after the composite blow-down L.stage r → M agree, provided the first pulls dense open sets back to dense sets (a local analytic isomorphism does, being an open map). The proof is the one-step uniqueness of lifts (liftStep_unique) applied stage by stage: off the exceptional divisor the blow-down is injective, the complement of the exceptional divisor is dense (IsBlowUp.dense_preimage_compl), and its preimage under the tail's blow-down is again dense because a blow-down pulls dense open sets back to dense sets (dense_preimage_blowUpπ: off the centre it is a local homeomorphism).

Consequences: the last-stage lift of a local analytic isomorphism h along L (pullbackLiftLast, the map induced by the pull-back of blow-up sequences of [Kol07, Definition 30 (30.1)]) is the unique continuous map over h pulling dense open sets back to dense sets (pullbackLiftLast_unique), and the lift of a composite is the composite of the lifts up to the identification pullback_comp of the pulled-back sequences (pullbackLiftLast_comp_apply). Not in the sources as such; these are the identities the transport of the chain of Step 2.1 (ChainTransport.lean) reads pointwise.

theorem Hironaka.Manifold.dense_preimage_blowUpπ {𝕜 : 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) {D : Set M.carrier} (hD : Dense D) : Dense (⇑(Manifold.blowUpπ ψ₀ hY) ⁻¹' D)

A blow-down pulls a dense set back to a dense set: off the centre it is a local homeomorphism onto the open set Yᶜ, and the complement of the exceptional divisor is dense (IsBlowUp.dense_preimage_compl).

theorem AnalyticManifold.BlowUpSequence.dense_preimage_stageMap_last {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) {D : Set M.carrier} : Dense D → Dense (⇑(L.toSuccession.stageMap (Fin.last L.toSuccession.length)) ⁻¹' D)

The composite blow-down of a list pulls dense sets back to dense sets (one blow-down at a time).

theorem AnalyticManifold.BlowUpSequence.eq_of_stageMap_last_comp_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) {Z : Type u} [TopologicalSpace Z] {f g : Z → (L.stage (Fin.last L.length)).carrier} : Continuous f → Continuous g → (∀ (D : Set (L.stage (Fin.last L.length)).carrier), IsOpen D → Dense D → Dense (f ⁻¹' D)) → (∀ (z : Z), (L.toSuccession.stageMap (Fin.last L.toSuccession.length)) (f z) = (L.toSuccession.stageMap (Fin.last L.toSuccession.length)) (g z)) → f = g

Two continuous maps into the last stage of L over the same map to M agree, provided the first pulls dense open sets of the last stage back to dense sets (an open map does). One blow-down at a time: the two maps into the blow-up agree off the exceptional divisor, where the blow-down is injective, and that set is dense in the source (dense_preimage_stageMap_last).

theorem AnalyticManifold.BlowUpSequence.dense_preimage_of_isLocalDiffeomorph {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {D : Set M.carrier} (hD : Dense D) : Dense (⇑h ⁻¹' D)

A local analytic isomorphism pulls dense sets back to dense sets (it is an open map).

theorem AnalyticManifold.BlowUpSequence.pullbackLiftLast_unique {𝕜 : 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) {G : ((L.pullback h hh).stage (Fin.last (L.pullback h hh).length)).carrier → (L.stage (Fin.last L.length)).carrier} (hG : Continuous G) (hGd : ∀ (D : Set (L.stage (Fin.last L.length)).carrier), IsOpen D → Dense D → Dense (G ⁻¹' D)) (hcomm : ∀ (q : ((L.pullback h hh).stage (Fin.last (L.pullback h hh).length)).carrier), (L.toSuccession.stageMap (Fin.last L.toSuccession.length)) (G q) = h (((L.pullback h hh).toSuccession.stageMap (Fin.last (L.pullback h hh).toSuccession.length)) q)) : G = ⇑(L.pullbackLiftLast h hh)

Uniqueness of the last-stage lift: a continuous map over h between the last stages of h^* L and L that pulls dense open sets back to dense sets is pullbackLiftLast.

theorem AnalyticManifold.BlowUpSequence.pullbackLiftLast_comp_apply {𝕜 : 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) {P : AnalyticManifold 𝕜 E} (k : AnalyticMap P N) (hk : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑k) (q : (((L.pullback h hh).pullback k hk).stage (Fin.last ((L.pullback h hh).pullback k hk).length)).carrier) : (L.pullbackLiftLast h hh) (((L.pullback h hh).pullbackLiftLast k hk) q) = (L.pullbackLiftLast (ContMDiffMap.comp h k) ⋯) ((stageOfEq ⋯) q)

The last-stage lift of a composite is the composite of the last-stage lifts, up to the identification pullback_comp of the pulled-back lists (uniqueness of lifts, read pointwise).