feat(topology/algebra/uniform_group): add characterization of total b…

…oundedness (#12808)

The main result is `totally_bounded_iff_subset_finite_Union_nhds_one`.
We prove it for noncommutative groups, which involves taking opposites.

Add `uniform_group` instance for the opposite group.

Adds several helper lemmas for
* (co-)map of opposites applied to neighborhood filter
* filter basis of uniformity in a uniform group in terms of neighborhood basis at identity

Simplified proofs for `totally_bounded_of_forall_symm` and `totally_bounded.closure`.

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/algebra/group/opposite.lean

@@ -115,6 +115,14 @@ We also generate additive structures on `αᵃᵒᵖ` using `to_additive`
 
 variable {α}
 
+@[simp, to_additive] lemma unop_div [div_inv_monoid α] (x y : αᵐᵒᵖ) :
+  unop (x / y) = (unop y)⁻¹ * unop x :=
+rfl
+
+@[simp, to_additive] lemma op_div [div_inv_monoid α] (x y : α) :
+  op (x / y) = (op y)⁻¹ * op x :=
+by simp [div_eq_mul_inv]
+
 @[simp, to_additive] lemma semiconj_by_op [has_mul α] {a x y : α} :
   semiconj_by (op a) (op y) (op x) ↔ semiconj_by a x y :=
 by simp only [semiconj_by, ← op_mul, op_inj, eq_comm]

src/topology/algebra/constructions.lean

@@ -19,6 +19,9 @@ topological space, opposite monoid, units
 
 variables {M X : Type*}
 
+open filter
+open_locale topological_space
+
 namespace mul_opposite
 
 /-- Put the same topological space structure on the opposite monoid as on the original space. -/
@@ -40,6 +43,18 @@ def op_homeomorph : M ≃ₜ Mᵐᵒᵖ :=
   continuous_to_fun := continuous_op,
   continuous_inv_fun := continuous_unop }
 
+@[simp, to_additive] lemma map_op_nhds (x : M) : map (op : M → Mᵐᵒᵖ) (𝓝 x) = 𝓝 (op x) :=
+op_homeomorph.map_nhds_eq x
+
+@[simp, to_additive] lemma map_unop_nhds (x : Mᵐᵒᵖ) : map (unop : Mᵐᵒᵖ → M) (𝓝 x) = 𝓝 (unop x) :=
+op_homeomorph.symm.map_nhds_eq x
+
+@[simp, to_additive] lemma comap_op_nhds (x : Mᵐᵒᵖ) : comap (op : M → Mᵐᵒᵖ) (𝓝 x) = 𝓝 (unop x) :=
+op_homeomorph.comap_nhds_eq x
+
+@[simp, to_additive] lemma comap_unop_nhds (x : M) : comap (unop : Mᵐᵒᵖ → M) (𝓝 x) = 𝓝 (op x) :=
+op_homeomorph.symm.comap_nhds_eq x
+
 end mul_opposite
 
 namespace units

src/topology/algebra/uniform_group.lean

@@ -19,7 +19,7 @@ import tactic.abel
 -/
 
 noncomputable theory
-open_locale classical uniformity topological_space filter
+open_locale classical uniformity topological_space filter pointwise
 
 section uniform_group
 open filter set
@@ -98,8 +98,18 @@ le_antisymm
   end,
   inj := mul_left_injective a }
 
+
+namespace mul_opposite
+
+@[to_additive] instance : uniform_group αᵐᵒᵖ :=
+⟨uniform_continuous_op.comp ((uniform_continuous_unop.comp uniform_continuous_snd).inv.mul $
+  uniform_continuous_unop.comp uniform_continuous_fst)⟩
+
+end mul_opposite
+
 section
 variables (α)
+
 @[to_additive] lemma uniformity_eq_comap_nhds_one : 𝓤 α = comap (λx:α×α, x.2 / x.1) (𝓝 (1:α)) :=
 begin
   rw [nhds_eq_comap_uniformity, filter.comap_comap],
@@ -116,8 +126,47 @@ begin
     refine ⟨_, ht, _⟩,
     rintros ⟨a, b⟩, simpa [subset_def] using hts 1 (b / a) a }
 end
