Source: ProCGroups.Generation.GeneratorConvergingPairs

1import ProCGroups.Generation.QuotientCriteria

2import ProCGroups.ProC.Quotients.LeftQuotientProjectionSections

4/-!

5# Partial converging generators modulo a closed normal subgroup

7`GeneratorConvergingPair` packages representatives that converge modulo a closed normal subgroup

8and generate together with that subgroup. The refinement preorder is developed far enough to

9construct upper bounds for chains and to extract finite generating data after passage to an open

10normal quotient.

11-/

13open Set

14open scoped Topology Pointwise

16namespace ProCGroups.Generation

18universe u v

20open ProCGroups.InverseSystems

21open ProCGroups.ProC

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

24 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

27/-- A partial generating set together with a closed normal subgroup modulo which it converges. -/

28structure GeneratorConvergingPair where

29 /-- The subgroup that is retained alongside the chosen generators. -/

30 N : Subgroup G

31 /-- The retained subgroup is normal, so convergence may be interpreted in the quotient. -/

32 normal_N : N.Normal

33 /-- The retained subgroup is closed in `G`. -/

34 closed_N : IsClosed (N : Set G)

35 /-- The selected representatives outside the retained subgroup. -/

36 X : Set G

37 /-- No selected representative lies in `N`. -/

38 subset_compl : X ⊆ (N : Set G)ᶜ

39 /--

40 For every open subgroup containing `N`, only finitely many selected representatives lie

41 outside that open subgroup; equivalently, their images converge to one modulo `N`.

42 -/

43 convergesToOneAlongOpenSubgroups_mod :

44 ∀ U : OpenSubgroup G, N ≤ (U : Subgroup G) → (X \ (U : Set G)).Finite

45 /-- The union of the selected representatives and `N` topologically generates `G`. -/

46 generates : TopologicallyGenerates (G := G) (X ∪ (N : Set G))

48/-- The order relation is the refinement relation on the corresponding data. -/

49instance instLEGeneratorConvergingPair : LE (GeneratorConvergingPair (G := G)) where

50 le A B := B.N ≤ A.N ∧ A.X ⊆ B.X ∧ B.X \ A.X ⊆ (A.N : Set G)

52/-- The preorder is induced by refinement of the corresponding data. -/

53instance instPreorderGeneratorConvergingPair : Preorder (GeneratorConvergingPair (G := G)) where

54 le_refl A := ⟨le_rfl, subset_rfl, by simp only [sdiff_self, empty_subset]⟩

55 le_trans A B C hAB hBC := by

56 rcases hAB with ⟨hABN, hABX, hABdiff⟩

57 rcases hBC with ⟨hBCN, hBCX, hBCdiff⟩

58 refine ⟨hBCN.trans hABN, hABX.trans hBCX, ?_⟩

59 intro x hx

60 rcases hx with ⟨hxC, hxA⟩

61 by_cases hxB : x ∈ B.X

62 · exact hABdiff ⟨hxB, hxA⟩

63 · exact hABN (hBCdiff ⟨hxC, hxB⟩)

65/-- The initial generator-converging pair. -/

66noncomputable def initialGeneratorConvergingPair : GeneratorConvergingPair (G := G) where

67 N := ⊤

68 normal_N := by infer_instance

69 closed_N := isClosed_univ

70 X := ∅

71 subset_compl := by intro x hx; simp only [mem_empty_iff_false] at hx

72 convergesToOneAlongOpenSubgroups_mod := by

73 intro U hU

74 simp only [empty_sdiff, finite_empty]

75 generates := by

76 simpa [TopologicallyGenerates, Set.empty_union, Subgroup.closure_eq] using

77 (top_unique (Subgroup.le_topologicalClosure (⊤ : Subgroup G)) :

78 (⊤ : Subgroup G).topologicalClosure = ⊤)

80/-- A finite subset of a chain has an upper element from that subset. -/

81theorem finite_subset_chain_has_upper {α : Type*} [Preorder α] {c : Set α}

82 (hc : IsChain (· ≤ ·) c) :

