Injective neighbourhoods of a retraction section

Let s : B → X be a continuous section of a continuous projection π : X → B. If a continuous map f : X → Y induces the topology on the section and is locally injective there, then it is injective on an open neighbourhood of the entire section. The section need not be compact or closed. The spaces X and Y are pseudometrizable.

Topology.IsInducing.exists_injOn_neighborhood_section supplies the injective neighbourhood. IsLocalHomeomorphOn.exists_isOpenEmbedding_near_section gives an open embedding when the map is a local homeomorphism near the section. Applied on the open local-invertibility locus of a normal exponential, with the bundle projection and zero section, this is the passage from local normal coordinates to globally injective tubular coordinates.

The proof uses the continuous subordinate radii of Topology.IsInducing.exists_continuous_radius_subordinate. Comparing the larger of two radii places both points in one injectivity patch. In addition to their distance from the section, control the distance of their images from the image of the section.

Reference: J. M. Lee, Introduction to Smooth Manifolds, second edition, Theorem 6.24 (shrinking in the tubular-neighbourhood theorem).

theorem Topology.IsInducing.exists_injOn_neighborhood_section {B : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace B] [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] [TopologicalSpace Y] [TopologicalSpace.PseudoMetrizableSpace Y] {f : X → Y} {s : B → X} (hind : IsInducing (f ∘ s)) (hf : Continuous f) (hs : Continuous s) (π : X → B) (hπ : Continuous π) (hsect : Function.LeftInverse π s) (hloc : ∀ (b : B), ∃ U ∈ nhds (s b), Set.InjOn f U) : ∃ (U : Set X), IsOpen U ∧ Set.range s ⊆ U ∧ Set.InjOn f U

A continuous map that induces the topology on a retraction section and is locally injective there is injective on an open neighbourhood of the whole section. No compactness or closedness of the section is required.

theorem IsLocalHomeomorphOn.exists_isOpenEmbedding_near_section {B : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace B] [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] [TopologicalSpace Y] [TopologicalSpace.PseudoMetrizableSpace Y] {f : X → Y} {s : B → X} {O : Set X} (hf : IsLocalHomeomorphOn f O) (hO : IsOpen O) (hsO : Set.range s ⊆ O) (hs : Continuous s) (π : X → B) (hπ : Continuous π) (hsect : Function.LeftInverse π s) (hind : Topology.IsInducing (f ∘ s)) : ∃ (U : Set X), IsOpen U ∧ Set.range s ⊆ U ∧ U ⊆ O ∧ Topology.IsOpenEmbedding (U.domRestrict f)

A map that is a local homeomorphism on an open neighbourhood of a continuous retraction section, and induces the topology on that section, restricts to an open embedding on a smaller open neighbourhood. The new neighbourhood stays inside the original one.