Source: ProCGroups.Generation.QuotientCriteria

1import ProCGroups.Generation.Basic

2import ProCGroups.InverseSystems.ProjectionImageSystems

3import ProCGroups.ProC.OpenNormalSubgroups.Basic

4import ProCGroups.ProC.OpenNormalSubgroups.ClosedAndCosets

5import ProCGroups.Profinite.Basic

7/-!

8# Detecting topological generation in finite quotients

10This module characterizes topological generation in inverse limits by generation of every

11finite-stage image. It specializes the criterion to quotients by open normal subgroups, both

12for a set alone and for a set together with a fixed subgroup.

13-/

15open Set

16open scoped Topology Pointwise

18namespace ProCGroups.Generation

20universe u v

22open ProCGroups.InverseSystems

23open ProCGroups.ProC

24open ProCGroups

26section Generators

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

29 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

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

32theorem topologicallyGenerates_iff_forall_projection_inverseLimit

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

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

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

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

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

38 {X : Set S.inverseLimit} :

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

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

41 classical

42 constructor

43 · intro hX i

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

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

46 map_one' := rfl

47 map_mul' := by

48 intro x y

49 rfl

50 }

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

52 have hmap :

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

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

55 have htop :

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

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

58 simpa [TopologicallyGenerates] using hX

59 exact DenseRange.topologicalClosure_map_subgroup

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

61 simpa [TopologicallyGenerates, hmap] using htop

62 · intro hproj

63 let Y : Set S.inverseLimit :=

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

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

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

67 intro i

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

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

70 map_one' := rfl

71 map_mul' := by

72 intro x y

73 rfl

74 }

75 have hmap :

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

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

78 have hsubset :

79 ((Subgroup.closure (S.projection i '' X) : Subgroup (S.X i)) : Set (S.X i)) ⊆

80 S.projection i '' Y := by

81 intro y hy

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

83 simpa [hmap] using hy

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

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

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

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

88 have hdense :

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

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

91 apply Set.eq_univ_iff_forall.2

92 intro y

93 have hy' :

94 y ∈ closure (((Subgroup.closure (S.projection i '' X) : Subgroup (S.X i)) : Set (S.X

95 i))) := by

96 rw [hdense.closure_eq]

97 simp only [mem_univ]

98 exact closure_minimal hsubset hclosedImg hy'

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

100 ext x

101 constructor

102 · intro hx

103 simp only [mem_univ]

104 · intro _

105 rw [S.mem_isClosed_iff_forall_projection_mem hdir hYclosed]

106 intro i

107 rw [hprojY i]

108 simp only [InverseSystem.projection_apply, mem_univ]

109 rw [TopologicallyGenerates]

110 exact SetLike.ext' hYuniv

111

112omit [T2Space G] in

113/--

114A closed-normal quotient version of topological generation: \(X \cup N\) generates if and only

115if the image of \(X\) generates modulo every open normal subgroup containing \(N\).

116-/

117theorem topologicallyGenerates_union_subgroup_iff_forall_openNormalQuotient

