The compatibility clause and the end-result embedding of a compatible family

[Wlo09, Theorem 2.0.3, (4)] for every compatible family: for relatively compact opens U₁ ≤ U₂ the restriction of the succession over U₂ is an extension ([Wlo09, Definition 3.2.6]) of the succession over U₁. Indeed compat says the value on U₁ is the value on U₂ pulled back along the open inclusion with the empty blow-ups erased; the restriction is stage-wise isomorphic to that pull-back (isExtensionOf_restrict_toSuccession_of_pullback), which is an extension of its cleaned list (isExtensionOf_toSuccession_eraseEmpty). By the second clause of [Kol07, 34.1] and [Wlo09, Theorem 3.5.1, (2)], the end-result embedding endResultEmbedding is an analytic open embedding over M onto the preimage of U₁, functorial and the identity on U₁ ≤ U₁, from the last-stage lemmas isLocalDiffeomorph_pullbackLiftLast, injective_pullbackLiftLast, stageMap_last_pullbackLiftLast, range_pullbackLiftLast, stageMap_last_eraseEmptyLast, stageMap_last_stageOfEq and eq_of_stageMap_last_comp_eq.

theorem Hironaka.Manifold.CompatibleFamily.isExtensionOf_restrict_seqOn {𝕜 : 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) (U₁ U₂ : TopologicalSpace.Opens M.carrier) (hU₁ : IsCompact (closure ↑U₁)) (hU₂ : IsCompact (closure ↑U₂)) (h : U₁ ≤ U₂) : ((C.seqOn U₂ hU₂).toSuccession.restrict h).IsExtensionOf (C.seqOn U₁ hU₁).toSuccession

For a compatible family and relatively compact opens U₁ ≤ U₂, the restriction to U₁ of the succession over U₂ is an extension of the succession over U₁: the clause isExtensionOf_restrict of the extension-compatible families, for every compatible family.

theorem Hironaka.Manifold.CompatibleFamily.isLocalDiffeomorph_endResultEmbedding {𝕜 : 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) {U₁ U₂ : TopologicalSpace.Opens M.carrier} (hU₁ : IsCompact (closure ↑U₁)) (hU₂ : IsCompact (closure ↑U₂)) (h : U₁ ≤ U₂) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(C.endResultEmbedding hU₁ hU₂ h)

The end-result embedding is a local analytic isomorphism (a composite of the last-stage lift of the open inclusion and two diffeomorphisms).

theorem Hironaka.Manifold.CompatibleFamily.isAnalyticOpenEmbedding_endResultEmbedding {𝕜 : 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) {U₁ U₂ : TopologicalSpace.Opens M.carrier} (hU₁ : IsCompact (closure ↑U₁)) (hU₂ : IsCompact (closure ↑U₂)) (h : U₁ ≤ U₂) : Manifold.IsAnalyticOpenEmbedding (C.endResultEmbedding hU₁ hU₂ h)

The embedding of end results is an analytic open embedding (Kollár's open immersion): a local analytic isomorphism, injective as the last-stage lift of the injective open inclusion after two diffeomorphisms.

theorem Hironaka.Manifold.CompatibleFamily.composite_endResultEmbedding {𝕜 : 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) {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)

The end-result embedding is OVER M — the composite blow-down of U₂'s end result after the embedding is the inclusion U₁ ⊆ U₂ after the composite blow-down of U₁'s end result (stageMap_last_pullbackLiftLast, stageMap_last_eraseEmptyLast, stageMap_last_stageOfEq).

theorem Hironaka.Manifold.CompatibleFamily.range_endResultEmbedding {𝕜 : 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) {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)

The image of the embedding of end results is the preimage of U₁ under the composite blow-down of U₂'s end result (range_pullbackLiftLast; the two diffeomorphisms are onto).

theorem Hironaka.Manifold.CompatibleFamily.endResultEmbedding_comp {𝕜 : 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) {U₁ U₂ : TopologicalSpace.Opens M.carrier} (hU₁ : IsCompact (closure ↑U₁)) (hU₂ : IsCompact (closure ↑U₂)) (h : U₁ ≤ U₂) {U₃ : TopologicalSpace.Opens M.carrier} (hU₃ : IsCompact (closure ↑U₃)) (h₂₃ : U₂ ≤ U₃) (p : ((C.seqOn U₁ hU₁).stage (Fin.last (C.seqOn U₁ hU₁).length)).carrier) : (C.endResultEmbedding hU₂ hU₃ h₂₃) ((C.endResultEmbedding hU₁ hU₂ h) p) = (C.endResultEmbedding hU₁ hU₃ ⋯) p

The embeddings compose — emb₂₃ ∘ emb₁₂ = emb₁₃ for U₁ ≤ U₂ ≤ U₃ (uniqueness of maps over M, eq_of_stageMap_last_comp_eq: both sides are open maps over M).

theorem Hironaka.Manifold.CompatibleFamily.endResultEmbedding_self {𝕜 : 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) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) (p : ((C.seqOn U hU).stage (Fin.last (C.seqOn U hU).length)).carrier) : (C.endResultEmbedding hU hU ⋯) p = p

The embedding of an open into itself is the identity, emb₁₁ = id (eq_of_stageMap_last_comp_eq against id).