Source: ProCGroups.Profinite.Basic

1import ProCGroups.Profinite.OpenSubgroups

3/-!

4# Separation in profinite groups

6This module proves that an element of a profinite group lying in every open normal subgroup is

7the identity.

8-/

10open Set

11open scoped Topology Pointwise

13namespace ProCGroups

15universe u

17section Permanence

19variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

21namespace ProfiniteGrp

23/-- In a profinite group, an element lying in every open normal subgroup must be \(1\). -/

24theorem eq_one_of_mem_all_openNormalSubgroups [CompactSpace G]

25 [TotallyDisconnectedSpace G] {x : G}

26 (hx : ∀ U : OpenNormalSubgroup G, x ∈ (U : Subgroup G)) : x = 1 := by

27 by_contra hxne

28 let W : Set G := ({x} : Set G)ᶜ

29 have hW : IsOpen W := by

30 simp only [isOpen_compl_iff, finite_singleton, Finite.isClosed, W]

31 have h1W : (1 : G) ∈ W := by

32 have hx1 : (1 : G) ≠ x := by

33 intro h1x

34 exact hxne h1x.symm

35 simp only [mem_compl_iff, mem_singleton_iff, hx1, not_false_eq_true, W]

36 rcases ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one

37 (G := G) hW h1W with ⟨U, hUW⟩

38 have hxU : x ∈ (U : Subgroup G) := hx U

39 have hxW : x ∈ W := hUW hxU

40 simp only [mem_compl_iff, mem_singleton_iff, not_true_eq_false, W] at hxW

42end ProfiniteGrp

44end Permanence

46end ProCGroups