Source: ProCGroups.Generation.QuotientGeneratorConvergingPairs

1import ProCGroups.Generation.Convergence

2import ProCGroups.Generation.GeneratorConvergingPairs

3import ProCGroups.ProC.Quotients.ClosedNormal

5/-!

6# Converging generators constructed through quotient refinements

8`QuotientGeneratorConvergingPair` records a convergent generating family in a closed-normal

9quotient together with coherent refinement maps. Chain upper bounds and strict extensions feed

10a maximality argument producing generators converging to one; the final results transport this

11property and the resulting topological rank across surjections and continuous equivalences.

12-/

14open Set

15open scoped Topology Pointwise

17namespace ProCGroups.Generation

19universe u v

21open ProCGroups.InverseSystems

22open ProCGroups.ProC

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

25 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

27section Proposition244

29/-- A quotient generator converging pair records compatible source and quotient generator data. -/

30structure QuotientGeneratorConvergingPair where

31 /-- The subgroup used to form the quotient carrying the generator family. -/

32 N : Subgroup G

33 /-- The quotienting subgroup is normal. -/

34 normal_N : N.Normal

35 /-- The quotienting subgroup is closed, so the quotient has the intended profinite topology. -/

36 closed_N : IsClosed (N : Set G)

37 /-- The distinguished generator set in `G ⧸ N`. -/

38 Y : Set (G ⧸ N)

39 /-- The quotient identity is excluded from the distinguished generator set. -/

40 subset_compl : Y ⊆ ({1} : Set (G ⧸ N))ᶜ

41 /-- The generator set converges to the quotient identity along open subgroups. -/

42 converges : ConvergesToOneAlongOpenSubgroups (G := G ⧸ N) Y

43 /-- The distinguished set topologically generates the entire quotient `G ⧸ N`. -/

44 generates : TopologicallyGenerates (G := G ⧸ N) Y

46attribute [instance] QuotientGeneratorConvergingPair.normal_N

48/-- The source set is the set of generators carried by the quotient generator pair. -/

49def QuotientGeneratorConvergingPair.sourceSet

50 (A : QuotientGeneratorConvergingPair (G := G)) :

51 Set (G ⧸ A.N) :=

52 ({1} : Set (G ⧸ A.N)) ∪ A.Y

54/--

55The source of a quotient generator-converging pair consists of the original group, index data,

56and generator family before passage to the quotient.

57-/

58abbrev QuotientGeneratorConvergingPair.Source

59 (A : QuotientGeneratorConvergingPair (G := G)) :=

60 ↥(A.sourceSet)

62/--

63The constructed object carries the topological space structure inherited from its construction.

64-/

65instance instTopologicalSpaceQuotientGeneratorConvergingPairSource

66 (A : QuotientGeneratorConvergingPair (G := G)) :

67 TopologicalSpace A.Source :=

68 inferInstanceAs (TopologicalSpace ↥(A.sourceSet))

70/-- The identity element belongs to the source data of the quotient generator pair. -/

71def QuotientGeneratorConvergingPair.sourceOne

72 (A : QuotientGeneratorConvergingPair (G := G)) : A.Source :=

73 ⟨1, Or.inl rfl⟩

75/-- The source of the selected generator is the source specified by the quotient generator pair. -/

76def QuotientGeneratorConvergingPair.sourceOfY

77 (A : QuotientGeneratorConvergingPair (G := G)) (y : A.Y) : A.Source :=

78 ⟨y.1, Or.inr y.2⟩

80omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

81/--

82Every source element of a quotient generator pair is either the distinguished identity source or

83comes from an element of the generator set.

84-/

85theorem QuotientGeneratorConvergingPair.source_cases

86 (A : QuotientGeneratorConvergingPair (G := G)) (x : A.Source) :

87 x = A.sourceOne ∨ ∃ y : A.Y, x = A.sourceOfY y := by

88 rcases x with ⟨x, hx⟩

89 rcases hx with hx1 | hxY

90 · left

91 ext

92 simpa [QuotientGeneratorConvergingPair.sourceOne] using hx1

93 · right

94 refine ⟨⟨x, hxY⟩, ?_⟩

95 ext

96 rfl

98/--

99The image of the distinguished generator set of one quotient generator pair under a chosen

100source map into another quotient.

101-/

102def QuotientGeneratorConvergingPair.yImage

103 (A B : QuotientGeneratorConvergingPair (G := G))

104 (σ : A.Source → G ⧸ B.N) : Set (G ⧸ B.N) :=

105 Set.range fun y : A.Y => σ (A.sourceOfY y)

106

107/-- This relation orders quotient generator pairs by refinement of their quotient data. -/

108def QuotientGeneratorConvergingPair.Le

109 (A B : QuotientGeneratorConvergingPair (G := G)) : Prop :=

110 ∃ hBA : B.N ≤ A.N,

111 ∃ σ : A.Source → (G ⧸ B.N),

112 Continuous σ ∧

113 (∀ x : A.Source, leftQuotientProjection (B.N) (A.N) hBA (σ x) = x.1) ∧

114 σ A.sourceOne = 1 ∧

115 (∀ y : A.Y, σ (A.sourceOfY y) ∈ B.Y) ∧

116 B.Y \ A.yImage B σ ⊆

117 {q : G ⧸ B.N | leftQuotientProjection (B.N) (A.N) hBA q = 1}

118

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

120instance instLEQuotientGeneratorConvergingPair :

121 LE (QuotientGeneratorConvergingPair (G := G)) where

122 le := QuotientGeneratorConvergingPair.Le

123

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

125instance instPreorderQuotientGeneratorConvergingPair :

126 Preorder (QuotientGeneratorConvergingPair (G := G)) where

127 le_refl A := by

128 refine ⟨le_rfl, Subtype.val, ?_, ?_, rfl, ?_, ?_⟩

129 · change Continuous (fun x : A.Source => (x : G ⧸ A.N))

130 exact continuous_subtype_val

131 · intro q

132 simp only [leftQuotientProjection_id, id_eq]

133 · intro y

134 simp only [QuotientGeneratorConvergingPair.sourceOfY, Subtype.coe_prop]

135 · simp only [QuotientGeneratorConvergingPair.yImage, QuotientGeneratorConvergingPair.sourceOfY,

136 Subtype.range_coe_subtype, setOf_mem_eq, sdiff_self, leftQuotientProjection_id, id_eq,

137 setOf_eq_eq_singleton, subset_singleton_iff, mem_empty_iff_false, IsEmpty.forall_iff,

138 implies_true]

139 le_trans A B C hAB hBC := by

140 classical

141 rcases hAB with ⟨hBA, σAB, hσABcont, hσABright, hσABone, hσABmem, hσABdiff⟩

142 rcases hBC with ⟨hCB, σBC, hσBCcont, hσBCright, hσBCone, hσBCmem, hσBCdiff⟩

143 let τ : A.Source → B.Source := fun x =>

144 ⟨σAB x, by

145 rcases A.source_cases x with h1 | ⟨y, rfl⟩

146 · rw [h1]

147 exact Or.inl hσABone

148 · exact Or.inr (hσABmem y)⟩

149 have hτcont : Continuous τ := by

150 exact hσABcont.subtype_mk <| by

151 intro x

152 rcases A.source_cases x with h1 | ⟨y, rfl⟩

153 · rw [h1]

154 exact Or.inl hσABone

155 · exact Or.inr (hσABmem y)

156 have hτone : τ A.sourceOne = B.sourceOne := by

157 apply Subtype.ext

158 exact hσABone

159 have hτofY (y : A.Y) :

160 τ (A.sourceOfY y) = B.sourceOfY ⟨σAB (A.sourceOfY y), hσABmem y⟩ := by

161 apply Subtype.ext

162 rfl

163 have hEqBC :

164 ∀ (y : B.Y) {q : G ⧸ C.N},

165 q ∈ C.Y →

166 leftQuotientProjection (C.N) (B.N) hCB q = y.1 →

167 q = σBC (B.sourceOfY y) := by

168 intro y q hqY hqproj

169 by_cases hqim : q ∈ B.yImage C σBC

170 · rcases hqim with ⟨y', hy'Eq⟩

171 have hproj' :

172 leftQuotientProjection (C.N) (B.N) hCB q = y'.1 := by

173 calc

174 leftQuotientProjection (C.N) (B.N) hCB q =

175 leftQuotientProjection (C.N) (B.N) hCB

