Source: ProCGroups.ProC.OpenNormalSubgroups.ClosedAndCosets
1import ProCGroups.Profinite.OpenSubgroups
3/-!
4# Closed subgroups and cosets
6This file expresses closed subgroups as intersections of open subgroups and develops separation by
7open subgroups. It also proves the disjointness and clopen properties of the relevant cosets.
8-/
10namespace ProCGroups.ProC
12universe u v
14section
16variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
18/--
19A closed subgroup of a profinite group is the intersection of all open subgroups containing it.
20-/
21theorem closedSubgroup_eq_sInf_open [CompactSpace G] [TotallyDisconnectedSpace G]
22 (H : ClosedSubgroup G) :
23 (H : Subgroup G) = sInf {N : Subgroup G | IsOpen (N : Set G) ∧ (H : Subgroup G) ≤ N} := by
24 ext x
25 constructor
26 · intro hx
27 simp only [Subgroup.mem_sInf, Set.mem_setOf_eq]
28 intro N hN
29 exact hN.2 hx
30 · intro hx
31 by_contra hxH
32 let W : Set G := { y : G | x * y⁻¹ ∉ (H : Set G) }
33 have hW : IsOpen W := by
34 change IsOpen ((fun y : G => x * y⁻¹) ⁻¹' ((H : Set G)ᶜ))
35 exact H.isClosed'.isOpen_compl.preimage (continuous_const.mul continuous_inv)
36 have h1W : (1 : G) ∈ W := by
37 simp only [W, Set.mem_setOf_eq, inv_one, mul_one]
38 exact hxH
39 rcases ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
40 (G := G) hW h1W with ⟨N, hNW⟩
41 let K : OpenSubgroup G :=
42 ⟨(H : Subgroup G) ⊔ (N : Subgroup G),
43 Subgroup.isOpen_of_openSubgroup ((H : Subgroup G) ⊔ (N : Subgroup G))
44 (show (N : Subgroup G) ≤ (H : Subgroup G) ⊔ (N : Subgroup G) from le_sup_right)⟩
45 have hHK : (H : Subgroup G) ≤ (K : Subgroup G) := by
46 intro y hy
47 exact Subgroup.mem_sup_left hy
48 have hxK : x ∈ (K : Subgroup G) := by
49 have hxall : ∀ N : Subgroup G, IsOpen (N : Set G) ∧ (H : Subgroup G) ≤ N → x ∈ N := by
50 simpa only [Subgroup.mem_sInf, Set.mem_setOf_eq] using hx
51 exact hxall (K : Subgroup G) ⟨openSubgroup_isOpen (G := G) K, hHK⟩
52 rcases
53 (Subgroup.mem_sup_of_normal_right (s := (H : Subgroup G)) (t := (N : Subgroup G))).1
54 hxK with
55 ⟨h, hhH, n, hnN, hxn⟩
56 have hnW : n ∈ W := hNW hnN
57 have : h ∉ (H : Set G) := by
58 simpa [W, hxn.symm, mul_assoc] using hnW
59 exact this hhH
61end
63section
65variable {G : Type u} [Group G]
67/--
68If the intersection of a family of subgroups is trivial, every nonidentity element is omitted by
69at least one member of the family.
70-/
71theorem exists_not_mem_of_iInf_eq_bot {ι : Type v} (U : ι → Subgroup G)
72 (hU : iInf U = (⊥ : Subgroup G)) {x : G} (hx : x ≠ 1) :
73 ∃ i : ι, x ∉ U i := by
74 by_contra h
75 have hxall : ∀ i : ι, x ∈ U i := by
76 intro i
77 by_contra hxi
78 exact h ⟨i, hxi⟩
79 have hxinf : x ∈ iInf U := by
80 simpa [Subgroup.mem_iInf] using hxall
81 have hxbot : x ∈ (⊥ : Subgroup G) := by
82 simpa [hU] using hxinf
83 exact hx (by simpa using hxbot)
85/-- Distinct left cosets of a subgroup are disjoint. -/
86theorem disjoint_leftCoset_of_not_mem (U : Subgroup G) {x y : G} (hxy : x⁻¹ * y ∉ U) :
87 Disjoint {g : G | x⁻¹ * g ∈ U} {g : G | y⁻¹ * g ∈ U} := by
88 refine Set.disjoint_left.2 ?_
89 intro g hx hg
90 apply hxy
91 have hmul : (x⁻¹ * g) * (y⁻¹ * g)⁻¹ ∈ U := U.mul_mem hx (U.inv_mem hg)
92 simpa [mul_assoc] using hmul
94variable [TopologicalSpace G] [IsTopologicalGroup G]
96/-- The left coset of an open subgroup is clopen. -/
97theorem isClopen_leftCoset_openSubgroup (U : OpenSubgroup G) (x : G) :
98 IsClopen {g : G | x⁻¹ * g ∈ (U : Subgroup G)} := by
99 let f : G → G := fun g => x⁻¹ * g
100 have hf : Continuous f := continuous_const.mul continuous_id
101 have hcoset :
102 {g : G | x⁻¹ * g ∈ (U : Subgroup G)} =
103 f ⁻¹' (U : Set G) := by
104 ext g
105 rfl
106 rw [hcoset]
107 refine ⟨?_, ?_⟩
108 · exact U.isClosed.preimage hf
109 · exact U.isOpen.preimage hf
111end
113end ProCGroups.ProC