feat(Topology/Group): Open normal subgroup in clopen nhds of one (#18377

)

Proving that there is always an open normal subgroup in a clopen nhd of compact topological group

Co-authored-by: NailinGuan <[email protected]> Yi Song <[email protected]> Xuchun Li <[email protected]>




Co-authored-by: Patrick Massot <[email protected]>

Mathlib.lean

@@ -4621,6 +4621,7 @@ import Mathlib.Topology.Algebra.Affine
 import Mathlib.Topology.Algebra.Algebra
 import Mathlib.Topology.Algebra.Algebra.Rat
 import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
+import Mathlib.Topology.Algebra.ClopenNhdofOne
 import Mathlib.Topology.Algebra.ClosedSubgroup
 import Mathlib.Topology.Algebra.ConstMulAction
 import Mathlib.Topology.Algebra.Constructions

Mathlib/Topology/Algebra/ClopenNhdofOne.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2024 Nailin Guan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nailin Guan, Yi Song, Xuchun Li
+-/
+import Mathlib.GroupTheory.Index
+import Mathlib.Topology.Algebra.ClosedSubgroup
+import Mathlib.Topology.Algebra.OpenSubgroup
+/-!
+# Existence of an open normal subgroup in any clopen neighborhood of the neutral element
+
+This file proves the lemma `TopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhd_of_one`, which
+states that in a compact topological group, for any clopen neighborhood of 1,
+there exists an open normal subgroup contained within it.
+
+This file is split out from the file `OpenSubgroup` because it needs more imports.
+-/
+
+namespace TopologicalGroup
+
+theorem exist_openNormalSubgroup_sub_clopen_nhd_of_one {G : Type*} [Group G] [TopologicalSpace G]
+    [TopologicalGroup G] [CompactSpace G] {W : Set G} (WClopen : IsClopen W) (einW : 1 ∈ W) :
+    ∃ H : OpenNormalSubgroup G, (H : Set G) ⊆ W := by
+  rcases exist_openSubgroup_sub_clopen_nhd_of_one WClopen einW with ⟨H, hH⟩
+  have : Subgroup.FiniteIndex H := H.finiteIndex_of_finite_quotient
+  use { toSubgroup := Subgroup.normalCore H
+        isOpen' := Subgroup.isOpen_of_isClosed_of_finiteIndex _ (H.normalCore_isClosed H.isClosed) }
+  exact fun _ b ↦ hH (H.normalCore_le b)
+
+end TopologicalGroup

Mathlib/Topology/Algebra/OpenSubgroup.lean

@@ -456,3 +456,110 @@ instance [ContinuousMul G] : Lattice (OpenNormalSubgroup G) :=
 end OpenNormalSubgroup
 
 end
+
+/-!
+# Existence of an open subgroup in any clopen neighborhood of the neutral element
+
+This section proves the lemma `TopologicalGroup.exist_openSubgroup_sub_clopen_nhd_of_one`, which
+states that in a compact topological group, for any clopen neighborhood of 1,
+there exists an open subgroup contained within it.
+-/
+
+open scoped Pointwise
+
+variable {G : Type*} [TopologicalSpace G]
+
+structure TopologicalAddGroup.addNegClosureNhd (T W : Set G) [AddGroup G] : Prop where
+  nhd : T ∈ 𝓝 0
+  neg : -T = T
+  isOpen : IsOpen T
+  add : W + T ⊆ W
+
+/-- For a set `W`, `T` is a neighborhood of `1` which is open, statble under inverse and satisfies
+`T * W ⊆ W`. -/
+@[to_additive
+"For a set `W`, `T` is a neighborhood of `0` which is open, stable under negation and satisfies
+`T + W ⊆ W`. "]
+structure TopologicalGroup.mulInvClosureNhd (T W : Set G) [Group G] : Prop where
+  nhd : T ∈ 𝓝 1
+  inv : T⁻¹ = T
+  isOpen : IsOpen T
+  mul : W * T ⊆ W
+
+namespace TopologicalGroup
+
+variable [Group G] [TopologicalGroup G] [CompactSpace G]
+
+open Set Filter
+
+@[to_additive]
+lemma exist_mul_closure_nhd {W : Set G} (WClopen : IsClopen W) : ∃ T ∈ 𝓝 (1 : G), W * T ⊆ W := by
+  apply WClopen.isClosed.isCompact.induction_on (p := fun S ↦ ∃ T ∈ 𝓝 (1 : G), S * T ⊆ W)
+    ⟨Set.univ ,by simp only [univ_mem, empty_mul, empty_subset, and_self]⟩
+    (fun _ _ huv ⟨T, hT, mem⟩ ↦ ⟨T, hT, (mul_subset_mul_right huv).trans mem⟩)
+    fun U V ⟨T₁, hT₁, mem1⟩ ⟨T₂, hT₂, mem2⟩ ↦ ⟨T₁ ∩ T₂, inter_mem hT₁ hT₂, by
+      rw [union_mul]
+      exact union_subset (mul_subset_mul_left inter_subset_left |>.trans mem1)
+        (mul_subset_mul_left inter_subset_right |>.trans mem2) ⟩
+  intro x memW
+  have : (x, 1) ∈ (fun p ↦ p.1 * p.2) ⁻¹' W := by simp [memW]
+  rcases isOpen_prod_iff.mp (continuous_mul.isOpen_preimage W <| WClopen.2) x 1 this with
+    ⟨U, V, Uopen, Vopen, xmemU, onememV, prodsub⟩
+  have h6 : U * V ⊆ W := mul_subset_iff.mpr (fun _ hx _ hy ↦ prodsub (mk_mem_prod hx hy))
+  exact ⟨U ∩ W, ⟨U, Uopen.mem_nhds xmemU, W, fun _ a ↦ a, rfl⟩,
+    V, IsOpen.mem_nhds Vopen onememV, fun _ a ↦ h6 ((mul_subset_mul_right inter_subset_left) a)⟩
+
+@[to_additive]
+lemma exists_mulInvClosureNhd {W : Set G} (WClopen : IsClopen W) :
+    ∃ T, mulInvClosureNhd T W := by
+  rcases exist_mul_closure_nhd WClopen with ⟨S, Smemnhds, mulclose⟩
+  rcases mem_nhds_iff.mp Smemnhds with ⟨U, UsubS, Uopen, onememU⟩
+  use U ∩ U⁻¹
+  constructor
+  · simp [Uopen.mem_nhds onememU, inv_mem_nhds_one]
+  · simp [inter_comm]
+  · exact Uopen.inter Uopen.inv
+  · exact fun a ha ↦ mulclose (mul_subset_mul_left UsubS (mul_subset_mul_left inter_subset_left ha))
+
+@[to_additive]
+theorem exist_openSubgroup_sub_clopen_nhd_of_one {G : Type*} [Group G] [TopologicalSpace G]
+    [TopologicalGroup G] [CompactSpace G] {W : Set G} (WClopen : IsClopen W) (einW : 1 ∈ W) :
+    ∃ H : OpenSubgroup G, (H : Set G) ⊆ W := by
+  rcases exists_mulInvClosureNhd WClopen with ⟨V, hV⟩
+  let S : Subgroup G := {
+    carrier := ⋃ n , V ^ (n + 1)
+    mul_mem' := fun ha hb ↦ by
+      rcases mem_iUnion.mp ha with ⟨k, hk⟩
+      rcases mem_iUnion.mp hb with ⟨l, hl⟩
+      apply mem_iUnion.mpr
+      use k + 1 + l
+      rw [add_assoc, pow_add]
+      exact Set.mul_mem_mul hk hl
+    one_mem' := by
+      apply mem_iUnion.mpr
+      use 0
+      simp [mem_of_mem_nhds hV.nhd]
+    inv_mem' := fun ha ↦ by
+      rcases mem_iUnion.mp ha with ⟨k, hk⟩
+      apply mem_iUnion.mpr
+      use k
+      rw [← hV.inv]
+      simpa only [inv_pow, Set.mem_inv, inv_inv] using hk }
+  have : IsOpen (⋃ n , V ^ (n + 1)) := by
+    refine isOpen_iUnion (fun n ↦ ?_)
+    rw [pow_succ]
+    exact hV.isOpen.mul_left
+  use ⟨S, this⟩
+  have mulVpow (n : ℕ) : W * V ^ (n + 1) ⊆ W := by
+    induction' n with n ih
+    · simp [hV.mul]
+    · rw [pow_succ, ← mul_assoc]
+      exact (Set.mul_subset_mul_right ih).trans hV.mul
+  have (n : ℕ) : V ^ (n + 1) ⊆ W * V ^ (n + 1) := by
+    intro x xin
+    rw [Set.mem_mul]
+    use 1, einW, x, xin
+    rw [one_mul]
+  apply iUnion_subset fun i _ a ↦ mulVpow i (this i a)
+
+end TopologicalGroup