feat(topology/algebra/uniform_group): add instance topological_group_is_uniform_of_compact_space (#16027)

ocfnash · ocfnash · commit 531db2ef0fdd · 2022-08-16T01:42:07.000Z
Also update doc string for `topological_group.to_uniform_space`. cc @ADedecker
diff --git a/src/analysis/normed_space/compact_operator.lean b/src/analysis/normed_space/compact_operator.lean
@@ -323,7 +323,7 @@ variables {𝕜₁ 𝕜₂ : Type*} [nontrivially_normed_field 𝕜₁] [nontriv
   (hf : is_compact_operator f) : continuous f :=
 begin
   letI : uniform_space M₂ := topological_add_group.to_uniform_space _,
-  haveI : uniform_add_group M₂ := topological_add_group_is_uniform,
+  haveI : uniform_add_group M₂ := topological_add_comm_group_is_uniform,
   -- Since `f` is linear, we only need to show that it is continuous at zero.
   -- Let `U` be a neighborhood of `0` in `M₂`.
   refine continuous_of_continuous_at_zero f (λ U hU, _),
diff --git a/src/topology/algebra/group.lean b/src/topology/algebra/group.lean
@@ -320,7 +320,7 @@ continuous.
 
 When you declare an instance that does not already have a `uniform_space` instance,
 you should also provide an instance of `uniform_space` and `uniform_group` using
-`topological_group.to_uniform_space` and `topological_group_is_uniform`. -/
+`topological_group.to_uniform_space` and `topological_comm_group_is_uniform`. -/
 @[to_additive]
 class topological_group (G : Type*) [topological_space G] [group G]
   extends has_continuous_mul G, has_continuous_inv G : Prop
diff --git a/src/topology/algebra/infinite_sum.lean b/src/topology/algebra/infinite_sum.lean
@@ -1322,7 +1322,7 @@ lemma summable.vanishing (hf : summable f) ⦃e : set G⦄ (he : e ∈ 𝓝 (0 :
   ∃ s : finset α, ∀ t, disjoint t s → ∑ k in t, f k ∈ e :=
 begin
   letI : uniform_space G := topological_add_group.to_uniform_space G,
-  letI : uniform_add_group G := topological_add_group_is_uniform,
+  letI : uniform_add_group G := topological_add_comm_group_is_uniform,
   rcases hf with ⟨y, hy⟩,
   exact cauchy_seq_finset_iff_vanishing.1 hy.cauchy_seq e he
 end
diff --git a/src/topology/algebra/module/finite_dimension.lean b/src/topology/algebra/module/finite_dimension.lean
@@ -205,7 +205,7 @@ private lemma continuous_equiv_fun_basis_aux [ht2 : t2_space E] {ι : Type v} [f
   (ξ : basis ι 𝕜 E) : continuous ξ.equiv_fun :=
 begin
   letI : uniform_space E := topological_add_group.to_uniform_space E,
-  letI : uniform_add_group E := topological_add_group_is_uniform,
+  letI : uniform_add_group E := topological_add_comm_group_is_uniform,
   letI : separated_space E := separated_iff_t2.mpr ht2,
   unfreezingI { induction hn : fintype.card ι with n IH generalizing ι E },
   { rw fintype.card_eq_zero_iff at hn,
diff --git a/src/topology/algebra/nonarchimedean/adic_topology.lean b/src/topology/algebra/nonarchimedean/adic_topology.lean
@@ -219,7 +219,7 @@ variables (R) [with_ideal R]
 topological_add_group.to_uniform_space R
 
 @[priority 100] instance : uniform_add_group R :=
-topological_add_group_is_uniform
+topological_add_comm_group_is_uniform
 
 /-- The adic topology on a `R` module coming from the ideal `with_ideal.I`.
 This cannot be an instance because `R` cannot be inferred from `M`. -/
diff --git a/src/topology/algebra/uniform_filter_basis.lean b/src/topology/algebra/uniform_filter_basis.lean
@@ -32,7 +32,7 @@ protected def uniform_space : uniform_space G :=
 /-- The uniform space structure associated to an abelian group filter basis via the associated
 topological abelian group structure is compatible with its group structure. -/
 protected lemma uniform_add_group : @uniform_add_group G B.uniform_space _:=
-@topological_add_group_is_uniform G _ B.topology B.is_topological_add_group
+@topological_add_comm_group_is_uniform G _ B.topology B.is_topological_add_group
 
 lemma cauchy_iff {F : filter G} :
   @cauchy G B.uniform_space F ↔ F.ne_bot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x y ∈ M, y - x ∈ U :=
diff --git a/src/topology/algebra/uniform_group.lean b/src/topology/algebra/uniform_group.lean
@@ -6,6 +6,7 @@ Authors: Patrick Massot, Johannes Hölzl
 import topology.uniform_space.uniform_convergence
 import topology.uniform_space.uniform_embedding
 import topology.uniform_space.complete_separated
+import topology.uniform_space.compact_separated
 import topology.algebra.group
 import tactic.abel
 
@@ -22,8 +23,8 @@ group naturally induces a uniform structure.
 
 ## Main results
 
-* `topological_add_group.to_uniform_space` and `topological_add_group_is_uniform` can be used to
-  construct a canonical uniformity for a topological add group.
+* `topological_add_group.to_uniform_space` and `topological_add_comm_group_is_uniform` can be used
+  to construct a canonical uniformity for a topological add group.
 
 * extension of ℤ-bilinear maps to complete groups (useful for ring completions)
 -/
@@ -347,8 +348,19 @@ section topological_group
 open filter
 variables (G : Type*) [group G] [topological_space G] [topological_group G]
 
-/-- The right uniformity on a topological group. -/
-@[to_additive "The right uniformity on a topological additive group"]
+/-- The right uniformity on a topological group (as opposed to the left uniformity).
+
+Warning: in general the right and left uniformities do not coincide and so one does not obtain a
+`uniform_group` structure. Two important special cases where they _do_ coincide are for
+commutative groups (see `topological_comm_group_is_uniform`) and for compact Hausdorff groups (see
+`topological_group_is_uniform_of_compact_space`). -/
+@[to_additive "The right uniformity on a topological additive group (as opposed to the left
+uniformity).
+
+Warning: in general the right and left uniformities do not coincide and so one does not obtain a
+`uniform_add_group` structure. Two important special cases where they _do_ coincide are for
+commutative additive groups (see `topological_add_comm_group_is_uniform`) and for compact Hausdorff
+additive groups (see `topological_add_comm_group_is_uniform_of_compact_space`)."]
 def topological_group.to_uniform_space : uniform_space G :=
 { uniformity          := comap (λp:G×G, p.2 / p.1) (𝓝 1),
   refl                :=
@@ -400,6 +412,14 @@ local attribute [instance] topological_group.to_uniform_space
 @[to_additive] lemma uniformity_eq_comap_nhds_one' :
   𝓤 G = comap (λp:G×G, p.2 / p.1) (𝓝 (1 : G)) := rfl
 
+@[to_additive] lemma topological_group_is_uniform_of_compact_space
+  [compact_space G] [t2_space G] : uniform_group G :=
+⟨begin
+  haveI : separated_space G := separated_iff_t2.mpr (by apply_instance),
+  apply compact_space.uniform_continuous_of_continuous,
+  exact continuous_div',
+end⟩
+
 variables {G}
 
 @[to_additive] lemma topological_group.tendsto_uniformly_iff
@@ -442,7 +462,7 @@ section
 local attribute [instance] topological_group.to_uniform_space
 
 variable {G}
-@[to_additive] lemma topological_group_is_uniform : uniform_group G :=
+@[to_additive] lemma topological_comm_group_is_uniform : uniform_group G :=
 have tendsto
     ((λp:(G×G), p.1 / p.2) ∘ (λp:(G×G)×(G×G), (p.1.2 / p.1.1, p.2.2 / p.2.1)))
     (comap (λp:(G×G)×(G×G), (p.1.2 / p.1.1, p.2.2 / p.2.1)) ((𝓝 1).prod (𝓝 1)))
@@ -460,7 +480,7 @@ open set
 @[to_additive] lemma topological_group.t2_space_iff_one_closed :
   t2_space G ↔ is_closed ({1} : set G) :=
 begin
-  haveI : uniform_group G := topological_group_is_uniform,
+  haveI : uniform_group G := topological_comm_group_is_uniform,
   rw [← separated_iff_t2, separated_space_iff, ← closure_eq_iff_is_closed],
   split; intro h,
   { apply subset.antisymm,
diff --git a/src/topology/algebra/valuation.lean b/src/topology/algebra/valuation.lean
@@ -102,7 +102,7 @@ structure. -/
 def mk' (v : valuation R Γ₀) : valued R Γ₀ :=
 { v := v,
   to_uniform_space := @topological_add_group.to_uniform_space R _ v.subgroups_basis.topology _,
-  to_uniform_add_group := @topological_add_group_is_uniform _ _ v.subgroups_basis.topology _,
+  to_uniform_add_group := @topological_add_comm_group_is_uniform _ _ v.subgroups_basis.topology _,
   is_topological_valuation :=
   begin
     letI := @topological_add_group.to_uniform_space R _ v.subgroups_basis.topology _,
diff --git a/src/topology/continuous_function/algebra.lean b/src/topology/continuous_function/algebra.lean
@@ -287,7 +287,7 @@ coe_injective.comm_group _ coe_one coe_mul coe_inv coe_div coe_pow coe_zpow
   [topological_space β] [comm_group β] [topological_group β] : topological_group C(α, β) :=
 { continuous_mul := by
   { letI : uniform_space β := topological_group.to_uniform_space β,
-    have : uniform_group β := topological_group_is_uniform,
+    have : uniform_group β := topological_comm_group_is_uniform,
     rw continuous_iff_continuous_at,
     rintros ⟨f, g⟩,
     rw [continuous_at, tendsto_iff_forall_compact_tendsto_uniformly_on, nhds_prod_eq],
@@ -296,7 +296,7 @@ coe_injective.comm_group _ coe_one coe_mul coe_inv coe_div coe_pow coe_zpow
       (tendsto_iff_forall_compact_tendsto_uniformly_on.mp filter.tendsto_id K hK)), },
   continuous_inv := by
   { letI : uniform_space β := topological_group.to_uniform_space β,
-    have : uniform_group β := topological_group_is_uniform,
+    have : uniform_group β := topological_comm_group_is_uniform,
     rw continuous_iff_continuous_at,
     intro f,
     rw [continuous_at, tendsto_iff_forall_compact_tendsto_uniformly_on],
