chore: Rename QuotientMap to IsQuotientMap (#18062)

`Function.Embedding` is a type while `Embedding` is a proposition, and there are many other kinds of embeddings than topological embeddings. Hence this PR is a step towards
1. renaming `Embedding` to `IsEmbedding` and similarly for neighboring declarations (which `QuotientMap` is)
2. namespacing it inside `Topology`

Author: YaelDillies

Mathlib/Analysis/Complex/ReImTopology.lean

@@ -18,7 +18,7 @@ Each statement about `Complex.re` listed below has a counterpart about `Complex.
 
 * `Complex.isHomeomorphicTrivialFiberBundle_re`: `Complex.re` turns `ℂ` into a trivial
   topological fiber bundle over `ℝ`;
-* `Complex.isOpenMap_re`, `Complex.quotientMap_re`: in particular, `Complex.re` is an open map
+* `Complex.isOpenMap_re`, `Complex.isQuotientMap_re`: in particular, `Complex.re` is an open map
   and is a quotient map;
 * `Complex.interior_preimage_re`, `Complex.closure_preimage_re`, `Complex.frontier_preimage_re`:
   formulas for `interior (Complex.re ⁻¹' s)` etc;
@@ -52,11 +52,17 @@ theorem isOpenMap_re : IsOpenMap re :=
 theorem isOpenMap_im : IsOpenMap im :=
   isHomeomorphicTrivialFiberBundle_im.isOpenMap_proj
 
-theorem quotientMap_re : QuotientMap re :=
-  isHomeomorphicTrivialFiberBundle_re.quotientMap_proj
+theorem isQuotientMap_re : IsQuotientMap re :=
+  isHomeomorphicTrivialFiberBundle_re.isQuotientMap_proj
 
-theorem quotientMap_im : QuotientMap im :=
-  isHomeomorphicTrivialFiberBundle_im.quotientMap_proj
+@[deprecated (since := "2024-10-22")]
+alias quotientMap_re := isQuotientMap_re
+
+theorem isQuotientMap_im : IsQuotientMap im :=
+  isHomeomorphicTrivialFiberBundle_im.isQuotientMap_proj
+
+@[deprecated (since := "2024-10-22")]
+alias quotientMap_im := isQuotientMap_im
 
 theorem interior_preimage_re (s : Set ℝ) : interior (re ⁻¹' s) = re ⁻¹' interior s :=
   (isOpenMap_re.preimage_interior_eq_interior_preimage continuous_re _).symm

Mathlib/Analysis/Normed/Operator/Banach.lean

@@ -249,8 +249,11 @@ protected theorem isOpenMap (surj : Surjective f) : IsOpenMap f := by
 
   exact Set.mem_image_of_mem _ (hε this)
 
-protected theorem quotientMap (surj : Surjective f) : QuotientMap f :=
-  (f.isOpenMap surj).to_quotientMap f.continuous surj
+theorem isQuotientMap (surj : Surjective f) : IsQuotientMap f :=
+  (f.isOpenMap surj).isQuotientMap f.continuous surj
+
+@[deprecated (since := "2024-10-22")]
+alias quotientMap := isQuotientMap
 
 end
 

Mathlib/Condensed/TopComparison.lean

@@ -31,7 +31,7 @@ variable {C : Type u} [Category.{v} C] (G : C ⥤ TopCat.{w})
   (X : Type w') [TopologicalSpace X]
 
 /--
-An auxiliary lemma to that allows us to use `QuotientMap.lift` in the proof of
+An auxiliary lemma to that allows us to use `IsQuotientMap.lift` in the proof of
 `equalizerCondition_yonedaPresheaf`.
 -/
 theorem factorsThrough_of_pullbackCondition {Z B : C} {π : Z ⟶ B} [HasPullback π π]
@@ -61,7 +61,7 @@ condition which is required to be a sheaf for the regular topology.
 -/
 theorem equalizerCondition_yonedaPresheaf
     [∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G]
-    (hq : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], QuotientMap (G.map π)) :
+    (hq : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], IsQuotientMap (G.map π)) :
       EqualizerCondition (yonedaPresheaf G X) := by
   apply EqualizerCondition.mk
   intro Z B π _ _
@@ -113,7 +113,7 @@ def TopCat.toSheafCompHausLike :
     apply (config := { allowSynthFailures := true }) equalizerCondition_yonedaPresheaf
       (CompHausLike.compHausLikeToTop.{u} P) X
     intro Z B π he
-    apply QuotientMap.of_surjective_continuous (hs _ he) π.continuous
+    apply IsQuotientMap.of_surjective_continuous (hs _ he) π.continuous
 
 /--
 `TopCat.toSheafCompHausLike` yields a functor from `TopCat.{max u w}` to

Mathlib/GroupTheory/QuotientGroup/Basic.lean

@@ -432,7 +432,7 @@ the equalities, since the type of `(A'.addSubgroupOf A : AddSubgroup A)` depends
 def equivQuotientSubgroupOfOfEq {A' A B' B : Subgroup G} [hAN : (A'.subgroupOf A).Normal]
     [hBN : (B'.subgroupOf B).Normal] (h' : A' = B') (h : A = B) :
     A ⧸ A'.subgroupOf A ≃* B ⧸ B'.subgroupOf B :=
-  MonoidHom.toMulEquiv (quotientMapSubgroupOfOfLe h'.le h.le) (quotientMapSubgroupOfOfLe h'.ge h.ge)
+  (quotientMapSubgroupOfOfLe h'.le h.le).toMulEquiv (quotientMapSubgroupOfOfLe h'.ge h.ge)
     (by ext ⟨x, hx⟩; rfl)
     (by ext ⟨x, hx⟩; rfl)
 

Mathlib/RingTheory/Jacobson.lean

@@ -285,8 +285,8 @@ theorem isIntegral_isLocalization_polynomial_quotient
     [IsLocalization.Away (pX.map (Quotient.mk (P.comap (C : R →+* R[X])))).leadingCoeff Rₘ]
     [Algebra (R[X] ⧸ P) Sₘ] [IsLocalization ((Submonoid.powers (pX.map (Quotient.mk (P.comap
       (C : R →+* R[X])))).leadingCoeff).map (quotientMap P C le_rfl) : Submonoid (R[X] ⧸ P)) Sₘ] :
-    (IsLocalization.map Sₘ (quotientMap P C le_rfl) (Submonoid.powers (pX.map (Quotient.mk (P.comap
-      (C : R →+* R[X])))).leadingCoeff).le_comap_map : Rₘ →+* Sₘ).IsIntegral := by
+    (IsLocalization.map Sₘ (quotientMap P C le_rfl) (Submonoid.powers (pX.map (Quotient.mk
+      (P.comap (C : R →+* R[X])))).leadingCoeff).le_comap_map : Rₘ →+* Sₘ).IsIntegral := by
   let P' : Ideal R := P.comap C
   let M : Submonoid (R ⧸ P') :=
     Submonoid.powers (pX.map (Quotient.mk (P.comap (C : R →+* R[X])))).leadingCoeff

Mathlib/Topology/Algebra/Constructions/DomMulAct.lean

@@ -52,7 +52,10 @@ theorem coe_mkHomeomorph_symm : ⇑(mkHomeomorph : M ≃ₜ Mᵈᵐᵃ).symm = m
 @[to_additive] theorem isOpenEmbedding_mk : IsOpenEmbedding (@mk M) := mkHomeomorph.isOpenEmbedding
 @[to_additive] theorem isClosedEmbedding_mk : IsClosedEmbedding (@mk M) :=
   mkHomeomorph.isClosedEmbedding
-@[to_additive] theorem quotientMap_mk : QuotientMap (@mk M) := mkHomeomorph.quotientMap
+@[to_additive] theorem isQuotientMap_mk : IsQuotientMap (@mk M) := mkHomeomorph.isQuotientMap
+
+@[deprecated (since := "2024-10-22")]
+alias quotientMap_mk := isQuotientMap_mk
 
 @[deprecated (since := "2024-10-20")]
 alias closedEmbedding_mk := isClosedEmbedding_mk
@@ -77,7 +80,10 @@ theorem isClosedEmbedding_mk_symm : IsClosedEmbedding (@mk M).symm :=
 alias closedEmbedding_mk_symm := isClosedEmbedding_mk_symm
 
 @[to_additive]
-theorem quotientMap_mk_symm : QuotientMap (@mk M).symm := mkHomeomorph.symm.quotientMap
+theorem isQuotientMap_mk_symm : IsQuotientMap (@mk M).symm := mkHomeomorph.symm.isQuotientMap
+
+@[deprecated (since := "2024-10-22")]
+alias quotientMap_mk_symm := isQuotientMap_mk_symm
 
 @[to_additive] instance instT0Space [T0Space M] : T0Space Mᵈᵐᵃ := embedding_mk_symm.t0Space
 @[to_additive] instance instT1Space [T1Space M] : T1Space Mᵈᵐᵃ := embedding_mk_symm.t1Space
@@ -106,7 +112,7 @@ instance instDiscreteTopology [DiscreteTopology M] : DiscreteTopology Mᵈᵐᵃ
 
 @[to_additive]
 instance instSeparableSpace [SeparableSpace M] : SeparableSpace Mᵈᵐᵃ :=
-  quotientMap_mk.separableSpace
+  isQuotientMap_mk.separableSpace
 
 @[to_additive]
 instance instFirstCountableTopology [FirstCountableTopology M] : FirstCountableTopology Mᵈᵐᵃ :=

Mathlib/Topology/Algebra/Group/Basic.lean

@@ -1047,7 +1047,8 @@ theorem MulAction.isClosedMap_quotient [CompactSpace α] :
     letI := orbitRel α β
     IsClosedMap (Quotient.mk' : β → Quotient (orbitRel α β)) := by
   intro t ht
-  rw [← quotientMap_quotient_mk'.isClosed_preimage, MulAction.quotient_preimage_image_eq_union_mul]
+  rw [← isQuotientMap_quotient_mk'.isClosed_preimage,
+    MulAction.quotient_preimage_image_eq_union_mul]
   convert ht.smul_left_of_isCompact (isCompact_univ (X := α))
   rw [← biUnion_univ, ← iUnion_smul_left_image]
   rfl

Mathlib/Topology/Algebra/Group/Quotient.lean

@@ -30,8 +30,11 @@ instance [CompactSpace G] (N : Subgroup G) : CompactSpace (G ⧸ N) :=
   Quotient.compactSpace
 
 @[to_additive]
-theorem quotientMap_mk (N : Subgroup G) : QuotientMap (mk : G → G ⧸ N) :=
-  quotientMap_quot_mk
+theorem isQuotientMap_mk (N : Subgroup G) : IsQuotientMap (mk : G → G ⧸ N) :=
+  isQuotientMap_quot_mk
+
+@[deprecated (since := "2024-10-22")]
+alias quotientMap_mk := isQuotientMap_mk
 
 @[to_additive]
 theorem continuous_mk {N : Subgroup G} : Continuous (mk : G → G ⧸ N) :=
@@ -121,13 +124,13 @@ theorem _root_.topologicalGroup_quotient [N.Normal] : TopologicalGroup (G ⧸ N)
 theorem isClosedMap_coe {H : Subgroup G} (hH : IsCompact (H : Set G)) :
     IsClosedMap ((↑) : G → G ⧸ H) := by
   intro t ht
-  rw [← (quotientMap_mk H).isClosed_preimage, preimage_image_mk_eq_mul]
+  rw [← (isQuotientMap_mk H).isClosed_preimage, preimage_image_mk_eq_mul]
   exact ht.mul_right_of_isCompact hH
 
 @[to_additive]
 instance instT3Space [N.Normal] [hN : IsClosed (N : Set G)] : T3Space (G ⧸ N) := by
   rw [← QuotientGroup.ker_mk' N] at hN
-  haveI := TopologicalGroup.t1Space (G ⧸ N) ((quotientMap_mk N).isClosed_preimage.mp hN)
+  haveI := TopologicalGroup.t1Space (G ⧸ N) ((isQuotientMap_mk N).isClosed_preimage.mp hN)
   infer_instance
 
 end QuotientGroup

Mathlib/Topology/Algebra/ProperAction/Basic.lean

@@ -113,7 +113,7 @@ theorem t2Space_quotient_mulAction_of_properSMul [ProperSMul G X] :
   let π : X → Quotient R := Quotient.mk'
   have : IsOpenQuotientMap (Prod.map π π) :=
     MulAction.isOpenQuotientMap_quotientMk.prodMap MulAction.isOpenQuotientMap_quotientMk
-  rw [← this.quotientMap.isClosed_preimage]
+  rw [← this.isQuotientMap.isClosed_preimage]
   convert ProperSMul.isProperMap_smul_pair.isClosedMap.isClosed_range
   · ext ⟨x₁, x₂⟩
     simp only [mem_preimage, map_apply, mem_diagonal_iff, mem_range, Prod.mk.injEq, Prod.exists,

Mathlib/Topology/Algebra/Ring/Ideal.lean

@@ -58,12 +58,15 @@ theorem QuotientRing.isOpenMap_coe : IsOpenMap (mk N) :=
 theorem QuotientRing.isOpenQuotientMap_mk : IsOpenQuotientMap (mk N) :=
   QuotientAddGroup.isOpenQuotientMap_mk
 
-theorem QuotientRing.quotientMap_coe_coe : QuotientMap fun p : R × R => (mk N p.1, mk N p.2) :=
-  ((isOpenQuotientMap_mk N).prodMap (isOpenQuotientMap_mk N)).quotientMap
+theorem QuotientRing.isQuotientMap_coe_coe : IsQuotientMap fun p : R × R => (mk N p.1, mk N p.2) :=
+  ((isOpenQuotientMap_mk N).prodMap (isOpenQuotientMap_mk N)).isQuotientMap
+
+@[deprecated (since := "2024-10-22")]
+alias QuotientRing.quotientMap_coe_coe := QuotientRing.isQuotientMap_coe_coe
 
 instance topologicalRing_quotient : TopologicalRing (R ⧸ N) where
   __ := QuotientAddGroup.instTopologicalAddGroup _
-  continuous_mul := (QuotientRing.quotientMap_coe_coe N).continuous_iff.2 <|
+  continuous_mul := (QuotientRing.isQuotientMap_coe_coe N).continuous_iff.2 <|
     continuous_quot_mk.comp continuous_mul
 
 end CommRing