From f000b64e687c7b599a43b35fdf6157fd40185e1c Mon Sep 17 00:00:00 2001 From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com> Date: Wed, 30 Oct 2024 20:23:47 +0000 Subject: [PATCH] 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 <3571819596@qq.com> Yi Song Xuchun Li Co-authored-by: Patrick Massot --- Mathlib.lean | 1 + Mathlib/Topology/Algebra/ClopenNhdofOne.lean | 30 ++++++ Mathlib/Topology/Algebra/OpenSubgroup.lean | 107 +++++++++++++++++++ 3 files changed, 138 insertions(+) create mode 100644 Mathlib/Topology/Algebra/ClopenNhdofOne.lean diff --git a/Mathlib.lean b/Mathlib.lean index 5ed50d844729df..00ed52d99121fa 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Topology/Algebra/ClopenNhdofOne.lean b/Mathlib/Topology/Algebra/ClopenNhdofOne.lean new file mode 100644 index 00000000000000..b254276d388f7d --- /dev/null +++ b/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 diff --git a/Mathlib/Topology/Algebra/OpenSubgroup.lean b/Mathlib/Topology/Algebra/OpenSubgroup.lean index 107bc286f59011..e604312216e17b 100644 --- a/Mathlib/Topology/Algebra/OpenSubgroup.lean +++ b/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