176 (σBC (B.sourceOfY y')) := congrArg

177 (leftQuotientProjection (C.N) (B.N) hCB) hy'Eq.symm

178 _ = y'.1 := by

179 exact hσBCright (B.sourceOfY y')

180 have hyEq : y' = y := by

181 apply Subtype.ext

182 exact hproj'.symm.trans hqproj

183 simpa [hyEq] using hy'Eq.symm

184 · have hker :

185 leftQuotientProjection (C.N) (B.N) hCB q = 1 := hσBCdiff ⟨hqY, hqim⟩

186 have hyne : y.1 ≠ 1 := by

187 simpa using B.subset_compl y.2

188 exact False.elim (hyne (hqproj.symm.trans hker))

189 refine ⟨hCB.trans hBA, fun x => σBC (τ x), hσBCcont.comp hτcont, ?_, ?_, ?_, ?_⟩

190 · intro x

191 calc

192 leftQuotientProjection (C.N) (A.N) (hCB.trans hBA) (σBC (τ x)) =

193 leftQuotientProjection (B.N) (A.N) hBA

194 (leftQuotientProjection (C.N) (B.N) hCB (σBC (τ x))) := by

195 exact leftQuotientProjection_comp_apply_symm

196 (K := (C.N : Subgroup G)) (H := (B.N : Subgroup G))

197 (L := (A.N : Subgroup G)) hCB hBA (σBC (τ x))

198 _ = leftQuotientProjection (B.N) (A.N) hBA ((τ x).1) := by

199 rw [hσBCright (τ x)]

200 _ = leftQuotientProjection (B.N) (A.N) hBA (σAB x) := by

201 rfl

202 _ = x.1 := hσABright x

203 · simpa [hτone] using hσBCone

204 · intro y

205 let yB : B.Y := ⟨σAB (A.sourceOfY y), hσABmem y⟩

206 simpa [hτofY, yB] using hσBCmem yB

207 · intro q hq

208 rcases hq with ⟨hqY, hqnotAC⟩

209 by_cases hqimB : q ∈ B.yImage C σBC

210 · rcases hqimB with ⟨z, hzEq⟩

211 have hzNotInA : z.1 ∉ A.yImage B σAB := by

212 intro hzInA

213 rcases hzInA with ⟨y, hyEq⟩

214 let yB : B.Y := ⟨σAB (A.sourceOfY y), hσABmem y⟩

215 have hprojqz :

216 leftQuotientProjection (C.N) (B.N) hCB q = z.1 := by

217 calc

218 leftQuotientProjection (C.N) (B.N) hCB q =

219 leftQuotientProjection (C.N) (B.N) hCB

220 (σBC (B.sourceOfY z)) := congrArg

221 (leftQuotientProjection (C.N) (B.N) hCB) hzEq.symm

222 _ = z.1 := by

223 exact hσBCright (B.sourceOfY z)

224 have hprojq :

225 leftQuotientProjection (C.N) (B.N) hCB q = yB.1 := by

226 calc

227 leftQuotientProjection (C.N) (B.N) hCB q = z.1 := hprojqz

228 _ = yB.1 := by

229 simpa [yB] using hyEq.symm

230 have hqEq : q = σBC (B.sourceOfY yB) := hEqBC yB hqY hprojq

231 have hqInAC : q ∈ A.yImage C (fun x => σBC (τ x)) := by

232 refine ⟨y, ?_⟩

233 simpa [hτofY] using hqEq.symm

234 exact hqnotAC hqInAC

235 have hzProjA :

236 leftQuotientProjection (B.N) (A.N) hBA z.1 = 1 :=

237 hσABdiff ⟨z.2, hzNotInA⟩

238 have hprojqB :

239 leftQuotientProjection (C.N) (B.N) hCB q = z.1 := by

240 calc

241 leftQuotientProjection (C.N) (B.N) hCB q =

242 leftQuotientProjection (C.N) (B.N) hCB

243 (σBC (B.sourceOfY z)) := congrArg

244 (leftQuotientProjection (C.N) (B.N) hCB) hzEq.symm

245 _ = z.1 := by

246 exact hσBCright (B.sourceOfY z)

247 calc

248 leftQuotientProjection (C.N) (A.N) (hCB.trans hBA) q =

249 leftQuotientProjection (B.N) (A.N) hBA

250 (leftQuotientProjection (C.N) (B.N) hCB q) := by

251 exact leftQuotientProjection_comp_apply_symm

252 (K := (C.N : Subgroup G)) (H := (B.N : Subgroup G))

253 (L := (A.N : Subgroup G)) hCB hBA q

254 _ = leftQuotientProjection (B.N) (A.N) hBA z.1 := by

255 rw [hprojqB]

256 _ = 1 := hzProjA

257 · have hprojqB :

258 leftQuotientProjection (C.N) (B.N) hCB q = 1 := hσBCdiff ⟨hqY, hqimB⟩

259 calc

260 leftQuotientProjection (C.N) (A.N) (hCB.trans hBA) q =

261 leftQuotientProjection (B.N) (A.N) hBA

262 (leftQuotientProjection (C.N) (B.N) hCB q) := by

263 exact leftQuotientProjection_comp_apply_symm

264 (K := (C.N : Subgroup G)) (H := (B.N : Subgroup G))

265 (L := (A.N : Subgroup G)) hCB hBA q

266 _ = leftQuotientProjection (B.N) (A.N) hBA 1 := by

267 rw [hprojqB]

268 _ = 1 := by

269 rfl

270

271noncomputable section

272

273omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

274/--

275The refinement relation includes the required compatibility between the source and target

276quotient data.

277-/

278theorem QuotientGeneratorConvergingPair.le_hBA

279 {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :

280 B.N ≤ A.N :=

281 Classical.choose hAB

282

283end

284

285/-- The refinement relation provides the induced map between quotient generator pairs. -/

286noncomputable def QuotientGeneratorConvergingPair.le_map

287 {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :

288 A.Source → G ⧸ B.N :=

289 Classical.choose (Classical.choose_spec hAB)

290

291omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

292/--

293For a refinement of quotient generator pairs, the chosen lift map between source sets is

294continuous.

295-/

296theorem QuotientGeneratorConvergingPair.le_map_continuous

297 {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :

298 Continuous (A.le_map hAB) :=

299 (Classical.choose_spec (Classical.choose_spec hAB)).1

300

301omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

302/-- The quotient generator pair is compatible with the specified quotient map. -/

303@[simp] theorem QuotientGeneratorConvergingPair.le_map_right

304 {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B)

305 (x : A.Source) :

306 leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) (A.le_map hAB x) = x.1 :=

307 (Classical.choose_spec (Classical.choose_spec hAB)).2.1 x

308

309omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

310/-- A refinement map sends the distinguished source element over `1` to the identity. -/

311@[simp] theorem QuotientGeneratorConvergingPair.le_map_one

312 {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :

313 A.le_map hAB A.sourceOne = 1 :=

314 (Classical.choose_spec (Classical.choose_spec hAB)).2.2.1

315

316omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

317/--

318Under a refinement, the chosen lift map sends every distinguished generator of the smaller pair

319into the distinguished set of the larger pair.

320-/

321@[simp] theorem QuotientGeneratorConvergingPair.le_map_mem

322 {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B)

323 (y : A.Y) :

324 A.le_map hAB (A.sourceOfY y) ∈ B.Y :=

325 (Classical.choose_spec (Classical.choose_spec hAB)).2.2.2.1 y

326

327omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

328/--

329Elements of the larger distinguished set not in the lifted image project to the identity in the

330smaller quotient.

331-/

332theorem QuotientGeneratorConvergingPair.le_map_diff

333 {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :

334 B.Y \ A.yImage B (A.le_map hAB) ⊆

335 {q : G ⧸ B.N |

336 leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) q = 1} :=

337 (Classical.choose_spec (Classical.choose_spec hAB)).2.2.2.2

338

339omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

340/-- The quotient generator comparison respects membership and projection equality. -/

341theorem QuotientGeneratorConvergingPair.eq_le_map_of_mem_of_proj_eq

342 {A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B)

343 (y : A.Y) {q : G ⧸ B.N}

344 (hqY : q ∈ B.Y)

345 (hqproj : leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) q = y.1) :

346 q = A.le_map hAB (A.sourceOfY y) := by

347 by_cases hqim : q ∈ A.yImage B (A.le_map hAB)

348 · rcases hqim with ⟨y', hy'Eq⟩

349 have hproj' :

350 leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) q = y'.1 := by

351 calc

352 leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) q =

353 leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB)

354 (A.le_map hAB (A.sourceOfY y')) := congrArg

355 (leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB))

356 hy'Eq.symm

357 _ = y'.1 := by

358 exact A.le_map_right hAB (A.sourceOfY y')

359 have hyEq : y' = y := by

360 ext

361 exact hproj'.symm.trans hqproj

362 simpa [hyEq] using hy'Eq.symm

363 · have hker :

364 leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) q = 1 :=

365 A.le_map_diff hAB ⟨hqY, hqim⟩

366 have hyne : y.1 ≠ 1 := by

367 simpa using A.subset_compl y.2

368 exact False.elim (hyne (hqproj.symm.trans hker))

369

370omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

371/-- The induced map between quotient generator pairs is compatible with refinement. -/

372theorem QuotientGeneratorConvergingPair.le_map_compat

373 {A B C : QuotientGeneratorConvergingPair (G := G)}

374 (hAB : A ≤ B) (hAC : A ≤ C) (hBC : B ≤ C)

375 (y : A.Y) :

376 leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)

377 (A.le_map hAC (A.sourceOfY y)) =

378 A.le_map hAB (A.sourceOfY y) := by

379 have hCy :

380 A.le_map hAC (A.sourceOfY y) ∈ C.Y := A.le_map_mem hAC y

381 have hIn :

382 A.le_map hAC (A.sourceOfY y) ∈ B.yImage C (B.le_map hBC) := by

383 by_contra hNot

384 have hker :

385 leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)

386 (A.le_map hAC (A.sourceOfY y)) = 1 :=

387 B.le_map_diff hBC ⟨hCy, hNot⟩

388 have hy1 : y.1 = 1 := by

389 calc

390 y.1 = leftQuotientProjection (C.N) (A.N) (A.le_hBA hAC)

391 (A.le_map hAC (A.sourceOfY y)) := by

392 exact (A.le_map_right hAC (A.sourceOfY y)).symm

393 _ = leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB)

394 (leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)

395 (A.le_map hAC (A.sourceOfY y))) := by

396 exact

397 (leftQuotientProjection_comp_apply_symm

398 (K := (C.N : Subgroup G)) (H := (B.N : Subgroup G))

399 (L := (A.N : Subgroup G)) (B.le_hBA hBC) (A.le_hBA hAB)

400 (A.le_map hAC (A.sourceOfY y)))

401 _ = leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) 1 := by rw [hker]

402 _ = 1 := by rfl

403 have hyne : y.1 ≠ 1 := by

404 simpa using A.subset_compl y.2

405 exact hyne hy1

406 rcases hIn with ⟨z, hzEq⟩

407 have hqY :

408 leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)

409 (A.le_map hAC (A.sourceOfY y)) ∈ B.Y := by

410 have hEq :

411 leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)

412 (A.le_map hAC (A.sourceOfY y)) = z.1 := by

413 calc

414 leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)

415 (A.le_map hAC (A.sourceOfY y)) =

416 leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)

417 (B.le_map hBC (B.sourceOfY z)) := congrArg

418 (leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC))

419 hzEq.symm

420 _ = z.1 := by

421 exact B.le_map_right hBC (B.sourceOfY z)

422 exact hEq ▸ z.2

423 have hqproj :

424 leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB)

425 (leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)

426 (A.le_map hAC (A.sourceOfY y))) = y.1 := by

427 exact (leftQuotientProjection_comp_apply

428 (K := (C.N : Subgroup G)) (H := (B.N : Subgroup G))

429 (L := (A.N : Subgroup G)) (B.le_hBA hBC) (A.le_hBA hAB)

430 (A.le_map hAC (A.sourceOfY y))).trans

431 (A.le_map_right hAC (A.sourceOfY y))

432 exact A.eq_le_map_of_mem_of_proj_eq hAB y hqY hqproj

433

434omit [T2Space G] in

435/-- The range subtype of a pointed map contains the chosen basepoint. -/

436theorem ConvergesToOneAlongOpenSubgroups.range_subtype_pointed

