The glued blow-down of a compatible family is proper

The blow-down σ = C.limitBlowDown Kex hemb hcomp : M̃ → M of a compatible family's direct limit (Hironaka.Resolution.Analytic.Functor.LimitFamily) is proper: Hironaka's canonical modification is a proper morphism ([Hir64, p. 155]), Włodarczyk's prin : M̃ → M is a proper bimeromorphic morphism ([Wlo09, Theorem 2.0.3, (1)]; [Wlo09, §4.1 and §4.3]), and the compatible families of the main theorems carry the clause IsProperMap F.map. Properness is local on the target (AnalyticSpace.isProperMap_of_restrictPreimage_cover): over the member M_m = relCompactOpen Kex m of the exhaustion's open cover, σ⁻¹(M_m) is the piece M'_m (limitBlowDown_preimage_relCompactOpen) and the restriction of σ is the piece's composite blow-down Π^{(m)} : M'_m → M_m, a finite composite of blow-ups, hence proper (FiniteSuccession.isProperMap_stageMap), after the homeomorphism toLimit m of the piece onto σ⁻¹(M_m). The theorem CompatibleFamily.isProperMap_limitBlowDown is stated for any C : CompatibleFamily T; the resolution family of the main theorems is an instance.

theorem Hironaka.Manifold.CompatibleFamily.isProperMap_limitBlowDown {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {T : Manifold.AnalyticTriple ψ₀ M} (C : CompatibleFamily T) (Kex : CompactExhaustion M.carrier) (hemb : ∀ (U₁ U₂ : TopologicalSpace.Opens M.carrier) (hU₁ : IsCompact (closure ↑U₁)) (hU₂ : IsCompact (closure ↑U₂)) (h : U₁ ≤ U₂), Manifold.IsAnalyticOpenEmbedding (C.endResultEmbedding hU₁ hU₂ h)) (hcomp : ∀ (U₁ U₂ : TopologicalSpace.Opens M.carrier) (hU₁ : IsCompact (closure ↑U₁)) (hU₂ : IsCompact (closure ↑U₂)) (h : U₁ ≤ U₂) (p : ((C.seqOn U₁ hU₁).stage (Fin.last (C.seqOn U₁ hU₁).length)).carrier), (C.seqOn U₂ hU₂).toSuccession.composite ((C.endResultEmbedding hU₁ hU₂ h) p) = (M.restrictLE h) ((C.seqOn U₁ hU₁).toSuccession.composite p)) (hrange : ∀ (U₁ U₂ : TopologicalSpace.Opens M.carrier) (hU₁ : IsCompact (closure ↑U₁)) (hU₂ : IsCompact (closure ↑U₂)) (h : U₁ ≤ U₂), Set.range ⇑(C.endResultEmbedding hU₁ hU₂ h) = ⇑(C.seqOn U₂ hU₂).toSuccession.composite ⁻¹' Set.range ⇑(M.restrictLE h)) : IsProperMap ⇑(C.limitBlowDown Kex hemb hcomp)

The glued blow-down σ : M̃ → M of a compatible family is proper — properness is local on the target for the open cover {M_m} (AnalyticSpace.isProperMap_of_restrictPreimage_cover), and over M_m the restriction of σ is the piece's composite blow-down (a finite composite of blow-ups, FiniteSuccession.isProperMap_stageMap) after the homeomorphism toLimit m : M'_m ≃ₜ σ⁻¹(M_m). Three properties of the end-result embeddings enter as the hypotheses hemb, hcomp, hrange.