Assembling local diffeomorphisms near a section

A map which is locally invertible near a retraction section, and induces the topology on that section, identifies a smaller neighbourhood with its image by a single partial diffeomorphism. Neither the section nor its image needs to be compact. The source can be kept inside a prescribed open set on which local invertibility is known. Nonemptiness of the ambient source is needed to define the inverse outside its target.

IsLocalDiffeomorphOn.exists_partialDiffeomorph_near_section is the smooth assembly step for normal-exponential coordinates: the section is the zero section of the normal bundle and the retraction is its bundle projection. The conclusion supplies a smooth inverse on one neighbourhood of the entire embedded submanifold.

The construction uses Topology.IsInducing.exists_injOn_neighborhood_section for global injectivity and IsLocalDiffeomorphOn.partialDiffeomorphOfInjOn for the smooth inverse.

Reference: J. M. Lee, Introduction to Smooth Manifolds, second edition, Theorem 6.24 (tubular neighbourhoods).

theorem IsLocalDiffeomorphOn.exists_partialDiffeomorph_near_section {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} {G : Type u_5} [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} {N : Type u_7} {B : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] [TopologicalSpace B] [TopologicalSpace.PseudoMetrizableSpace M] [TopologicalSpace.PseudoMetrizableSpace N] [Nonempty M] {n : WithTop ℕ∞} {f : M → N} {s : B → M} {O : Set M} (hf : IsLocalDiffeomorphOn I J n f O) (hO : IsOpen O) (hsO : Set.range s ⊆ O) (hs : Continuous s) (π : M → B) (hπ : Continuous π) (hsect : Function.LeftInverse π s) (hind : Topology.IsInducing (f ∘ s)) : ∃ (Φ : PartialDiffeomorph I J M N n), Set.range s ⊆ Φ.source ∧ Φ.source ⊆ O ∧ Φ.target = f '' Φ.source ∧ ↑Φ.toPartialEquiv = f

Local diffeomorphisms near a continuous retraction section whose image induces the base topology assemble to a partial diffeomorphism on a neighbourhood of the whole section. The source stays inside the original open domain, and the forward map is unchanged.