+
+@[to_additive] lemma uniformity_eq_comap_nhds_one_swapped :
+  𝓤 α = comap (λx:α×α, x.1 / x.2) (𝓝 (1:α)) :=
+by { rw [← comap_swap_uniformity, uniformity_eq_comap_nhds_one, comap_comap, (∘)], refl }
+
+open mul_opposite
+
+@[to_additive]
+lemma uniformity_eq_comap_inv_mul_nhds_one : 𝓤 α = comap (λx:α×α, x.1⁻¹ * x.2) (𝓝 (1:α)) :=
+begin
+  rw [← comap_uniformity_mul_opposite, uniformity_eq_comap_nhds_one, ← op_one, ← comap_unop_nhds,
+    comap_comap, comap_comap],
+  simp [(∘)]
 end
 
+@[to_additive] lemma uniformity_eq_comap_inv_mul_nhds_one_swapped :
+  𝓤 α = comap (λx:α×α, x.2⁻¹ * x.1) (𝓝 (1:α)) :=
+by { rw [← comap_swap_uniformity, uniformity_eq_comap_inv_mul_nhds_one, comap_comap, (∘)], refl }
+
+end
+
+@[to_additive] lemma filter.has_basis.uniformity_of_nhds_one {ι} {p : ι → Prop} {U : ι → set α}
+  (h : (𝓝 (1 : α)).has_basis p U) :
+  (𝓤 α).has_basis p (λ i, {x : α × α | x.2 / x.1 ∈ U i}) :=
+by { rw uniformity_eq_comap_nhds_one, exact h.comap _ }
+
+@[to_additive] lemma filter.has_basis.uniformity_of_nhds_one_inv_mul
+  {ι} {p : ι → Prop} {U : ι → set α} (h : (𝓝 (1 : α)).has_basis p U) :
+  (𝓤 α).has_basis p (λ i, {x : α × α | x.1⁻¹ * x.2 ∈ U i}) :=
+by { rw uniformity_eq_comap_inv_mul_nhds_one, exact h.comap _ }
+
+@[to_additive] lemma filter.has_basis.uniformity_of_nhds_one_swapped
+  {ι} {p : ι → Prop} {U : ι → set α} (h : (𝓝 (1 : α)).has_basis p U) :
+  (𝓤 α).has_basis p (λ i, {x : α × α | x.1 / x.2 ∈ U i}) :=
+by { rw uniformity_eq_comap_nhds_one_swapped, exact h.comap _ }
+
+@[to_additive] lemma filter.has_basis.uniformity_of_nhds_one_inv_mul_swapped
+  {ι} {p : ι → Prop} {U : ι → set α} (h : (𝓝 (1 : α)).has_basis p U) :
+  (𝓤 α).has_basis p (λ i, {x : α × α | x.2⁻¹ * x.1 ∈ U i}) :=
+by { rw uniformity_eq_comap_inv_mul_nhds_one_swapped, exact h.comap _ }
+
 @[to_additive] lemma group_separation_rel (x y : α) :
   (x, y) ∈ separation_rel α ↔ x / y ∈ closure ({1} : set α) :=
 have embedding (λa, a * (y / x)), from (uniform_embedding_translate_mul (y / x)).embedding,
@@ -180,6 +229,11 @@ uniform_continuous_mul.comp_cauchy_seq (hu.prod hv)
   {u : ι → α} (h : cauchy_seq u) : cauchy_seq (u⁻¹) :=
 uniform_continuous_inv.comp_cauchy_seq h
 
+@[to_additive] lemma totally_bounded_iff_subset_finite_Union_nhds_one {s : set α} :
+  totally_bounded s ↔ ∀ U ∈ 𝓝 (1 : α), ∃ (t : set α), t.finite ∧ s ⊆ ⋃ y ∈ t, y • U :=
+(𝓝 (1 : α)).basis_sets.uniformity_of_nhds_one_inv_mul_swapped.totally_bounded_iff.trans $
+  by simp [← preimage_smul_inv, preimage]
+
 end uniform_group
 
 section topological_comm_group

