refactor(Normed/Group/Quotient): generalise to non-abelian groups

Mathlib/Analysis/Normed/Group/Quotient.lean

@@ -102,11 +102,16 @@ noncomputable section
 open Metric Set Topology NNReal
 
 namespace QuotientGroup
-variable {M : Type*} [SeminormedCommGroup M] {S T : Subgroup M} {x : M ⧸ S} {m : M} {r ε : ℝ}
+variable {M : Type*}
+
+section SeminormedGroup
+variable [SeminormedGroup M] {S T : Subgroup M} {x : M ⧸ S} {m : M} {r ε : ℝ}
 
 @[to_additive add_norm_aux]
 private lemma norm_aux (x : M ⧸ S) : {m : M | (m : M ⧸ S) = x}.Nonempty := Quot.exists_rep x
 
+variable [S.Normal] [T.Normal]
+
 /-- The norm of `x` on the quotient by a subgroup `S` is defined as the infimum of the norm on
 `x * M`. -/
 @[to_additive
@@ -157,6 +162,29 @@ lemma nhds_one_hasBasis : (𝓝 (1 : M ⧸ S)).HasBasis (fun ε ↦ 0 < ε) fun
   rw [← mk_one, nhds_eq, ← funext this]
   exact .map _ Metric.nhds_basis_ball
 
+/-- The norm of the projection is smaller or equal to the norm of the original element. -/
+@[to_additive
+/-- The norm of the projection is smaller or equal to the norm of the original element. -/]
+lemma norm_mk_le_norm : ‖(m : M ⧸ S)‖ ≤ ‖m‖ :=
+  (infDist_le_dist_of_mem (by simp)).trans_eq (dist_one_left _)
+
+/-- For any `x : M ⧸ S` and any `0 < ε`, there is `m : M` such that `mk' S m = x`
+and `‖m‖ < ‖x‖ + ε`. -/
+@[to_additive /-- For any `x : M ⧸ S` and any `0 < ε`, there is `m : M` such that `mk' S m = x`
+and `‖m‖ < ‖x‖ + ε`. -/]
+lemma exists_norm_mk_lt (x : M ⧸ S) (hε : 0 < ε) : ∃ m : M, m = x ∧ ‖m‖ < ‖x‖ + ε :=
+  norm_lt_iff.1 <| lt_add_of_pos_right _ hε
+
+/-- For any `m : M` and any `0 < ε`, there is `s ∈ S` such that `‖m * s‖ < ‖mk' S m‖ + ε`. -/
+@[to_additive
+/-- For any `m : M` and any `0 < ε`, there is `s ∈ S` such that `‖m + s‖ < ‖mk' S m‖ + ε`. -/]
+lemma exists_norm_mul_lt (S : Subgroup M) [S.Normal] (m : M) {ε : ℝ} (hε : 0 < ε) :
+    ∃ s ∈ S, ‖m * s‖ < ‖mk' S m‖ + ε := by
+  obtain ⟨n : M, hn, hn'⟩ := exists_norm_mk_lt (QuotientGroup.mk' S m) hε
+  exact ⟨m⁻¹ * n, by simpa [eq_comm, QuotientGroup.eq] using hn, by simpa⟩
+
+variable [IsIsometricSMul M M]
+
 /-- An alternative definition of the norm on the quotient group: the norm of `((x : M) : M ⧸ S)` is
 equal to the distance from `x` to `S`. -/
 @[to_additive
@@ -167,12 +195,6 @@ lemma norm_mk (x : M) : ‖(x : M ⧸ S)‖ = infDist x S := by
     ← IsometryEquiv.preimage_symm]
   simp
 
-/-- The norm of the projection is smaller or equal to the norm of the original element. -/
-@[to_additive
-/-- The norm of the projection is smaller or equal to the norm of the original element. -/]
-lemma norm_mk_le_norm : ‖(m : M ⧸ S)‖ ≤ ‖m‖ :=
-  (infDist_le_dist_of_mem (by simp)).trans_eq (dist_one_left _)
-
 /-- The norm of the image of `m : M` in the quotient by `S` is zero if and only if `m` belongs
 to the closure of `S`. -/
 @[to_additive /-- The norm of the image of `m : M` in the quotient by `S` is zero if and only if `m`
@@ -188,46 +210,29 @@ if and only if `m ∈ S`. -/]
 lemma norm_mk_eq_zero [hS : IsClosed (S : Set M)] : ‖(m : M ⧸ S)‖ = 0 ↔ m ∈ S := by
   rw [norm_mk_eq_zero_iff_mem_closure, hS.closure_eq, SetLike.mem_coe]
 
