feat: miscellaneous lemmas about local homeomorphisms (#7655)

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Author: alreadydone

Mathlib/Topology/IsLocallyHomeomorph.lean

@@ -34,6 +34,21 @@ def IsLocallyHomeomorphOn :=
   ∀ x ∈ s, ∃ e : LocalHomeomorph X Y, x ∈ e.source ∧ f = e
 #align is_locally_homeomorph_on IsLocallyHomeomorphOn
 
+theorem isLocallyHomeomorphOn_iff_openEmbedding_restrict {f : X → Y} :
+    IsLocallyHomeomorphOn f s ↔ ∀ x ∈ s, ∃ U ∈ 𝓝 x, OpenEmbedding (U.restrict f) := by
+  refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ ?_⟩
+  · obtain ⟨e, hxe, rfl⟩ := h x hx
+    exact ⟨e.source, e.open_source.mem_nhds hxe, e.openEmbedding_restrict⟩
+  · obtain ⟨U, hU, emb⟩ := h x hx
+    have : OpenEmbedding ((interior U).restrict f)
+    · refine emb.comp ⟨embedding_inclusion interior_subset, ?_⟩
+      rw [Set.range_inclusion]; exact isOpen_induced isOpen_interior
+    obtain ⟨cont, inj, openMap⟩ := openEmbedding_iff_continuous_injective_open.mp this
+    haveI : Nonempty X := ⟨x⟩
+    exact ⟨LocalHomeomorph.ofContinuousOpenRestrict (Set.injOn_iff_injective.mpr inj).toLocalEquiv
+      (continuousOn_iff_continuous_restrict.mpr cont) openMap isOpen_interior,
+      mem_interior_iff_mem_nhds.mpr hU, rfl⟩
+
 namespace IsLocallyHomeomorphOn
 
 /-- Proves that `f` satisfies `IsLocallyHomeomorphOn f s`. The condition `h` is weaker than the
@@ -55,6 +70,31 @@ theorem mk (h : ∀ x ∈ s, ∃ e : LocalHomeomorph X Y, x ∈ e.source ∧ ∀
 
 variable {g f s t}
 
+theorem mono {t : Set X} (hf : IsLocallyHomeomorphOn f t) (hst : s ⊆ t) :
+    IsLocallyHomeomorphOn f s := fun x hx ↦ hf x (hst hx)
+
+theorem of_comp_left (hgf : IsLocallyHomeomorphOn (g ∘ f) s) (hg : IsLocallyHomeomorphOn g (f '' s))
+    (cont : ∀ x ∈ s, ContinuousAt f x) : IsLocallyHomeomorphOn f s := mk f s fun x hx ↦ by
+  obtain ⟨g, hxg, rfl⟩ := hg (f x) ⟨x, hx, rfl⟩
+  obtain ⟨gf, hgf, he⟩ := hgf x hx
+  refine ⟨(gf.restr <| f ⁻¹' g.source).trans g.symm, ⟨⟨hgf, mem_interior_iff_mem_nhds.mpr
+    ((cont x hx).preimage_mem_nhds <| g.open_source.mem_nhds hxg)⟩, he ▸ g.map_source hxg⟩,
+    fun y hy ↦ ?_⟩
+  change f y = g.symm (gf y)
+  have : f y ∈ g.source := by apply interior_subset hy.1.2
+  rw [← he, g.eq_symm_apply this (by apply g.map_source this)]
+  rfl
+
+theorem of_comp_right (hgf : IsLocallyHomeomorphOn (g ∘ f) s) (hf : IsLocallyHomeomorphOn f s) :
+    IsLocallyHomeomorphOn g (f '' s) := mk g _ <| by
+  rintro _ ⟨x, hx, rfl⟩
+  obtain ⟨f, hxf, rfl⟩ := hf x hx
+  obtain ⟨gf, hgf, he⟩ := hgf x hx
+  refine ⟨f.symm.trans gf, ⟨f.map_source hxf, ?_⟩, fun y hy ↦ ?_⟩
+  · apply (f.left_inv hxf).symm ▸ hgf
+  · change g y = gf (f.symm y)
+    rw [← he, Function.comp_apply, f.right_inv hy.1]
+
 theorem map_nhds_eq (hf : IsLocallyHomeomorphOn f s) {x : X} (hx : x ∈ s) : (𝓝 x).map f = 𝓝 (f x) :=
   let ⟨e, hx, he⟩ := hf x hx
   he.symm ▸ e.map_nhds_eq hx
@@ -85,18 +125,29 @@ def IsLocallyHomeomorph :=
   ∀ x : X, ∃ e : LocalHomeomorph X Y, x ∈ e.source ∧ f = e
 #align is_locally_homeomorph IsLocallyHomeomorph
 
-variable {f}
+theorem isLocallyHomeomorph_homeomorph (f : X ≃ₜ Y) : IsLocallyHomeomorph f :=
+  fun _ ↦ ⟨f.toLocalHomeomorph, trivial, rfl⟩
+
+variable {f s}
 
 theorem isLocallyHomeomorph_iff_isLocallyHomeomorphOn_univ :
-    IsLocallyHomeomorph f ↔ IsLocallyHomeomorphOn f Set.univ := by
-  simp only [IsLocallyHomeomorph, IsLocallyHomeomorphOn, Set.mem_univ, forall_true_left]
+    IsLocallyHomeomorph f ↔ IsLocallyHomeomorphOn f Set.univ :=
+  ⟨fun h x _ ↦ h x, fun h x ↦ h x trivial⟩
 #align is_locally_homeomorph_iff_is_locally_homeomorph_on_univ isLocallyHomeomorph_iff_isLocallyHomeomorphOn_univ
 
 protected theorem IsLocallyHomeomorph.isLocallyHomeomorphOn (hf : IsLocallyHomeomorph f) :
-    IsLocallyHomeomorphOn f Set.univ :=
-  isLocallyHomeomorph_iff_isLocallyHomeomorphOn_univ.mp hf
+    IsLocallyHomeomorphOn f s := fun x _ ↦ hf x
 #align is_locally_homeomorph.is_locally_homeomorph_on IsLocallyHomeomorph.isLocallyHomeomorphOn
 
+theorem isLocallyHomeomorph_iff_openEmbedding_restrict {f : X → Y} :
+    IsLocallyHomeomorph f ↔ ∀ x : X, ∃ U ∈ 𝓝 x, OpenEmbedding (U.restrict f) := by
+  simp_rw [isLocallyHomeomorph_iff_isLocallyHomeomorphOn_univ,
+    isLocallyHomeomorphOn_iff_openEmbedding_restrict, imp_iff_right (Set.mem_univ _)]
+
+theorem OpenEmbedding.isLocallyHomeomorph (hf : OpenEmbedding f) : IsLocallyHomeomorph f :=
+  isLocallyHomeomorph_iff_openEmbedding_restrict.mpr fun _ ↦
+    ⟨_, Filter.univ_mem, hf.comp (Homeomorph.Set.univ X).openEmbedding⟩
+
 variable (f)
 
 namespace IsLocallyHomeomorph
@@ -112,6 +163,11 @@ theorem mk (h : ∀ x : X, ∃ e : LocalHomeomorph X Y, x ∈ e.source ∧ ∀ y
 
 variable {g f}
 
+theorem of_comp (hgf : IsLocallyHomeomorph (g ∘ f)) (hg : IsLocallyHomeomorph g)
+    (cont : Continuous f) : IsLocallyHomeomorph f :=
+  isLocallyHomeomorph_iff_isLocallyHomeomorphOn_univ.mpr <|
+    hgf.isLocallyHomeomorphOn.of_comp_left hg.isLocallyHomeomorphOn fun _ _ ↦ cont.continuousAt
+
 theorem map_nhds_eq (hf : IsLocallyHomeomorph f) (x : X) : (𝓝 x).map f = 𝓝 (f x) :=
   hf.isLocallyHomeomorphOn.map_nhds_eq (Set.mem_univ x)
 #align is_locally_homeomorph.map_nhds_eq IsLocallyHomeomorph.map_nhds_eq
@@ -130,5 +186,30 @@ protected theorem comp (hg : IsLocallyHomeomorph g) (hf : IsLocallyHomeomorph f)
     (hg.isLocallyHomeomorphOn.comp hf.isLocallyHomeomorphOn (Set.univ.mapsTo_univ f))
 #align is_locally_homeomorph.comp IsLocallyHomeomorph.comp
 
-end IsLocallyHomeomorph
+theorem openEmbedding_of_injective (hf : IsLocallyHomeomorph f) (hi : f.Injective) :
+    OpenEmbedding f :=
+  openEmbedding_of_continuous_injective_open hf.continuous hi hf.isOpenMap
+
+/-- Continuous local sections of a local homeomorphism are open embeddings. -/
+theorem openEmbedding_of_comp (hf : IsLocallyHomeomorph g) (hgf : OpenEmbedding (g ∘ f))
+    (cont : Continuous f) : OpenEmbedding f :=
+  (hgf.isLocallyHomeomorph.of_comp hf cont).openEmbedding_of_injective hgf.inj.of_comp
+
+open TopologicalSpace in
+/-- Ranges of continuous local sections of a local homeomorphism form a basis of the total space. -/
+theorem isTopologicalBasis (hf : IsLocallyHomeomorph f) : IsTopologicalBasis
+    {U : Set X | ∃ V : Set Y, IsOpen V ∧ ∃ s : C(V,X), f ∘ s = (↑) ∧ Set.range s = U} := by
+  refine isTopologicalBasis_of_open_of_nhds ?_ fun x U hx hU ↦ ?_
+  · rintro _ ⟨U, hU, s, hs, rfl⟩
+    refine (openEmbedding_of_comp hf (hs ▸ ⟨embedding_subtype_val, ?_⟩) s.continuous).open_range
+    rwa [Subtype.range_val]
+  · obtain ⟨f, hxf, rfl⟩ := hf x
+    refine ⟨f.source ∩ U, ⟨f.target ∩ f.symm ⁻¹' U, f.symm.preimage_open_of_open hU,
+      ⟨_, continuousOn_iff_continuous_restrict.mp (f.continuous_invFun.mono fun _ h ↦ h.1)⟩,
+      ?_, (Set.range_restrict _ _).trans ?_⟩, ⟨hxf, hx⟩, fun _ h ↦ h.2⟩
+    · ext y; exact f.right_inv y.2.1
+    · apply (f.symm_image_target_inter_eq _).trans
+      rw [Set.preimage_inter, ← Set.inter_assoc, Set.inter_eq_self_of_subset_left
+        f.source_preimage_target, f.source_inter_preimage_inv_preimage]
 
+end IsLocallyHomeomorph

Mathlib/Topology/LocalHomeomorph.lean

@@ -1266,18 +1266,18 @@ def toHomeomorphOfSourceEqUnivTargetEqUniv (h : e.source = (univ : Set α)) (h'
     simpa only [continuous_iff_continuousOn_univ, h'] using e.continuousOn_symm
 #align local_homeomorph.to_homeomorph_of_source_eq_univ_target_eq_univ LocalHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv
 
+theorem openEmbedding_restrict : OpenEmbedding (e.source.restrict e) := by
+  refine openEmbedding_of_continuous_injective_open (e.continuousOn.comp_continuous
+    continuous_subtype_val Subtype.prop) e.injOn.injective fun V hV ↦ ?_
+  rw [Set.restrict_eq, Set.image_comp]
+  exact e.image_open_of_open (e.open_source.isOpenMap_subtype_val V hV) fun _ ⟨x, _, h⟩ ↦ h ▸ x.2
+
 /-- A local homeomorphism whose source is all of `α` defines an open embedding of `α` into `β`.  The
 converse is also true; see `OpenEmbedding.toLocalHomeomorph`. -/
-theorem to_openEmbedding (h : e.source = Set.univ) : OpenEmbedding e := by
-  apply openEmbedding_of_continuous_injective_open
-  · apply continuous_iff_continuousOn_univ.mpr
-    rw [← h]
-    exact e.continuousOn
-  · apply Set.injective_iff_injOn_univ.mpr
-    rw [← h]
-    exact e.injOn
-  · intro U hU
-    simpa only [h, subset_univ, mfld_simps] using e.image_open_of_open hU
+theorem to_openEmbedding (h : e.source = Set.univ) : OpenEmbedding e :=
+  e.openEmbedding_restrict.comp
+    ((Homeomorph.setCongr h).trans <| Homeomorph.Set.univ α).symm.openEmbedding
+
 #align local_homeomorph.to_open_embedding LocalHomeomorph.to_openEmbedding
 
 end LocalHomeomorph