feat: a few misc results about open (quotient) maps (leanprover-community#40715)

In particular, we upgrade `IsOpen[Quotient]Map.prodMap` to an `iff` when both factors are nonempty.

Author: ADedecker

Mathlib/Topology/Constructions/SumProd.lean

@@ -6,7 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot
 module
 
 public import Mathlib.Topology.Homeomorph.Defs
-public import Mathlib.Topology.Maps.Basic
+public import Mathlib.Topology.Maps.OpenQuotient
 public import Mathlib.Topology.Separation.SeparatedNhds
 
 /-!
@@ -358,6 +358,16 @@ theorem ContinuousAt.prodMap' {f : X → Z} {g : Y → W} {x : X} {y : Y} (hf :
     (hg : ContinuousAt g y) : ContinuousAt (Prod.map f g) (x, y) :=
   hf.prodMap hg
 
+@[simp]
+theorem continuousAt_prodMap_iff {f : X → Z} {g : Y → W} {x : X} {y : Y} :
+    ContinuousAt (Prod.map f g) (x, y) ↔ ContinuousAt f x ∧ ContinuousAt g y := by
+  simp [ContinuousAt, nhds_prod_eq, tendsto_iff_comap, comap_prodMap_prod]
+
+@[simp]
+theorem continuous_prodMap_iff [Nonempty Z] [Nonempty W] {f : Z → X} {g : W → Y} :
+    Continuous (Prod.map f g) ↔ Continuous f ∧ Continuous g := by
+  simp [continuous_iff_continuousAt, forall_and]
+
 theorem ContinuousAt.comp₂ {f : Y × Z → W} {g : X → Y} {h : X → Z} {x : X}
     (hf : ContinuousAt f (g x, h x)) (hg : ContinuousAt g x) (hh : ContinuousAt h x) :
     ContinuousAt (fun x ↦ f (g x, h x)) x :=
@@ -494,11 +504,17 @@ theorem isOpen_prod_iff' {s : Set X} {t : Set Y} :
       simp only [st.1.ne_empty, st.2.ne_empty, or_false] at H
       exact H.1.prod H.2
 
+theorem isOpenQuotientMap_fst [Nonempty Y] : IsOpenQuotientMap (Prod.fst : X × Y → X) :=
+  ⟨Prod.fst_surjective, continuous_fst, isOpenMap_fst⟩
+
+theorem isOpenQuotientMap_snd [Nonempty X] : IsOpenQuotientMap (Prod.snd : X × Y → Y) :=
+  ⟨Prod.snd_surjective, continuous_snd, isOpenMap_snd⟩
+
 theorem isQuotientMap_fst [Nonempty Y] : IsQuotientMap (Prod.fst : X × Y → X) :=
-  isOpenMap_fst.isQuotientMap continuous_fst Prod.fst_surjective
+  isOpenQuotientMap_fst.isQuotientMap
 
 theorem isQuotientMap_snd [Nonempty X] : IsQuotientMap (Prod.snd : X × Y → Y) :=
-  isOpenMap_snd.isQuotientMap continuous_snd Prod.snd_surjective
+  isOpenQuotientMap_snd.isQuotientMap
 
 theorem closure_prod_eq {s : Set X} {t : Set Y} : closure (s ×ˢ t) = closure s ×ˢ closure t :=
   ext fun ⟨a, b⟩ => by
@@ -589,6 +605,15 @@ protected theorem IsOpenMap.prodMap {f : X → Y} {g : Z → W} (hf : IsOpenMap
   rw [nhds_prod_eq, nhds_prod_eq, ← Filter.prod_map_map_eq']
   exact Filter.prod_mono (hf.nhds_le a) (hg.nhds_le b)
 
+@[simp]
+theorem isOpenMap_prodMap_iff [Nonempty X] [Nonempty Z] {f : X → Y} {g : Z → W} :
+    IsOpenMap (Prod.map f g) ↔ IsOpenMap f ∧ IsOpenMap g := by
+  refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨hf, hg⟩ ↦ hf.prodMap hg⟩
+  · rw [(isOpenQuotientMap_fst (Y := Z)).isOpenMap_iff]
+    exact isOpenMap_fst.comp h
+  · rw [(isOpenQuotientMap_snd (X := X)).isOpenMap_iff]
+    exact isOpenMap_snd.comp h
+
 protected lemma Topology.IsOpenEmbedding.prodMap {f : X → Y} {g : Z → W} (hf : IsOpenEmbedding f)
     (hg : IsOpenEmbedding g) : IsOpenEmbedding (Prod.map f g) :=
   .of_isEmbedding_isOpenMap (hf.1.prodMap hg.1) (hf.isOpenMap.prodMap hg.isOpenMap)
@@ -612,6 +637,13 @@ theorem IsOpenQuotientMap.prodMap {f : X → Y} {g : Z → W} (hf : IsOpenQuotie
     (hg : IsOpenQuotientMap g) : IsOpenQuotientMap (Prod.map f g) :=
   ⟨.prodMap hf.1 hg.1, .prodMap hf.2 hg.2, .prodMap hf.3 hg.3⟩
 
+@[simp]
+theorem isOpenQuotientMap_prodMap_iff [Nonempty X] [Nonempty Z] {f : X → Y} {g : Z → W} :
+    IsOpenQuotientMap (Prod.map f g) ↔ IsOpenQuotientMap f ∧ IsOpenQuotientMap g := by
+  have : Nonempty Y := .map f inferInstance
+  have : Nonempty W := .map g inferInstance
+  grind [isOpenQuotientMap_iff, continuous_prodMap_iff, isOpenMap_prodMap_iff, Prod.map_surjective]
+
 theorem TopologicalSpace.prod_mono {α β : Type*} {σ₁ σ₂ : TopologicalSpace α}
     {τ₁ τ₂ : TopologicalSpace β} (hσ : σ₁ ≤ σ₂) (hτ : τ₁ ≤ τ₂) :
     @instTopologicalSpaceProd α β σ₁ τ₁ ≤ @instTopologicalSpaceProd α β σ₂ τ₂ :=

Mathlib/Topology/Homeomorph/Defs.lean

@@ -6,7 +6,7 @@ Authors: Johannes Hölzl, Patrick Massot, Sébastien Gouëzel, Zhouhang Zhou, Re
 module
 
 public import Mathlib.Topology.ContinuousMap.Defs
-public import Mathlib.Topology.Maps.Basic
+public import Mathlib.Topology.Maps.OpenQuotient
 
 /-!
 # Homeomorphisms
@@ -342,6 +342,20 @@ theorem comp_isOpenMap_iff' (h : X ≃ₜ Y) {f : Y → Z} : IsOpenMap (f ∘ h)
   rw [← Function.comp_id f, ← h.self_comp_symm, ← Function.comp_assoc]
   exact hf.comp h.symm.isOpenMap
 
+/-- Open quotient maps are preserved by precomposing with a homeomorphism. -/
+@[simp]
+theorem isOpenQuotient_comp_iff (e : X ≃ₜ Y) {f : Y → Z} :
+    IsOpenQuotientMap (f ∘ e) ↔ IsOpenQuotientMap f :=
+  ⟨fun h ↦ by simpa [Function.comp_assoc] using h.comp e.symm.isOpenQuotientMap,
+    fun hf ↦ hf.comp e.isOpenQuotientMap⟩
+
+/-- Open quotient maps are preserved by postcomposing with a homeomorphism. -/
+@[simp]
+theorem comp_isOpenQuotientMap_iff (e : Y ≃ₜ Z) {f : X → Y} :
+    IsOpenQuotientMap (e ∘ f) ↔ IsOpenQuotientMap f :=
+  ⟨fun h ↦ by simpa [← Function.comp_assoc] using e.symm.isOpenQuotientMap.comp h,
+    fun hf ↦ e.isOpenQuotientMap.comp hf⟩
+
 variable (X Y) in
 /-- If both `X` and `Y` have a unique element, then `X ≃ₜ Y`. -/
 @[simps!]

Mathlib/Topology/Maps/Basic.lean

@@ -369,6 +369,12 @@ protected theorem id : IsOpenMap (@id X) := fun s hs => by rwa [image_id]
 protected theorem comp (hg : IsOpenMap g) (hf : IsOpenMap f) :
     IsOpenMap (g ∘ f) := fun s hs => by rw [image_comp]; exact hg _ (hf _ hs)
 
+/-- If `g ∘ f` is open, where `f` is continuous and surjective, then `g` is open. -/
+theorem of_comp (hf : Continuous f) (f_surj : Surjective f) (h : IsOpenMap (g ∘ f)) :
+    IsOpenMap g := fun s hs => by
+  rw [← f_surj.image_preimage s, ← image_comp]
+  exact h _ (hs.preimage hf)
+
 theorem isOpen_range (hf : IsOpenMap f) : IsOpen (range f) := by
   rw [← image_univ]
   exact hf _ isOpen_univ

Mathlib/Topology/Maps/OpenQuotient.lean

@@ -49,6 +49,15 @@ theorem comp {g : Y → Z} (hg : IsOpenQuotientMap g) (hf : IsOpenQuotientMap f)
     IsOpenQuotientMap (g ∘ f) :=
   ⟨.comp hg.1 hf.1, .comp hg.2 hf.2, .comp hg.3 hf.3⟩
 
+theorem of_comp {g : Y → Z} (hf : Continuous f) (f_surj : Surjective f) (hg : Continuous g)
+    (h : IsOpenQuotientMap (g ∘ f)) : IsOpenQuotientMap g :=
+  ⟨.of_comp h.surjective, hg, .of_comp hf f_surj h.isOpenMap ⟩
+
+theorem of_comp_iff {g : Y → Z} (hf : IsOpenQuotientMap f) :
+    IsOpenQuotientMap (g ∘ f) ↔ IsOpenQuotientMap g :=
+  ⟨fun h ↦ .of_comp hf.continuous hf.surjective
+    (hf.isQuotientMap.continuous_iff.mpr h.continuous) h, fun hg ↦ hg.comp hf⟩
+
 theorem map_nhds_eq (h : IsOpenQuotientMap f) (x : X) : map f (𝓝 x) = 𝓝 (f x) :=
   le_antisymm h.continuous.continuousAt <| h.isOpenMap.nhds_le _
 
@@ -60,6 +69,10 @@ theorem continuousAt_comp_iff (h : IsOpenQuotientMap f) {g : Y → Z} {x : X} :
     ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x) := by
   simp only [ContinuousAt, ← h.map_nhds_eq, tendsto_map'_iff, comp_def]
 
+theorem isOpenMap_iff (hf : IsOpenQuotientMap f) {g : Y → Z} :
+    IsOpenMap g ↔ IsOpenMap (g ∘ f) :=
+  ⟨fun hg ↦ hg.comp hf.isOpenMap, fun h ↦ .of_comp hf.continuous hf.surjective h⟩
+
 theorem dense_preimage_iff (h : IsOpenQuotientMap f) {s : Set Y} : Dense (f ⁻¹' s) ↔ Dense s :=
   ⟨fun hs ↦ h.surjective.denseRange.dense_of_mapsTo h.continuous hs (mapsTo_preimage _ _),
     fun hs ↦ hs.preimage h.isOpenMap⟩