feat: multiplication by closure {1} in topological groups does not …

…change closed and open subsets (#7858)

Mathlib/Data/Set/Pointwise/SMul.lean

@@ -86,7 +86,7 @@ theorem image2_smul : image2 SMul.smul s t = s • t :=
 #align set.image2_smul Set.image2_smul
 #align set.image2_vadd Set.image2_vadd
 
--- @[to_additive add_image_prod] -- Porting note: bug in mathlib3
+@[to_additive vadd_image_prod]
 theorem image_smul_prod : (fun x : α × β ↦ x.fst • x.snd) '' s ×ˢ t = s • t :=
   image_prod _
 #align set.image_smul_prod Set.image_smul_prod

Mathlib/Topology/Algebra/Group/Basic.lean

@@ -694,11 +694,11 @@ instance (S : Subgroup G) : TopologicalGroup S :=
 
 end Subgroup
 
-/-- The (topological-space) closure of a subgroup of a space `M` with `ContinuousMul` is
+/-- The (topological-space) closure of a subgroup of a topological group is
 itself a subgroup. -/
 @[to_additive
-  "The (topological-space) closure of an additive subgroup of a space `M` with
-  `ContinuousAdd` is itself an additive subgroup."]
+  "The (topological-space) closure of an additive subgroup of an additive topological group is
+  itself an additive subgroup."]
 def Subgroup.topologicalClosure (s : Subgroup G) : Subgroup G :=
   { s.toSubmonoid.topologicalClosure with
     carrier := _root_.closure (s : Set G)
@@ -797,6 +797,11 @@ def Subgroup.commGroupTopologicalClosure [T2Space G] (s : Subgroup G)
 #align subgroup.comm_group_topological_closure Subgroup.commGroupTopologicalClosure
 #align add_subgroup.add_comm_group_topological_closure AddSubgroup.addCommGroupTopologicalClosure
 
+variable (G) in
+@[to_additive]
+lemma Subgroup.coe_topologicalClosure_bot :
+    ((⊥ : Subgroup G).topologicalClosure : Set G) = _root_.closure ({1} : Set G) := by simp
+
 @[to_additive exists_nhds_half_neg]
 theorem exists_nhds_split_inv {s : Set G} (hs : s ∈ 𝓝 (1 : G)) :
     ∃ V ∈ 𝓝 (1 : G), ∀ v ∈ V, ∀ w ∈ V, v / w ∈ s := by
@@ -1378,7 +1383,7 @@ end ContinuousConstSMulOp
 
 section TopologicalGroup
 
-variable [TopologicalSpace α] [Group α] [TopologicalGroup α] {s t : Set α}
+variable [TopologicalSpace G] [Group G] [TopologicalGroup G] {s t : Set G}
 
 @[to_additive]
 theorem IsOpen.div_left (ht : IsOpen t) : IsOpen (s / t) := by
@@ -1413,7 +1418,7 @@ theorem subset_interior_div : interior s / interior t ⊆ interior (s / t) :=
 #align subset_interior_sub subset_interior_sub
 
 @[to_additive]
-theorem IsOpen.mul_closure (hs : IsOpen s) (t : Set α) : s * closure t = s * t := by
+theorem IsOpen.mul_closure (hs : IsOpen s) (t : Set G) : s * closure t = s * t := by
   refine' (mul_subset_iff.2 fun a ha b hb => _).antisymm (mul_subset_mul_left subset_closure)
   rw [mem_closure_iff] at hb
   have hbU : b ∈ s⁻¹ * {a * b} := ⟨a⁻¹, a * b, Set.inv_mem_inv.2 ha, rfl, inv_mul_cancel_left _ _⟩
@@ -1423,20 +1428,20 @@ theorem IsOpen.mul_closure (hs : IsOpen s) (t : Set α) : s * closure t = s * t
 #align is_open.add_closure IsOpen.add_closure
 
 @[to_additive]
-theorem IsOpen.closure_mul (ht : IsOpen t) (s : Set α) : closure s * t = s * t := by
+theorem IsOpen.closure_mul (ht : IsOpen t) (s : Set G) : closure s * t = s * t := by
   rw [← inv_inv (closure s * t), mul_inv_rev, inv_closure, ht.inv.mul_closure, mul_inv_rev, inv_inv,
     inv_inv]
 #align is_open.closure_mul IsOpen.closure_mul
 #align is_open.closure_add IsOpen.closure_add
 
 @[to_additive]
-theorem IsOpen.div_closure (hs : IsOpen s) (t : Set α) : s / closure t = s / t := by
+theorem IsOpen.div_closure (hs : IsOpen s) (t : Set G) : s / closure t = s / t := by
   simp_rw [div_eq_mul_inv, inv_closure, hs.mul_closure]
 #align is_open.div_closure IsOpen.div_closure
 #align is_open.sub_closure IsOpen.sub_closure
 
 @[to_additive]
-theorem IsOpen.closure_div (ht : IsOpen t) (s : Set α) : closure s / t = s / t := by
+theorem IsOpen.closure_div (ht : IsOpen t) (s : Set G) : closure s / t = s / t := by
   simp_rw [div_eq_mul_inv, ht.inv.closure_mul]
 #align is_open.closure_div IsOpen.closure_div
 #align is_open.closure_sub IsOpen.closure_sub
@@ -1452,15 +1457,66 @@ theorem IsClosed.mul_right_of_isCompact (ht : IsClosed t) (hs : IsCompact s) :
   exact IsClosed.smul_left_of_isCompact ht (hs.image continuous_op)
 
 @[to_additive]
-theorem QuotientGroup.isClosedMap_coe {H : Subgroup α} (hH : IsCompact (H : Set α)) :
-    IsClosedMap ((↑) : α → α ⧸ H) := by
+theorem QuotientGroup.isClosedMap_coe {H : Subgroup G} (hH : IsCompact (H : Set G)) :
+    IsClosedMap ((↑) : G → G ⧸ H) := by
   intro t ht
   rw [← quotientMap_quotient_mk'.isClosed_preimage]
   convert ht.mul_right_of_isCompact hH
   refine (QuotientGroup.preimage_image_mk_eq_iUnion_image _ _).trans ?_
   rw [iUnion_subtype, ← iUnion_mul_right_image]
   rfl
 
+@[to_additive]
+lemma subset_mul_closure_one (s : Set G) : s ⊆ s * (closure {1} : Set G) := by
+  have : s ⊆ s * ({1} : Set G) := by simpa using Subset.rfl
+  exact this.trans (smul_subset_smul_left subset_closure)
+
+@[to_additive]
+lemma IsCompact.mul_closure_one_eq_closure {K : Set G} (hK : IsCompact K) :
+    K * (closure {1} : Set G) = closure K := by
+  apply Subset.antisymm ?_ ?_
+  · calc
+    K * (closure {1} : Set G) ⊆ closure K * (closure {1} : Set G) :=
+      smul_subset_smul_right subset_closure
+    _ ⊆ closure (K * ({1} : Set G)) := smul_set_closure_subset _ _
+    _ = closure K := by simp
+  · have : IsClosed (K * (closure {1} : Set G)) :=
+      IsClosed.smul_left_of_isCompact isClosed_closure hK
+    rw [IsClosed.closure_subset_iff this]
+    exact subset_mul_closure_one K
+
+@[to_additive]
+lemma IsClosed.mul_closure_one_eq {F : Set G} (hF : IsClosed F) :
+    F * (closure {1} : Set G) = F := by
+  refine Subset.antisymm ?_ (subset_mul_closure_one F)
+  calc
+  F * (closure {1} : Set G) = closure F * closure ({1} : Set G) := by rw [hF.closure_eq]
+  _ ⊆ closure (F * ({1} : Set G)) := smul_set_closure_subset _ _
+  _ = F := by simp [hF.closure_eq]
+
+@[to_additive]
+lemma compl_mul_closure_one_eq {t : Set G} (ht : t * (closure {1} : Set G) = t) :
+    tᶜ * (closure {1} : Set G) = tᶜ := by
+  refine Subset.antisymm ?_ (subset_mul_closure_one tᶜ)
+  rintro - ⟨x, g, hx, hg, rfl⟩
+  by_contra H
+  have : x ∈ t * (closure {1} : Set G) := by
+    rw [← Subgroup.coe_topologicalClosure_bot G] at hg ⊢
+    simp only [smul_eq_mul, mem_compl_iff, not_not] at H
+    exact ⟨x * g, g⁻¹, H, Subgroup.inv_mem _ hg, by simp⟩
+  rw [ht] at this
+  exact hx this
+
+@[to_additive]
+lemma compl_mul_closure_one_eq_iff {t : Set G} :
+    tᶜ * (closure {1} : Set G) = tᶜ ↔ t * (closure {1} : Set G) = t :=
+  ⟨fun h ↦ by simpa using compl_mul_closure_one_eq h, fun h ↦ compl_mul_closure_one_eq h⟩
+
+@[to_additive]
+lemma IsOpen.mul_closure_one_eq {U : Set G} (hU : IsOpen U) :
+    U * (closure {1} : Set G) = U :=
+  compl_mul_closure_one_eq_iff.1 (hU.isClosed_compl.mul_closure_one_eq)
+
 end TopologicalGroup
 
 section FilterMul
@@ -1726,6 +1782,59 @@ theorem exists_isCompact_isClosed_subset_isCompact_nhds_one
   rcases exists_mem_nhds_isClosed_subset L1 with ⟨K, hK, K_closed, KL⟩
   exact ⟨K, Lcomp.of_isClosed_subset K_closed KL, K_closed, KL, hK⟩
 
+/-- If a point in a topological group has a compact neighborhood, then the group is
+locally compact. -/
+@[to_additive]
+theorem IsCompact.locallyCompactSpace_of_mem_nhds_of_group {K : Set G} (hK : IsCompact K) {x : G}
+    (h : K ∈ 𝓝 x) : LocallyCompactSpace G := by
+  refine ⟨fun y n hn ↦ ?_⟩
+  have A : (y * x⁻¹) • K ∈ 𝓝 y := by
+    rw [← preimage_smul_inv]
+    exact (continuous_const_smul _).continuousAt.preimage_mem_nhds (by simpa using h)
+  rcases exists_mem_nhds_isClosed_subset (inter_mem A hn) with ⟨L, hL, L_closed, LK⟩
+  refine ⟨L, hL, LK.trans (inter_subset_right _ _), ?_⟩
+  exact (hK.smul (y * x⁻¹)).of_isClosed_subset L_closed (LK.trans (inter_subset_left _ _))
+
+-- The next instance creates a loop between weakly locally compact space and locally compact space
+-- for topological groups. Hopefully, it shouldn't create problems.
+/-- A topological group which is weakly locally compact is automatically locally compact. -/
+@[to_additive]
+instance (priority := 90) instLocallyCompactSpaceOfWeaklyOfGroup [WeaklyLocallyCompactSpace G] :
+    LocallyCompactSpace G := by
+  rcases exists_compact_mem_nhds (1 : G) with ⟨K, K_comp, hK⟩
+  exact K_comp.locallyCompactSpace_of_mem_nhds_of_group hK
+
+/-- If a function defined on a topological group has a support contained in a
+compact set, then either the function is trivial or the group is locally compact. -/
+@[to_additive
+      "If a function defined on a topological additive group has a support contained in a compact
+      set, then either the function is trivial or the group is locally compact."]
+theorem eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group
+    [TopologicalSpace α] [Zero α] [T1Space α]
+    {f : G → α} {k : Set G} (hk : IsCompact k) (hf : support f ⊆ k) (h'f : Continuous f) :
+    f = 0 ∨ LocallyCompactSpace G := by
+  by_cases h : ∀ x, f x = 0
+  · apply Or.inl
+    ext x
+    exact h x
+  apply Or.inr
+  push_neg at h
+  obtain ⟨x, hx⟩ : ∃ x, f x ≠ 0 := h
+  have : k ∈ 𝓝 x :=
+    mem_of_superset (h'f.isOpen_support.mem_nhds hx) hf
+  exact IsCompact.locallyCompactSpace_of_mem_nhds_of_group hk this
+
+/-- If a function defined on a topological group has compact support, then either
+the function is trivial or the group is locally compact. -/
+@[to_additive
+      "If a function defined on a topological additive group has compact support,
+      then either the function is trivial or the group is locally compact."]
+theorem HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group
+    [TopologicalSpace α] [Zero α] [T1Space α]
+    {f : G → α} (hf : HasCompactSupport f) (h'f : Continuous f) :
+    f = 0 ∨ LocallyCompactSpace G :=
+  eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group hf (subset_tsupport f) h'f
+
 /-- In a locally compact group, any neighborhood of the identity contains a compact closed
 neighborhood of the identity, even without separation assumptions on the space. -/
 @[to_additive
@@ -1750,6 +1859,18 @@ theorem exists_isCompact_isClosed_nhds_one [WeaklyLocallyCompactSpace G] :
   let ⟨K, Kcl, Kcomp, _, K1⟩ := exists_isCompact_isClosed_subset_isCompact_nhds_one Lcomp L1
   ⟨K, Kcl, Kcomp, K1⟩
 
+/-- A quotient of a locally compact group is locally compact. -/
+@[to_additive]
+instance [LocallyCompactSpace G] (N : Subgroup G) : LocallyCompactSpace (G ⧸ N) := by
+  refine ⟨fun x n hn ↦ ?_⟩
+  let π := ((↑) : G → G ⧸ N)
+  have C : Continuous π := continuous_coinduced_rng
+  obtain ⟨y, rfl⟩ : ∃ y, π y = x := Quot.exists_rep x
+  have : π ⁻¹' n ∈ 𝓝 y := preimage_nhds_coinduced hn
+  rcases local_compact_nhds this with ⟨s, s_mem, hs, s_comp⟩
+  exact ⟨π '' s, (QuotientGroup.isOpenMap_coe N).image_mem_nhds s_mem, mapsTo'.mp hs,
+    s_comp.image C⟩
+
 end
 
 section

Mathlib/Topology/Algebra/MulAction.lean

@@ -140,6 +140,26 @@ instance MulOpposite.continuousSMul : ContinuousSMul M Xᵐᵒᵖ :=
 #align mul_opposite.has_continuous_smul MulOpposite.continuousSMul
 #align add_opposite.has_continuous_vadd AddOpposite.continuousVAdd
 
+@[to_additive]
+lemma IsCompact.smul_set {k : Set M} {u : Set X} (hk : IsCompact k) (hu : IsCompact u) :
+    IsCompact (k • u) := by
+  rw [← Set.image_smul_prod]
+  exact IsCompact.image (hk.prod hu) continuous_smul
+
+@[to_additive]
+lemma smul_set_closure_subset (K : Set M) (L : Set X) :
+    closure K • closure L ⊆ closure (K • L) := by
+  rintro - ⟨x, y, hx, hy, rfl⟩
+  apply mem_closure_iff_nhds.2 (fun u hu ↦ ?_)
+  have A : (fun p ↦ p.fst • p.snd) ⁻¹' u ∈ 𝓝 (x, y) :=
+    (continuous_smul.continuousAt (x := (x, y))).preimage_mem_nhds hu
+  obtain ⟨a, ha, b, hb, hab⟩ :
+    ∃ a, a ∈ 𝓝 x ∧ ∃ b, b ∈ 𝓝 y ∧ a ×ˢ b ⊆ (fun p ↦ p.fst • p.snd) ⁻¹' u :=
+      mem_nhds_prod_iff.1 A
+  obtain ⟨x', ⟨x'a, x'K⟩⟩ : Set.Nonempty (a ∩ K) := mem_closure_iff_nhds.1 hx a ha
+  obtain ⟨y', ⟨y'b, y'L⟩⟩ : Set.Nonempty (b ∩ L) := mem_closure_iff_nhds.1 hy b hb
+  refine ⟨x' • y', hab (Set.mk_mem_prod x'a y'b), Set.smul_mem_smul x'K y'L⟩
+
 end SMul
 
 section Monoid