ProCGroups/ProC/OpenNormalSubgroups/CountableChains.lean
1import ProCGroups.Profinite.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/ProC/OpenNormalSubgroups/CountableChains.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Pro-C groups and open normal quotients
14Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.
15-/
17namespace ProCGroups.ProC
19universe u v
21section
23variable {G : Type u} [Group G] [TopologicalSpace G]
25/-- Preparatory countable-chain layer for later use: `1` has a countable
26fundamental system of open normal subgroups.
28This isolates the part of the corollary that does not yet depend on the still-unformalized
30generators.
31-/
33 (G : Type u) [Group G] [TopologicalSpace G] : Prop :=
34 ∃ U : ℕ → OpenNormalSubgroup G,
35 Antitone (fun n => (U n : Subgroup G)) ∧
36 ∀ W : Set G, IsOpen W → (1 : G) ∈ W →
37 ∃ n : ℕ, (((U n : Subgroup G) : Set G)) ⊆ W
39/-- Compactness lemma for descending families of closed subgroups: if the total intersection lies
41theorem exists_term_le_openSubgroup_of_iInf_le [CompactSpace G]
42 (H : ℕ → Subgroup G) (hmono : Antitone H)
43 (hclosed : ∀ n, IsClosed (((H n : Subgroup G) : Set G)))
44 (U : OpenSubgroup G) (hInf : iInf H ≤ (U : Subgroup G)) :
45 ∃ n : ℕ, H n ≤ (U : Subgroup G) := by
46 let K : Set G := (((U : Subgroup G) : Set G))ᶜ
47 have hKclosed : IsClosed K := by
48 simpa [K] using (openSubgroup_isOpen (G := G) U).isClosed_compl
50 have havoid : K ∩ ⋂ n, (((H n : Subgroup G) : Set G)) = ∅ := by
51 ext x
52 constructor
53 · intro hx
54 have hxInf : x ∈ iInf H := by
55 simpa using hx.2
56 exact False.elim (hx.1 (hInf hxInf))
57 · intro hx
58 simp only [Set.mem_empty_iff_false] at hx
59 have hdir : Directed (fun s t : Set G => s ⊇ t) (fun n => (((H n : Subgroup G) : Set G))) := by
60 intro i j
61 refine ⟨max i j, ?_, ?_⟩
62 · exact hmono (Nat.le_max_left i j)
63 · exact hmono (Nat.le_max_right i j)
64 rcases hKcompact.elim_directed_family_closed
65 (fun n => (((H n : Subgroup G) : Set G))) hclosed havoid hdir with ⟨n, hn⟩
66 refine ⟨n, ?_⟩
67 intro x hx
68 by_contra hxU
69 have hxK : x ∈ K := by
70 simpa [K] using hxU
71 have hmem : x ∈ K ∩ (((H n : Subgroup G) : Set G)) := by
72 exact ⟨hxK, hx⟩
73 have : x ∈ (∅ : Set G) := by
74 simp only [hn, Set.mem_empty_iff_false] at hmem
75 simp only [Set.mem_empty_iff_false] at this
77/-- Preparatory countable-chain / neighborhood-basis equivalence for profinite groups:
78for a profinite group, giving a countable descending chain of open normal subgroups with trivial
79intersection is equivalent to giving a countable neighborhood basis at `1` formed by a descending
80chain of open normal subgroups.
84-/
86 [IsTopologicalGroup G] [CompactSpace G] [T1Space G] [TotallyDisconnectedSpace G] :
88 ∃ U : ℕ → OpenNormalSubgroup G,
89 Antitone (fun n => (U n : Subgroup G)) ∧
90 iInf (fun n => (U n : Subgroup G)) = (⊥ : Subgroup G) := by
91 constructor
92 · rintro ⟨U, hmono, hbasis⟩
93 refine ⟨U, hmono, ?_⟩
94 apply le_antisymm
95 · intro x hx
96 change x = 1
97 by_contra hxne
98 let W : Set G := ({x} : Set G)ᶜ
99 have hW : IsOpen W := by
100 simp only [isOpen_compl_iff, Set.finite_singleton, Set.Finite.isClosed, W]
101 have h1W : (1 : G) ∈ W := by
102 have hx1 : (1 : G) ≠ x := by
103 intro h1x
104 exact hxne h1x.symm
105 simpa [W] using hx1
106 rcases hbasis W hW h1W with ⟨n, hnW⟩
107 have hxall : ∀ n : ℕ, x ∈ (((U n : Subgroup G) : Set G)) := by
108 simpa using hx
109 have hxW : x ∈ W := hnW (hxall n)
110 have : x ∉ ({x} : Set G) := by
111 simp only [Set.mem_compl_iff, Set.mem_singleton_iff, not_true_eq_false, W] at hxW
112 exact this (by simp only [Set.mem_singleton_iff])
113 · exact bot_le
114 · rintro ⟨U, hmono, hinf⟩
115 refine ⟨U, hmono, ?_⟩
116 intro W hW h1W
117 rcases ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
118 (G := G) hW h1W with ⟨N, hNW⟩
119 have hInfLe : iInf (fun n => (U n : Subgroup G)) ≤ (N : Subgroup G) := by
120 simp only [hinf, bot_le]
121 rcases exists_term_le_openSubgroup_of_iInf_le (G := G)
122 (fun n => (U n : Subgroup G)) hmono
123 (fun n => openNormalSubgroup_isClosed (G := G) (U n))
124 N.toOpenSubgroup hInfLe with ⟨n, hnN⟩
125 exact ⟨n, fun x hx => hNW (hnN hx)⟩
127/-- The same preparatory countable-chain equivalence, packaged with the working
128`IsProfiniteGroup` predicate used throughout this file. -/
130 [IsTopologicalGroup G]
131 (hprof : IsProfiniteGroup G) :
133 ∃ U : ℕ → OpenNormalSubgroup G,
134 Antitone (fun n => (U n : Subgroup G)) ∧
135 iInf (fun n => (U n : Subgroup G)) = (⊥ : Subgroup G) := by
136 letI : CompactSpace G := IsProfiniteGroup.compactSpace hprof
137 letI : T2Space G := IsProfiniteGroup.t2Space hprof
138 letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hprof
139 simpa using
142end
144end ProCGroups.ProC