feat: trivial homeomorphisms between quotient spaces (#39266)

Author: ADedecker

Mathlib.lean

@@ -7723,6 +7723,7 @@ public import Mathlib.Topology.Hom.ContinuousEvalConst
 public import Mathlib.Topology.Hom.Open
 public import Mathlib.Topology.Homeomorph.Defs
 public import Mathlib.Topology.Homeomorph.Lemmas
+public import Mathlib.Topology.Homeomorph.Quotient
 public import Mathlib.Topology.Homeomorph.TransferInstance
 public import Mathlib.Topology.Homotopy.Affine
 public import Mathlib.Topology.Homotopy.Basic

Mathlib/Data/Setoid/Basic.lean

@@ -228,6 +228,14 @@ def map_sInf {S : Set (Setoid α)} {s : Setoid α} (h : s ∈ S) :
     Quotient (sInf S) → Quotient s :=
   Setoid.map_of_le fun _ _ a ↦ a s h
 
+/-- The quotient by the trivial relation is equivalent to the original space. -/
+def quotientBotEquiv :
+    Quotient (⊥ : Setoid α) ≃ α where
+  toFun := Quotient.lift id (fun _ _ ↦ id)
+  invFun := Quotient.mk''
+  left_inv := Quotient.ind fun _ ↦ rfl
+  right_inv := fun _ ↦ rfl
+
 section EqvGen
 
 open Relation

Mathlib/Topology/Constructions.lean

@@ -702,6 +702,12 @@ theorem continuous_quot_lift {f : X → Y} (hr : ∀ a b, r a b → f a = f b) (
     Continuous (Quot.lift f hr : Quot r → Y) :=
   continuous_coinduced_dom.2 h
 
+@[continuity, fun_prop]
+theorem continuous_quot_map {r' : Y → Y → Prop} {f : X → Y} (hr : ∀ a b, r a b → r' (f a) (f b))
+    (h : Continuous f) :
+    Continuous (Quot.map f hr : Quot r → Quot r') :=
+  continuous_quot_lift _ (continuous_quot_mk.comp h)
+
 theorem isQuotientMap_quotient_mk' : IsQuotientMap (@Quotient.mk' X s) :=
   isQuotientMap_quot_mk
 

Mathlib/Topology/Homeomorph/Quotient.lean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2026 Anatole Dedecker. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anatole Dedecker
+-/
+module
+
+public import Mathlib.Topology.Homeomorph.Lemmas
+
+/-!
+# Homeomorphisms between quotient spaces
+-/
+
+@[expose] public section
+
+namespace Homeomorph
+
+variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
+
+namespace Quot
+
+/-- An homeomorphism `e : X ≃ₜ Y` generXtes an homeomorphism between quotient spaces,
+if `rX x₁ x₂ ↔ rY (e x₁) (e x₂)`. -/
+protected def congr {rX : X → X → Prop} {rY : Y → Y → Prop} (e : X ≃ₜ Y)
+    (eq : ∀ x₁ x₂, rX x₁ x₂ ↔ rY (e x₁) (e x₂)) : Quot rX ≃ₜ Quot rY where
+  toEquiv := _root_.Quot.congr e eq
+  continuous_toFun := continuous_quot_map (fun x y ↦ by simp [eq]) e.continuous
+  continuous_invFun := continuous_quot_map (fun x y ↦ by simp [eq]) e.symm.continuous
+
+/-- Quotient spaces for equal relations are homeomorphic. -/
+protected def congrRight {r r' : X → X → Prop} (eq : ∀ x₁ x₂, r x₁ x₂ ↔ r' x₁ x₂) :
+    Quot r ≃ₜ Quot r' := Quot.congr (Homeomorph.refl X) eq
+
+/-- An homeomorphism `e : X ≃ₜ Y` generXtes an equivalence between the quotient space of `X`
+by a relation `rX` and the quotient space of `Y` by the image of this relation under `e`. -/
+protected def congrLeft {r : X → X → Prop} (e : X ≃ₜ Y) :
+    Quot r ≃ₜ Quot fun y₁ y₂ ↦ r (e.symm y₁) (e.symm y₂) :=
+  Quot.congr e fun _ _ ↦ by simp only [e.symm_apply_apply]
+
+end Quot
+
+namespace Quotient
+
+/-- An homeomorphism `e : X ≃ₜ Y` generXtes an homeomorphism between quotient spaces,
+if `rX x₁ x₂ ↔ rY (e x₁) (e x₂)`. -/
+protected def congr {rX : Setoid X} {rY : Setoid Y} (e : X ≃ₜ Y)
+    (eq : ∀ x₁ x₂, rX x₁ x₂ ↔ rY (e x₁) (e x₂)) :
+    Quotient rX ≃ₜ Quotient rY := Quot.congr e eq
+
+/-- Quotient spaces for equal relations are homeomorphic. -/
+protected def congrRight {r r' : Setoid X}
+    (eq : ∀ x₁ x₂, r x₁ x₂ ↔ r' x₁ x₂) : Quotient r ≃ₜ Quotient r' :=
+  Quot.congrRight eq
+
+end Quotient
+
+/-- The quotient by the trivial relation is homeomorphic to the original space. -/
+def quotientBot :
+    Quotient (⊥ : Setoid X) ≃ₜ X where
+  toEquiv := Setoid.quotientBotEquiv
+  continuous_toFun := continuous_quot_lift _ continuous_id
+  continuous_invFun := continuous_quot_mk
+
+end Homeomorph