src/topology/uniform_space/basic.lean

@@ -370,6 +370,9 @@ from map_le_iff_le_comap.1 tendsto_swap_uniformity
 lemma uniformity_eq_symm : 𝓤 α = (@prod.swap α α) <$> 𝓤 α :=
 le_antisymm uniformity_le_symm symm_le_uniformity
 
+@[simp] lemma comap_swap_uniformity : comap (@prod.swap α α) (𝓤 α) = 𝓤 α :=
+(congr_arg _ uniformity_eq_symm).trans $ comap_map prod.swap_injective
+
 lemma symmetrize_mem_uniformity {V : set (α × α)} (h : V ∈ 𝓤 α) : symmetrize_rel V ∈ 𝓤 α :=
 begin
   apply (𝓤 α).inter_sets h,
@@ -1200,6 +1203,10 @@ lemma uniformity_mul_opposite [uniform_space α] :
   𝓤 (αᵐᵒᵖ) = comap (λ q : αᵐᵒᵖ × αᵐᵒᵖ, (q.1.unop, q.2.unop)) (𝓤 α) :=
 rfl
 
+@[simp, to_additive] lemma comap_uniformity_mul_opposite [uniform_space α] :
+  comap (λ p : α × α, (mul_opposite.op p.1, mul_opposite.op p.2)) (𝓤 αᵐᵒᵖ) = 𝓤 α :=
+by simpa [uniformity_mul_opposite, comap_comap, (∘)] using comap_id
+
 namespace mul_opposite
 
 @[to_additive]

src/topology/uniform_space/cauchy.lean

@@ -418,13 +418,14 @@ lemma is_closed.is_complete [complete_space α] {s : set α}
 /-- A set `s` is totally bounded if for every entourage `d` there is a finite
   set of points `t` such that every element of `s` is `d`-near to some element of `t`. -/
 def totally_bounded (s : set α) : Prop :=
-∀d ∈ 𝓤 α, ∃t : set α, finite t ∧ s ⊆ (⋃y∈t, {x | (x,y) ∈ d})
+∀d ∈ 𝓤 α, ∃t : set α, finite t ∧ s ⊆ (⋃ y ∈ t, {x | (x, y) ∈ d})
 
-theorem totally_bounded_iff_subset {s : set α} : totally_bounded s ↔
-  ∀d ∈ 𝓤 α, ∃t ⊆ s, finite t ∧ s ⊆ (⋃y∈t, {x | (x,y) ∈ d}) :=
-⟨λ H d hd, begin
-  rcases comp_symm_of_uniformity hd with ⟨r, hr, rs, rd⟩,
-  rcases H r hr with ⟨k, fk, ks⟩,
+theorem totally_bounded.exists_subset {s : set α} (hs : totally_bounded s) {U : set (α × α)}
+  (hU : U ∈ 𝓤 α) :
+  ∃ t ⊆ s, finite t ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U} :=
+begin
+  rcases comp_symm_of_uniformity hU with ⟨r, hr, rs, rU⟩,
+  rcases hs r hr with ⟨k, fk, ks⟩,
   let u := k ∩ {y | ∃ x ∈ s, (x, y) ∈ r},
   choose hk f hfs hfr using λ x : u, x.coe_prop,
   refine ⟨range f, _, _, _⟩,
@@ -435,21 +436,23 @@ theorem totally_bounded_iff_subset {s : set α} : totally_bounded s ↔
     obtain ⟨y, hy, xy⟩ : ∃ y ∈ k, (x, y) ∈ r, from mem_Union₂.1 (ks xs),
     rw [bUnion_range, mem_Union],
     set z : ↥u := ⟨y, hy, ⟨x, xs, xy⟩⟩,
