feat(topology/algebra/group): add small topology lemma (#12931)

Adds a small topology lemma by splitting `compact_open_separated_mul` into `compact_open_separated_mul_left/right`, which was useful in my proof of `Steinhaus theorem` (see #12932), as in a non-abelian group, the current version was not sufficient.



Co-authored-by: YaelDillies <yael.dillies@gmail.com>

src/algebra/ring/opposite.lean

@@ -82,6 +82,77 @@ instance [group_with_zero α] : group_with_zero αᵐᵒᵖ :=
 
 end mul_opposite
 
+namespace add_opposite
+
+instance [distrib α] : distrib αᵃᵒᵖ :=
+{ left_distrib := λ x y z, unop_injective $ mul_add x _ _,
+  right_distrib := λ x y z, unop_injective $ add_mul _ _ z,
+  .. add_opposite.has_add α, .. @add_opposite.has_mul α _}
+
+instance [mul_zero_class α] : mul_zero_class αᵃᵒᵖ :=
+{ zero := 0,
+  mul := (*),
+  zero_mul := λ x, unop_injective $ zero_mul $ unop x,
+  mul_zero := λ x, unop_injective $ mul_zero $ unop x }
+
+instance [mul_zero_one_class α] : mul_zero_one_class αᵃᵒᵖ :=
+{ .. add_opposite.mul_zero_class α, .. add_opposite.mul_one_class α }
+
+instance [semigroup_with_zero α] : semigroup_with_zero αᵃᵒᵖ :=
+{ .. add_opposite.semigroup α, .. add_opposite.mul_zero_class α }
+
+instance [monoid_with_zero α] : monoid_with_zero αᵃᵒᵖ :=
+{ .. add_opposite.monoid α, .. add_opposite.mul_zero_one_class α }
+
+instance [non_unital_non_assoc_semiring α] : non_unital_non_assoc_semiring αᵃᵒᵖ :=
+{ .. add_opposite.add_comm_monoid α, .. add_opposite.mul_zero_class α, .. add_opposite.distrib α }
+
+instance [non_unital_semiring α] : non_unital_semiring αᵃᵒᵖ :=
+{ .. add_opposite.semigroup_with_zero α, .. add_opposite.non_unital_non_assoc_semiring α }
+
+instance [non_assoc_semiring α] : non_assoc_semiring αᵃᵒᵖ :=
+{ .. add_opposite.mul_zero_one_class α, .. add_opposite.non_unital_non_assoc_semiring α }
+
+instance [semiring α] : semiring αᵃᵒᵖ :=
+{ .. add_opposite.non_unital_semiring α, .. add_opposite.non_assoc_semiring α,
+  .. add_opposite.monoid_with_zero α }
+
+instance [comm_semiring α] : comm_semiring αᵃᵒᵖ :=
+{ .. add_opposite.semiring α, .. add_opposite.comm_semigroup α }
+
+instance [non_unital_non_assoc_ring α] : non_unital_non_assoc_ring αᵃᵒᵖ :=
+{ .. add_opposite.add_comm_group α, .. add_opposite.mul_zero_class α, .. add_opposite.distrib α}
+
+instance [non_unital_ring α] : non_unital_ring αᵃᵒᵖ :=
+{ .. add_opposite.add_comm_group α, .. add_opposite.semigroup_with_zero α,
+  .. add_opposite.distrib α}
+
+instance [non_assoc_ring α] : non_assoc_ring αᵃᵒᵖ :=
+{ .. add_opposite.add_comm_group α, .. add_opposite.mul_zero_one_class α, .. add_opposite.distrib α}
+
+instance [ring α] : ring αᵃᵒᵖ :=
+{ .. add_opposite.add_comm_group α, .. add_opposite.monoid α, .. add_opposite.semiring α }
+
+instance [comm_ring α] : comm_ring αᵃᵒᵖ :=
+{ .. add_opposite.ring α, .. add_opposite.comm_semiring α }
+
+instance [has_zero α] [has_mul α] [no_zero_divisors α] : no_zero_divisors αᵃᵒᵖ :=
+{ eq_zero_or_eq_zero_of_mul_eq_zero := λ x y (H : op (_ * _) = op (0:α)),
+  or.imp (λ hx, unop_injective hx) (λ hy, unop_injective hy)
+  ((@eq_zero_or_eq_zero_of_mul_eq_zero α _ _ _ _ _) $ op_injective H) }
+
+instance [ring α] [is_domain α] : is_domain αᵃᵒᵖ :=
+{ .. add_opposite.no_zero_divisors α, .. add_opposite.ring α, .. add_opposite.nontrivial α }
+
+instance [group_with_zero α] : group_with_zero αᵃᵒᵖ :=
+{ mul_inv_cancel := λ x hx, unop_injective $ mul_inv_cancel $ unop_injective.ne hx,
+  inv_zero := unop_injective inv_zero,
+  .. add_opposite.monoid_with_zero α, .. add_opposite.div_inv_monoid α,
+  .. add_opposite.nontrivial α }
+
+
+end add_opposite
+
 open mul_opposite
 
 /-- A ring homomorphism `f : R →+* S` such that `f x` commutes with `f y` for all `x, y` defines

src/data/set/pointwise.lean

@@ -5,6 +5,8 @@ Authors: Johan Commelin, Floris van Doorn
 -/
 import algebra.module.basic
 import data.set.finite
+import algebra.opposites
+import data.set.opposite
 import group_theory.submonoid.basic
 
 /-!
@@ -355,6 +357,19 @@ begin
   exact mul_le_mul' (hbA hxa) (hbB hxb),
 end
 
+open mul_opposite
+
+@[to_additive]
+lemma image_op_mul {α : Type*} [has_mul α] {s t : set α} :  op '' (s * t) = (op '' t) * (op '' s) :=
+begin
+  ext x,
+  split,
+  { rintro ⟨-, ⟨x, y, hx, hy, rfl⟩, rfl⟩,
+    apply mul_mem_mul (mem_image_of_mem op hy) (mem_image_of_mem op hx) },
+  { rintro ⟨-, -, ⟨y, hy, rfl⟩, ⟨z, hz, rfl⟩, rfl⟩,
+    refine ⟨z*y, mul_mem_mul hz hy, op_mul z y⟩ }
+end
+
 end mul
 
 open_locale pointwise

src/measure_theory/measure/haar.lean

@@ -417,28 +417,32 @@ begin
   rcases compact_compact_separated K₁.2 K₂.2 (disjoint_iff.mp h) with
     ⟨U₁, U₂, h1U₁, h1U₂, h2U₁, h2U₂, hU⟩,
   rw [← disjoint_iff_inter_eq_empty] at hU,
-  rcases compact_open_separated_mul K₁.2 h1U₁ h2U₁ with ⟨V₁, h1V₁, h2V₁, h3V₁⟩,
-  rcases compact_open_separated_mul K₂.2 h1U₂ h2U₂ with ⟨V₂, h1V₂, h2V₂, h3V₂⟩,
+  rcases compact_open_separated_mul_right K₁.2 h1U₁ h2U₁ with ⟨L₁, h1L₁, h2L₁⟩,
+  rcases mem_nhds_iff.mp h1L₁ with ⟨V₁, h1V₁, h2V₁, h3V₁⟩,
+  replace h2L₁ := subset.trans (mul_subset_mul_left h1V₁) h2L₁,
+  rcases compact_open_separated_mul_right K₂.2 h1U₂ h2U₂ with ⟨L₂, h1L₂, h2L₂⟩,
+  rcases mem_nhds_iff.mp h1L₂ with ⟨V₂, h1V₂, h2V₂, h3V₂⟩,
+  replace h2L₂ := subset.trans (mul_subset_mul_left h1V₂) h2L₂,
   let eval : (compacts G → ℝ) → ℝ := λ f, f K₁ + f K₂ - f (K₁ ⊔ K₂),
   have : continuous eval :=
     ((@continuous_add ℝ _ _ _).comp ((continuous_apply K₁).prod_mk (continuous_apply K₂))).sub
       (continuous_apply (K₁ ⊔ K₂)),
   rw [eq_comm, ← sub_eq_zero], show chaar K₀ ∈ eval ⁻¹' {(0 : ℝ)},
   let V := V₁ ∩ V₂,
   apply mem_of_subset_of_mem _ (chaar_mem_cl_prehaar K₀
-    ⟨V⁻¹, (is_open.inter h1V₁ h1V₂).preimage continuous_inv,
-    by simp only [mem_inv, one_inv, h2V₁, h2V₂, V, mem_inter_eq, true_and]⟩),
+    ⟨V⁻¹, (is_open.inter h2V₁ h2V₂).preimage continuous_inv,
+    by simp only [mem_inv, one_inv, h3V₁, h3V₂, V, mem_inter_eq, true_and]⟩),
   unfold cl_prehaar, rw is_closed.closure_subset_iff,
   { rintro _ ⟨U, ⟨h1U, h2U, h3U⟩, rfl⟩,
     simp only [mem_preimage, eval, sub_eq_zero, mem_singleton_iff], rw [eq_comm],
     apply prehaar_sup_eq,
     { rw h2U.interior_eq, exact ⟨1, h3U⟩ },
     { refine disjoint_of_subset _ _ hU,
-      { refine subset.trans (mul_subset_mul subset.rfl _) h3V₁,
+      { refine subset.trans (mul_subset_mul subset.rfl _) h2L₁,
         exact subset.trans (inv_subset.mpr h1U) (inter_subset_left _ _) },
-      { refine subset.trans (mul_subset_mul subset.rfl _) h3V₂,
+      { refine subset.trans (mul_subset_mul subset.rfl _) h2L₂,
         exact subset.trans (inv_subset.mpr h1U) (inter_subset_right _ _) }}},
-  { apply continuous_iff_is_closed.mp this, exact is_closed_singleton },
+  { apply continuous_iff_is_closed.mp this, exact is_closed_singleton }
 end
 
 @[to_additive is_left_invariant_add_chaar]

src/topology/algebra/group.lean

@@ -8,6 +8,7 @@ import order.filter.pointwise
 import topology.algebra.monoid
 import topology.compact_open
 import topology.sets.compacts
+import topology.algebra.constructions
 
 /-!
 # Theory of topological groups
@@ -464,6 +465,17 @@ instance pi.topological_group {C : β → Type*} [∀ b, topological_space (C b)
   [∀ b, group (C b)] [∀ b, topological_group (C b)] : topological_group (Π b, C b) :=
 { continuous_inv := continuous_pi (λ i, (continuous_apply i).inv) }
 
+open mul_opposite
+
+@[to_additive]
+instance [group α] [has_continuous_inv α] : has_continuous_inv αᵐᵒᵖ :=
+{ continuous_inv := continuous_induced_rng $ (@continuous_inv α _ _ _).comp continuous_unop }
+
+/-- If multiplication is continuous in `α`, then it also is in `αᵐᵒᵖ`. -/
+@[to_additive "If addition is continuous in `α`, then it also is in `αᵃᵒᵖ`."]
+instance [group α] [topological_group α] :
+  topological_group αᵐᵒᵖ := { }
+
 variable (G)
 
 /-- Inversion in a topological group as a homeomorphism. -/
@@ -916,27 +928,43 @@ section
 variables [topological_space G] [group G] [topological_group G]
 
 /-- Given a compact set `K` inside an open set `U`, there is a open neighborhood `V` of `1`
-  such that `KV ⊆ U`. -/
+  such that `K * V ⊆ U`. -/
 @[to_additive "Given a compact set `K` inside an open set `U`, there is a open neighborhood `V` of
 `0` such that `K + V ⊆ U`."]
-lemma compact_open_separated_mul {K U : set G} (hK : is_compact K) (hU : is_open U) (hKU : K ⊆ U) :
-  ∃ V : set G, is_open V ∧ (1 : G) ∈ V ∧ K * V ⊆ U :=
+lemma compact_open_separated_mul_right {K U : set G} (hK : is_compact K) (hU : is_open U)
+  (hKU : K ⊆ U) : ∃ V ∈ 𝓝 (1 : G), K * V ⊆ U :=
+begin
+  apply hK.induction_on,
+  { exact ⟨univ, by simp⟩ },
+  { rintros s t hst ⟨V, hV, hV'⟩,
+    exact ⟨V, hV, (mul_subset_mul_right hst).trans hV'⟩ },
+  { rintros s t  ⟨V, V_in, hV'⟩ ⟨W, W_in, hW'⟩,
+    use [V ∩ W, inter_mem V_in W_in],
+    rw union_mul,
+    exact union_subset ((mul_subset_mul_left (V.inter_subset_left W)).trans hV')
+                       ((mul_subset_mul_left (V.inter_subset_right W)).trans hW') },
+  { intros x hx,
+    have := tendsto_mul (show U ∈ 𝓝 (x * 1), by simpa using hU.mem_nhds (hKU hx)),
+    rw [nhds_prod_eq, mem_map, mem_prod_iff] at this,
+    rcases this with ⟨t, ht, s, hs, h⟩,
+    rw [← image_subset_iff, image_mul_prod] at h,
+    exact ⟨t, mem_nhds_within_of_mem_nhds ht, s, hs, h⟩ }
+end
+
+open mul_opposite
+
+/-- Given a compact set `K` inside an open set `U`, there is a open neighborhood `V` of `1`
+  such that `V * K ⊆ U`. -/
+@[to_additive "Given a compact set `K` inside an open set `U`, there is a open neighborhood `V` of
+`0` such that `V + K ⊆ U`."]
+lemma compact_open_separated_mul_left {K U : set G} (hK : is_compact K) (hU : is_open U)
+  (hKU : K ⊆ U) : ∃ V ∈ 𝓝 (1 : G), V * K ⊆ U :=
 begin
-  let W : G → set G := λ x, (λ y, x * y) ⁻¹' U,
-  have h1W : ∀ x, is_open (W x) := λ x, hU.preimage (continuous_mul_left x),
-  have h2W : ∀ x ∈ K, (1 : G) ∈ W x := λ x hx, by simp only [mem_preimage, mul_one, hKU hx],
-  choose V hV using λ x : K, exists_open_nhds_one_mul_subset ((h1W x).mem_nhds (h2W x.1 x.2)),
-  let X : K → set G := λ x, (λ y, (x : G)⁻¹ * y) ⁻¹' (V x),
-  obtain ⟨t, ht⟩ : ∃ t : finset ↥K, K ⊆ ⋃ i ∈ t, X i,
-  { refine hK.elim_finite_subcover X (λ x, (hV x).1.preimage (continuous_mul_left x⁻¹)) _,
-    intros x hx, rw [mem_Union], use ⟨x, hx⟩, rw [mem_preimage], convert (hV _).2.1,
-    simp only [mul_left_inv, subtype.coe_mk] },
-  refine ⟨⋂ x ∈ t, V x, is_open_bInter (finite_mem_finset _) (λ x hx, (hV x).1), _, _⟩,
-  { simp only [mem_Inter], intros x hx, exact (hV x).2.1 },
-  rintro _ ⟨x, y, hx, hy, rfl⟩, simp only [mem_Inter] at hy,
-  have := ht hx, simp only [mem_Union, mem_preimage] at this, rcases this with ⟨z, h1z, h2z⟩,
-  have : (z : G)⁻¹ * x * y ∈ W z := (hV z).2.2 (mul_mem_mul h2z (hy z h1z)),
-  rw [mem_preimage] at this, convert this using 1, simp only [mul_assoc, mul_inv_cancel_left]
+  rcases compact_open_separated_mul_right (hK.image continuous_op) (op_homeomorph.is_open_map U hU)
+    (image_subset op hKU) with ⟨V, (hV : V ∈ 𝓝 (op (1 : G))), hV' : op '' K * V ⊆ op '' U⟩,
+  refine ⟨op ⁻¹' V, continuous_op.continuous_at hV, _⟩,
+  rwa [← image_preimage_eq V op_surjective, ← image_op_mul, image_subset_iff,
+    preimage_image_eq _ op_injective] at hV'
 end
 
 /-- A compact set is covered by finitely many left multiplicative translates of a set

src/topology/algebra/ring.lean

@@ -100,6 +100,32 @@ instance {β : Type*} {C : β → Type*} [∀ b, topological_space (C b)]
   [Π b, semiring (C b)] [Π b, topological_ring (C b)] : topological_ring (Π b, C b) := {}
 end
 
+section mul_opposite
+open mul_opposite
+
+instance [semiring α] [topological_space α] [has_continuous_add α] : has_continuous_add αᵐᵒᵖ :=
+{ continuous_add := continuous_induced_rng $ (@continuous_add α _ _ _).comp
+  (continuous_unop.prod_map continuous_unop) }
+
+instance [semiring α] [topological_space α] [topological_ring α] :
+  topological_ring αᵐᵒᵖ := {}
+
+end mul_opposite
+
+section add_opposite
+open add_opposite
+
+instance [semiring α] [topological_space α] [has_continuous_mul α] :
+  has_continuous_mul αᵃᵒᵖ :=
+{ continuous_mul := by convert
+  (continuous_op.comp $ (@continuous_mul α _ _ _).comp $ continuous_unop.prod_map continuous_unop) }
+
+instance [semiring α] [topological_space α] [topological_ring α] :
+  topological_ring αᵃᵒᵖ := {}
+
+end add_opposite
+
+
 section
 variables {R : Type*} [ring R] [topological_space R]