feat(analysis/calculus/inverse): a map that has an invertible strict derivative at every point is an open map (#5753)

More generally, the same is true for a map that is a local homeomorphism near every point.

Author: urkud

src/analysis/calculus/inverse.lean

@@ -415,6 +415,9 @@ lemma image_mem_to_local_homeomorph_target (hf : has_strict_fderiv_at f (f' : E
   f a ∈ (hf.to_local_homeomorph f).target :=
 (hf.to_local_homeomorph f).map_source hf.mem_to_local_homeomorph_source
 
+lemma map_nhds_eq (hf : has_strict_fderiv_at f (f' : E →L[𝕜] F) a) : map f (𝓝 a) = 𝓝 (f a) :=
+(hf.to_local_homeomorph f).map_nhds_eq hf.mem_to_local_homeomorph_source
+
 variables (f f' a)
 
 /-- Given a function `f` with an invertible derivative, returns a function that is locally inverse
@@ -473,6 +476,12 @@ hf.to_local_inverse.congr_of_eventually_eq $ (hf.local_inverse_unique hg).mono $
 
 end has_strict_fderiv_at
 
+/-- If a function has an invertible strict derivative at all points, then it is an open map. -/
+lemma open_map_of_strict_fderiv [complete_space E] {f : E → F} {f' : E → E ≃L[𝕜] F}
+  (hf : ∀ x, has_strict_fderiv_at f (f' x : E →L[𝕜] F) x) :
+  is_open_map f :=
+is_open_map_iff_nhds_le.2 $ λ x, (hf x).map_nhds_eq.ge
+
 /-!
 ### Inverse function theorem, 1D case
 
@@ -496,6 +505,9 @@ variables (f f' a)
 
 variables {f f' a}
 
+lemma map_nhds_eq : map f (𝓝 a) = 𝓝 (f a) :=
+(hf.has_strict_fderiv_at_equiv hf').map_nhds_eq
+
 theorem to_local_inverse : has_strict_deriv_at (hf.local_inverse f f' a hf') f'⁻¹ (f a) :=
 (hf.has_strict_fderiv_at_equiv hf').to_local_inverse
 
@@ -505,6 +517,12 @@ theorem to_local_left_inverse {g : 𝕜 → 𝕜} (hg : ∀ᶠ x in 𝓝 a, g (f
 
 end has_strict_deriv_at
 
+/-- If a function has a non-zero strict derivative at all points, then it is an open map. -/
+lemma open_map_of_strict_deriv [complete_space 𝕜] {f f' : 𝕜 → 𝕜}
+  (hf : ∀ x, has_strict_deriv_at f (f' x) x) (h0 : ∀ x, f' x ≠ 0) :
+  is_open_map f :=
+is_open_map_iff_nhds_le.2 $ λ x, ((hf x).map_nhds_eq (h0 x)).ge
+
 /-!
 ### Inverse function theorem, smooth case
 

src/order/filter/basic.lean

@@ -1318,6 +1318,8 @@ iff.intro
 @[simp] lemma map_id : filter.map id f = f :=
 filter_eq $ rfl
 
+@[simp] lemma map_id' : filter.map (λ x, x) f = f := map_id
+
 @[simp] lemma map_compose : filter.map m' ∘ filter.map m = filter.map (m' ∘ m) :=
 funext $ assume _, filter_eq $ rfl
 
@@ -1773,7 +1775,7 @@ le_antisymm
 lemma map_swap_eq_comap_swap {f : filter (α × β)} : prod.swap <$> f = comap prod.swap f :=
 map_eq_comap_of_inverse prod.swap_swap_eq prod.swap_swap_eq
 
-lemma le_map {f : filter α} {m : α → β} {g : filter β} (h : ∀s∈ f, m '' s ∈ g) :
+lemma le_map {f : filter α} {m : α → β} {g : filter β} (h : ∀ s ∈ f, m '' s ∈ g) :
   g ≤ f.map m :=
 assume s hs, mem_sets_of_superset (h _ hs) $ image_preimage_subset _ _
 
@@ -2024,6 +2026,11 @@ mt hf.eventually h
 @[simp] lemma tendsto_bot {f : α → β} {l : filter β} : tendsto f ⊥ l := by simp [tendsto]
 @[simp] lemma tendsto_top {f : α → β} {l : filter α} : tendsto f l ⊤ := le_top
 
+lemma le_map_of_right_inverse {mab : α → β} {mba : β → α} {f : filter α} {g : filter β}
+  (h₁ : mab ∘ mba =ᶠ[g] id) (h₂ : tendsto mba g f) :
+  g ≤ map mab f :=
+by { rw [← @map_id _ g, ← map_congr h₁, ← map_map], exact map_mono h₂ }
+
 lemma tendsto_of_not_nonempty {f : α → β} {la : filter α} {lb : filter β} (h : ¬nonempty α) :
   tendsto f la lb :=
 by simp only [filter_eq_bot_of_not_nonempty la h, tendsto_bot]

src/topology/local_homeomorph.lean

@@ -37,7 +37,7 @@ especially when restricting to subsets, as these should be open subsets.
 For design notes, see `local_equiv.lean`.
 -/
 
-open function set
+open function set filter
 open_locale topological_space
 
 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
@@ -121,15 +121,15 @@ end
 
 lemma eventually_left_inverse (e : local_homeomorph α β) {x} (hx : x ∈ e.source) :
   ∀ᶠ y in 𝓝 x, e.symm (e y) = y :=
-filter.eventually.mono (mem_nhds_sets e.open_source hx) e.left_inv'
+(e.open_source.eventually_mem hx).mono e.left_inv'
 
 lemma eventually_left_inverse' (e : local_homeomorph α β) {x} (hx : x ∈ e.target) :
   ∀ᶠ y in 𝓝 (e.symm x), e.symm (e y) = y :=
 e.eventually_left_inverse (e.map_target hx)
 
 lemma eventually_right_inverse (e : local_homeomorph α β) {x} (hx : x ∈ e.target) :
   ∀ᶠ y in 𝓝 x, e (e.symm y) = y :=
-filter.eventually.mono (mem_nhds_sets e.open_target hx) e.right_inv'
+(e.open_target.eventually_mem hx).mono e.right_inv'
 
 lemma eventually_right_inverse' (e : local_homeomorph α β) {x} (hx : x ∈ e.source) :
   ∀ᶠ y in 𝓝 (e x), e (e.symm y) = y :=
@@ -180,9 +180,14 @@ lemma continuous_at_symm {x : β} (h : x ∈ e.target) : continuous_at e.symm x
 e.symm.continuous_at h
 
 lemma tendsto_symm (e : local_homeomorph α β) {x} (hx : x ∈ e.source) :
-  filter.tendsto e.symm (𝓝 (e x)) (𝓝 x) :=
+  tendsto e.symm (𝓝 (e x)) (𝓝 x) :=
 by simpa only [continuous_at, e.left_inv hx] using e.continuous_at_symm (e.map_source hx)
 
+lemma map_nhds_eq (e : local_homeomorph α β) {x} (hx : x ∈ e.source) :
+  map e (𝓝 x) = 𝓝 (e x) :=
+le_antisymm (e.continuous_at hx) $
+  le_map_of_right_inverse (e.eventually_right_inverse' hx) (e.tendsto_symm hx)
+
 /-- Preimage of interior or interior of preimage coincide for local homeomorphisms, when restricted
 to the source. -/
 lemma preimage_interior (s : set β) :

src/topology/maps.lean

@@ -205,7 +205,7 @@ def is_open_map [topological_space α] [topological_space β] (f : α → β) :=
 ∀ U : set α, is_open U → is_open (f '' U)
 
 namespace is_open_map
-variables [topological_space α] [topological_space β] [topological_space γ]
+variables [topological_space α] [topological_space β] [topological_space γ] {f : α → β}
 open function
 
 protected lemma id : is_open_map (@id α) := assume s hs, by rwa [image_id]
@@ -214,24 +214,27 @@ protected lemma comp
   {g : β → γ} {f : α → β} (hg : is_open_map g) (hf : is_open_map f) : is_open_map (g ∘ f) :=
 by intros s hs; rw [image_comp]; exact hg _ (hf _ hs)
 
-lemma is_open_range {f : α → β} (hf : is_open_map f) : is_open (range f) :=
+lemma is_open_range (hf : is_open_map f) : is_open (range f) :=
 by { rw ← image_univ, exact hf _ is_open_univ }
 
-lemma image_mem_nhds {f : α → β} (hf : is_open_map f) {x : α} {s : set α} (hx : s ∈ 𝓝 x) :
+lemma image_mem_nhds (hf : is_open_map f) {x : α} {s : set α} (hx : s ∈ 𝓝 x) :
   f '' s ∈ 𝓝 (f x) :=
 let ⟨t, hts, ht, hxt⟩ := mem_nhds_sets_iff.1 hx in
 mem_sets_of_superset (mem_nhds_sets (hf t ht) (mem_image_of_mem _ hxt)) (image_subset _ hts)
 
-lemma nhds_le {f : α → β} (hf : is_open_map f) (a : α) : 𝓝 (f a) ≤ (𝓝 a).map f :=
+lemma nhds_le (hf : is_open_map f) (a : α) : 𝓝 (f a) ≤ (𝓝 a).map f :=
 le_map $ λ s, hf.image_mem_nhds
 
+lemma of_nhds_le (hf : ∀ a, 𝓝 (f a) ≤ map f (𝓝 a)) : is_open_map f :=
+λ s hs, is_open_iff_mem_nhds.2 $ λ b ⟨a, has, hab⟩,
+  hab ▸ hf _ (image_mem_map $ mem_nhds_sets hs has)
+
 lemma of_inverse {f : α → β} {f' : β → α}
   (h : continuous f') (l_inv : left_inverse f f') (r_inv : right_inverse f f') :
   is_open_map f :=
 begin
   assume s hs,
-  have : f' ⁻¹' s = f '' s, by ext x; simp [mem_image_iff_of_inverse r_inv l_inv],
-  rw ← this,
+  rw [image_eq_preimage_of_inverse r_inv l_inv],
   exact hs.preimage h
 end
 
@@ -253,15 +256,13 @@ end is_open_map
 
 lemma is_open_map_iff_nhds_le [topological_space α] [topological_space β] {f : α → β} :
   is_open_map f ↔ ∀(a:α), 𝓝 (f a) ≤ (𝓝 a).map f :=
-begin
-  refine ⟨λ hf, hf.nhds_le, λ h s hs, is_open_iff_mem_nhds.2 _⟩,
-  rintros b ⟨a, ha, rfl⟩,
-  exact h _ (filter.image_mem_map $ mem_nhds_sets hs ha)
-end
+⟨λ hf, hf.nhds_le, is_open_map.of_nhds_le⟩
 
 section is_closed_map
 variables [topological_space α] [topological_space β]
 
+/-- A map `f : α → β` is said to be a *closed map*, if the image of any closed `U : set α`
+is closed in `β`. -/
 def is_closed_map (f : α → β) := ∀ U : set α, is_closed U → is_closed (f '' U)
 
 end is_closed_map