83 ∀ s : Finset α, ↑s ⊆ c → s.Nonempty → ∃ m ∈ s, ∀ z ∈ s, z ≤ m := by

84 classical

85 intro s

86 refine Finset.induction_on s ?_ ?_

87 · intro hs hne

88 exact False.elim (hne.ne_empty rfl)

89 · intro a s ha ih hs hne

90 by_cases hsne : s.Nonempty

91 · rcases ih

92 (by

93 intro z hz

94 exact hs (by simp only [Finset.coe_insert, mem_insert_iff, hz, or_true]))

95 hsne with ⟨m, hm, hmax⟩

96 have ha' : a ∈ c := hs (by simp only [Finset.coe_insert, mem_insert_iff, SetLike.mem_coe,

97 true_or])

98 have hm' : m ∈ c := hs (by simp only [Finset.coe_insert, mem_insert_iff, SetLike.mem_coe,

99 hm, or_true])

100 have hcmp : a ≤ m ∨ m ≤ a := by

101 by_cases hEq : a = m

102 · exact Or.inl (hEq ▸ le_rfl)

103 · exact hc ha' hm' hEq

104 cases hcmp with

105 | inl ham =>

106 refine ⟨m, by simp only [Finset.mem_insert, hm, or_true], ?_⟩

107 intro z hz

108 rcases Finset.mem_insert.mp hz with rfl | hz'

109 · exact ham

110 · exact hmax z hz'

111 | inr hma =>

112 refine ⟨a, by simp only [Finset.mem_insert, true_or], ?_⟩

113 intro z hz

114 rcases Finset.mem_insert.mp hz with rfl | hz'

115 · exact le_rfl

