refactor(topology/algebra/group): split file (#17697)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/dynamics/flow.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jean Lo
 -/
 
-import topology.algebra.group
+import topology.algebra.group.basic
 import logic.function.iterate
 
 /-!

src/measure_theory/integral/riesz_markov_kakutani.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jesse Reimann, Kalle Kytölä
 -/
 import topology.continuous_function.bounded
+import topology.sets.compacts
 
 /-!
 #  Riesz–Markov–Kakutani representation theorem

src/measure_theory/measure/haar.lean

@@ -6,6 +6,7 @@ Authors: Floris van Doorn
 import measure_theory.measure.content
 import measure_theory.group.prod
 import group_theory.divisible
+import topology.algebra.group.compact
 
 /-!
 # Haar measure

src/topology/algebra/affine.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Frédéric Dupuis
 -/
 import linear_algebra.affine_space.affine_map
-import topology.algebra.group
+import topology.algebra.group.basic
 import topology.algebra.mul_action
 
 /-!

src/topology/algebra/group.lean → src/topology/algebra/group/basic.lean

@@ -8,8 +8,6 @@ import group_theory.group_action.quotient
 import group_theory.quotient_group
 import order.filter.pointwise
 import topology.algebra.monoid
-import topology.compact_open
-import topology.sets.compacts
 import topology.algebra.constructions
 
 /-!
@@ -1190,25 +1188,6 @@ begin
     exact ⟨n, hn⟩ }
 end
 
