feat(topology/fiber_bundle): Each fiber of a trivialization is homeom…

…orphic to the specified fiber (#16079)

This PR adds `topological_fiber_bundle.trivialization.preimage_singleton_homeomorph`, which states that each fiber of a trivialization is homeomorphic to the specified fiber.

src/topology/fiber_bundle.lean

@@ -361,6 +361,57 @@ lemma map_proj_nhds (ex : x ∈ e.source) : map proj (𝓝 x) = 𝓝 (proj x) :=
 by rw [← e.coe_fst ex, ← map_congr (e.coe_fst_eventually_eq_proj ex), ← map_map, ← e.coe_coe,
   e.to_local_homeomorph.map_nhds_eq ex, map_fst_nhds]
 
+lemma preimage_subset_source {s : set B} (hb : s ⊆ e.base_set) : proj ⁻¹' s ⊆ e.source :=
+λ p hp, e.mem_source.mpr (hb hp)
+
+lemma image_preimage_eq_prod_univ {s : set B} (hb : s ⊆ e.base_set) :
+  e '' (proj ⁻¹' s) = s ×ˢ univ :=
+subset.antisymm (image_subset_iff.mpr (λ p hp,
+  ⟨(e.proj_to_fun p (e.preimage_subset_source hb hp)).symm ▸ hp, trivial⟩)) (λ p hp,
+  let hp' : p ∈ e.target := e.mem_target.mpr (hb hp.1) in
+  ⟨e.inv_fun p, mem_preimage.mpr ((e.proj_symm_apply hp').symm ▸ hp.1), e.apply_symm_apply hp'⟩)
+
+/-- The preimage of a subset of the base set is homeomorphic to the product with the fiber. -/
+def preimage_homeomorph {s : set B} (hb : s ⊆ e.base_set) : proj ⁻¹' s ≃ₜ s × F :=
+(e.to_local_homeomorph.homeomorph_of_image_subset_source (e.preimage_subset_source hb)
+  (e.image_preimage_eq_prod_univ hb)).trans
+  ((homeomorph.set.prod s univ).trans ((homeomorph.refl s).prod_congr (homeomorph.set.univ F)))
+
+@[simp] lemma preimage_homeomorph_apply {s : set B} (hb : s ⊆ e.base_set) (p : proj ⁻¹' s) :
+  e.preimage_homeomorph hb p = (⟨proj p, p.2⟩, (e p).2) :=
+prod.ext (subtype.ext (e.proj_to_fun p (e.mem_source.mpr (hb p.2)))) rfl
+
+@[simp] lemma preimage_homeomorph_symm_apply {s : set B} (hb : s ⊆ e.base_set) (p : s × F) :
+  (e.preimage_homeomorph hb).symm p = ⟨e.symm (p.1, p.2), ((e.preimage_homeomorph hb).symm p).2⟩ :=
+rfl
+
+/-- The source is homeomorphic to the product of the base set with the fiber. -/
+def source_homeomorph_base_set_prod : e.source ≃ₜ e.base_set × F :=
+(homeomorph.set_congr e.source_eq).trans (e.preimage_homeomorph subset_rfl)
+
+@[simp] lemma source_homeomorph_base_set_prod_apply (p : e.source) :
+  e.source_homeomorph_base_set_prod p = (⟨proj p, e.mem_source.mp p.2⟩, (e p).2) :=
+e.preimage_homeomorph_apply subset_rfl ⟨p, e.mem_source.mp p.2⟩
+
+@[simp] lemma source_homeomorph_base_set_prod_symm_apply (p : e.base_set × F) :
+  e.source_homeomorph_base_set_prod.symm p =
+    ⟨e.symm (p.1, p.2), (e.source_homeomorph_base_set_prod.symm p).2⟩ :=
+rfl
+
+/-- Each fiber of a trivialization is homeomorphic to the specified fiber. -/
+def preimage_singleton_homeomorph {b : B} (hb : b ∈ e.base_set) : proj ⁻¹' {b} ≃ₜ F :=
+(e.preimage_homeomorph (set.singleton_subset_iff.mpr hb)).trans (((homeomorph.homeomorph_of_unique
+  ({b} : set B) punit).prod_congr (homeomorph.refl F)).trans (homeomorph.punit_prod F))
+
+@[simp] lemma preimage_singleton_homeomorph_apply {b : B} (hb : b ∈ e.base_set)
+  (p : proj ⁻¹' {b}) : e.preimage_singleton_homeomorph hb p = (e p).2 :=
+rfl
+
+@[simp] lemma preimage_singleton_homeomorph_symm_apply {b : B} (hb : b ∈ e.base_set) (p : F) :
+  (e.preimage_singleton_homeomorph hb).symm p =
+    ⟨e.symm (b, p), by rw [mem_preimage, e.proj_symm_apply' hb, mem_singleton_iff]⟩ :=
+rfl
+
 /-- In the domain of a bundle trivialization, the projection is continuous-/
 lemma continuous_at_proj (ex : x ∈ e.source) : continuous_at proj x :=
 (e.map_proj_nhds ex).le

src/topology/homeomorph.lean

@@ -379,6 +379,12 @@ def punit_prod : punit × α ≃ₜ α :=
 
 @[simp] lemma coe_punit_prod : ⇑(punit_prod α) = prod.snd := rfl
 
+/-- If both `α` and `β` have a unique element, then `α ≃ₜ β`. -/
+@[simps] def _root_.homeomorph.homeomorph_of_unique [unique α] [unique β] : α ≃ₜ β :=
+{ continuous_to_fun := @continuous_const α β _ _ default,
+  continuous_inv_fun := @continuous_const β α _ _ default,
+  .. equiv.equiv_of_unique α β }
+
 end
 
 /-- `ulift α` is homeomorphic to `α`. -/

src/topology/local_homeomorph.lean

@@ -985,16 +985,24 @@ end
 
 end continuity
 
+/-- The homeomorphism obtained by restricting a `local_homeomorph` to a subset of the source. -/
+@[simps] def homeomorph_of_image_subset_source
+  {s : set α} {t : set β} (hs : s ⊆ e.source) (ht : e '' s = t) : s ≃ₜ t :=
+{ to_fun := λ a, ⟨e a, (congr_arg ((∈) (e a)) ht).mp ⟨a, a.2, rfl⟩⟩,
+  inv_fun := λ b, ⟨e.symm b, let ⟨a, ha1, ha2⟩ := (congr_arg ((∈) ↑b) ht).mpr b.2 in
+    ha2 ▸ (e.left_inv (hs ha1)).symm ▸ ha1⟩,
+  left_inv := λ a, subtype.ext (e.left_inv (hs a.2)),
+  right_inv := λ b, let ⟨a, ha1, ha2⟩ := (congr_arg ((∈) ↑b) ht).mpr b.2 in
+    subtype.ext (e.right_inv (ha2 ▸ e.map_source (hs ha1))),
+  continuous_to_fun := (continuous_on_iff_continuous_restrict.mp
+    (e.continuous_on.mono hs)).subtype_mk _,
+  continuous_inv_fun := (continuous_on_iff_continuous_restrict.mp
+    (e.continuous_on_symm.mono (λ b hb, let ⟨a, ha1, ha2⟩ := show b ∈ e '' s, from ht.symm ▸ hb in
+      ha2 ▸ e.map_source (hs ha1)))).subtype_mk _ }
+
 /-- A local homeomrphism defines a homeomorphism between its source and target. -/
 def to_homeomorph_source_target : e.source ≃ₜ e.target :=
-{ to_fun := e.maps_to.restrict _ _ _,
-  inv_fun := e.symm_maps_to.restrict _ _ _,
-  left_inv := λ x, subtype.eq $ e.left_inv x.2,
-  right_inv := λ x, subtype.eq $ e.right_inv x.2,
-  continuous_to_fun :=
-    (continuous_on_iff_continuous_restrict.1 e.continuous_on).subtype_mk _,
-  continuous_inv_fun :=
-    (continuous_on_iff_continuous_restrict.1 e.symm.continuous_on).subtype_mk _ }
+e.homeomorph_of_image_subset_source subset_rfl e.image_source_eq_target
 
 lemma second_countable_topology_source [second_countable_topology β]
   (e : local_homeomorph α β) :