Source: ProCGroups.ProC.OpenNormalSubgroups.CountableChains
1import ProCGroups.Profinite.Basic
3/-!
4# Countable descending open-normal chains
6This file defines countable open-normal bases at the identity and characterizes them by descending
7chains with trivial intersection. It also supplies the refinement property needed to use such
8chains as neighborhood bases.
9-/
11namespace ProCGroups.ProC
13universe u v
15section
17variable {G : Type u} [Group G] [TopologicalSpace G]
19/--
20Preparatory countable-chain layer for later use: \(1\) has a countable fundamental system of
21open normal subgroups. This isolates the part of the corollary that does not yet depend on the
22not-yet-formalized cardinal invariant \(w_0(G)\) or on the generator-counting statements from
23the later section on generators.
24-/
25def HasCountableOpenNormalBasisAtOne
26 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
27 ∃ U : ℕ → OpenNormalSubgroup G,
28 Antitone (fun n => (U n : Subgroup G)) ∧
29 ∀ W : Set G, IsOpen W → (1 : G) ∈ W →
30 ∃ n : ℕ, (((U n : Subgroup G) : Set G)) ⊆ W
32/--
33Compactness lemma for descending families of closed subgroups: if the total intersection lies
34inside an open subgroup, then one term already lies inside that open subgroup.
35-/
36theorem exists_term_le_openSubgroup_of_iInf_le [CompactSpace G]
37 (H : ℕ → Subgroup G) (hmono : Antitone H)
38 (hclosed : ∀ n, IsClosed (((H n : Subgroup G) : Set G)))
39 (U : OpenSubgroup G) (hInf : iInf H ≤ (U : Subgroup G)) :
40 ∃ n : ℕ, H n ≤ (U : Subgroup G) := by
41 let K : Set G := (((U : Subgroup G) : Set G))ᶜ
42 have hKclosed : IsClosed K := by
43 simpa [K] using (openSubgroup_isOpen (G := G) U).isClosed_compl
44 have hKcompact : IsCompact K := hKclosed.isCompact
45 have havoid : K ∩ ⋂ n, (((H n : Subgroup G) : Set G)) = ∅ := by
46 ext x
47 constructor
48 · intro hx
49 have hxInf : x ∈ iInf H := by
50 simpa using hx.2
51 exact False.elim (hx.1 (hInf hxInf))
52 · intro hx
53 simp only [Set.mem_empty_iff_false] at hx
54 have hdir : Directed (fun s t : Set G => s ⊇ t) (fun n => (((H n : Subgroup G) : Set G))) := by
55 intro i j
56 refine ⟨max i j, ?_, ?_⟩
57 · exact hmono (Nat.le_max_left i j)
58 · exact hmono (Nat.le_max_right i j)
59 rcases hKcompact.elim_directed_family_closed
60 (fun n => (((H n : Subgroup G) : Set G))) hclosed havoid hdir with ⟨n, hn⟩
61 refine ⟨n, ?_⟩
62 intro x hx
63 by_contra hxU
64 have hxK : x ∈ K := by
65 simpa [K] using hxU
66 have hmem : x ∈ K ∩ (((H n : Subgroup G) : Set G)) := by
67 exact ⟨hxK, hx⟩
68 have : x ∈ (∅ : Set G) := by
69 simp only [hn, Set.mem_empty_iff_false] at hmem
70 simp only [Set.mem_empty_iff_false] at this
72/--
73Preparatory countable-chain / neighborhood-basis equivalence for profinite groups: for a
74profinite group, giving a countable descending chain of open normal subgroups with trivial
75intersection is equivalent to giving a countable neighborhood basis at \(1\) formed by a
76descending chain of open normal subgroups. This is exactly the chain-theoretic content of the
77corollary; the generator-cardinality half will be added later once the \(w_0(G)\) /
78convergent-generator formulation is in place.
79-/
80theorem hasCountableOpenNormalBasisAtOne_iff_exists_descending_openNormalChain
81 [IsTopologicalGroup G] [CompactSpace G] [T1Space G] [TotallyDisconnectedSpace G] :
82 HasCountableOpenNormalBasisAtOne G ↔
83 ∃ U : ℕ → OpenNormalSubgroup G,
84 Antitone (fun n => (U n : Subgroup G)) ∧
85 iInf (fun n => (U n : Subgroup G)) = (⊥ : Subgroup G) := by
86 constructor
87 · rintro ⟨U, hmono, hbasis⟩
88 refine ⟨U, hmono, ?_⟩
89 apply le_antisymm
90 · intro x hx
91 change x = 1
92 by_contra hxne
93 let W : Set G := ({x} : Set G)ᶜ
94 have hW : IsOpen W := by
95 simp only [isOpen_compl_iff, Set.finite_singleton, Set.Finite.isClosed, W]
96 have h1W : (1 : G) ∈ W := by
97 have hx1 : (1 : G) ≠ x := by
98 intro h1x
99 exact hxne h1x.symm
100 simpa [W] using hx1
101 rcases hbasis W hW h1W with ⟨n, hnW⟩
102 have hxall : ∀ n : ℕ, x ∈ (((U n : Subgroup G) : Set G)) := by
103 simpa using hx
104 have hxW : x ∈ W := hnW (hxall n)
105 have : x ∉ ({x} : Set G) := by
106 simp only [Set.mem_compl_iff, Set.mem_singleton_iff, not_true_eq_false, W] at hxW
107 exact this (by simp only [Set.mem_singleton_iff])
108 · exact bot_le
109 · rintro ⟨U, hmono, hinf⟩
110 refine ⟨U, hmono, ?_⟩
111 intro W hW h1W
112 rcases ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
113 (G := G) hW h1W with ⟨N, hNW⟩
114 have hInfLe : iInf (fun n => (U n : Subgroup G)) ≤ (N : Subgroup G) := by
115 simp only [hinf, bot_le]
116 rcases exists_term_le_openSubgroup_of_iInf_le (G := G)
117 (fun n => (U n : Subgroup G)) hmono
118 (fun n => openNormalSubgroup_isClosed (G := G) (U n))
119 N.toOpenSubgroup hInfLe with ⟨n, hnN⟩
120 exact ⟨n, fun x hx => hNW (hnN hx)⟩
122end
124end ProCGroups.ProC