chore(Topology/Group): move QuotientGroup to a new file (#17473)

Mathlib.lean

@@ -4499,6 +4499,7 @@ import Mathlib.Topology.Algebra.FilterBasis
 import Mathlib.Topology.Algebra.Group.Basic
 import Mathlib.Topology.Algebra.Group.Compact
 import Mathlib.Topology.Algebra.Group.OpenMapping
+import Mathlib.Topology.Algebra.Group.Quotient
 import Mathlib.Topology.Algebra.Group.SubmonoidClosure
 import Mathlib.Topology.Algebra.Group.TopologicalAbelianization
 import Mathlib.Topology.Algebra.GroupCompletion

Mathlib/MeasureTheory/Constructions/Polish/Basic.lean

@@ -631,10 +631,7 @@ instance CosetSpace.borelSpace {G : Type*} [TopologicalSpace G] [PolishSpace G]
 instance QuotientGroup.borelSpace {G : Type*} [TopologicalSpace G] [PolishSpace G] [Group G]
     [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {N : Subgroup G} [N.Normal]
     [IsClosed (N : Set G)] : BorelSpace (G ⧸ N) :=
-  -- Porting note: 1st and 3rd `haveI`s were not needed in Lean 3
-  haveI := Subgroup.t3_quotient_of_isClosed N
-  haveI := QuotientGroup.secondCountableTopology (Γ := N)
-  Quotient.borelSpace
+  ⟨continuous_mk.map_eq_borel mk_surjective⟩
 
 namespace MeasureTheory
 

Mathlib/MeasureTheory/Measure/Haar/Quotient.lean

@@ -57,7 +57,7 @@ instance QuotientGroup.measurableSMul {G : Type*} [Group G] {Γ : Subgroup G} [M
     [TopologicalSpace G] [TopologicalGroup G] [BorelSpace G] [BorelSpace (G ⧸ Γ)] :
     MeasurableSMul G (G ⧸ Γ) where
   measurable_const_smul g := (continuous_const_smul g).measurable
-  measurable_smul_const x := (QuotientGroup.continuous_smul₁ x).measurable
+  measurable_smul_const _ := (continuous_id.smul continuous_const).measurable
 
 end
 

Mathlib/Topology/Algebra/Group/Basic.lean

@@ -3,13 +3,9 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot
 -/
-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.Group.Subgroup.Pointwise
 import Mathlib.Algebra.Order.Archimedean.Basic
-import Mathlib.GroupTheory.QuotientGroup.Basic
+import Mathlib.Topology.Algebra.Monoid
 
 /-!
 # Topological groups
@@ -847,87 +843,6 @@ theorem TopologicalGroup.exists_antitone_basis_nhds_one [FirstCountableTopology
 
 end TopologicalGroup
 
-namespace QuotientGroup
-
-variable [TopologicalSpace G] [Group G]
-
-@[to_additive]
-instance instTopologicalSpace (N : Subgroup G) : TopologicalSpace (G ⧸ N) :=
-  instTopologicalSpaceQuotient
-
-@[to_additive]
-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
-
-@[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 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 :=
-  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 instContinuousSMul : ContinuousSMul G (G ⧸ N) where
-  continuous_smul := by
-    rw [← (IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).continuous_comp_iff]
-    exact continuous_mk.comp continuous_mul
-
-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) :=
-  (isOpenQuotientMap_mk.map_nhds_eq _).symm
-
-@[to_additive]
-instance instFirstCountableTopology [FirstCountableTopology G] :
-    FirstCountableTopology (G ⧸ N) where
-  nhds_generated_countable := mk_surjective.forall.2 fun x ↦ nhds_eq N x ▸ inferInstance
-
-@[to_additive (attr := deprecated (since := "2024-08-05"))]
-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
 automatically holds for topological additive groups but it also holds, e.g., for `ℝ≥0`. -/
 class ContinuousSub (G : Type*) [TopologicalSpace G] [Sub G] : Prop where
@@ -1250,13 +1165,6 @@ theorem IsClosed.mul_right_of_isCompact (ht : IsClosed t) (hs : IsCompact s) :
   rw [← image_op_smul]
   exact IsClosed.smul_left_of_isCompact ht (hs.image continuous_op)
 
-@[to_additive]
-theorem QuotientGroup.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]
-  exact ht.mul_right_of_isCompact hH
-
 @[to_additive]
 lemma subset_mul_closure_one {G} [MulOneClass G] [TopologicalSpace G] (s : Set G) :
     s ⊆ s * (closure {1} : Set G) := by
@@ -1382,13 +1290,6 @@ theorem exists_closed_nhds_one_inv_eq_mul_subset {U : Set G} (hU : U ∈ 𝓝 1)
 
 variable (S : Subgroup G) [Subgroup.Normal S] [IsClosed (S : Set G)]
 
-@[to_additive]
-instance Subgroup.t3_quotient_of_isClosed (S : Subgroup G) [Subgroup.Normal S]
-    [hS : IsClosed (S : Set G)] : T3Space (G ⧸ S) := by
-  rw [← QuotientGroup.ker_mk' S] at hS
-  haveI := TopologicalGroup.t1Space (G ⧸ S) (quotientMap_quotient_mk'.isClosed_preimage.mp hS)
-  infer_instance
-
 /-- A subgroup `S` of a topological group `G` acts on `G` properly discontinuously on the left, if
 it is discrete in the sense that `S ∩ K` is finite for all compact `K`. (See also
 `DiscreteTopology`.) -/
@@ -1618,18 +1519,6 @@ theorem exists_isCompact_isClosed_nhds_one [WeaklyLocallyCompactSpace G] :
   let ⟨K, hK₁, hKcomp, hKcl⟩ := exists_mem_nhds_isCompact_isClosed (1 : G)
   ⟨K, hKcomp, hKcl, hK₁⟩
 
-/-- A quotient of a locally compact group is locally compact. -/
-@[to_additive]
-instance [LocallyCompactSpace G] (N : Subgroup G) : LocallyCompactSpace (G ⧸ N) := by
-  refine ⟨fun x n hn ↦ ?_⟩
-  let π := ((↑) : G → G ⧸ N)
-  have C : Continuous π := continuous_quotient_mk'
-  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.image_mem_nhds s_mem, mapsTo'.mp hs,
-    s_comp.image C⟩
-
 end
 
 section
@@ -1665,30 +1554,6 @@ instance {G} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] :
     TopologicalGroup (Multiplicative G) where
   continuous_inv := @continuous_neg G _ _ _
 
-section Quotient
-
-variable [Group G] [TopologicalSpace G] [ContinuousMul G] {Γ : Subgroup G}
-
-@[to_additive]
-instance QuotientGroup.continuousConstSMul : ContinuousConstSMul G (G ⧸ Γ) where
-  continuous_const_smul g := by
-     convert ((@continuous_const _ _ _ _ g).mul continuous_id).quotient_map' _
-
-@[to_additive]
-theorem QuotientGroup.continuous_smul₁ (x : G ⧸ Γ) : Continuous fun g : G => g • x := by
-  induction x using QuotientGroup.induction_on
-  exact continuous_quotient_mk'.comp (continuous_mul_right _)
-
-/-- The quotient of a second countable topological group by a subgroup is second countable. -/
-@[to_additive
-  "The quotient of a second countable additive topological group by a subgroup is second
-  countable."]
-instance QuotientGroup.secondCountableTopology [SecondCountableTopology G] :
-    SecondCountableTopology (G ⧸ Γ) :=
-  ContinuousConstSMul.secondCountableTopology
-
-end Quotient
-
 /-- If `G` is a group with topological `⁻¹`, then it is homeomorphic to its units. -/
 @[to_additive " If `G` is an additive group with topological negation, then it is homeomorphic to
 its additive units."]
@@ -1944,4 +1809,4 @@ theorem coinduced_continuous {α β : Type*} [t : TopologicalSpace α] [Group β
 
 end GroupTopology
 
-set_option linter.style.longFile 2100
+set_option linter.style.longFile 2000

Mathlib/Topology/Algebra/Group/Quotient.lean

@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot, Yury Kudryashov
+-/
+import Mathlib.GroupTheory.GroupAction.Quotient
+import Mathlib.GroupTheory.QuotientGroup.Basic
+import Mathlib.Topology.Algebra.Group.Basic
+import Mathlib.Topology.Maps.OpenQuotient
+
+/-!
+# Topology on the quotient group
+
+In this file we define topology on `G ⧸ N`, where `N` is a subgroup of `G`,
+and prove basic properties of this topology.
+-/
+
+open scoped Pointwise Topology
+
+variable {G : Type*} [TopologicalSpace G] [Group G]
+
+namespace QuotientGroup
+
+@[to_additive]
+instance instTopologicalSpace (N : Subgroup G) : TopologicalSpace (G ⧸ N) :=
+  instTopologicalSpaceQuotient
+
+@[to_additive]
+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
+
+@[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 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 :=
+  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 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]
+instance instContinuousConstSMul : ContinuousConstSMul G (G ⧸ N) := inferInstance
+
+/-- A quotient of a locally compact group is locally compact. -/
+@[to_additive]
+instance instLocallyCompactSpace [LocallyCompactSpace G] (N : Subgroup G) :
+    LocallyCompactSpace (G ⧸ N) :=
+  QuotientGroup.isOpenQuotientMap_mk.locallyCompactSpace
+
+@[to_additive (attr := deprecated (since := "2024-10-05"))]
+theorem continuous_smul₁ (x : G ⧸ N) : Continuous fun g : G => g • x :=
+  continuous_id.smul continuous_const
+
+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) :=
+  (isOpenQuotientMap_mk.map_nhds_eq _).symm
+
+@[to_additive]
+instance instFirstCountableTopology [FirstCountableTopology G] :
+    FirstCountableTopology (G ⧸ N) where
+  nhds_generated_countable := mk_surjective.forall.2 fun x ↦ nhds_eq N x ▸ inferInstance
+
+/-- The quotient of a second countable topological group by a subgroup is second countable. -/
+@[to_additive
+  "The quotient of a second countable additive topological group by a subgroup is second
+  countable."]
+instance instSecondCountableTopology [SecondCountableTopology G] :
+    SecondCountableTopology (G ⧸ N) :=
+  ContinuousConstSMul.secondCountableTopology
+
+@[to_additive (attr := deprecated (since := "2024-08-05"))]
+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
+
+@[to_additive]
+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]
+  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)
+  infer_instance
+
+end QuotientGroup

Mathlib/Topology/Algebra/Module/Basic.lean

@@ -2393,7 +2393,7 @@ instance continuousSMul_quotient [TopologicalSpace R] [TopologicalAddGroup M] [C
 instance t3_quotient_of_isClosed [TopologicalAddGroup M] [IsClosed (S : Set M)] :
     T3Space (M ⧸ S) :=
   letI : IsClosed (S.toAddSubgroup : Set M) := ‹_›
-  S.toAddSubgroup.t3_quotient_of_isClosed
+  QuotientAddGroup.instT3Space S.toAddSubgroup
 
 end Submodule
 

Mathlib/Topology/Algebra/OpenSubgroup.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Nailin Guan
 -/
 import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.Topology.Algebra.Group.Quotient
 import Mathlib.Topology.Algebra.Ring.Basic
 import Mathlib.Topology.Sets.Opens
 

Mathlib/Topology/Algebra/ProperAction/Basic.lean

@@ -5,6 +5,7 @@ Authors: Anatole Dedeker, Etienne Marion, Florestan Martin-Baillon, Vincent Guir
 -/
 import Mathlib.Topology.Algebra.MulAction
 import Mathlib.Topology.Maps.Proper.Basic
+import Mathlib.Topology.Maps.OpenQuotient
 
 /-!
 # Proper group action

Mathlib/Topology/Algebra/Ring/Ideal.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot
 -/
 import Mathlib.Topology.Algebra.Ring.Basic
+import Mathlib.Topology.Algebra.Group.Quotient
 import Mathlib.RingTheory.Ideal.Quotient
 
 /-!

Mathlib/Topology/Algebra/UniformGroup.lean

@@ -7,7 +7,7 @@ import Mathlib.Topology.UniformSpace.UniformConvergence
 import Mathlib.Topology.UniformSpace.UniformEmbedding
 import Mathlib.Topology.UniformSpace.CompleteSeparated
 import Mathlib.Topology.UniformSpace.Compact
-import Mathlib.Topology.Algebra.Group.Basic
+import Mathlib.Topology.Algebra.Group.Quotient
 import Mathlib.Topology.DiscreteSubset
 import Mathlib.Tactic.Abel