-/-- For any `x : M ⧸ S` and any `0 < ε`, there is `m : M` such that `mk' S m = x`
-and `‖m‖ < ‖x‖ + ε`. -/
-@[to_additive /-- For any `x : M ⧸ S` and any `0 < ε`, there is `m : M` such that `mk' S m = x`
-and `‖m‖ < ‖x‖ + ε`. -/]
-lemma exists_norm_mk_lt (x : M ⧸ S) (hε : 0 < ε) : ∃ m : M, m = x ∧ ‖m‖ < ‖x‖ + ε :=
-  norm_lt_iff.1 <| lt_add_of_pos_right _ hε
-
-/-- For any `m : M` and any `0 < ε`, there is `s ∈ S` such that `‖m * s‖ < ‖mk' S m‖ + ε`. -/
-@[to_additive
-/-- For any `m : M` and any `0 < ε`, there is `s ∈ S` such that `‖m + s‖ < ‖mk' S m‖ + ε`. -/]
-lemma exists_norm_mul_lt (S : Subgroup M) (m : M) {ε : ℝ} (hε : 0 < ε) :
-    ∃ s ∈ S, ‖m * s‖ < ‖mk' S m‖ + ε := by
-  obtain ⟨n : M, hn, hn'⟩ := exists_norm_mk_lt (QuotientGroup.mk' S m) hε
-  exact ⟨m⁻¹ * n, by simpa [eq_comm, QuotientGroup.eq] using hn, by simpa⟩
-
 variable (S) in
 /-- The seminormed group structure on the quotient by a subgroup. -/
 @[to_additive /-- The seminormed group structure on the quotient by an additive subgroup. -/]
-noncomputable instance instSeminormedCommGroup : SeminormedCommGroup (M ⧸ S) where
+noncomputable instance instSeminormedGroup : SeminormedGroup (M ⧸ S) where
   toUniformSpace := IsTopologicalGroup.rightUniformSpace (M ⧸ S)