437 {H : Type v} [Group H] [TopologicalSpace H]

438 {X : Set G}

439 {f : ↥((({1} : Set G) ∪ X)) → H}

440 (hf : Continuous f)

441 (hf1 : f ⟨1, Or.inl rfl⟩ = 1)

442 (hX : ConvergesToOneAlongOpenSubgroups (G := G) X) :

443 ConvergesToOneAlongOpenSubgroups (G := H)

444 (Set.range fun x : X => f ⟨x.1, Or.inr x.2⟩) := by

445 let S : Set G := ({1} : Set G) ∪ X

446 let g : X → H := fun x => f ⟨x.1, Or.inr x.2⟩

447 intro U

448 have hpre : IsOpen (f ⁻¹' (U : Set H)) :=

449 (openSubgroup_isOpen (G := H) U).preimage hf

450 have h1pre : (⟨1, Or.inl rfl⟩ : ↥S) ∈ f ⁻¹' (U : Set H) := by

451 change f ⟨1, Or.inl rfl⟩ ∈ U

452 rw [hf1]

453 exact U.one_mem'

454 rcases isOpen_induced_iff.mp hpre with ⟨W, hWopen, hWeq⟩

455 have h1W : (1 : G) ∈ W := by

456 have : (⟨1, Or.inl rfl⟩ : ↥S) ∈ Subtype.val ⁻¹' W := by

457 exact hWeq.symm ▸ h1pre

458 simpa using this

459 rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hWopen h1W with ⟨V, hVW⟩

460 have hsubset :

461 Set.range g \ (U : Set H) ⊆ g '' {x : X | (x : G) ∉ (V : Set G)} := by

462 intro y hy

463 rcases hy with ⟨hyY, hyU⟩

464 rcases hyY with ⟨x, rfl⟩

465 refine ⟨x, ?_, rfl⟩

466 intro hxV

467 have hxW : (x : G) ∈ W := hVW hxV

468 have hxpre : (⟨x.1, Or.inr x.2⟩ : ↥S) ∈ Subtype.val ⁻¹' W := by

469 change (x : G) ∈ W

470 exact hxW

471 have hxpreU : (⟨x.1, Or.inr x.2⟩ : ↥S) ∈ f ⁻¹' (U : Set H) := by

472 exact hWeq ▸ hxpre

473 have : g x ∈ (U : Set H) := by

474 change f ⟨x.1, Or.inr x.2⟩ ∈ U

475 exact hxpreU

476 exact hyU this

477 have hfinite_pre : {x : X | (x : G) ∉ (V : Set G)}.Finite := by

478 let e : X ↪ G := ⟨Subtype.val, Subtype.val_injective⟩

479 have hfinite : (X \ (V : Set G)).Finite := hX V.toOpenSubgroup

480 have hfinite' : {x : X | e x ∈ X ∧ e x ∉ (V : Set G)}.Finite := by

481 simpa [Set.preimage] using hfinite.preimage_embedding e

482 have hEq : {x : X | e x ∈ X ∧ e x ∉ (V : Set G)} = {x : X | (x : G) ∉ (V : Set G)} := by

483 ext x

484 simp only [Function.Embedding.coeFn_mk, Subtype.coe_prop, SetLike.mem_coe, true_and,

485 mem_setOf_eq, e]

486 exact hEq ▸ hfinite'

487 exact hfinite_pre.image g |>.subset hsubset

488

489omit [T2Space G] [TotallyDisconnectedSpace G] in

490/--

491The quotient generator-converging-pair construction is compatible with open-normal finite

492quotients and refinement maps.

493-/

494theorem exists_quotientPair_le_openSubgroup_of_chain_iInf_le

495 {c : Set (QuotientGeneratorConvergingPair (G := G))}

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

497 (U : OpenSubgroup G)

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

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

500 classical

501 have hInter :

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

503 intro x hx

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

505 rcases finite_iInter_subgroup_subset_openSubgroup (G := G)

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

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

508 U hInter with ⟨s, hs⟩

509 by_cases hsne : s.Nonempty

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

511 intro a ha b hb hne

512 have hne' : (a : QuotientGeneratorConvergingPair (G := G)) ≠ b := by

513 intro h

514 exact hne (Subtype.ext h)

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

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

517 ⟨m, hm, hmax⟩

518 refine ⟨m, ?_⟩

519 intro x hx

520 have hx' :

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

522 refine mem_iInter₂.2 ?_

523 intro p hp

524 exact (QuotientGeneratorConvergingPair.le_hBA (hmax p hp)) hx

525 exact hs hx'

526 · rcases hcne with ⟨p, hp⟩

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

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

529 have :

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

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

532 intro x hx

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

534

535omit [T2Space G] [TotallyDisconnectedSpace G] in

536/--

537A chain of quotient generator pairs has a refinement lifting to the intersection of its kernels.

538-/

539theorem quotientGeneratorPair_exists_liftToInf

540 {c : Set (QuotientGeneratorConvergingPair (G := G))}

541 (hc : IsChain (· ≤ ·) c) (a : c) :

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

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

544 ∃ σ : a.1.Source → G ⧸ K,

545 Continuous σ ∧

546 (∀ b : c, ∀ hab : a.1 ≤ b.1,

547 leftQuotientProjection K b.1.N

548 (iInf_le (fun p : c => p.1.N) b) ∘ σ =

549 a.1.le_map hab) ∧

550 σ a.1.sourceOne = 1 := by

551 classical

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

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

554 let Tail := {b : c // a.1 ≤ b.1}

555 letI : Nonempty Tail := ⟨⟨a, le_rfl⟩⟩

556 let L : Tail → ClosedSubgroup G := fun b =>

557 ⟨b.1.1.N, b.1.1.closed_N⟩

558 have hL : ∀ {i j : Tail}, i ≤ j → (L j : Subgroup G) ≤ (L i : Subgroup G) := by

559 intro i j hij

560 exact QuotientGeneratorConvergingPair.le_hBA hij

561 have hdir : Directed (· ≤ ·) (id : Tail → Tail) := by

562 intro i j

563 by_cases hij : i ≤ j

564 · exact ⟨j, hij, le_rfl⟩

565 · have hji : j ≤ i := by

566 by_cases hEq : i = j

567 · exact hEq ▸ le_rfl

568 · rcases hc i.1.2 j.1.2 (by

569 intro h

570 exact hEq (Subtype.ext (Subtype.ext h))) with hij' | hji'

571 · exact False.elim (hij hij')

572 · exact hji'

573 exact ⟨i, le_rfl, hji⟩

574 let η : ∀ b : Tail, a.1.Source → G ⧸ (L b : Subgroup G) := fun b =>

575 a.1.le_map b.2

576 have hηcont : ∀ b : Tail, Continuous (η b) := by

577 intro b

578 exact a.1.le_map_continuous b.2

579 have hηcompat : ∀ {i j : Tail} (hij : i ≤ j),

580 leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij) ∘ η j = η i := by

581 intro i j hij

582 funext x

583 rcases a.1.source_cases x with rfl | ⟨y, rfl⟩

584 · have h1j : η j a.1.sourceOne = 1 := by

585 change a.1.le_map j.2 a.1.sourceOne = 1

586 exact a.1.le_map_one j.2

587 have h1i : η i a.1.sourceOne = 1 := by

588 change a.1.le_map i.2 a.1.sourceOne = 1

589 exact a.1.le_map_one i.2

590 calc

591 (leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij) ∘ η j)

592 a.1.sourceOne

593 = leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij)

594 (η j a.1.sourceOne) := by

595 simp only [Function.comp]

596 _ = leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij) 1 := by

597 rw [h1j]

598 _ = 1 := by rfl

599 _ = η i a.1.sourceOne := by rw [h1i]

600 · simpa [η] using a.1.le_map_compat i.2 j.2 hij y

601 have hηone : ∀ b : Tail, η b a.1.sourceOne = 1 := by

602 intro b

603 change a.1.le_map b.2 a.1.sourceOne = 1

604 exact a.1.le_map_one b.2

605 obtain ⟨ηinf, hηinf_continuous, hηinf_fac, hηinf_one⟩ :=

606 exists_continuous_leftQuotient_lift_of_directed

607 (G := G) L hL hdir η hηcont hηcompat a.1.sourceOne hηone

