feat(topology/algebra/group): continuity of action of a group on its …

…own coset space (#11772)

Given a subgroup `Γ` of a topological group `G`, there is an induced scalar action of `G` on the coset space `G ⧸ Γ`, and there is also an induced topology on `G ⧸ Γ`.  We prove that this action is continuous in each variable, and, if the group `G` is locally compact, also jointly continuous.

Co-authored-by: Alex Kontorovich <58564076+AlexKontorovich@users.noreply.github.com>

src/topology/algebra/group.lean

@@ -8,6 +8,8 @@ import order.filter.pointwise
 import topology.algebra.monoid
 import topology.homeomorph
 import topology.compacts
+import topology.algebra.mul_action
+import topology.compact_open
 
 /-!
 # Theory of topological groups
@@ -769,6 +771,40 @@ instance multiplicative.topological_group {G} [h : topological_space G]
   [add_group G] [topological_add_group G] : @topological_group (multiplicative G) h _ :=
 { continuous_inv := @continuous_neg G _ _ _ }
 
+section quotient
+variables [group G] [topological_space G] [topological_group G] {Γ : subgroup G}
+
+@[to_additive]
+instance quotient_group.has_continuous_smul₂ : has_continuous_smul₂ G (G ⧸ Γ) :=
+{ continuous_smul₂ := λ g₀, begin
+    apply continuous_coinduced_dom,
+    change continuous (λ g : G, quotient_group.mk (g₀ * g)),
+    exact continuous_coinduced_rng.comp (continuous_mul_left g₀),
+  end }
+
+@[to_additive]
+lemma quotient_group.continuous_smul₁ (x : G ⧸ Γ) : continuous (λ g : G, g • x) :=
+begin
+  obtain ⟨g₀, rfl⟩ : ∃ g₀, quotient_group.mk g₀ = x,
+  { exact @quotient.exists_rep _ (quotient_group.left_rel Γ) x },
+  change continuous (λ g, quotient_group.mk (g * g₀)),
+  exact continuous_coinduced_rng.comp (continuous_mul_right g₀)
+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 }
+
+end quotient
+
 namespace units
 
 variables [monoid α] [topological_space α] [has_continuous_mul α] [monoid β] [topological_space β]

src/topology/algebra/group_completion.lean

@@ -85,7 +85,7 @@ instance : add_monoid (completion α) :=
 instance : sub_neg_monoid (completion α) :=
 { sub_eq_add_neg := λ a b, completion.induction_on₂ a b
     (is_closed_eq (continuous_map₂ continuous_fst continuous_snd)
-      (continuous_map₂ continuous_fst (continuous_map.comp continuous_snd)))
+      (continuous_map₂ continuous_fst (completion.continuous_map.comp continuous_snd)))
    (λ a b, by exact_mod_cast congr_arg coe (sub_eq_add_neg a b)),
   .. completion.add_monoid, .. completion.has_neg, .. completion.has_sub }
 

src/topology/compact_open.lean

@@ -7,6 +7,7 @@ import tactic.tidy
 import topology.continuous_function.basic
 import topology.homeomorph
 import topology.subset_properties
+import topology.maps
 
 /-!
 # The compact-open topology
@@ -336,3 +337,39 @@ rfl
 rfl
 
 end homeomorph
+
+section quotient_map
+
+variables {X₀ X Y Z : Type*} [topological_space X₀] [topological_space X]
+  [topological_space Y] [topological_space Z] [locally_compact_space Y] {f : X₀ → X}
+
+lemma quotient_map.continuous_lift_prod_left (hf : quotient_map f) {g : X × Y → Z}
+  (hg : continuous (λ p : X₀ × Y, g (f p.1, p.2))) : continuous g :=
+begin
+  let Gf : C(X₀, C(Y, Z)) := continuous_map.curry ⟨_, hg⟩,
+  have h : ∀ x : X, continuous (λ y, g (x, y)),
+  { intros x,
+    obtain ⟨x₀, rfl⟩ := hf.surjective x,
+    exact (Gf x₀).continuous },
+  let G : X → C(Y, Z) := λ x, ⟨_, h x⟩,
+  have : continuous G,
+  { rw hf.continuous_iff,
+    exact Gf.continuous },
+  convert continuous_map.continuous_uncurry_of_continuous ⟨G, this⟩,
+  ext x,
+  cases x,
+  refl,
+end
+
+lemma quotient_map.continuous_lift_prod_right (hf : quotient_map f) {g : Y × X → Z}
+  (hg : continuous (λ p : Y × X₀, g (p.1, f p.2))) : continuous g :=
+begin
+  have : continuous (λ p : X₀ × Y, g ((prod.swap p).1, f (prod.swap p).2)),
+  { exact hg.comp continuous_swap },
+  have : continuous (λ p : X₀ × Y, (g ∘ prod.swap) (f p.1, p.2)) := this,
+  convert (hf.continuous_lift_prod_left this).comp continuous_swap,
+  ext x,
+  simp,
+end
+
+end quotient_map