-  __ := groupSeminorm.toSeminormedCommGroup
+  __ := groupSeminorm.toSeminormedGroup
   uniformity_dist := by
     rw [uniformity_eq_comap_nhds_one', (nhds_one_hasBasis.comap _).eq_biInf]
     simp only [dist, preimage_setOf_eq, norm_eq_groupSeminorm, map_div_rev]
 
 variable (S) in
 /-- The quotient in the category of normed groups. -/
 @[to_additive /-- The quotient in the category of normed groups. -/]
-noncomputable instance instNormedCommGroup [hS : IsClosed (S : Set M)] :
-    NormedCommGroup (M ⧸ S) where
+noncomputable instance instNormedGroup [hS : IsClosed (S : Set M)] : NormedGroup (M ⧸ S) where
   __ := MetricSpace.ofT0PseudoMetricSpace _
 
 -- This is a sanity check left here on purpose to ensure that potential refactors won't destroy
 -- this important property.
 example :
     (instTopologicalSpaceQuotient : TopologicalSpace <| M ⧸ S) =
-      (instSeminormedCommGroup S).toUniformSpace.toTopologicalSpace := rfl
+      (instSeminormedGroup S).toUniformSpace.toTopologicalSpace := rfl
 
-example [IsClosed (S : Set M)] :
-    (instSeminormedCommGroup S) = NormedCommGroup.toSeminormedCommGroup := rfl
+example [IsClosed (S : Set M)] : (instSeminormedGroup S) = NormedGroup.toSeminormedGroup := rfl
 
 /-- An isometric version of `Subgroup.quotientEquivOfEq`. -/
 @[to_additive /-- An isometric version of `AddSubgroup.quotientEquivOfEq`. -/]
@@ -245,6 +250,21 @@ def quotientBotIsometryEquiv : M ⧸ (⊥ : Subgroup M) ≃ᵢ M where
     change ‖x‖ = ‖QuotientGroup.mk x‖
     simp [norm_mk]
 
+end SeminormedGroup
+
+variable [SeminormedCommGroup M] {S T : Subgroup M}
+
+variable (S) in
+/-- The seminormed group structure on the quotient by a subgroup. -/
+@[to_additive /-- The seminormed group structure on the quotient by an additive subgroup. -/]
+noncomputable instance instSeminormedCommGroup : SeminormedCommGroup (M ⧸ S) where
+
+variable (S) in
+/-- The quotient in the category of normed groups. -/
+@[to_additive /-- The quotient in the category of normed groups. -/]
+noncomputable instance instNormedCommGroup [hS : IsClosed (S : Set M)] :
+    NormedCommGroup (M ⧸ S) where
+
 /-- An isometric version of `QuotientGroup.quotientQuotientEquivQuotient`. -/
 @[to_additive /-- An isometric version of `QuotientAddGroup.quotientQuotientEquivQuotient`. -/]
 def quotientQuotientIsometryEquivQuotient (h : S ≤ T) : (M ⧸ S) ⧸ T.map (mk' S) ≃ᵢ M ⧸ T where

Mathlib/Analysis/Normed/Group/Uniform.lean

@@ -21,7 +21,7 @@ groups.
 
 variable {𝓕 E F : Type*}
 
-open Filter Function Metric Bornology
+open Filter Function Metric Bornology Finset
 open scoped ENNReal NNReal Uniformity Pointwise Topology
 
 section SeminormedGroup
@@ -187,15 +187,15 @@ theorem uniformContinuous_norm' : UniformContinuous (norm : E → ℝ) :=
 theorem uniformContinuous_nnnorm' : UniformContinuous fun a : E => ‖a‖₊ :=
   uniformContinuous_norm'.subtype_mk _
 
-end SeminormedGroup
+namespace AntilipschitzWith
 
-section SeminormedCommGroup
+@[to_additive le_mul_norm_sub]
+theorem le_mul_norm_div {K : ℝ≥0} {f : E → F} (hf : AntilipschitzWith K f) (x y : E) :
+    ‖x / y‖ ≤ K * ‖f x / f y‖ := by simp [← dist_eq_norm_div, hf.le_mul_dist x y]
 
-variable [SeminormedCommGroup E] [SeminormedCommGroup F] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ}
+end AntilipschitzWith
 
-@[to_additive]
-instance NormedGroup.to_isIsometricSMul_left : IsIsometricSMul E E :=
-  ⟨fun a => Isometry.of_dist_eq fun b c => by simp [dist_eq_norm_div]⟩
+variable [IsIsometricSMul E E] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ}
 
 @[to_additive (attr := simp)]
 theorem dist_self_mul_right (a b : E) : dist a (a * b) = ‖b‖ := by
@@ -237,8 +237,6 @@ theorem abs_dist_sub_le_dist_mul_mul (a₁ a₂ b₁ b₂ : E) :
   simpa only [dist_mul_left, dist_mul_right, dist_comm b₂] using
     abs_dist_sub_le (a₁ * a₂) (b₁ * b₂) (b₁ * a₂)
 
-open Finset
-
 @[to_additive]
 theorem nndist_mul_mul_le (a₁ a₂ b₁ b₂ : E) :
     nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂ :=
@@ -252,8 +250,7 @@ theorem edist_mul_mul_le (a₁ a₂ b₁ b₂ : E) :
   apply nndist_mul_mul_le
 
 section PseudoEMetricSpace
-variable {α E : Type*} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K Kf Kg : ℝ≥0}
-  {f g : α → E} {s : Set α}
+variable {α : Type*} [PseudoEMetricSpace α] {K Kf Kg : ℝ≥0} {f g : α → E} {s : Set α}
 
 @[to_additive (attr := simp)]
 lemma lipschitzWith_inv_iff : LipschitzWith K f⁻¹ ↔ LipschitzWith K f := by simp [LipschitzWith]