608 let H : Subgroup G := ((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G)

609 have hKeq : H = K := by

610 apply le_antisymm

611 · refine le_iInf ?_

612 intro p

613 by_cases hap : a.1 ≤ p.1

614 · exact iInf_le (fun b : Tail => (L b : Subgroup G)) ⟨p, hap⟩

615 · have hKa :

616 H ≤ a.1.N :=

617 iInf_le (fun b : Tail => (L b : Subgroup G)) ⟨a, le_rfl⟩

618 by_cases hEq : p = a

619 · simpa [K, hEq] using hKa

620 · rcases hc p.2 a.2 (by

621 intro h

622 exact hEq (Subtype.ext h)) with hpa | hap'

623 · exact hKa.trans (QuotientGeneratorConvergingPair.le_hBA hpa)

624 · exact False.elim (hap hap')

625 · refine le_iInf ?_

626 intro b

627 exact iInf_le (fun p : c => p.1.N) b.1

628 letI : H.Normal := by

629 exact Subgroup.normal_iInf_normal fun b : Tail => b.1.1.normal_N

630 have hGoal :

631 ∃ σ : a.1.Source → G ⧸ H,

632 Continuous σ ∧

633 (∀ b : c, ∀ hab : a.1 ≤ b.1,

634 leftQuotientProjection H b.1.N

635 (closedSubgroup_sInf_le (L := L) ⟨b, hab⟩) ∘ σ =

636 a.1.le_map hab) ∧

637 σ a.1.sourceOne = 1 := by

638 refine ⟨ηinf, hηinf_continuous, ?_, hηinf_one⟩

639 intro b hab

640 simpa [Tail, L, η] using hηinf_fac ⟨b, hab⟩

641 have hGoal' :

642 ∃ σ : a.1.Source → G ⧸ H,

643 Continuous σ ∧

644 (∀ b : c, ∀ hab : a.1 ≤ b.1,

645 leftQuotientProjection H b.1.N

646 (hKeq.trans_le (iInf_le (fun p : c => p.1.N) b)) ∘ σ =

647 a.1.le_map hab) ∧

648 σ a.1.sourceOne = 1 := by

649 rcases hGoal with ⟨σ, hσcont, hσfac, hσone⟩

650 refine ⟨σ, hσcont, ?_, hσone⟩

651 intro b hab

652 simpa using hσfac b hab

653 change

654 ∃ σ : a.1.Source → G ⧸ K,

655 Continuous σ ∧

656 (∀ b : c, ∀ hab : a.1 ≤ b.1,

657 leftQuotientProjection K b.1.N

658 (iInf_le (fun p : c => p.1.N) b) ∘ σ =

659 a.1.le_map hab) ∧

660 σ a.1.sourceOne = 1

661 let Data : Type _ := { J : Subgroup G // J.Normal ∧ ∀ b : c, J ≤ b.1.N }

662 let P : Data → Prop := fun d =>

663 letI : d.1.Normal := d.2.1

664 ∃ σ : a.1.Source → G ⧸ d.1,

665 Continuous σ ∧

666 (∀ b : c, ∀ hab : a.1 ≤ b.1,

667 leftQuotientProjection d.1 b.1.N (d.2.2 b) ∘ σ =

668 a.1.le_map hab) ∧

669 σ a.1.sourceOne = 1

670 let dH : Data :=

671 ⟨H, ⟨inferInstance, fun b => hKeq.trans_le (iInf_le (fun p : c => p.1.N) b)⟩⟩

672 let dK : Data :=

673 ⟨K, ⟨inferInstance, fun b => iInf_le (fun p : c => p.1.N) b⟩⟩

674 have hd : dH = dK := by

675 apply Subtype.ext

676 exact hKeq

677 have hPdH : P dH := by

678 simpa [P, dH] using hGoal'

679 have hPdK : P dK := by

680 exact Eq.mp (congrArg P hd) hPdH

681 simpa [P, dK] using hPdK

682

683/-- The top quotient generator pair is the maximal object in the quotient-generator construction. -/

684noncomputable def quotientGeneratorPairTop :

685 QuotientGeneratorConvergingPair (G := G) where

686 N := ⊤

687 normal_N := by infer_instance

688 closed_N := isClosed_univ

689 Y := ∅

690 subset_compl := by intro q hq; simp only [mem_empty_iff_false] at hq

691 converges := by intro U; simp only [empty_sdiff, finite_empty]

692 generates := by

693 classical

694 rw [TopologicallyGenerates]

695 apply top_unique

696 intro q hq

697 rcases Quotient.exists_rep q with ⟨g, rfl⟩

698 have hg1 : QuotientGroup.mk' (⊤ : Subgroup G) g = (1 : G ⧸ (⊤ : Subgroup G)) := by

699 exact (QuotientGroup.eq_one_iff (N := (⊤ : Subgroup G)) g).2 (by simp only [Subgroup.mem_top])

700 have hbot :

701 QuotientGroup.mk' (⊤ : Subgroup G) g ∈ (⊥ : Subgroup (G ⧸ (⊤ : Subgroup G))) := by

702 change QuotientGroup.mk' (⊤ : Subgroup G) g = (1 : G ⧸ (⊤ : Subgroup G))

703 exact hg1

704 simpa [Subgroup.closure_eq] using

705 (Subgroup.le_topologicalClosure (⊥ : Subgroup (G ⧸ (⊤ : Subgroup G))) hbot)

706

707/-- A nonmaximal quotient generator pair admits a strict extension refining its quotient data. -/

708theorem quotientGeneratorPair_exists_strictExtension

709 (p : QuotientGeneratorConvergingPair (G := G))

710 (hne : p.N ≠ ⊥) :

711 ∃ p' : QuotientGeneratorConvergingPair (G := G), p ≤ p' ∧ ¬ p' ≤ p := by

712 classical

713 rcases (Subgroup.ne_bot_iff_exists_ne_one).1 hne with ⟨m, hmne⟩

714 have hmne' : (m : G) ≠ 1 := by

715 intro hm1

716 apply hmne

717 ext

718 simpa using hm1

719 rcases exists_openNormalSubgroup_not_mem (G := G) hmne' with ⟨U, hmU⟩

720 let N' : Subgroup G := (U : Subgroup G) ⊓ p.N

721 have hN'closed : IsClosed (N' : Set G) := by

722 exact (openNormalSubgroup_isClosed (G := G) U).inter p.closed_N

723 have hN'proper : ¬ p.N ≤ N' := by

724 intro hp

725 exact hmU (hp m.2).1

726 obtain ⟨σ, hσcont, hσright, hσone⟩ :=

727 leftQuotientProjection_hasContinuousSection

728 (G := G)

729 ⟨N', hN'closed⟩

730 ⟨p.N, p.closed_N⟩

731 inf_le_right

732 rcases exists_finite_subset_generating_subgroup_mod_openNormal (G := G)

733 (M := p.N) (hMclosed := p.closed_N) U with ⟨T, hTfin, hTsub, hTgen⟩

734 let Tbar : Set (G ⧸ N') := (QuotientGroup.mk' N') '' T

735 let Y' : Set (G ⧸ N') := σ '' p.Y ∪ Tbar

736 have hY'compl : Y' ⊆ ({1} : Set (G ⧸ N'))ᶜ := by

737 intro q hq

738 rcases hq with hq | hq

739 · rcases hq with ⟨y, hy, rfl⟩

740 intro hq1

741 have hσy1 : σ y = 1 := by

742 simpa using hq1

743 have : y = 1 := by

744 calc

745 y = leftQuotientProjection (N') (p.N) inf_le_right (σ y) := (hσright y).symm

746 _ = leftQuotientProjection (N') (p.N) inf_le_right 1 := by rw [hσy1]

747 _ = 1 := rfl

748 exact p.subset_compl hy this

749 · rcases hq with ⟨t, ht, rfl⟩

750 intro hq1

751 have htN' : t ∈ N' := (QuotientGroup.eq_one_iff (N := N') t).1 hq1

752 exact (hTsub ht).2 htN'

753 have hY'conv : ConvergesToOneAlongOpenSubgroups (G := G ⧸ N') Y' := by

754 letI : IsClosed (p.N : Set G) := p.closed_N

755 letI : TotallyDisconnectedSpace (G ⧸ p.N) :=

756 ProCGroups.totallyDisconnectedSpace_quotient_closedNormal p.N p.closed_N

757 intro V

758 have hσconv :

759 ((σ '' p.Y) \ (V : Set (G ⧸ N'))).Finite := by

760 exact

761 (ConvergesToOneAlongOpenSubgroups.image_of_continuous_pointed

762 (G := G ⧸ p.N) (H := G ⧸ N')

763 hσcont hσone p.converges) V

764 have hTconv : (Tbar \ (V : Set (G ⧸ N'))).Finite :=

765 (hTfin.image (QuotientGroup.mk' N')).subset (by

766 intro q hq

767 exact hq.1)

768 exact (hσconv.union hTconv).subset (by

769 intro q hq

770 rcases hq with ⟨hqY, hqV⟩

771 rcases hqY with hqσ | hqT

772 · exact Or.inl ⟨hqσ, hqV⟩

773 · exact Or.inr ⟨hqT, hqV⟩)

774 have hY'gen :

775 TopologicallyGenerates (G := G ⧸ N') Y' := by

776 exact topologicallyGenerates_of_quotient_section_union_kernel

777 (G := G) p.closed_N hN'closed inf_le_right

778 p.generates hσright hTgen

779 refine ⟨{ N := N'

780 normal_N := by infer_instance

781 closed_N := hN'closed

782 Y := Y'

783 subset_compl := hY'compl

784 converges := hY'conv

785 generates := hY'gen }, ?_, ?_⟩

786 · let σ' : p.Source → G ⧸ N' := fun x => σ x.1

787 refine ⟨inf_le_right, σ', ?_, ?_, ?_, ?_, ?_⟩

788 · change Continuous (fun x : p.Source => σ x.1)

789 exact hσcont.comp continuous_subtype_val

790 · intro x

791 exact hσright x.1

792 · exact hσone

793 · intro q

794 exact Or.inl ⟨q.1, q.2, rfl⟩

795 · intro q hq

796 rcases hq with ⟨hqY', hqnotσ⟩

797 rcases hqY' with hqσ | hqT

798 · rcases hqσ with ⟨y, hy, rfl⟩

799 exact False.elim (hqnotσ ⟨⟨y, hy⟩, rfl⟩)

800 · rcases hqT with ⟨t, ht, rfl⟩

801 have htN : t ∈ p.N := (hTsub ht).1

802 simpa [leftQuotientProjection_mk] using

803 (QuotientGroup.eq_one_iff (N := p.N) t).2 htN

804 · intro hp'

805 exact hN'proper hp'.1

806

807/-- The closed-normal quotient section at the bottom subgroup is the identity section. -/

808theorem closedNormalQuotientSection_bot_eq

809 (hbotClosed : IsClosed (((⊥ : Subgroup G) : Set G))) :

810 closedNormalQuotientSection (G := G)

811 (N := (⊥ : Subgroup G)) hbotClosed =

812 (quotientBotContinuousMulEquiv (G := G)).symm := by

813 funext q

814 apply (quotientBotContinuousMulEquiv (G := G)).injective

815 have h1 :

816 quotientBotContinuousMulEquiv (G := G)

817 (closedNormalQuotientSection (G := G)

818 (N := (⊥ : Subgroup G)) hbotClosed q) = q := by

819 simpa [quotientBotContinuousMulEquiv] using

820 (closedNormalQuotientSection_rightInverse (G := G)

821 (N := (⊥ : Subgroup G)) hbotClosed q)

822 have h2 :

823 quotientBotContinuousMulEquiv (G := G)

824 ((quotientBotContinuousMulEquiv (G := G)).symm q) = q := by

825 simp only [ContinuousMulEquiv.apply_symm_apply]

826 exact h1.trans h2.symm

827

828/-- The quotient generator pair maps its source set into the ambient generating set. -/

829noncomputable def QuotientGeneratorConvergingPair.toAmbientSet

830 (p : QuotientGeneratorConvergingPair (G := G)) : Set G :=

831 closedNormalQuotientSection (G := G) (N := p.N) p.closed_N '' p.Y

832

833/--

834The ambient representatives attached to a quotient generator pair topologically generate and

835converge to one.

836-/

837theorem QuotientGeneratorConvergingPair.toAmbientSet_generatesAndConvergesToOneAlongOpenSubgroups

838 (p : QuotientGeneratorConvergingPair (G := G))

839 (hbot : p.N = ⊥) :

840 GeneratesAndConvergesToOneAlongOpenSubgroups (G := G) p.toAmbientSet := by

841 rcases p with ⟨N, hNnormal, hNclosed, Y, hYcompl, hYconv, hYgen⟩

842 cases hbot

843 have hbotClosed : IsClosed (((⊥ : Subgroup G) : Set G)) :=

844 (isClosed_singleton : IsClosed ({(1 : G)} : Set G))

845 constructor

846 · let e : (G ⧸ (⊥ : Subgroup G)) ≃ₜ* G := (quotientBotContinuousMulEquiv (G := G)).symm

847 have hgen :

848 TopologicallyGenerates (G := G)

849 (e '' Y) := topologicallyGenerates_continuousMulEquiv_image

850 (G := G ⧸ (⊥ : Subgroup G)) e hYgen

851 rw [QuotientGeneratorConvergingPair.toAmbientSet,

852 closedNormalQuotientSection_bot_eq (G := G) hbotClosed]

853 simpa using hgen

854 · letI : IsClosed (((⊥ : Subgroup G) : Set G)) := hbotClosed

855 letI : TotallyDisconnectedSpace (G ⧸ (⊥ : Subgroup G)) :=

856 ProCGroups.totallyDisconnectedSpace_quotient_closedNormal

857 (⊥ : Subgroup G) hbotClosed

858 have hconv :

859 ConvergesToOneAlongOpenSubgroups (G := G)

860 ((closedNormalQuotientSection (G := G)

861 (N := (⊥ : Subgroup G)) hbotClosed) '' Y) := by

862 exact ConvergesToOneAlongOpenSubgroups.image_of_continuous_pointed

863 (G := G ⧸ (⊥ : Subgroup G)) (H := G)

864 (closedNormalQuotientSection_continuous (G := G)

865 (N := (⊥ : Subgroup G)) hbotClosed)

866 (closedNormalQuotientSection_one (G := G)

867 (N := (⊥ : Subgroup G)) hbotClosed)

868 hYconv

869 rw [QuotientGeneratorConvergingPair.toAmbientSet]

870 exact hconv

871

872end Proposition244

873section Generators

874

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

876 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

877

878

879/-- Every nonempty chain of quotient generator pairs has an upper bound. -/

880theorem quotientGeneratorPair_exists_upperBound_of_chain

881 (c : Set (QuotientGeneratorConvergingPair (G := G)))

882 (hc : IsChain (· ≤ ·) c) (hcn : c.Nonempty) :

883 ∃ ub : QuotientGeneratorConvergingPair (G := G), ∀ a ∈ c, a ≤ ub := by

884 classical

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

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

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

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

889 letI : IsClosed (K : Set G) := hKclosed

890 letI : TotallyDisconnectedSpace (G ⧸ K) :=

891 ProCGroups.totallyDisconnectedSpace_quotient_closedNormal K hKclosed

892 let lift : (a : c) → a.1.Source → G ⧸ K := fun a =>

893 Classical.choose (quotientGeneratorPair_exists_liftToInf (G := G) hc a)

894 have hlift_continuous : ∀ a : c, Continuous (lift a) := by

895 intro a

896 exact (Classical.choose_spec

897 (quotientGeneratorPair_exists_liftToInf (G := G) hc a)).1

898 have hlift_fac :

899 ∀ (a b : c) (hab : a.1 ≤ b.1),

900 leftQuotientProjection K b.1.N

901 (iInf_le (fun p : c => p.1.N) b) ∘ lift a =

902 a.1.le_map hab := by

903 intro a b hab

904 exact (Classical.choose_spec

905 (quotientGeneratorPair_exists_liftToInf (G := G) hc a)).2.1 b hab

906 have hlift_one : ∀ a : c, lift a a.1.sourceOne = 1 := by

907 intro a

908 exact (Classical.choose_spec

909 (quotientGeneratorPair_exists_liftToInf (G := G) hc a)).2.2

910 have exists_stage_above_le_open :

911 ∀ (a : c) {U : OpenSubgroup G}, K ≤ (U : Subgroup G) →

912 ∃ b : c, a.1 ≤ b.1 ∧ b.1.N ≤ (U : Subgroup G) := by

913 intro a U hKU

914 let d : Set (QuotientGeneratorConvergingPair (G := G)) :=

915 {p | p ∈ c ∧ a.1 ≤ p}

916 have hdchain : IsChain (· ≤ ·) d := by

917 intro x hx y hy hxy

918 exact hc hx.1 hy.1 hxy

919 have hdne : d.Nonempty := ⟨a.1, a.2, le_rfl⟩

920 have hdEq : iInf (fun p : d => p.1.N) = K := by

921 apply le_antisymm

922 · refine le_iInf ?_

923 intro p

924 by_cases hap : a.1 ≤ p.1

925 · exact iInf_le (fun q : d => q.1.N) ⟨p.1, p.2, hap⟩

926 · have hda :

927 iInf (fun q : d => q.1.N) ≤ a.1.N :=

928 iInf_le (fun q : d => q.1.N) ⟨a.1, a.2, le_rfl⟩

929 by_cases hEq : p.1 = a.1

930 · simpa [hEq] using hda

931 · rcases hc p.2 a.2 hEq with hpa | hap'

932 · exact hda.trans (QuotientGeneratorConvergingPair.le_hBA hpa)

933 · exact False.elim (hap hap')

934 · refine le_iInf ?_

935 intro p

936 exact iInf_le (fun q : c => q.1.N) ⟨p.1, p.2.1⟩

937 have hdKU : iInf (fun p : d => p.1.N) ≤ (U : Subgroup G) := by

938 simpa [hdEq] using hKU

939 rcases exists_quotientPair_le_openSubgroup_of_chain_iInf_le

940 (G := G) hdchain hdne U hdKU with ⟨b, hbU⟩

941 exact ⟨⟨b.1, b.2.1⟩, b.2.2, hbU⟩

942 let stageImage : c → Set (G ⧸ K) := fun a =>

943 Set.range fun y : a.1.Y => lift a (a.1.sourceOfY y)

944 have hlift_eq_of_le :

945 ∀ {a b : c} (hAB : a.1 ≤ b.1) (y : a.1.Y),

946 lift a (a.1.sourceOfY y) =

947 lift b (b.1.sourceOfY

948 ⟨a.1.le_map hAB (a.1.sourceOfY y), a.1.le_map_mem hAB y⟩) := by

949 intro a b hAB y

950 let yb : b.1.Y :=

951 ⟨a.1.le_map hAB (a.1.sourceOfY y), a.1.le_map_mem hAB y⟩

952 let q1 := lift a (a.1.sourceOfY y)

953 let q2 := lift b (b.1.sourceOfY yb)

954 have hmem :

955 ∀ W : OpenNormalSubgroup (G ⧸ K), q1⁻¹ * q2 ∈ (W : Set (G ⧸ K)) := by

956 intro W

957 let V : OpenNormalSubgroup G :=

958 OpenNormalSubgroup.comap (QuotientGroup.mk' K) QuotientGroup.continuous_mk W

959 have hKV : K ≤ (V : Subgroup G) := by

960 intro g hg

961 change QuotientGroup.mk' K g ∈ W

962 have hg1 : QuotientGroup.mk' K g = (1 : G ⧸ K) :=

963 (QuotientGroup.eq_one_iff (N := K) g).2 hg

964 rw [hg1]

965 exact W.one_mem'

966 obtain ⟨p, hbp, hpV⟩ := exists_stage_above_le_open b hKV

967 have hcompat :

968 a.1.le_map (hAB.trans hbp) (a.1.sourceOfY y) =

969 b.1.le_map hbp (b.1.sourceOfY yb) := by

970 have hqY :

971 a.1.le_map (hAB.trans hbp) (a.1.sourceOfY y) ∈ p.1.Y :=

972 a.1.le_map_mem (hAB.trans hbp) y

973 have hqproj :

974 leftQuotientProjection (p.1.N) (b.1.N) (b.1.le_hBA hbp)

975 (a.1.le_map (hAB.trans hbp) (a.1.sourceOfY y)) = yb.1 := by

976 simpa [yb] using a.1.le_map_compat hAB (hAB.trans hbp) hbp y

977 exact b.1.eq_le_map_of_mem_of_proj_eq hbp yb hqY hqproj

978 have hEqp :

979 leftQuotientProjection K p.1.N

980 (iInf_le (fun r : c => r.1.N) p) q1 =

981 leftQuotientProjection K p.1.N

982 (iInf_le (fun r : c => r.1.N) p) q2 := by

983 have hq1 :=

984 congrFun (hlift_fac a p (hAB.trans hbp)) (a.1.sourceOfY y)

985 have hq2 :=

986 congrFun (hlift_fac b p hbp) (b.1.sourceOfY yb)

987 calc

988 leftQuotientProjection K p.1.N

989 (iInf_le (fun r : c => r.1.N) p) q1

990 = a.1.le_map (hAB.trans hbp) (a.1.sourceOfY y) := by

991 simpa [q1] using hq1

992 _ = b.1.le_map hbp (b.1.sourceOfY yb) := hcompat

993 _ = leftQuotientProjection K p.1.N

994 (iInf_le (fun r : c => r.1.N) p) q2 := by

995 simpa [q2] using hq2.symm

996 have hEqV :

997 leftQuotientProjection K (V : Subgroup G) hKV q1 =

998 leftQuotientProjection K (V : Subgroup G) hKV q2 := by

999 calc

1000 leftQuotientProjection K (V : Subgroup G) hKV q1

1001 = leftQuotientProjection (p.1.N) (V : Subgroup G) hpV

1002 (leftQuotientProjection K p.1.N

1003 (iInf_le (fun r : c => r.1.N) p) q1) := by

1004 exact

1005 leftQuotientProjection_comp_apply_symm

1006 (K := (K : Subgroup G)) (H := (p.1.N : Subgroup G))

1007 (L := (V : Subgroup G)) (iInf_le (fun r : c => r.1.N) p)

1008 hpV q1

1009 _ = leftQuotientProjection (p.1.N) (V : Subgroup G) hpV

1010 (leftQuotientProjection K p.1.N

1011 (iInf_le (fun r : c => r.1.N) p) q2) := by

1012 rw [hEqp]

1013 _ = leftQuotientProjection K (V : Subgroup G) hKV q2 := by

1014 exact (leftQuotientProjection_comp_apply_symm

1015 (K := (K : Subgroup G)) (H := (p.1.N : Subgroup G))

1016 (L := (V : Subgroup G)) (iInf_le (fun r : c => r.1.N) p) hpV q2).symm

1017 revert hEqV

1018 refine Quotient.inductionOn₂' q1 q2 ?_

1019 intro g1 g2 hEqV

1020 change QuotientGroup.mk' K (g1⁻¹ * g2) ∈ W

1021 have hEqV' :

1022 QuotientGroup.mk' (V : Subgroup G) g1 =

1023 QuotientGroup.mk' (V : Subgroup G) g2 := by

1024 simpa [leftQuotientProjection_mk] using hEqV

1025 have hgV : g1⁻¹ * g2 ∈ (V : Subgroup G) := (QuotientGroup.eq).1 hEqV'

1026 change QuotientGroup.mk' K (g1⁻¹ * g2) ∈ W at hgV

1027 exact hgV

1028 have hq1 :

1029 q1⁻¹ * q2 = 1 := by

1030 exact ProfiniteGrp.eq_one_of_mem_all_openNormalSubgroups

1031 (G := G ⧸ K) hmem

1032 calc

1033 q1 = q1 * 1 := by simp only [mul_one]

1034 _ = q1 * (q1⁻¹ * q2) := by rw [hq1]

1035 _ = q2 := by simp only [mul_inv_cancel_left]

1036 have hstage_mono :

1037 ∀ {a b : c} (hAB : a.1 ≤ b.1), stageImage a ⊆ stageImage b := by

1038 intro a b hAB q hq

1039 rcases hq with ⟨y, rfl⟩

1040 refine ⟨⟨a.1.le_map hAB (a.1.sourceOfY y), a.1.le_map_mem hAB y⟩, ?_⟩

1041 exact (hlift_eq_of_le hAB y).symm

1042 have hstage_diff :

1043 ∀ {a b : c} (hAB : a.1 ≤ b.1),

1044 stageImage b \ stageImage a ⊆

1045 {q : G ⧸ K |

1046 leftQuotientProjection K a.1.N

1047 (iInf_le (fun p : c => p.1.N) a) q = 1} := by

1048 intro a b hAB q hq

1049 rcases hq.1 with ⟨yb, rfl⟩

1050 by_cases hybim : yb.1 ∈ a.1.yImage b.1 (a.1.le_map hAB)

1051 · rcases hybim with ⟨y, hyEq⟩

1052 have hEq :

1053 lift b (b.1.sourceOfY yb) = lift a (a.1.sourceOfY y) := by

1054 calc

1055 lift b (b.1.sourceOfY yb)

1056 = lift b (b.1.sourceOfY

1057 ⟨a.1.le_map hAB (a.1.sourceOfY y), a.1.le_map_mem hAB y⟩) := by

1058 simp only [hyEq, Subtype.coe_eta]

1059 _ = lift a (a.1.sourceOfY y) := (hlift_eq_of_le hAB y).symm

1060 exact False.elim (hq.2 ⟨y, hEq.symm⟩)

1061 · have hybker :

1062 leftQuotientProjection (b.1.N) (a.1.N) (a.1.le_hBA hAB) yb.1 = 1 :=

1063 a.1.le_map_diff hAB ⟨yb.2, hybim⟩

1064 have hqb :

1065 leftQuotientProjection K b.1.N

1066 (iInf_le (fun p : c => p.1.N) b)

1067 (lift b (b.1.sourceOfY yb)) = yb.1 := by

1068 calc

1069 leftQuotientProjection K b.1.N

1070 (iInf_le (fun p : c => p.1.N) b)

1071 (lift b (b.1.sourceOfY yb)) = b.1.le_map le_rfl (b.1.sourceOfY yb) := by

1072 exact congrFun (hlift_fac b b le_rfl) (b.1.sourceOfY yb)

1073 _ = yb.1 := by

1074 simpa only [leftQuotientProjection_id, id_eq,

1075 QuotientGeneratorConvergingPair.sourceOfY] using

1076 b.1.le_map_right le_rfl (b.1.sourceOfY yb)

1077 calc

1078 leftQuotientProjection K a.1.N

1079 (iInf_le (fun p : c => p.1.N) a)

1080 (lift b (b.1.sourceOfY yb))

1081 = leftQuotientProjection (b.1.N) (a.1.N) (a.1.le_hBA hAB)

1082 (leftQuotientProjection K b.1.N

1083 (iInf_le (fun p : c => p.1.N) b)

1084 (lift b (b.1.sourceOfY yb))) := by

1085 exact

1086 (leftQuotientProjection_comp_apply

1087 (K := (K : Subgroup G)) (H := (b.1.N : Subgroup G))

1088 (L := (a.1.N : Subgroup G)) (iInf_le (fun p : c => p.1.N) b)

1089 (a.1.le_hBA hAB) (lift b (b.1.sourceOfY yb))).symm

1090 _ = leftQuotientProjection (b.1.N) (a.1.N) (a.1.le_hBA hAB) yb.1 := by

1091 rw [hqb]

1092 _ = 1 := hybker

1093 let Y : Set (G ⧸ K) := ⋃ a : c, stageImage a

1094 have hYcompl : Y ⊆ ({1} : Set (G ⧸ K))ᶜ := by

1095 intro q hq

1096 rcases mem_iUnion.mp hq with ⟨a, hqa⟩

1097 rcases hqa with ⟨y, rfl⟩

1098 have hqy :

1099 leftQuotientProjection K a.1.N

1100 (iInf_le (fun p : c => p.1.N) a)

1101 (lift a (a.1.sourceOfY y)) = y.1 := by

1102 have hliftProjection := congrFun (hlift_fac a a le_rfl) (a.1.sourceOfY y)

1103 calc

1104 leftQuotientProjection K a.1.N

1105 (iInf_le (fun p : c => p.1.N) a)

1106 (lift a (a.1.sourceOfY y))

1107 = a.1.le_map le_rfl (a.1.sourceOfY y) := by

1108 simpa using hliftProjection

1109 _ = y.1 := by

1110 simpa only [leftQuotientProjection_id, id_eq,

1111 QuotientGeneratorConvergingPair.sourceOfY] using

1112 a.1.le_map_right le_rfl (a.1.sourceOfY y)

1113 intro hq1

1114 have hq1' : lift a (a.1.sourceOfY y) = 1 := by simpa using hq1

1115 have hy1 : y.1 = 1 := by

1116 calc

1117 y.1 = leftQuotientProjection K a.1.N

1118 (iInf_le (fun p : c => p.1.N) a)

1119 (lift a (a.1.sourceOfY y)) := hqy.symm

1120 _ = leftQuotientProjection K a.1.N

1121 (iInf_le (fun p : c => p.1.N) a) 1 := by rw [hq1']

1122 _ = 1 := by rfl

1123 exact a.1.subset_compl y.2 hy1

1124 have hYconv : ConvergesToOneAlongOpenSubgroups (G := G ⧸ K) Y := by

1125 intro W

1126 let V : OpenSubgroup G :=

1127 OpenSubgroup.comap (QuotientGroup.mk' K) QuotientGroup.continuous_mk W

1128 have hKV : K ≤ (V : Subgroup G) := by

1129 intro g hg

1130 change QuotientGroup.mk' K g ∈ W

1131 have hg1 : QuotientGroup.mk' K g = (1 : G ⧸ K) :=

1132 (QuotientGroup.eq_one_iff (N := K) g).2 hg

1133 rw [hg1]

1134 exact W.one_mem'

1135 rcases exists_quotientPair_le_openSubgroup_of_chain_iInf_le

1136 (G := G) hc hcn V (by simpa [K] using hKV) with ⟨a, haV⟩

1137 have hstageconv : ConvergesToOneAlongOpenSubgroups (G := G ⧸ K) (stageImage a) := by

1138 letI : IsClosed (a.1.N : Set G) := a.1.closed_N

1139 letI : TotallyDisconnectedSpace (G ⧸ a.1.N) :=

1140 ProCGroups.totallyDisconnectedSpace_quotient_closedNormal

1141 a.1.N a.1.closed_N

1142 have hconv :=

1143 ConvergesToOneAlongOpenSubgroups.range_subtype_pointed

1144 (G := G ⧸ a.1.N) (H := G ⧸ K)

1145 (hf := hlift_continuous a) (hf1 := hlift_one a) (hX := a.1.converges)

1146 have himage :

1147 stageImage a =

1148 Set.range (fun y : a.1.Y =>

1149 lift a ⟨y.1, Or.inr y.2⟩) := by

1150 ext q

1151 constructor <;> rintro ⟨y, rfl⟩ <;> exact ⟨y, rfl⟩

1152 rw [himage]

1153 exact hconv

1154 have hsubset : Y \ (W : Set (G ⧸ K)) ⊆ stageImage a \ (W : Set (G ⧸ K)) := by

1155 intro q hq

1156 rcases hq with ⟨hqY, hqW⟩

1157 rcases mem_iUnion.mp hqY with ⟨b, hbq⟩

1158 by_cases hba : b.1 ≤ a.1

1159 · exact ⟨hstage_mono hba hbq, hqW⟩

1160 · have hcmp : a.1 ≤ b.1 := by

1161 by_cases hEq : a = b

1162 · exact hEq ▸ le_rfl

1163 · rcases hc a.2 b.2 (by

1164 intro h

1165 exact hEq (Subtype.ext h)) with hab | hba'

1166 · exact hab

1167 · exact False.elim (hba hba')

1168 by_cases hqa : q ∈ stageImage a

1169 · exact ⟨hqa, hqW⟩

1170 · have hq1 :

1171 leftQuotientProjection K a.1.N

1172 (iInf_le (fun p : c => p.1.N) a) q = 1 :=

1173 hstage_diff hcmp ⟨hbq, hqa⟩

1174 have hqWin : q ∈ W := by

1175 rcases Quotient.exists_rep q with ⟨g, rfl⟩

1176 change QuotientGroup.mk' K g ∈ W

1177 have hgA : g ∈ a.1.N := by

1178 simpa [leftQuotientProjection_mk] using

1179 (QuotientGroup.eq_one_iff (N := a.1.N) g).1 hq1

1180 have hgV : g ∈ (V : Subgroup G) := haV hgA

1181 simpa [V, OpenSubgroup.mem_comap] using hgV

1182 exact False.elim (hqW hqWin)

1183 exact (hstageconv W).subset hsubset

1184 have hYgen : TopologicallyGenerates (G := G ⧸ K) Y := by

1185 have hbotclosed : IsClosed ((⊥ : Subgroup (G ⧸ K)) : Set (G ⧸ K)) := by

1186 change IsClosed ({(1 : G ⧸ K)} : Set (G ⧸ K))

1187 simp only [finite_singleton, Finite.isClosed]

1188 have hgen1 :

1189 TopologicallyGenerates (G := G ⧸ K) (Y ∪ ({1} : Set (G ⧸ K))) := by

1190 apply (topologicallyGenerates_union_subgroup_iff_forall_openNormalQuotient

1191 (G := G ⧸ K)

1192 (N := (⊥ : Subgroup (G ⧸ K))) (X := Y)).2

1193 intro W hbotW

1194 let V : OpenNormalSubgroup G :=

1195 OpenNormalSubgroup.comap (QuotientGroup.mk' K) QuotientGroup.continuous_mk W

1196 have hKV : K ≤ (V : Subgroup G) := by

1197 intro g hg

1198 change QuotientGroup.mk' K g ∈ W

1199 have hg1 : QuotientGroup.mk' K g = (1 : G ⧸ K) :=

1200 (QuotientGroup.eq_one_iff (N := K) g).2 hg

1201 rw [hg1]

1202 exact W.one_mem'

1203 rcases exists_quotientPair_le_openSubgroup_of_chain_iInf_le

1204 (G := G) hc hcn V.toOpenSubgroup (by simpa [K] using hKV) with ⟨a, haV⟩

1205 have hVaClosed : IsClosed ((V : Subgroup G) : Set G) :=

1206 openNormalSubgroup_isClosed (G := G) V

1207 have hmapW :

1208 ((V : Subgroup G).map (QuotientGroup.mk' K)) = (W : Subgroup (G ⧸ K)) := by

1209 ext q

1210 rcases Quotient.exists_rep q with ⟨g, rfl⟩

1211 constructor

1212 · rintro ⟨g', hg'V, hg'q⟩

1213 have : QuotientGroup.mk' K g' ∈ W := by

1214 change QuotientGroup.mk' K g' ∈ W at hg'V

1215 exact hg'V

1216 change QuotientGroup.mk' K g ∈ W

1217 have hg'q' :

1218 QuotientGroup.mk' K g' = QuotientGroup.mk' K g := hg'q

1219 exact hg'q' ▸ this

1220 · intro hgW

1221 refine ⟨g, ?_, rfl⟩

1222 change QuotientGroup.mk' K g ∈ W

1223 exact hgW

1224 let QV : Subgroup (G ⧸ K) := (V : Subgroup G).map (QuotientGroup.mk' K)

1225 let Wmap : OpenNormalSubgroup (G ⧸ K) :=

1226 { toOpenSubgroup :=

1227 { toSubgroup := QV

1228 isOpen' := by

1229 simpa [QV, hmapW] using W.isOpen' }

1230 isNormal' := by

1231 simpa [QV, hmapW] using (show (W : Subgroup (G ⧸ K)).Normal from inferInstance) }

1232 have hWmap : Wmap = W := by

1233 ext q

1234 change q ∈ QV ↔ q ∈ (W : Subgroup (G ⧸ K))

1235 simp only [hmapW, OpenSubgroup.mem_toSubgroup, QV]

1236 let e0 :

1237 ((G ⧸ K) ⧸ QV) ≃ₜ* G ⧸ (V : Subgroup G) :=

1238 quotientQuotientContinuousMulEquiv

1239 (G := G) hVaClosed hKV

1240 have hstageProj :

1241 ∀ y : a.1.Y,

1242 leftQuotientProjection K (V : Subgroup G) hKV

1243 (lift a (a.1.sourceOfY y)) =

1244 leftQuotientProjection a.1.N (V : Subgroup G) haV y.1 := by

1245 intro y

1246 have hqy0 :=

1247 congrFun (hlift_fac a a le_rfl) (a.1.sourceOfY y)

1248 have hqy :

1249 leftQuotientProjection K a.1.N

1250 (iInf_le (fun p : c => p.1.N) a)

1251 (lift a (a.1.sourceOfY y)) = y.1 := by

1252 calc

1253 leftQuotientProjection K a.1.N

1254 (iInf_le (fun p : c => p.1.N) a)

1255 (lift a (a.1.sourceOfY y)) = a.1.le_map le_rfl (a.1.sourceOfY y) := by

1256 exact hqy0

1257 _ = y.1 := by

1258 simpa only [leftQuotientProjection_id, id_eq,

1259 QuotientGeneratorConvergingPair.sourceOfY] using

1260 a.1.le_map_right le_rfl (a.1.sourceOfY y)

1261 calc

1262 leftQuotientProjection K (V : Subgroup G) hKV

1263 (lift a (a.1.sourceOfY y))

1264 = leftQuotientProjection (a.1.N) (V : Subgroup G) haV

1265 (leftQuotientProjection K a.1.N

1266 (iInf_le (fun p : c => p.1.N) a)

1267 (lift a (a.1.sourceOfY y))) := by

1268 exact

1269 leftQuotientProjection_comp_apply_symm

1270 (K := (K : Subgroup G)) (H := (a.1.N : Subgroup G))

1271 (L := (V : Subgroup G)) (iInf_le (fun p : c => p.1.N) a) haV

1272 (lift a (a.1.sourceOfY y))

1273 _ = leftQuotientProjection (a.1.N) (V : Subgroup G) haV y.1 := by

1274 rw [hqy]

1275 have hstageImgEq :

1276 (leftQuotientProjection K (V : Subgroup G) hKV) '' stageImage a =

1277 (leftQuotientProjection a.1.N (V : Subgroup G) haV) '' a.1.Y := by

1278 ext q

1279 constructor

1280 · rintro ⟨x, ⟨y, rfl⟩, rfl⟩

1281 exact ⟨y.1, y.2, (hstageProj y).symm⟩

1282 · rintro ⟨y, hyY, hyq⟩

1283 let y' : a.1.Y := ⟨y, hyY⟩

1284 refine ⟨lift a (a.1.sourceOfY y'), ⟨y', rfl⟩, ?_⟩

1285 calc

1286 leftQuotientProjection K (V : Subgroup G) hKV

1287 (lift a (a.1.sourceOfY y'))

1288 = leftQuotientProjection a.1.N (V : Subgroup G) haV y := by

1289 simpa [y'] using hstageProj y'

1290 _ = q := hyq

1291 have hstageGenV :

1292 TopologicallyGenerates (G := G ⧸ (V : Subgroup G))

1293 ((leftQuotientProjection K (V : Subgroup G) hKV) '' stageImage a) := by

1294 let fV : (G ⧸ a.1.N) →* G ⧸ (V : Subgroup G) :=

1295 { toFun := leftQuotientProjection a.1.N (V : Subgroup G) haV

1296 map_one' := rfl

1297 map_mul' := by

1298 intro x y

1299 refine Quotient.inductionOn₂' x y ?_

1300 intro g h

1301 rfl }

1302 have hgenV :

1303 TopologicallyGenerates (G := G ⧸ (V : Subgroup G))

1304 (fV '' a.1.Y) := by

1305 exact topologicallyGenerates_image_of_continuousSurjective

1306 (G := G ⧸ a.1.N) (H := G ⧸ (V : Subgroup G)) fV

1307 (by

1308 simpa [fV] using

1309 (continuous_leftQuotientProjection

1310 (G := G) (K := a.1.N) (H := (V : Subgroup G)) haV))

1311 (by

1312 simpa [fV] using

1313 (surjective_leftQuotientProjection

1314 (G := G) (K := a.1.N) (H := (V : Subgroup G)) haV))

1315 a.1.generates

1316 rw [hstageImgEq]

1317 simpa [fV] using hgenV

1318 have hquotProj0 :

1319 ∀ y : G ⧸ K,

1320 e0 ((QuotientGroup.mk' QV) y) =

1321 leftQuotientProjection K (V : Subgroup G) hKV y := by

1322 intro y

1323 refine Quotient.inductionOn y ?_

1324 intro g

1325 rfl

1326 have hquotPreimgEq0 :

1327 e0.symm '' ((leftQuotientProjection K (V : Subgroup G) hKV) '' Y) =

1328 (QuotientGroup.mk' QV '' Y) := by

1329 ext q

1330 constructor

1331 · rintro ⟨z, ⟨y, hy, hzy⟩, hqz⟩

1332 refine ⟨y, hy, ?_⟩

1333 have hzq : z = e0 q := by

1334 calc

1335 z = e0 (e0.symm z) := by symm; exact e0.right_inv z

1336 _ = e0 q := by rw [hqz]

1337 have heqy : e0 ((QuotientGroup.mk' QV) y) = z := by

1338 exact (hquotProj0 y).trans hzy

1339 exact e0.injective (heqy.trans hzq)

1340 · rintro ⟨y, hy, rfl⟩

1341 refine ⟨leftQuotientProjection K (V : Subgroup G) hKV y, ⟨y, hy, rfl⟩, ?_⟩

1342 calc

1343 e0.symm (leftQuotientProjection K (V : Subgroup G) hKV y)

1344 = e0.symm (e0 ((QuotientGroup.mk' QV) y)) := by

1345 rw [hquotProj0 y]

1346 _ = QuotientGroup.mk' QV y := e0.left_inv _

1347 have hgenYV :

1348 TopologicallyGenerates (G := G ⧸ (V : Subgroup G))

1349 ((leftQuotientProjection K (V : Subgroup G) hKV) '' Y) := by

1350 exact topologicallyGenerates_mono hstageGenV (by

1351 intro q hq

1352 rcases hq with ⟨x, hx, rfl⟩

1353 exact ⟨x, mem_iUnion.mpr ⟨a, hx⟩, rfl⟩)

1354 have hgenQuot0 :

1355 TopologicallyGenerates (G := ((G ⧸ K) ⧸ QV))

1356 ((QuotientGroup.mk' QV) '' Y) := by

1357 rw [← hquotPreimgEq0]

1358 exact topologicallyGenerates_continuousMulEquiv_image

1359 (G := G ⧸ (V : Subgroup G)) e0.symm hgenYV

1360 have hgenQuotMap :

1361 TopologicallyGenerates

1362 (G := ((G ⧸ K) ⧸ (Wmap : Subgroup (G ⧸ K))))

1363 ((QuotientGroup.mk' (Wmap : Subgroup (G ⧸ K))) '' Y) := by

1364 simpa [QV, Wmap] using hgenQuot0

1365 have hgenQuot :

1366 TopologicallyGenerates (G := ((G ⧸ K) ⧸ (W : Subgroup (G ⧸ K))))

1367 ((QuotientGroup.mk' (W : Subgroup (G ⧸ K))) '' Y) := by

1368 simpa using (hWmap ▸ hgenQuotMap)

1369 exact hgenQuot

1370 exact (topologicallyGenerates_union_one_iff (G := G ⧸ K) (X := Y)).1 hgen1

1371 refine ⟨{ N := K

1372 normal_N := inferInstance

1373 closed_N := hKclosed

1374 Y := Y

1375 subset_compl := hYcompl

1376 converges := hYconv

1377 generates := hYgen }, ?_⟩

1378 intro a ha

1379 let a' : c := ⟨a, ha⟩

1380 refine ⟨iInf_le (fun p : c => p.1.N) a', lift a', ?_, ?_, ?_, ?_, ?_⟩

1381 · exact hlift_continuous a'

1382 · intro x

1383 have hliftProjection := congrFun (hlift_fac a' a' le_rfl) x

1384 calc

1385 leftQuotientProjection K a.N (iInf_le (fun p : c => p.1.N) a')

1386 (lift a' x) = a.le_map le_rfl x := by

1387 simpa using hliftProjection

1388 _ = x.1 := by

1389 simpa [QuotientGeneratorConvergingPair.le_map,

1390 QuotientGeneratorConvergingPair.le_hBA] using

1391 a.le_map_right le_rfl x

1392 · exact hlift_one a'

1393 · intro y

1394 exact mem_iUnion.mpr ⟨a', ⟨y, rfl⟩⟩

1395 · intro q hq

1396 rcases mem_iUnion.mp hq.1 with ⟨b, hbq⟩

1397 by_cases hba : b.1 ≤ a

1398 · exact False.elim (hq.2 (hstage_mono (a := b) (b := a') hba hbq))

1399 · have hab : a ≤ b.1 := by

1400 by_cases hEq : a = b.1

1401 · exact hEq ▸ le_rfl

1402 · rcases hc ha b.2 (by

1403 intro h

1404 exact hEq h) with hab | hba'

1405 · exact hab

1406 · exact False.elim (hba hba')

1407 exact hstage_diff (a := a') (b := b) hab ⟨hbq, hq.2⟩

1408

1409/-- 4.4. Existence theorem used by the public theorem. -/

1410theorem exists_generatorsConvergingToOne :

1411 ∃ X : Set G, GeneratesAndConvergesToOneAlongOpenSubgroups (G := G) X := by

1412 classical

1413 let Pair := QuotientGeneratorConvergingPair (G := G)

1414 letI : Nonempty Pair := ⟨quotientGeneratorPairTop (G := G)⟩

1415 obtain ⟨m, hmmax⟩ := zorn_le_nonempty (α := Pair) <| by

1416 intro c hc hcn

1417 rcases quotientGeneratorPair_exists_upperBound_of_chain (G := G) c hc hcn with

1418 ⟨ub, hub⟩

1419 exact ⟨ub, hub⟩

1420 have hmbot : m.N = ⊥ := by

1421 by_contra hne

1422 rcases quotientGeneratorPair_exists_strictExtension (G := G) m hne with

1423 ⟨m', hmm', hm'm⟩

1424 exact hm'm (hmmax hmm')

1425 exact ⟨m.toAmbientSet, m.toAmbientSet_generatesAndConvergesToOneAlongOpenSubgroups hmbot⟩

1426

1427

1428

1429omit [T2Space G] in

1430/-- A surjective continuous homomorphism preserves generating sets converging to `1`. -/

1431theorem GeneratesAndConvergesToOneAlongOpenSubgroups.image_of_continuousSurjective

1432 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

1433 (f : G →* H) (hf : Continuous f) (hfsurj : Function.Surjective f)

1434 {X : Set G} (hX : GeneratesAndConvergesToOneAlongOpenSubgroups (G := G) X) :

1435 GeneratesAndConvergesToOneAlongOpenSubgroups (G := H) (f '' X) := by

1436 refine ⟨?_, ?_⟩

1437 · exact topologicallyGenerates_image_of_continuousSurjective

1438 (G := G) (H := H) f hf hfsurj hX.1

1439 · exact ConvergesToOneAlongOpenSubgroups.image_of_continuous_pointed

1440 (G := G) (H := H) hf (by simp only [map_one]) hX.2

1441

1442omit [T2Space G] in

1443/-- A continuous multiplicative equivalence preserves generating sets converging to `1`. -/

1444theorem GeneratesAndConvergesToOneAlongOpenSubgroups.image_of_continuousMulEquiv

1445 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

1446 (e : G ≃ₜ* H) {X : Set G}

1447 (hX : GeneratesAndConvergesToOneAlongOpenSubgroups (G := G) X) :

1448 GeneratesAndConvergesToOneAlongOpenSubgroups (G := H) (e '' X) := by

1449 refine ⟨?_, ?_⟩

1450 · exact topologicallyGenerates_continuousMulEquiv_image

1451 (G := G) e hX.1

1452 · exact ConvergesToOneAlongOpenSubgroups.image_of_continuous_pointed

1453 (G := G) (H := H) e.continuous (by simp only [Homeomorph.homeomorph_mk_coe,

1454 ContinuousMulEquiv.toMulEquiv_eq_coe, MulEquiv.toEquiv_eq_coe,

1455 EquivLike.coe_coe, map_one]) hX.2

1456

1457omit [T2Space G] in

1458/-- A continuous multiplicative equivalence preserves and reflects convergence to `1`. -/

1459theorem ConvergesToOneAlongOpenSubgroups.image_of_continuousMulEquiv_iff

1460 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

1461 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]

1462 (e : G ≃ₜ* H) {X : Set G} :

1463 ConvergesToOneAlongOpenSubgroups (G := H) (e '' X) ↔ ConvergesToOneAlongOpenSubgroups (G :=

1464 G) X := by

1465 constructor

1466 · intro h

1467 have hback : ConvergesToOneAlongOpenSubgroups (G := G) (e.symm '' (e '' X)) :=

1468 ConvergesToOneAlongOpenSubgroups.image_of_continuous_pointed

1469 (G := H) (H := G) e.symm.continuous (by simp only [Homeomorph.homeomorph_mk_coe,

1470 ContinuousMulEquiv.toMulEquiv_eq_coe, MulEquiv.toEquiv_eq_coe,

1471 EquivLike.coe_coe, map_one]) (X := e '' X) h

1472 have himage : e.symm '' (e '' X) = X := by

1473 ext x

1474 constructor

1475 · rintro ⟨y, ⟨z, hz, rfl⟩, rfl⟩

1476 simpa using hz

1477 · intro hx

1478 exact ⟨e x, ⟨x, hx, rfl⟩, by simp only [ContinuousMulEquiv.symm_apply_apply]⟩

1479 simpa [himage] using hback

1480 · intro h

1481 exact ConvergesToOneAlongOpenSubgroups.image_of_continuous_pointed

1482 (G := G) (H := H) e.continuous (by simp only [Homeomorph.homeomorph_mk_coe,

1483 ContinuousMulEquiv.toMulEquiv_eq_coe, MulEquiv.toEquiv_eq_coe,

1484 EquivLike.coe_coe, map_one]) h

1485

1486omit [T2Space G] in

1487/-- A continuous multiplicative equivalence preserves and reflects the combined predicate. -/

1488theorem GeneratesAndConvergesToOneAlongOpenSubgroups.image_of_continuousMulEquiv_iff

1489 {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

1490 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]

1491 (e : G ≃ₜ* H) {X : Set G} :

1492 GeneratesAndConvergesToOneAlongOpenSubgroups (G := H) (e '' X) ↔

1493 GeneratesAndConvergesToOneAlongOpenSubgroups (G := G) X := by

1494 constructor

1495 · intro h

1496 exact ⟨

1497 (topologicallyGenerates_continuousMulEquiv_image_iff (G := G) (H := H) e (X := X)).1 h.1,

1498 (ConvergesToOneAlongOpenSubgroups.image_of_continuousMulEquiv_iff

1499 (G := G) (H := H) e (X := X)).1 h.2⟩

1500 · intro h

1501 exact ⟨

1502 (topologicallyGenerates_continuousMulEquiv_image_iff (G := G) (H := H) e (X := X)).2 h.1,

1503 (ConvergesToOneAlongOpenSubgroups.image_of_continuousMulEquiv_iff

1504 (G := G) (H := H) e (X := X)).2 h.2⟩

1505

1506omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

1507/-- Topological rank is invariant under continuous multiplicative equivalence. -/

1508theorem topologicalRank_eq_of_continuousMulEquiv

1509 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

1510 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]

1511 (e : G ≃ₜ* H) :

1512 topologicalRank G = topologicalRank H := by

1513 apply le_antisymm

1514 · rcases exists_topologicallyGenerates_card_eq_topologicalRank (G := H) with

1515 ⟨Ymin, hYmin, hYcard⟩

1516 calc

1517 topologicalRank G ≤ Cardinal.mk (e.symm '' Ymin) := by

1518 exact topologicalRank_le_mk_of_topologicallyGenerates

1519 (G := G)

1520 (topologicallyGenerates_continuousMulEquiv_image

1521 (G := H) e.symm hYmin)

1522 _ ≤ Cardinal.mk Ymin := Cardinal.mk_image_le

1523 _ = topologicalRank H := hYcard

1524 · rcases exists_topologicallyGenerates_card_eq_topologicalRank (G := G) with

1525 ⟨Xmin, hXmin, hXcard⟩

1526 calc

1527 topologicalRank H ≤ Cardinal.mk (e '' Xmin) := by

1528 exact topologicalRank_le_mk_of_topologicallyGenerates

1529 (G := H)

1530 (topologicallyGenerates_continuousMulEquiv_image

1531 (G := G) e hXmin)

1532 _ ≤ Cardinal.mk Xmin := Cardinal.mk_image_le

1533 _ = topologicalRank G := hXcard

1534

1535

1536end Generators

1537

1538end ProCGroups.Generation