feat(Topology/Group): drop an unneeded assumption (#16551)

- prove that the quotient map `G → G ⧸ N` is an open quotient map;
- use recently added lemmas to drop a `[LocallyCompactSpace G]` assumption in `QuotientGroup.continuousSMul` (now called `QuotientGroup.instContinuousSMul`).

Author: urkud

Mathlib/MeasureTheory/Measure/Haar/Quotient.lean

@@ -223,7 +223,7 @@ theorem MeasureTheory.QuotientMeasureEqMeasurePreimage.haarMeasure_quotient [Loc
     [IsFiniteMeasure μ] : IsHaarMeasure μ := by
   obtain ⟨K⟩ := PositiveCompacts.nonempty' (α := G)
   let K' : PositiveCompacts (G ⧸ Γ) :=
-    K.map π continuous_coinduced_rng (QuotientGroup.isOpenMap_coe Γ)
+    K.map π QuotientGroup.continuous_mk QuotientGroup.isOpenMap_coe
   haveI : IsMulLeftInvariant μ :=
     MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient ν
   rw [haarMeasure_unique μ K']

Mathlib/Topology/Algebra/ConstMulAction.lean

@@ -451,6 +451,11 @@ theorem isOpenMap_quotient_mk'_mul [ContinuousConstSMul Γ T] :
   rw [isOpen_coinduced, MulAction.quotient_preimage_image_eq_union_mul U]
   exact isOpen_iUnion fun γ => isOpenMap_smul γ U hU
 
+@[to_additive]
+theorem MulAction.isOpenQuotientMap_quotientMk [ContinuousConstSMul Γ T] :
+    IsOpenQuotientMap (Quotient.mk (MulAction.orbitRel Γ T)) :=
+  ⟨surjective_quot_mk _, continuous_quot_mk, isOpenMap_quotient_mk'_mul⟩
+
 /-- The quotient by a discontinuous group action of a locally compact t2 space is t2. -/
 @[to_additive "The quotient by a discontinuous group action of a locally compact t2
 space is t2."]

Mathlib/Topology/Algebra/Group/Basic.lean

@@ -7,6 +7,7 @@ import Mathlib.GroupTheory.GroupAction.ConjAct
 import Mathlib.GroupTheory.GroupAction.Quotient
 import Mathlib.Topology.Algebra.Monoid
 import Mathlib.Topology.Algebra.Constructions
+import Mathlib.Topology.Maps.OpenQuotient
 import Mathlib.Algebra.Order.Archimedean.Basic
 import Mathlib.GroupTheory.QuotientGroup.Basic
 
@@ -862,44 +863,43 @@ instance [CompactSpace G] (N : Subgroup G) : CompactSpace (G ⧸ N) :=
 theorem quotientMap_mk (N : Subgroup G) : QuotientMap (mk : G → G ⧸ N) :=
   quotientMap_quot_mk
 
-variable [TopologicalGroup G] (N : Subgroup G)
+@[to_additive]
+theorem continuous_mk {N : Subgroup G} : Continuous (mk : G → G ⧸ N) :=
+  continuous_quot_mk
+
+section ContinuousMul
+
+variable [ContinuousMul G] {N : Subgroup G}
+
+@[to_additive]
+theorem isOpenMap_coe : IsOpenMap ((↑) : G → G ⧸ N) := isOpenMap_quotient_mk'_mul
 
 @[to_additive]
-theorem isOpenMap_coe : IsOpenMap ((↑) : G → G ⧸ N) :=
-  isOpenMap_quotient_mk'_mul
+theorem isOpenQuotientMap_mk : IsOpenQuotientMap (mk : G → G ⧸ N) :=
+  MulAction.isOpenQuotientMap_quotientMk
 
 @[to_additive (attr := simp)]
 theorem dense_preimage_mk {s : Set (G ⧸ N)} : Dense ((↑) ⁻¹' s : Set G) ↔ Dense s :=
-  letI := leftRel N -- `Dense.quotient` assumes `[Setoid G]`
-  ⟨fun h ↦ h.quotient.mono <| image_preimage_subset _ _, fun h ↦ h.preimage <| isOpenMap_coe _⟩
+  isOpenQuotientMap_mk.dense_preimage_iff
 
 @[to_additive]
 theorem dense_image_mk {s : Set G} :
     Dense (mk '' s : Set (G ⧸ N)) ↔ Dense (s * (N : Set G)) := by
   rw [← dense_preimage_mk, preimage_image_mk_eq_mul]
 
 @[to_additive]
-instance instTopologicalGroup [N.Normal] : TopologicalGroup (G ⧸ N) where
-  continuous_mul := by
-    have cont : Continuous (((↑) : G → G ⧸ N) ∘ fun p : G × G ↦ p.fst * p.snd) :=
-      continuous_quot_mk.comp continuous_mul
-    have quot : QuotientMap fun p : G × G ↦ ((p.1 : G ⧸ N), (p.2 : G ⧸ N)) := by
-      apply IsOpenMap.to_quotientMap
-      · exact (QuotientGroup.isOpenMap_coe N).prod (QuotientGroup.isOpenMap_coe N)
-      · exact continuous_quot_mk.prod_map continuous_quot_mk
-      · exact (surjective_quot_mk _).prodMap (surjective_quot_mk _)
-    exact quot.continuous_iff.2 cont
-  continuous_inv := continuous_inv.quotient_map' _
+instance instContinuousSMul : ContinuousSMul G (G ⧸ N) where
+  continuous_smul := by
+    rw [← (IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).continuous_comp_iff]
+    exact continuous_mk.comp continuous_mul
 
-@[to_additive (attr := deprecated (since := "2024-08-05"))]
-theorem _root_.topologicalGroup_quotient [N.Normal] : TopologicalGroup (G ⧸ N) :=
-  instTopologicalGroup N
+variable (N)
 
 /-- Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient. -/
 @[to_additive
   "Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient."]
 theorem nhds_eq (x : G) : 𝓝 (x : G ⧸ N) = Filter.map (↑) (𝓝 x) :=
-  le_antisymm ((QuotientGroup.isOpenMap_coe N).nhds_le x) continuous_quot_mk.continuousAt
+  (isOpenQuotientMap_mk.map_nhds_eq _).symm
 
 @[to_additive]
 instance instFirstCountableTopology [FirstCountableTopology G] :
@@ -911,6 +911,21 @@ theorem nhds_one_isCountablyGenerated [FirstCountableTopology G] [N.Normal] :
     (𝓝 (1 : G ⧸ N)).IsCountablyGenerated :=
   inferInstance
 
+end ContinuousMul
+
+variable [TopologicalGroup G] (N : Subgroup G)
+
+@[to_additive]
+instance instTopologicalGroup [N.Normal] : TopologicalGroup (G ⧸ N) where
+  continuous_mul := by
+    rw [← (isOpenQuotientMap_mk.prodMap isOpenQuotientMap_mk).continuous_comp_iff]
+    exact continuous_mk.comp continuous_mul
+  continuous_inv := continuous_inv.quotient_map' _
+
+@[to_additive (attr := deprecated (since := "2024-08-05"))]
+theorem _root_.topologicalGroup_quotient [N.Normal] : TopologicalGroup (G ⧸ N) :=
+  instTopologicalGroup N
+
 end QuotientGroup
 
 /-- A typeclass saying that `p : G × G ↦ p.1 - p.2` is a continuous function. This property
@@ -1612,7 +1627,7 @@ instance [LocallyCompactSpace G] (N : Subgroup G) : LocallyCompactSpace (G ⧸ N
   obtain ⟨y, rfl⟩ : ∃ y, π y = x := Quot.exists_rep x
   have : π ⁻¹' n ∈ 𝓝 y := preimage_nhds_coinduced hn
   rcases local_compact_nhds this with ⟨s, s_mem, hs, s_comp⟩
-  exact ⟨π '' s, (QuotientGroup.isOpenMap_coe N).image_mem_nhds s_mem, mapsTo'.mp hs,
+  exact ⟨π '' s, QuotientGroup.isOpenMap_coe.image_mem_nhds s_mem, mapsTo'.mp hs,
     s_comp.image C⟩
 
 end

Mathlib/Topology/Algebra/Group/Compact.lean

@@ -4,24 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot
 -/
 import Mathlib.Topology.Algebra.Group.Basic
-import Mathlib.Topology.CompactOpen
 import Mathlib.Topology.Sets.Compacts
 
 /-!
 # Additional results on topological groups
 
-Two results on topological groups that have been separated out as they require more substantial
-imports developing either positive compacts or the compact open topology.
-
+A result on topological groups that has been separated out
+as it requires more substantial imports developing positive compacts.
 -/
 
-universe u v w x
-
-variable {α : Type u} {β : Type v} {G : Type w} {H : Type x}
 
-section
-
-variable [TopologicalSpace G] [Group G] [TopologicalGroup G]
+universe u
+variable {G : Type u} [TopologicalSpace G] [Group G] [TopologicalGroup G]
 
 /-- Every topological group in which there exists a compact set with nonempty interior
 is locally compact. -/
@@ -32,21 +26,3 @@ theorem TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group
     (K : PositiveCompacts G) : LocallyCompactSpace G :=
   let ⟨_x, hx⟩ := K.interior_nonempty
   K.isCompact.locallyCompactSpace_of_mem_nhds_of_group (mem_interior_iff_mem_nhds.1 hx)
-
-end
-
-section Quotient
-
-variable [Group G] [TopologicalSpace G] [TopologicalGroup G] {Γ : Subgroup G}
-
-@[to_additive]
-instance QuotientGroup.continuousSMul [LocallyCompactSpace G] : ContinuousSMul G (G ⧸ Γ) where
-  continuous_smul := by
-    let F : G × G ⧸ Γ → G ⧸ Γ := fun p => p.1 • p.2
-    change Continuous F
-    have H : Continuous (F ∘ fun p : G × G => (p.1, QuotientGroup.mk p.2)) := by
-      change Continuous fun p : G × G => QuotientGroup.mk (p.1 * p.2)
-      exact continuous_coinduced_rng.comp continuous_mul
-    exact QuotientMap.continuous_lift_prod_right quotientMap_quotient_mk' H
-
-end Quotient

Mathlib/Topology/Algebra/Module/Basic.lean

@@ -2375,21 +2375,20 @@ variable {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [TopologicalSpace
 instance _root_.QuotientModule.Quotient.topologicalSpace : TopologicalSpace (M ⧸ S) :=
   inferInstanceAs (TopologicalSpace (Quotient S.quotientRel))
 
-theorem isOpenMap_mkQ [TopologicalAddGroup M] : IsOpenMap S.mkQ :=
-  QuotientAddGroup.isOpenMap_coe S.toAddSubgroup
+theorem isOpenMap_mkQ [ContinuousAdd M] : IsOpenMap S.mkQ :=
+  QuotientAddGroup.isOpenMap_coe
+
+theorem isOpenQuotientMap_mkQ [ContinuousAdd M] : IsOpenQuotientMap S.mkQ :=
+  QuotientAddGroup.isOpenQuotientMap_mk
 
 instance topologicalAddGroup_quotient [TopologicalAddGroup M] : TopologicalAddGroup (M ⧸ S) :=
   inferInstanceAs <| TopologicalAddGroup (M ⧸ S.toAddSubgroup)
 
 instance continuousSMul_quotient [TopologicalSpace R] [TopologicalAddGroup M] [ContinuousSMul R M] :
-    ContinuousSMul R (M ⧸ S) := by
-  constructor
-  have quot : QuotientMap fun au : R × M => (au.1, S.mkQ au.2) :=
-    IsOpenMap.to_quotientMap (IsOpenMap.id.prod S.isOpenMap_mkQ)
-      (continuous_id.prod_map continuous_quot_mk)
-      (Function.surjective_id.prodMap <| surjective_quot_mk _)
-  rw [quot.continuous_iff]
-  exact continuous_quot_mk.comp continuous_smul
+    ContinuousSMul R (M ⧸ S) where
+  continuous_smul := by
+    rw [← (IsOpenQuotientMap.id.prodMap S.isOpenQuotientMap_mkQ).continuous_comp_iff]
+    exact continuous_quot_mk.comp continuous_smul
 
 instance t3_quotient_of_isClosed [TopologicalAddGroup M] [IsClosed (S : Set M)] :
     T3Space (M ⧸ S) :=

Mathlib/Topology/Algebra/ProperAction.lean

@@ -129,11 +129,9 @@ theorem t2Space_quotient_mulAction_of_properSMul [ProperSMul G X] :
   rw [t2_iff_isClosed_diagonal]
   set R := MulAction.orbitRel G X
   let π : X → Quotient R := Quotient.mk'
-  have : QuotientMap (Prod.map π π) :=
-    (isOpenMap_quotient_mk'_mul.prod isOpenMap_quotient_mk'_mul).to_quotientMap
-      (continuous_quotient_mk'.prod_map continuous_quotient_mk')
-      ((surjective_quotient_mk' _).prodMap (surjective_quotient_mk' _))
-  rw [← this.isClosed_preimage]
+  have : IsOpenQuotientMap (Prod.map π π) :=
+    MulAction.isOpenQuotientMap_quotientMk.prodMap MulAction.isOpenQuotientMap_quotientMk
+  rw [← this.quotientMap.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

@@ -51,26 +51,18 @@ instance topologicalRingQuotientTopology : TopologicalSpace (R ⧸ N) :=
 -- note for the reader: in the following, `mk` is `Ideal.Quotient.mk`, the canonical map `R → R/I`.
 variable [TopologicalRing R]
 
-theorem QuotientRing.isOpenMap_coe : IsOpenMap (mk N) := by
-  intro s s_op
-  change IsOpen (mk N ⁻¹' (mk N '' s))
-  rw [quotient_ring_saturate]
-  exact isOpen_iUnion fun ⟨n, _⟩ => isOpenMap_add_left n s s_op
+theorem QuotientRing.isOpenMap_coe : IsOpenMap (mk N) :=
+  QuotientAddGroup.isOpenMap_coe
+
+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) :=
-  IsOpenMap.to_quotientMap ((QuotientRing.isOpenMap_coe N).prod (QuotientRing.isOpenMap_coe N))
-    ((continuous_quot_mk.comp continuous_fst).prod_mk (continuous_quot_mk.comp continuous_snd))
-    (by rintro ⟨⟨x⟩, ⟨y⟩⟩; exact ⟨(x, y), rfl⟩)
-
-instance topologicalRing_quotient : TopologicalRing (R ⧸ N) :=
-  TopologicalSemiring.toTopologicalRing
-    { continuous_add :=
-        have cont : Continuous (mk N ∘ fun p : R × R => p.fst + p.snd) :=
-          continuous_quot_mk.comp continuous_add
-        (QuotientMap.continuous_iff (QuotientRing.quotientMap_coe_coe N)).mpr cont
-      continuous_mul :=
-        have cont : Continuous (mk N ∘ fun p : R × R => p.fst * p.snd) :=
-          continuous_quot_mk.comp continuous_mul
-        (QuotientMap.continuous_iff (QuotientRing.quotientMap_coe_coe N)).mpr cont }
+  ((isOpenQuotientMap_mk N).prodMap (isOpenQuotientMap_mk N)).quotientMap
+
+instance topologicalRing_quotient : TopologicalRing (R ⧸ N) where
+  __ := QuotientAddGroup.instTopologicalAddGroup _
+  continuous_mul := (QuotientRing.quotientMap_coe_coe N).continuous_iff.2 <|
+    continuous_quot_mk.comp continuous_mul
 
 end CommRing

Mathlib/Topology/Maps/OpenQuotient.lean

@@ -22,7 +22,7 @@ Contrary to general quotient maps,
 the category of open quotient maps is closed under `Prod.map`.
 -/
 
-open Function Filter
+open Function Set Filter
 open scoped Topology
 
 variable {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y}
@@ -57,4 +57,8 @@ 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 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⟩
+
 end IsOpenQuotientMap