118 {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 constructor

126 · intro hX U hNU

127 have hmap :

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

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

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

131 have himg :

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

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

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

135 ext y

136 constructor

137 · intro hy

138 rcases hy with ⟨x, hx, rfl⟩

139 rcases hx with hxX | hxN

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

141 · exact Or.inr (by

142 simp only [QuotientGroup.mk'_apply, mem_singleton_iff, QuotientGroup.eq_one_iff, hNU

143 hxN])

144 · intro hy

145 rcases hy with hyX | hy1

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

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

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

149 simpa using hy1.symm

150 have hmap' :

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

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

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

154 rwa [← himg]

155 exact

156 (topologicallyGenerates_union_one_iff

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

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

159 · intro hquot

160 let H : ClosedSubgroup G :=

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

162 isClosed' := Subgroup.isClosed_topologicalClosure _ }

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

164 intro x hx

165 exact Subgroup.le_topologicalClosure _

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

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

168 intro n hn

169 exact Subgroup.le_topologicalClosure _

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

171 by_contra hH

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

173 have hHproper :

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

175 intro hEq

176 apply hH

177 change (H : Subgroup G) = ⊤

178 ext x

179 constructor

180 · intro _

181 simp only [Subgroup.mem_top]

182 · intro _

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

184 rwa [← hEq] at hx'

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

186 simpa [Set.eq_univ_iff_forall] using hHproper

187 push Not at hxNotAll

188 rcases hxNotAll with ⟨x, hxH⟩

189 have hxNotAll :

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

191 intro hxAll

192 apply hxH

193 change x ∈ (H : Subgroup G)

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

195 rw [Subgroup.mem_sInf]

196 intro V hV

197 exact hxAll V hV.1 hV.2

198 push Not at hxNotAll

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

200 have hVfin : Subgroup.FiniteIndex V := by

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

202 exact Subgroup.finiteIndex_of_finite_quotient

203 letI : Subgroup.FiniteIndex V := hVfin

204 let U : OpenNormalSubgroup G :=

205 { toSubgroup := Subgroup.normalCore V

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

207 (Subgroup.isClosed_of_isOpen V hVopen)) }

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

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

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

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

212 change Subgroup.normalCore V ≤ V

213 exact Subgroup.normalCore_le V

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

215 intro hxU

216 exact hxV (hUV hxU)

217 have hgen := hquot U hNU

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

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

220 have himage_le_qH :

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

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

223 intro y hy

224 rcases hy with ⟨z, hzX, rfl⟩

225 exact ⟨z, hXleH hzX, rfl⟩

226 have hcl_le_qH :

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

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

229 have hclosure_le_qH :

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

231 qH := by

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

233 QuotientGroup.discreteTopology U.toOpenSubgroup.isOpen'

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

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

236 exact Subgroup.topologicalClosure_minimal _ hcl_le_qH hqHclosed

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

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

239 intro hxq

240 rcases hxq with ⟨z, hzH, hzx⟩

241 have hzV : z ∈ V := hHV hzH

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

243 exact (QuotientGroup.eq).1 hzx

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

245 have hxV' : x ∈ V := by

246 simpa [mul_assoc] using V.mul_mem hzV hdivV

247 exact hxV hxV'

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

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

250 simp only [Subgroup.coe_top, mem_univ]

251 have htop :

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

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

254 simpa [TopologicallyGenerates] using hgen

255 exact hx_not_qH (hclosure_le_qH (htop hxtop))

256

257omit [T2Space G] in

258/--

259This is the direct finite-quotient test for topological generation, phrased with the bundled

260quotient projections.

261-/

262theorem topologicallyGenerates_iff_forall_quotientProj_image

263 {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 have h :=

269 topologicallyGenerates_union_subgroup_iff_forall_openNormalQuotient

270 (G := G) (N := (⊥ : Subgroup G)) (X := X)

271 constructor

272 · intro hX U

273 have hUnion :

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

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

276 ext x

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

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

279 have hproj :

280 (OpenNormalSubgroup.quotientProj U :

281 G → G ⧸ (U : Subgroup G)) =

282 (QuotientGroup.mk' (U : Subgroup G) :

283 G → G ⧸ (U : Subgroup G)) := by

284 rfl

285 rw [hproj]

286 exact h.1 hUnion U bot_le

287 · intro hquot

288 have hUnion :

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

290 h.2 (fun U _hU => by

291 have hproj :

292 (OpenNormalSubgroup.quotientProj U :

293 G → G ⧸ (U : Subgroup G)) =

294 (QuotientGroup.mk' (U : Subgroup G) :

295 G → G ⧸ (U : Subgroup G)) := by

296 rfl

297 rw [← hproj]

298 exact hquot U)

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

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

301 ext x

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

303 exact hUnion

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

305

306

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

308

309end Generators

310end ProCGroups.Generation