@@ -343,17 +340,47 @@ theorem mul_lipschitzWith (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg g
       sub_le_sub (hf.mul_le_dist x y) (hg.dist_le_mul x y)
     _ ≤ _ := le_trans (le_abs_self _) (abs_dist_sub_le_dist_mul_mul _ _ _ _)
 
+end AntilipschitzWith
+end PseudoEMetricSpace
+
+-- See note [lower instance priority]
+@[to_additive]
+instance (priority := 100) SeminormedGroup.to_lipschitzMul : LipschitzMul E :=
+  ⟨⟨1 + 1, LipschitzWith.prod_fst.mul LipschitzWith.prod_snd⟩⟩
+
+-- See note [lower instance priority]
+/-- A seminormed group is a uniform group, i.e., multiplication and division are uniformly
+continuous. -/
+@[to_additive /-- A seminormed group is a uniform additive group, i.e., addition and subtraction are
+uniformly continuous. -/]
+instance (priority := 100) SeminormedGroup.to_isUniformGroup : IsUniformGroup E :=
+  ⟨(LipschitzWith.prod_fst.div LipschitzWith.prod_snd).uniformContinuous⟩
+
+-- short-circuit type class inference
+-- See note [lower instance priority]
+@[to_additive]
+instance (priority := 100) SeminormedGroup.toIsTopologicalGroup : IsTopologicalGroup E :=
+  inferInstance
+
+end SeminormedGroup
+
+section SeminormedCommGroup
+variable [SeminormedCommGroup E] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ}
+
+-- See note [lower instance priority]
+@[to_additive]
+instance (priority := 100) NormedGroup.to_isIsometricSMul_left : IsIsometricSMul E E :=
+  ⟨fun a => Isometry.of_dist_eq fun b c => by simp [dist_eq_norm_div]⟩
+
+namespace AntilipschitzWith
+variable {α : Type*} [PseudoEMetricSpace α] {Kf Kg : ℝ≥0} {f g : α → E}
+
 @[to_additive]
 theorem mul_div_lipschitzWith (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg (g / f))
     (hK : Kg < Kf⁻¹) : AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g := by
   simpa only [Pi.div_apply, mul_div_cancel] using hf.mul_lipschitzWith hg hK
 
-@[to_additive le_mul_norm_sub]
-theorem le_mul_norm_div {f : E → F} (hf : AntilipschitzWith K f) (x y : E) :
-    ‖x / y‖ ≤ K * ‖f x / f y‖ := by simp [← dist_eq_norm_div, hf.le_mul_dist x y]
-
 end AntilipschitzWith
-end PseudoEMetricSpace
 
 -- See note [lower instance priority]
 @[to_additive]

Mathlib/GroupTheory/GroupAction/Quotient.lean