-    exact ⟨z, rd $ mem_comp_rel.2 ⟨y, xy, rs (hfr z)⟩⟩ }
-end,
-λ H d hd, let ⟨t, _, ht⟩ := H d hd in ⟨t, ht⟩⟩
+    exact ⟨z, rU $ mem_comp_rel.2 ⟨y, xy, rs (hfr z)⟩⟩ }
+end
+
+theorem totally_bounded_iff_subset {s : set α} : totally_bounded s ↔
+  ∀d ∈ 𝓤 α, ∃t ⊆ s, finite t ∧ s ⊆ (⋃y∈t, {x | (x,y) ∈ d}) :=
+⟨λ H d hd, H.exists_subset hd, λ H d hd, let ⟨t, _, ht⟩ := H d hd in ⟨t, ht⟩⟩
+
+lemma filter.has_basis.totally_bounded_iff {ι} {p : ι → Prop} {U : ι → set (α × α)}
+  (H : (𝓤 α).has_basis p U) {s : set α} :
+  totally_bounded s ↔ ∀ i, p i → ∃ t : set α, finite t ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i} :=
+H.forall_iff $ λ U V hUV h, h.imp $ λ t ht, ⟨ht.1, ht.2.trans $ Union₂_mono $ λ x hx y hy, hUV hy⟩
 
 lemma totally_bounded_of_forall_symm {s : set α}
   (h : ∀ V ∈ 𝓤 α, symmetric_rel V → ∃ t : set α, finite t ∧ s ⊆ ⋃ y ∈ t, ball y V) :
-totally_bounded s :=
-begin
-  intros V V_in,
-  rcases h _ (symmetrize_mem_uniformity V_in) (symmetric_symmetrize_rel V) with ⟨t, tfin, h⟩,
-  refine ⟨t, tfin, subset.trans h _⟩,
-  mono,
-  intros x x_in z z_in,
-  exact z_in.right
-end
+  totally_bounded s :=
+uniform_space.has_basis_symmetric.totally_bounded_iff.2 $ λ V hV,
+  by simpa only [ball_eq_of_symmetry hV.2] using h V hV.1 hV.2
 
 lemma totally_bounded_subset {s₁ s₂ : set α} (hs : s₁ ⊆ s₂)
   (h : totally_bounded s₂) : totally_bounded s₁ :=
@@ -461,14 +464,9 @@ lemma totally_bounded_empty : totally_bounded (∅ : set α) :=
 /-- The closure of a totally bounded set is totally bounded. -/
 lemma totally_bounded.closure {s : set α} (h : totally_bounded s) :
   totally_bounded (closure s) :=
-assume t ht,
-let ⟨t', ht', hct', htt'⟩ := mem_uniformity_is_closed ht, ⟨c, hcf, hc⟩ := h t' ht' in
-⟨c, hcf,
-  calc closure s ⊆ closure (⋃ (y : α) (H : y ∈ c), {x : α | (x, y) ∈ t'}) : closure_mono hc
-    ... = _ : is_closed.closure_eq $ is_closed_bUnion hcf $ assume i hi,
-      continuous_iff_is_closed.mp (continuous_id.prod_mk continuous_const) _ hct'
-    ... ⊆ _ : Union₂_subset $ assume i hi, subset.trans (assume x, @htt' (x, i))
-      (subset_bUnion_of_mem hi)⟩
+uniformity_has_basis_closed.totally_bounded_iff.2 $ λ V hV, let ⟨t, htf, hst⟩ := h V hV.1
+  in ⟨t, htf, closure_minimal hst $ is_closed_bUnion htf $
+    λ y hy, hV.2.preimage (continuous_id.prod_mk continuous_const)⟩
 
 /-- The image of a totally bounded set under a uniformly continuous map is totally bounded. -/
 lemma totally_bounded.image [uniform_space β] {f : α → β} {s : set α}
@@ -548,7 +546,7 @@ lemma compact_iff_totally_bounded_complete {s : set α} :
  λ ⟨ht, hc⟩, is_compact_iff_ultrafilter_le_nhds.2
    (λf hf, hc _ (totally_bounded_iff_ultrafilter.1 ht f hf) hf)⟩
 
-lemma is_compact.totally_bounded {s : set α} (h : is_compact s) : totally_bounded s :=
+protected lemma is_compact.totally_bounded {s : set α} (h : is_compact s) : totally_bounded s :=
 (compact_iff_totally_bounded_complete.1 h).1
 
 protected lemma is_compact.is_complete {s : set α} (h : is_compact s) : is_complete s :=