The last-stage lift of an injective local isomorphism is an open embedding

A local analytic isomorphism h : N → M lifts to the blow-up sequence pulled back along it [Kol07, Definition 30.1], pullbackLiftLast : (L.pullback h).stage r → L.stage r, with image the preimage of range h under the composite blow-down (range_pullbackLiftLast). When h is INJECTIVE — the case of an open inclusion W' ↪ W, through which the local resolutions over two opens of one piece, and over the overlap of two pieces, are compared (the open neighbourhoods A⁰_X ⊂ A_X of [Kol07, Theorem 36, proof]; the embeddings Y_{Z_i ∩ Z_j} → Y_{Z_i} of [Wlo09, §4, (3)⇒(4)]) — the lift is an open embedding and a diffeomorphism onto its open image. This module proves that in two general lemmas about any injective local analytic isomorphism (AnalyticMap.isOpenEmbedding_of_injective, AnalyticMap.diffeomorphOntoImage) and their instances at the lift (BlowUpSequence.isOpenEmbedding_pullbackLiftLast, BlowUpSequence.pullbackLiftLastDiffeomorphOntoImage, with coe_image_isLocalDiffeomorph_pullbackLiftLast identifying the image open). Not in the sources; routine.

theorem Hironaka.Manifold.AnalyticMap.isOpenEmbedding_of_injective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (f : AnalyticMap N M) (hf : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑f) (hi : Function.Injective ⇑f) : Topology.IsOpenEmbedding ⇑f

An injective local analytic isomorphism is an open embedding (Mathlib's IsLocalDiffeomorph.isOpenMap with IsOpenEmbedding.of_continuous_injective_isOpenMap).

theorem Hironaka.Manifold.AnalyticMap.image_top_subset_image {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (f : AnalyticMap N M) (hf : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑f) : ⇑f '' ↑⊤ ⊆ ↑hf.image

The image of the whole source under f is the range, inside Mathlib's image open (IsLocalDiffeomorph.image).

noncomputable def Hironaka.Manifold.AnalyticMap.diffeomorphOntoImage {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (f : AnalyticMap N M) (hf : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑f) (hi : Function.Injective ⇑f) : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N.carrier (M.restrict hf.image).carrier ⊤

An injective local analytic isomorphism is a diffeomorphism onto its image, the open hf.image = ⟨range f, _⟩ of Mathlib (IsLocalDiffeomorph.image), read as the open submanifold M.restrict hf.image: the codomain restriction of f is a bijective local diffeomorphism (AnalyticMap.isLocalDiffeomorph_restrictMap at U' = ⊤, surjective_restrictMap, IsLocalDiffeomorph.toDiffeomorphOfBijective), after the identification N.restrict ⊤ ≃ N (restrictTopDiffeomorph).

Equations

• Hironaka.Manifold.AnalyticMap.diffeomorphOntoImage f hf hi = N.restrictTopDiffeomorph.symm.trans (⋯.toDiffeomorphOfBijective ⋯)

theorem Hironaka.Manifold.AnalyticMap.coe_diffeomorphOntoImage {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {N M : AnalyticManifold 𝕜 E} (f : AnalyticMap N M) (hf : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑f) (hi : Function.Injective ⇑f) (p : N.carrier) : ↑((diffeomorphOntoImage f hf hi) p) = f p

On points the diffeomorphism onto the image is f.

theorem AnalyticManifold.BlowUpSequence.isOpenEmbedding_pullbackLiftLast {𝕜 : 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) (hi : Function.Injective ⇑h) : Topology.IsOpenEmbedding ⇑(L.pullbackLiftLast h hh)

The last-stage lift of an injective local analytic isomorphism is an open embedding (injective_pullbackLiftLast, isLocalDiffeomorph_pullbackLiftLast, AnalyticMap.isOpenEmbedding_of_injective); the lift of [Kol07, Definition 30.1].

theorem AnalyticManifold.BlowUpSequence.coe_image_isLocalDiffeomorph_pullbackLiftLast {𝕜 : 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) : ↑⋯.image = ⇑(L.toSuccession.stageMap (Fin.last L.toSuccession.length)) ⁻¹' Set.range ⇑h

The image open of the last-stage lift is the preimage of range h under the composite blow-down (range_pullbackLiftLast).

noncomputable def AnalyticManifold.BlowUpSequence.pullbackLiftLastDiffeomorphOntoImage {𝕜 : 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) (hi : Function.Injective ⇑h) : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ((L.pullback h hh).stage (Fin.last (L.pullback h hh).length)).carrier ((L.stage (Fin.last L.length)).restrict ⋯.image).carrier ⊤

The last-stage lift of an injective local analytic isomorphism, as a diffeomorphism onto its image — the open submanifold of the last stage over range h ([Kol07, Definition 30.1]). The form used when h is the open inclusion W' ↪ W of two ambient opens of a piece.

Equations

• L.pullbackLiftLastDiffeomorphOntoImage h hh hi = Hironaka.Manifold.AnalyticMap.diffeomorphOntoImage (L.pullbackLiftLast h hh) ⋯ ⋯

theorem AnalyticManifold.BlowUpSequence.coe_pullbackLiftLastDiffeomorphOntoImage {𝕜 : 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) (hi : Function.Injective ⇑h) (p : ((L.pullback h hh).stage (Fin.last (L.pullback h hh).length)).carrier) : ↑((L.pullbackLiftLastDiffeomorphOntoImage h hh hi) p) = (L.pullbackLiftLast h hh) p

On points the diffeomorphism onto the image is the lift.