@@ -264,10 +264,12 @@ theorem sum_card_fixedBy_eq_card_orbits_mul_card_group [Fintype α] [∀ a : α,
 
 @[to_additive]
 instance isPretransitive_quotient (G) [Group G] (H : Subgroup G) : IsPretransitive G (G ⧸ H) where
-  exists_smul_eq := by
-    { rintro ⟨x⟩ ⟨y⟩
-      refine ⟨y * x⁻¹, QuotientGroup.eq.mpr ?_⟩
-      simp only [smul_eq_mul, H.one_mem, inv_mul_cancel, inv_mul_cancel_right]}
+  exists_smul_eq := by rintro ⟨x⟩ ⟨y⟩; exact ⟨y * x⁻¹, QuotientGroup.eq.mpr <| by simp⟩
+
+@[to_additive]
+instance isPretransitive_mulOpposite_quotient (G) [Group G] (H : Subgroup G) [H.Normal] :
+    IsPretransitive Gᵐᵒᵖ (G ⧸ H) where
+  exists_smul_eq := by rintro ⟨x⟩ ⟨y⟩; exact ⟨.op <| x⁻¹ * y, QuotientGroup.eq.mpr <| by simp⟩
 
 variable {α}
 

Mathlib/Topology/Algebra/ConstMulAction.lean

@@ -202,6 +202,10 @@ theorem tendsto_const_smul_iff {f : β → α} {l : Filter β} {a : α} (c : G)
     Tendsto (fun x => c • f x) l (𝓝 <| c • a) ↔ Tendsto f l (𝓝 a) :=
   ⟨fun h => by simpa only [inv_smul_smul] using h.const_smul c⁻¹, fun h => h.const_smul _⟩
 
+@[to_additive]
+instance Subgroup.continuousConstSMul {S : Subgroup G} : ContinuousConstSMul S α :=
+  IsInducing.id.continuousConstSMul Subtype.val rfl
+
 variable [TopologicalSpace β] {f : β → α} {b : β} {s : Set β}
 
 @[to_additive]

Mathlib/Topology/Algebra/Group/Quotient.lean

@@ -24,7 +24,7 @@ assert_not_exists Cardinal
 open Topology
 open scoped Pointwise
 
-variable {G : Type*} [TopologicalSpace G] [Group G]
+variable {G M : Type*} [TopologicalSpace G] [Group G] [TopologicalSpace M] [Monoid M]
 
 namespace QuotientGroup
 
@@ -44,9 +44,8 @@ theorem isQuotientMap_mk (N : Subgroup G) : IsQuotientMap (mk : G → G ⧸ N) :
 theorem continuous_mk {N : Subgroup G} : Continuous (mk : G → G ⧸ N) :=
   continuous_quot_mk
 
-section ContinuousMul
-
-variable [ContinuousMul G] {N : Subgroup G}
+section ContinuousMulConst
+variable [ContinuousConstSMul Gᵐᵒᵖ G] {N : Subgroup G}
 
 @[to_additive]
 theorem isOpenMap_coe : IsOpenMap ((↑) : G → G ⧸ N) := isOpenMap_quotient_mk'_mul
@@ -65,24 +64,42 @@ theorem dense_image_mk {s : Set G} :
   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
+instance instContinuousConstSMul [MulAction M G] [ContinuousConstSMul M G]
+    [MulAction.QuotientAction M N] : ContinuousConstSMul M (G ⧸ N) where
+  continuous_const_smul m := by
+    rw [← isOpenQuotientMap_mk.continuous_comp_iff]
+    exact continuous_mk.comp (continuous_const_smul _)
+
+variable (N) in
+/-- 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 instContinuousConstSMul : ContinuousConstSMul G (G ⧸ N) := inferInstance
+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
+
+variable [ContinuousConstSMul G G]
 
 @[to_additive]
-theorem t1Space_iff :
-    T1Space (G ⧸ N) ↔ IsClosed (N : Set G) := by
+theorem t1Space_iff : T1Space (G ⧸ N) ↔ IsClosed (N : Set G) := by
   rw [← QuotientGroup.preimage_mk_one, MulAction.IsPretransitive.t1Space_iff G (mk 1),
-      isClosed_coinduced]
+    isClosed_coinduced]
   rfl
 
 @[to_additive]
-theorem discreteTopology_iff :
-    DiscreteTopology (G ⧸ N) ↔ IsOpen (N : Set G) := by
+theorem discreteTopology_iff : DiscreteTopology (G ⧸ N) ↔ IsOpen (N : Set G) := by
   rw [← QuotientGroup.preimage_mk_one, MulAction.IsPretransitive.discreteTopology_iff G (mk 1),
       isOpen_coinduced]
   rfl
@@ -118,26 +135,16 @@ instance instLocallyCompactSpace [LocallyCompactSpace G] (N : Subgroup G) :
     LocallyCompactSpace (G ⧸ N) :=
   QuotientGroup.isOpenQuotientMap_mk.locallyCompactSpace
 
-variable (N)
+end ContinuousMulConst
 
-/-- 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
+section ContinuousMul
+variable [ContinuousMul G] {N : Subgroup G}
 
 @[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
+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
 
 end ContinuousMul
 

Mathlib/Topology/Bornology/BoundedOperation.lean

@@ -156,8 +156,8 @@ variable {R : Type*} [SeminormedAddCommGroup R]
 
 lemma SeminormedAddCommGroup.lipschitzWith_sub :
     LipschitzWith 2 (fun (p : R × R) ↦ p.1 - p.2) := by
-  convert LipschitzWith.prod_fst.sub LipschitzWith.prod_snd
-  norm_num
+  rw [← one_add_one_eq_two]
+  exact LipschitzWith.prod_fst.sub LipschitzWith.prod_snd
 
 instance : BoundedSub R := boundedSub_of_lipschitzWith_sub SeminormedAddCommGroup.lipschitzWith_sub