116 · exact (hmax z hz').trans hma

117 · have hs0 : s = ∅ := Finset.not_nonempty_iff_eq_empty.mp hsne

118 refine ⟨a, by simp only [hs0, insert_empty_eq, Finset.mem_singleton], ?_⟩

119 intro z hz

120 have hz' : z = a := by simpa [hs0] using hz

121 subst z

122 exact le_rfl

123

124omit [T2Space G] [TotallyDisconnectedSpace G] in

125/--

126If the infimum of the closed normal subgroups in a chain lies in an open subgroup, then one

127stage already lies in that open subgroup.

128-/

129theorem exists_pair_le_openSubgroup_of_chain_iInf_le

130 {c : Set (GeneratorConvergingPair (G := G))}

131 (hc : IsChain (· ≤ ·) c) (hcne : c.Nonempty)

132 (U : OpenSubgroup G)

133 (hInf : iInf (fun p : c => p.1.N) ≤ (U : Subgroup G)) :

134 ∃ p : c, p.1.N ≤ (U : Subgroup G) := by

135 classical

136 have hInter :

137 (⋂ p : c, (((p.1.N : Subgroup G) : Set G))) ⊆ ((U : Subgroup G) : Set G) := by

138 intro x hx

139 exact hInf (by simpa [Subgroup.mem_iInf] using hx)

140 rcases finite_iInter_subgroup_subset_openSubgroup (G := G)

141 (H := fun p : c => p.1.N)

142 (hclosed := fun p => p.1.closed_N)

143 U hInter with ⟨s, hs⟩

144 by_cases hsne : s.Nonempty

145 · have hc' : IsChain (· ≤ ·) (Set.univ : Set c) := by

146 intro a ha b hb hne

147 have hne' : (a : GeneratorConvergingPair (G := G)) ≠ b := by

148 intro h

149 exact hne (Subtype.ext h)

150 simpa using hc a.2 b.2 hne'

151 rcases finite_subset_chain_has_upper hc' s (by intro z hz; simp only [mem_univ]) hsne with

152 ⟨m, hm, hmax⟩

153 refine ⟨m, ?_⟩

154 intro x hx

155 have hx' :

156 x ∈ ⋂ p ∈ s, (((p.1.N : Subgroup G) : Set G)) := by

157 refine mem_iInter₂.2 ?_

158 intro p hp

159 exact (hmax p hp).1 hx

160 exact hs hx'

161 · rcases hcne with ⟨p, hp⟩

162 refine ⟨⟨p, hp⟩, ?_⟩

163 have htop : ((⊤ : Subgroup G) : Set G) ⊆ ((U : Subgroup G) : Set G) := by

164 have : (⋂ p ∈ s, (((p.1.N : Subgroup G) : Set G))) ⊆ ((U : Subgroup G) : Set G) := hs

165 simpa [Finset.not_nonempty_iff_eq_empty.mp hsne] using this

166 intro x hx

167 exact htop (by simp only [Subgroup.coe_top, mem_univ])

168

169/-- Upper bound of a nonempty chain of generator-converging pairs. -/

170noncomputable def chainUpperBoundOfNonempty

171 {c : Set (GeneratorConvergingPair (G := G))}

172 (hc : IsChain (· ≤ ·) c) (hcne : c.Nonempty) :

173 GeneratorConvergingPair (G := G) where

174 N := iInf fun p : c => p.1.N

175 normal_N := by

176 classical

177 exact Subgroup.normal_iInf_normal fun p : c => p.1.normal_N

178 closed_N := by

179 classical

180 simpa using isClosed_iInter (fun p : c => p.1.closed_N)

181 X := ⋃ p : c, p.1.X

182 subset_compl := by

183 intro x hx

184 rcases mem_iUnion.mp hx with ⟨p, hpx⟩

185 refine by

186 intro hxK

187 exact p.1.subset_compl hpx ((iInf_le (fun q : c => q.1.N) p) hxK)

188 convergesToOneAlongOpenSubgroups_mod := by

189 intro U hKU

190 rcases exists_pair_le_openSubgroup_of_chain_iInf_le (G := G) hc hcne U

191 hKU with ⟨p, hpU⟩

192 have hEq : ((⋃ q : c, q.1.X) \ (U : Set G)) = (p.1.X \ (U : Set G)) := by

193 ext x

194 constructor

195 · intro hx

196 rcases hx with ⟨hxX, hxU⟩

197 rcases mem_iUnion.mp hxX with ⟨q, hqx⟩

198 have hcmp :

199 (q.1 ≤ p.1) ∨ (p.1 ≤ q.1) := by

200 by_cases hqp : q = p

201 · exact Or.inl (hqp ▸ le_rfl)

202 · have hqp' : (q : GeneratorConvergingPair (G := G)) ≠ p := by

203 intro h

204 exact hqp (Subtype.ext h)

205 exact hc q.2 p.2 hqp'

206 cases hcmp with

207 | inl hqp =>

208 exact ⟨hqp.2.1 hqx, hxU⟩

209 | inr hpq =>

210 by_cases hxp : x ∈ p.1.X

211 · exact ⟨hxp, hxU⟩

212 · have hxN : x ∈ (p.1.N : Set G) := hpq.2.2 ⟨hqx, hxp⟩

213 exact False.elim (hxU (hpU hxN))

214 · intro hx

215 exact ⟨mem_iUnion.mpr ⟨p, hx.1⟩, hx.2⟩

216 rw [hEq]

217 exact p.1.convergesToOneAlongOpenSubgroups_mod U hpU

218 generates := by

219 let K : Subgroup G := iInf fun p : c => p.1.N

220 letI : K.Normal := Subgroup.normal_iInf_normal fun p : c => p.1.normal_N

221 have hKclosed : IsClosed (K : Set G) := by

222 simpa [K] using isClosed_iInter (fun p : c => p.1.closed_N)

223 apply (topologicallyGenerates_union_subgroup_iff_forall_openNormalQuotient

224 (G := G)

225 (N := K) (X := ⋃ p : c, p.1.X)).2

226 intro U hKU

227 rcases exists_pair_le_openSubgroup_of_chain_iInf_le (G := G) hc hcne U.toOpenSubgroup

228 (by simpa [K] using hKU) with ⟨p, hpU⟩

229 have hpgen :

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

231 ((QuotientGroup.mk' (U : Subgroup G)) '' p.1.X) := by

232 letI : p.1.N.Normal := p.1.normal_N

233 exact

234 (topologicallyGenerates_union_subgroup_iff_forall_openNormalQuotient

235 (G := G)

236 (N := p.1.N) (X := p.1.X)).1

237 p.1.generates U hpU

238 exact topologicallyGenerates_mono hpgen (by

239 intro y hy

240 rcases hy with ⟨x, hx, rfl⟩

241 exact ⟨x, mem_iUnion.mpr ⟨p, hx⟩, rfl⟩)

242

243omit [T2Space G] in

244/-- The generator-converging-pair order is inductive over chains. -/

245theorem chain_bounded_generatorConvergingPair

246 (c : Set (GeneratorConvergingPair (G := G)))

247 (hc : IsChain (· ≤ ·) c) :

248 BddAbove c := by

249 classical

250 rcases c.eq_empty_or_nonempty with rfl | hcne

251 · exact ⟨initialGeneratorConvergingPair (G := G), by intro a ha; cases ha⟩

252 · refine ⟨chainUpperBoundOfNonempty (G := G) hc hcne, ?_⟩

253 intro p hp

254 refine ⟨?_, ?_, ?_⟩

255 · exact iInf_le (fun q : {q // q ∈ c} => q.1.N) ⟨p, hp⟩

256 · intro x hx

257 exact mem_iUnion.mpr ⟨⟨p, hp⟩, hx⟩

258 · intro x hx

259 rcases hx with ⟨hxX, hxpX⟩

260 rcases mem_iUnion.mp hxX with ⟨q, hqx⟩

261 by_cases hqp : q = ⟨p, hp⟩

262 · exact False.elim (hxpX (by simpa [hqp] using hqx))

263 · have hqp' : (q : GeneratorConvergingPair (G := G)) ≠ p := by

264 intro h

265 exact hqp (Subtype.ext h)

266 rcases hc q.2 hp hqp' with hqle | hple

267 · exact False.elim (hxpX (hqle.2.1 hqx))

268 · exact hple.2.2 ⟨hqx, hxpX⟩

269

270omit [T2Space G] [TotallyDisconnectedSpace G] in

271/--

272An open-normal quotient of a closed normal subgroup has a finite generating set modulo the

273intersection with the open normal subgroup.

274-/

275theorem exists_finite_subset_generating_subgroup_mod_openNormal

276 {M : Subgroup G}

277 (hMclosed : IsClosed (M : Set G)) (U : OpenNormalSubgroup G) :

278 ∃ T : Set G,

279 T.Finite ∧

280 T ⊆ (M : Set G) \ (((U : Subgroup G) ⊓ M : Subgroup G) : Set G) ∧

281 M ≤ Subgroup.closure (T ∪ ((((U : Subgroup G) ⊓ M : Subgroup G) : Subgroup G) : Set G)) := by

282 classical

283 letI : IsClosed (M : Set G) := hMclosed

284 letI : CompactSpace M := hMclosed.isClosedEmbedding_subtypeVal.compactSpace

285 let UM : OpenNormalSubgroup M :=

286 OpenNormalSubgroup.comap (M.subtype) continuous_subtype_val U

287 obtain ⟨σ, -, hσright, -⟩ :=

288 quotient_openNormalSubgroup_hasContinuousSection (G := M) UM

289 let q1 : M ⧸ (UM : Subgroup M) := ((1 : M) : M ⧸ (UM : Subgroup M))

290 let Tsub : Set M := σ '' ({q1} : Set (M ⧸ (UM : Subgroup M)))ᶜ

291 let T : Set G := Subtype.val '' Tsub

292 refine ⟨T, ?_, ?_, ?_⟩

293 · letI : Finite (M ⧸ (UM : Subgroup M)) := openNormalSubgroup_finiteQuotient (G := M) UM

294 have hfin : ({q1} : Set (M ⧸ (UM : Subgroup M)))ᶜ.Finite := Set.toFinite _

295 exact hfin.image σ |>.image Subtype.val

296 · intro x hx

297 rcases hx with ⟨y, hy, rfl⟩

298 rcases hy with ⟨q, hq, rfl⟩

299 refine ⟨(σ q).2, ?_⟩

300 intro hxUM

301 have hσUM : σ q ∈ (UM : Subgroup M) := by

302 change (((σ q : M) : G) ∈ (U : Subgroup G))

303 exact hxUM.1

304 have : q = q1 := by

305 calc

306 q = QuotientGroup.mk' (UM : Subgroup M) (σ q) := (hσright q).symm

307 _ = q1 := by

308 have hq1 :

309 QuotientGroup.mk' (UM : Subgroup M) (σ q) = (1 : M ⧸ (UM : Subgroup M)) :=

310 (QuotientGroup.eq_one_iff (N := (UM : Subgroup M)) (σ q)).2 hσUM

311 simpa [q1] using hq1

312 exact hq this

313 · intro m hmM

314 let mM : M := ⟨m, hmM⟩

315 let q : M ⧸ (UM : Subgroup M) := QuotientGroup.mk' (UM : Subgroup M) mM

316 by_cases hq : q = q1

317 · have hmUM : (⟨m, hmM⟩ : M) ∈ (UM : Subgroup M) := by

318 have hq1 : QuotientGroup.mk' (UM : Subgroup M) mM = (1 : M ⧸ (UM : Subgroup M)) := by

319 simpa [q, q1, mM] using hq

320 exact (QuotientGroup.eq_one_iff (N := (UM : Subgroup M)) mM).1 hq1

321 have hmN' : m ∈ ((U : Subgroup G) ⊓ M : Subgroup G) := by

322 refine ⟨?_, hmM⟩

323 have hmU := hmUM

324 change m ∈ (U : Subgroup G) at hmU

325 exact hmU

326 exact Subgroup.subset_closure (Or.inr hmN')

327 · have hT : ((σ q : M) : G) ∈ T := by

328 exact ⟨σ q, ⟨q, hq, rfl⟩, rfl⟩

329 have hEq :

330 QuotientGroup.mk' (UM : Subgroup M) (σ q) =

331 QuotientGroup.mk' (UM : Subgroup M) mM := by

332 simpa [q, mM] using hσright q

333 have hdiv : (σ q)⁻¹ * mM ∈ (UM : Subgroup M) := by

334 exact (QuotientGroup.eq).1 hEq

335 have hdivU : (((σ q : M) : G)⁻¹ * m) ∈ (U : Subgroup G) := by

336 have hdiv' := hdiv

337 change ((↑(σ q) : G)⁻¹ * m) ∈ (U : Subgroup G) at hdiv'

338 exact hdiv'

339 have hdivM : (((σ q : M) : G)⁻¹ * m) ∈ M := by

340 change ((((σ q)⁻¹ * mM : M) : G) ∈ M)

341 exact (((σ q)⁻¹ * mM : M)).2

342 have hN' : (((σ q : M) : G)⁻¹ * m) ∈ ((U : Subgroup G) ⊓ M : Subgroup G) := by

343 exact ⟨hdivU, hdivM⟩

344 have hσ' :

345 ((σ q : M) : G) ∈

346 Subgroup.closure (T ∪ ((((U : Subgroup G) ⊓ M : Subgroup G) : Subgroup G) : Set G)) :=

347 Subgroup.subset_closure (Or.inl hT)

348 have hdiv' :

349 ((σ q : M) : G)⁻¹ * m ∈

350 Subgroup.closure (T ∪ ((((U : Subgroup G) ⊓ M : Subgroup G) : Subgroup G) : Set G)) :=

351 Subgroup.subset_closure (Or.inr hN')

352 have hmEq : m = ((σ q : M) : G) * (((σ q : M) : G)⁻¹ * m) := by

353 simp only [mul_inv_cancel_left]

354 rw [hmEq]

355 exact (Subgroup.closure _).mul_mem hσ' hdiv'

356

357

358end ProCGroups.Generation