ProCGroups/Generation/QuotientCriteria.lean

1import ProCGroups.Generation.Basic

2import ProCGroups.InverseSystems.ProjectionImageSystems

3import ProCGroups.ProC.OpenNormalSubgroups.Basic

4import ProCGroups.ProC.OpenNormalSubgroups.ClosedAndCosets

5import ProCGroups.Profinite.Basic

7/-

8PUBLIC_PAGE_SNAPSHOT

9generated_at: 2026-05-27T09:47:29+09:00

10lean_source: lean4/ProCGroups/Generation/QuotientCriteria.lean

11translation_root: data/translation

12purpose: identifies the local data snapshot used to build pages/

13placement: after imports, never before imports

14-/

15/-!

16# Topological generation

18Develops topological generation, generating families, convergence-to-one criteria, quotient generation, and profinite generation lemmas.

19-/

21open Set

22open scoped Topology Pointwise

24namespace ProCGroups.Generation

26universe u v

28open ProCGroups.InverseSystems

29open ProCGroups.ProC

30open ProCGroups

32section Generators

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

36/-- Topological generation in a surjective inverse system can be checked after every projection. -/

37theorem topologicallyGenerates_iff_forall_projection_inverseLimit

38 {I : Type v} [Preorder I] {S : InverseSystem (I := I)} [Nonempty I]

39 [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]

40 [∀ i, IsTopologicalGroup (S.X i)] [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]

41 (hdir : Directed (· ≤ ·) (id : I → I))

42 (hsurj : ∀ {i j : I} (hij : i ≤ j), Function.Surjective (S.map hij))

43 {X : Set S.inverseLimit} :

44 TopologicallyGenerates (G := S.inverseLimit) X ↔

45 ∀ i, TopologicallyGenerates (G := S.X i) (S.projection i '' X) := by

46 classical

47 constructor

48 · intro hX i

49 let πi : S.inverseLimit →* S.X i := {

50 toFun := fun x => S.projection i x

51 map_one' := rfl

52 map_mul' := by

53 intro x y

54 rfl

55 }

56 have hπsurj : Function.Surjective πi := S.surjective_π hdir hsurj i

57 have hmap :

58 (Subgroup.closure X).map πi = Subgroup.closure (S.projection i '' X) := by

59 simpa [πi] using (MonoidHom.map_closure πi X)

60 have htop :

61 ((Subgroup.closure X).map πi).topologicalClosure = ⊤ := by

62 have hX' : (Subgroup.closure X).topologicalClosure = ⊤ := by

63 simpa [TopologicallyGenerates] using hX

64 exact DenseRange.topologicalClosure_map_subgroup