-/-- Every separated topological group in which there exists a compact set with nonempty interior
-is locally compact. -/
-@[to_additive "Every separated topological group in which there exists a compact set with nonempty
-interior is locally compact."]
-lemma topological_space.positive_compacts.locally_compact_space_of_group
-  [t2_space G] (K : positive_compacts G) :
-  locally_compact_space G :=
-begin
-  refine locally_compact_of_compact_nhds (λ x, _),
-  obtain ⟨y, hy⟩ := K.interior_nonempty,
-  let F := homeomorph.mul_left (x * y⁻¹),
-  refine ⟨F '' K, _, K.is_compact.image F.continuous⟩,
-  suffices : F.symm ⁻¹' K ∈ 𝓝 x, by { convert this, apply equiv.image_eq_preimage },
-  apply continuous_at.preimage_mem_nhds F.symm.continuous.continuous_at,
-  have : F.symm x = y, by simp [F, homeomorph.mul_left_symm],
-  rw this,
-  exact mem_interior_iff_mem_nhds.1 hy
-end
-
 /-- Given two compact sets in a noncompact topological group, there is a translate of the second
 one that is disjoint from the first one. -/
 @[to_additive "Given two compact sets in a noncompact additive topological group, there is a
@@ -1314,18 +1293,6 @@ begin
   exact continuous_quotient_mk.comp (continuous_mul_right x)
 end
 
-@[to_additive]
-instance quotient_group.has_continuous_smul [locally_compact_space G] :
-  has_continuous_smul G (G ⧸ Γ) :=
-{ continuous_smul := begin
-    let F : G × G ⧸ Γ → G ⧸ Γ := λ p, p.1 • p.2,
-    change continuous F,
-    have H : continuous (F ∘ (λ p : G × G, (p.1, quotient_group.mk p.2))),
-    { change continuous (λ p : G × G, quotient_group.mk (p.1 * p.2)),
-      refine continuous_coinduced_rng.comp continuous_mul },
-    exact quotient_map.continuous_lift_prod_right quotient_map_quotient_mk H,
-  end }
-
 /-- 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."]

src/topology/algebra/group/compact.lean

@@ -0,0 +1,66 @@
+/-
+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 topology.algebra.group.basic
+import topology.compact_open
+import 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.
+
+-/
+
+open classical set filter topological_space function
+open_locale classical topological_space filter pointwise
+
+universes u v w x
+variables {α : Type u} {β : Type v} {G : Type w} {H : Type x}
+
+section
+
+/-! Some results about an open set containing the product of two sets in a topological group. -/
+
+variables [topological_space G] [group G] [topological_group G]
+
+/-- Every separated topological group in which there exists a compact set with nonempty interior
+is locally compact. -/
+@[to_additive "Every separated topological group in which there exists a compact set with nonempty
+interior is locally compact."]
+lemma topological_space.positive_compacts.locally_compact_space_of_group
+  [t2_space G] (K : positive_compacts G) :
+  locally_compact_space G :=
+begin
+  refine locally_compact_of_compact_nhds (λ x, _),
+  obtain ⟨y, hy⟩ := K.interior_nonempty,
+  let F := homeomorph.mul_left (x * y⁻¹),
+  refine ⟨F '' K, _, K.is_compact.image F.continuous⟩,
+  suffices : F.symm ⁻¹' K ∈ 𝓝 x, by { convert this, apply equiv.image_eq_preimage },
+  apply continuous_at.preimage_mem_nhds F.symm.continuous.continuous_at,
+  have : F.symm x = y, by simp [F, homeomorph.mul_left_symm],
+  rw this,
+  exact mem_interior_iff_mem_nhds.1 hy
+end
+
+end
+
+section quotient
+variables [group G] [topological_space G] [topological_group G] {Γ : subgroup G}
+
+@[to_additive]
+instance quotient_group.has_continuous_smul [locally_compact_space G] :
+  has_continuous_smul G (G ⧸ Γ) :=
+{ continuous_smul := begin
+    let F : G × G ⧸ Γ → G ⧸ Γ := λ p, p.1 • p.2,
+    change continuous F,
+    have H : continuous (F ∘ (λ p : G × G, (p.1, quotient_group.mk p.2))),
+    { change continuous (λ p : G × G, quotient_group.mk (p.1 * p.2)),
+      refine continuous_coinduced_rng.comp continuous_mul },
+    exact quotient_map.continuous_lift_prod_right quotient_map_quotient_mk H,
+  end }
+
+end quotient

src/topology/algebra/module/basic.lean

@@ -7,6 +7,7 @@ Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo, Yury Kudryashov, Fréd
 import topology.algebra.ring
 import topology.algebra.mul_action
 import topology.algebra.uniform_group
+import topology.continuous_function.basic
 import topology.uniform_space.uniform_embedding
 import algebra.algebra.basic
 import linear_algebra.projection

src/topology/algebra/order/basic.lean

@@ -6,7 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
 import data.set.intervals.pi
 import data.set.pointwise.interval
 import order.filter.interval
-import topology.algebra.group
+import topology.algebra.group.basic
 import topology.algebra.order.left_right
 
 /-!
@@ -1624,7 +1624,7 @@ instance linear_ordered_add_comm_group.topological_add_group : topological_add_g
         calc |x - a + (y - b)| ≤ |x - a| + |y - b| : abs_add _ _
         ... < δ + (ε - δ) : add_lt_add hx hy
         ... = ε : add_sub_cancel'_right _ _ },
-      { -- Otherewise `ε`-nhd of each point `a` is `{a}`
+      { -- Otherwise `ε`-nhd of each point `a` is `{a}`
         have hε : ∀ {x y}, |x - y| < ε → x = y,
         { intros x y h,
           simpa [sub_eq_zero] using h₂ _ h },

src/topology/algebra/ring.lean

@@ -6,7 +6,7 @@ Authors: Patrick Massot, Johannes Hölzl
 import algebra.ring.prod
 import ring_theory.ideal.quotient
 import ring_theory.subring.basic
-import topology.algebra.group
+import topology.algebra.group.basic
 
 /-!
 

src/topology/algebra/uniform_group.lean

@@ -7,7 +7,7 @@ import topology.uniform_space.uniform_convergence
 import topology.uniform_space.uniform_embedding
 import topology.uniform_space.complete_separated
 import topology.uniform_space.compact
-import topology.algebra.group
+import topology.algebra.group.basic
 import tactic.abel
 
 /-!

src/topology/metric_space/baire.lean

@@ -6,6 +6,7 @@ Authors: Sébastien Gouëzel
 import analysis.specific_limits.basic
 import order.filter.countable_Inter
 import topology.G_delta
+import topology.sets.compacts
 
 /-!
 # Baire theorem

src/topology/path_connected.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot
 -/
 import topology.algebra.order.proj_Icc
+import topology.compact_open
 import topology.continuous_function.basic
 import topology.unit_interval