65 (f := πi) (hf := S.continuous_projection i) (hf' := hπsurj.denseRange) hX'

66 simpa [TopologicallyGenerates, hmap] using htop

67 · intro hproj

68 let Y : Set S.inverseLimit :=

69 (((Subgroup.closure X).topologicalClosure : Subgroup S.inverseLimit) : Set S.inverseLimit)

70 have hYclosed : IsClosed Y := Subgroup.isClosed_topologicalClosure _

71 have hprojY : ∀ i, S.projection i '' Y = (Set.univ : Set (S.X i)) := by

72 intro i

73 let πi : S.inverseLimit →* S.X i := {

74 toFun := fun x => S.projection i x

75 map_one' := rfl

76 map_mul' := by

77 intro x y

78 rfl

79 }

80 have hmap :

81 (Subgroup.closure X).map πi = Subgroup.closure (S.projection i '' X) := by

82 simpa [πi] using (MonoidHom.map_closure πi X)

83 have hsubset :

84 ((Subgroup.closure (S.projection i '' X) : Subgroup (S.X i)) : Set (S.X i)) ⊆ S.projection i '' Y := by

85 intro y hy

86 have hy' : y ∈ (Subgroup.closure X).map πi := by

87 simpa [hmap] using hy

88 rcases hy' with ⟨z, hz, rfl⟩

89 exact ⟨z, Subgroup.le_topologicalClosure _ hz, rfl⟩

90 have hclosedImg : IsClosed (S.projection i '' Y) := by

91 exact (hYclosed.isCompact.image (S.continuous_projection i)).isClosed

92 have hdense :

93 Dense (((Subgroup.closure (S.projection i '' X) : Subgroup (S.X i)) : Set (S.X i))) :=

94 (topologicallyGenerates_iff_dense (G := S.X i) (X := S.projection i '' X)).1 (hproj i)

95 apply Set.eq_univ_iff_forall.2

96 intro y

97 have hy' :

98 y ∈ closure (((Subgroup.closure (S.projection i '' X) : Subgroup (S.X i)) : Set (S.X i))) := by

99 rw [hdense.closure_eq]

100 simp only [mem_univ]

101 exact closure_minimal hsubset hclosedImg hy'

102 have hYuniv : Y = (Set.univ : Set S.inverseLimit) := by

103 ext x

104 constructor

105 · intro hx

106 simp only [mem_univ]

107 · intro _

108 rw [S.mem_isClosed_iff_forall_projection_mem hdir hYclosed]

109 intro i

110 rw [hprojY i]

111 simp only [InverseSystem.projection_apply, mem_univ]

112 rw [TopologicallyGenerates]

113 exact SetLike.ext' hYuniv

114

115/-- A closed-normal quotient version of topological generation: `X ∪ N` generates iff the image

116of `X` generates modulo every open normal subgroup containing `N`. -/

117theorem topologicallyGenerates_union_subgroup_iff_forall_openNormalQuotient

118 (hG : IsProfiniteGroup G) {N : Subgroup G} [N.Normal]

119 {X : Set G} :

120 TopologicallyGenerates (G := G) (X ∪ (N : Set G)) ↔

121 ∀ U : OpenNormalSubgroup G, N ≤ (U : Subgroup G) →

122 TopologicallyGenerates (G := G ⧸ (U : Subgroup G))

123 ((QuotientGroup.mk' (U : Subgroup G)) '' X) := by

124 classical

125 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG

126 letI : TotallyDisconnectedSpace G :=

127 IsProfiniteGroup.totallyDisconnectedSpace hG

128 letI : T2Space G := IsProfiniteGroup.t2Space hG

129 constructor

130 · intro hX U hNU

131 have hmap :

132 TopologicallyGenerates (G := G ⧸ (U : Subgroup G))

133 ((QuotientGroup.mk' (U : Subgroup G)) '' (X ∪ (N : Set G))) :=

134 topologicallyGenerates_quotient_image (G := G) (N := (U : Subgroup G)) hX

135 have himg :

136 (QuotientGroup.mk' (U : Subgroup G) '' (X ∪ (N : Set G))) =

137 ((QuotientGroup.mk' (U : Subgroup G)) '' X) ∪

138 ({1} : Set (G ⧸ (U : Subgroup G))) := by

139 ext y

140 constructor

141 · intro hy

142 rcases hy with ⟨x, hx, rfl⟩

143 rcases hx with hxX | hxN

144 · exact Or.inl ⟨x, hxX, rfl⟩

145 · exact Or.inr (by

146 simp only [QuotientGroup.mk'_apply, mem_singleton_iff, QuotientGroup.eq_one_iff, hNU hxN])

147 · intro hy

148 rcases hy with hyX | hy1

149 · rcases hyX with ⟨x, hxX, rfl⟩

150 exact ⟨x, Or.inl hxX, rfl⟩

151 · refine ⟨1, Or.inr N.one_mem, ?_⟩

152 simpa using hy1.symm

153 have hmap' :

154 TopologicallyGenerates (G := G ⧸ (U : Subgroup G))

155 ((((QuotientGroup.mk' (U : Subgroup G)) '' X) ∪

156 ({1} : Set (G ⧸ (U : Subgroup G))))) := by

157 rwa [← himg]

158 exact

159 (topologicallyGenerates_union_one_iff

160 (G := G ⧸ (U : Subgroup G))

161 (X := ((QuotientGroup.mk' (U : Subgroup G)) '' X))).1 hmap'

162 · intro hquot

163 let H : ClosedSubgroup G :=

164 { toSubgroup := (Subgroup.closure (X ∪ (N : Set G))).topologicalClosure

165 isClosed' := Subgroup.isClosed_topologicalClosure _ }

166 have hXleH : X ⊆ (H : Subgroup G) := by

167 intro x hx

168 exact Subgroup.le_topologicalClosure _

169 (Subgroup.subset_closure (Or.inl hx))

170 have hNleH : N ≤ (H : Subgroup G) := by

171 intro n hn

172 exact Subgroup.le_topologicalClosure _

173 (Subgroup.subset_closure (Or.inr hn))

174 by_contra hH

175 change ¬ ((Subgroup.closure (X ∪ (N : Set G))).topologicalClosure = ⊤) at hH

176 have hHproper :

177 ((H : Subgroup G) : Set G) ≠ (Set.univ : Set G) := by

178 intro hEq

179 apply hH

180 change (H : Subgroup G) = ⊤

181 ext x

182 constructor

183 · intro _

184 simp only [Subgroup.mem_top]

185 · intro _

186 have hx' : x ∈ (Set.univ : Set G) := by simp only [mem_univ]

187 rwa [← hEq] at hx'

188 have hxNotAll : ¬ ∀ x : G, x ∈ ((H : Subgroup G) : Set G) := by

189 simpa [Set.eq_univ_iff_forall] using hHproper

190 push_neg at hxNotAll

191 rcases hxNotAll with ⟨x, hxH⟩

192 have hxNotAll :

193 ¬ ∀ V : Subgroup G, IsOpen (V : Set G) → (H : Subgroup G) ≤ V → x ∈ V := by

194 intro hxAll

195 apply hxH

196 change x ∈ (H : Subgroup G)

197 rw [closedSubgroup_eq_sInf_open (G := G) H]

198 rw [Subgroup.mem_sInf]

199 intro V hV

200 exact hxAll V hV.1 hV.2

201 push_neg at hxNotAll

202 rcases hxNotAll with ⟨V, hVopen, hHV, hxV⟩

203 have hVfin : Subgroup.FiniteIndex V := by

204 letI : Finite (G ⧸ V) := Subgroup.quotient_finite_of_isOpen V hVopen

205 exact Subgroup.finiteIndex_of_finite_quotient

206 letI : Subgroup.FiniteIndex V := hVfin

207 let U : OpenNormalSubgroup G :=

208 { toSubgroup := Subgroup.normalCore V

209 isOpen' := Subgroup.isOpen_of_isClosed_of_finiteIndex _ (V.normalCore_isClosed

210 (Subgroup.isClosed_of_isOpen V hVopen)) }

211 letI : (U : Subgroup G).Normal := U.isNormal'

212 have hNU : N ≤ (U : Subgroup G) :=

213 (Subgroup.normal_le_normalCore).2 (hNleH.trans hHV)

214 have hUV : (U : Subgroup G) ≤ V := by

215 change Subgroup.normalCore V ≤ V

216 exact Subgroup.normalCore_le V

217 have hxU : x ∉ (U : Set G) := by

218 intro hxU

219 exact hxV (hUV hxU)

220 have hgen := hquot U hNU

221 let qH : Subgroup (G ⧸ (U : Subgroup G)) :=

222 (H : Subgroup G).map (QuotientGroup.mk' (U : Subgroup G))

223 have himage_le_qH :

224 ((QuotientGroup.mk' (U : Subgroup G)) '' X) ⊆

225 (qH : Set (G ⧸ (U : Subgroup G))) := by

226 intro y hy

227 rcases hy with ⟨z, hzX, rfl⟩

228 exact ⟨z, hXleH hzX, rfl⟩

229 have hcl_le_qH :

230 Subgroup.closure (((QuotientGroup.mk' (U : Subgroup G)) '' X)) ≤ qH :=

231 (Subgroup.closure_le (K := qH)).2 himage_le_qH

232 have hclosure_le_qH :

233 (Subgroup.closure (((QuotientGroup.mk' (U : Subgroup G)) '' X))).topologicalClosure ≤

234 qH := by

235 letI : DiscreteTopology (G ⧸ (U : Subgroup G)) :=

236 QuotientGroup.discreteTopology U.toOpenSubgroup.isOpen'

237 have hqHclosed : IsClosed (qH : Set (G ⧸ (U : Subgroup G))) := by

238 exact isClosed_discrete (qH : Set (G ⧸ (U : Subgroup G)))

239 exact Subgroup.topologicalClosure_minimal _ hcl_le_qH hqHclosed

240 let qx : G ⧸ (U : Subgroup G) := QuotientGroup.mk' (U : Subgroup G) x

241 have hx_not_qH : qx ∉ (qH : Set (G ⧸ (U : Subgroup G))) := by

242 intro hxq

243 rcases hxq with ⟨z, hzH, hzx⟩

244 have hzV : z ∈ V := hHV hzH

245 have hdiv : z⁻¹ * x ∈ (U : Subgroup G) := by

246 exact (QuotientGroup.eq).1 hzx

247 have hdivV : z⁻¹ * x ∈ V := hUV hdiv

248 have hxV' : x ∈ V := by

249 simpa [mul_assoc] using V.mul_mem hzV hdivV

250 exact hxV hxV'

251 have hxtop : qx ∈ (((⊤ : Subgroup (G ⧸ (U : Subgroup G))) :

252 Set (G ⧸ (U : Subgroup G)))) := by

253 simp only [Subgroup.coe_top, mem_univ]

254 have htop :

255 (⊤ : Subgroup (G ⧸ (U : Subgroup G))) ≤

256 (Subgroup.closure (((QuotientGroup.mk' (U : Subgroup G)) '' X))).topologicalClosure := by

257 simpa [TopologicallyGenerates] using hgen

258 exact hx_not_qH (hclosure_le_qH (htop hxtop))

259

260/-- Direct finite-quotient test for topological generation, phrased with the bundled quotient

261projections. -/

262theorem topologicallyGenerates_iff_forall_quotientProj_image

263 (hG : IsProfiniteGroup G) {X : Set G} :

264 TopologicallyGenerates (G := G) X ↔

265 ∀ U : OpenNormalSubgroup G,

266 TopologicallyGenerates (G := G ⧸ (U : Subgroup G))

267 (OpenNormalSubgroup.quotientProj U '' X) := by

268 letI : T2Space G := IsProfiniteGroup.t2Space hG

269 have h :=

270 topologicallyGenerates_union_subgroup_iff_forall_openNormalQuotient

271 (G := G) hG (N := (⊥ : Subgroup G)) (X := X)

272 constructor

273 · intro hX U

274 have hUnion :

275 TopologicallyGenerates (G := G) (X ∪ (((⊥ : Subgroup G) : Set G))) := by

276 rw [show X ∪ (((⊥ : Subgroup G) : Set G)) = X ∪ ({1} : Set G) by

277 ext x

278 simp only [Subgroup.coe_bot, union_singleton, mem_insert_iff]]

279 exact (topologicallyGenerates_union_one_iff (G := G) (X := X)).2 hX

280 simpa [OpenNormalSubgroup.quotientProj] using h.1 hUnion U bot_le

281 · intro hquot

282 have hUnion :

283 TopologicallyGenerates (G := G) (X ∪ (((⊥ : Subgroup G) : Set G))) :=

284 h.2 (fun U _hU => by

285 simpa [OpenNormalSubgroup.quotientProj] using hquot U)

286 have hUnionOne : TopologicallyGenerates (G := G) (X ∪ ({1} : Set G)) := by

287 rw [show X ∪ ({1} : Set G) = X ∪ (((⊥ : Subgroup G) : Set G)) by

288 ext x

289 simp only [union_singleton, mem_insert_iff, Subgroup.coe_bot]]

290 exact hUnion

291 exact (topologicallyGenerates_union_one_iff (G := G) (X := X)).1 hUnionOne

292

293

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

295

296end Generators

297end ProCGroups.Generation