Source: ProCGroups.Abelian.TopologicalAbelianizationLimits

1import ProCGroups.Abelian.TopologicalAbelianizationFunctoriality

2import ProCGroups.InverseSystems.Quotients

3import ProCGroups.InverseSystems.StagewiseIso

4import ProCGroups.ProC.Quotients.ClosedNormal

6/-!

7# Topological abelianization and inverse limits

9This module applies topological abelianization stagewise to inverse systems and compares the

10resulting limit with the abelianization of the original limit.

11-/

13open scoped Topology

15namespace ProCGroups.Abelian

17open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups

19universe u v

20/-- The stagewise inverse system obtained by applying topological abelianization. -/

21noncomputable def abelianizationInverseSystem

22 {I : Type u} [Preorder I]

23 (S : InverseSystems.InverseSystem (I := I))

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

25 [∀ i, IsTopologicalGroup (S.X i)] :

26 InverseSystems.InverseSystem (I := I) where

27 X := fun i => TopologicalAbelianization (S.X i)

28 topologicalSpace := fun i => inferInstance

29 map := fun {i j} hij =>

30 TopologicalAbelianization.map

31 { toMonoidHom :=

32 { toFun := S.map hij

33 map_one' := InverseSystems.IsGroupSystem.map_one (S := S) hij

34 map_mul' := InverseSystems.IsGroupSystem.map_mul (S := S) hij }

35 continuous_toFun := S.continuous_map hij }

36 continuous_map := by

37 intro i j hij

38 exact (TopologicalAbelianization.map

39 { toMonoidHom :=

40 { toFun := S.map hij

41 map_one' := InverseSystems.IsGroupSystem.map_one (S := S) hij

42 map_mul' := InverseSystems.IsGroupSystem.map_mul (S := S) hij }

43 continuous_toFun := S.continuous_map hij }).continuous_toFun

44 map_id := by

45 intro i

46 funext x

47 refine Quotient.inductionOn' x ?_

48 intro a

49 change

50 QuotientGroup.mk'

51 (Subgroup.topologicalClosure (commutator (S.X i)))

52 (S.map (le_rfl : i ≤ i) a) =

53 QuotientGroup.mk'

54 (Subgroup.topologicalClosure (commutator (S.X i)))

55 a

56 exact congrArg

57 (QuotientGroup.mk' (Subgroup.topologicalClosure (commutator (S.X i))))

58 (S.map_id_apply i a)

59 map_comp := by

60 intro i j k hij hjk

61 funext x

62 refine Quotient.inductionOn' x ?_

63 intro a

64 change

65 QuotientGroup.mk'

66 (Subgroup.topologicalClosure (commutator (S.X i)))

67 (S.map hij (S.map hjk a)) =

68 QuotientGroup.mk'

69 (Subgroup.topologicalClosure (commutator (S.X i)))

70 (S.map (hij.trans hjk) a)

71 exact congrArg

72 (QuotientGroup.mk' (Subgroup.topologicalClosure (commutator (S.X i))))

73 (S.map_comp_apply hij hjk a)

75/-- Each stage of the abelianization inverse system inherits its quotient group structure. -/

76instance abelianizationInverseSystem_stageGroup

77 {I : Type u} [Preorder I]

78 (S : InverseSystems.InverseSystem (I := I))

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

80 [∀ i, IsTopologicalGroup (S.X i)] (i : I) :

81 Group ((abelianizationInverseSystem S).X i) := by

82 change Group (TopologicalAbelianization (S.X i))

83 infer_instance

85/-- The abelianization inverse system is a group-valued inverse system. -/

86instance abelianizationInverseSystem_isGroupSystem

87 {I : Type u} [Preorder I]

88 (S : InverseSystems.InverseSystem (I := I))

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

90 [∀ i, IsTopologicalGroup (S.X i)] :

91 InverseSystems.IsGroupSystem (abelianizationInverseSystem S) where

92 map_one := by

93 intro i j hij

94 exact (TopologicalAbelianization.map

95 { toMonoidHom :=

96 { toFun := S.map hij

97 map_one' := InverseSystems.IsGroupSystem.map_one (S := S) hij

98 map_mul' := InverseSystems.IsGroupSystem.map_mul (S := S) hij }

99 continuous_toFun := S.continuous_map hij }).map_one

100 map_mul := by

101 intro i j hij x y

102 exact (TopologicalAbelianization.map

103 { toMonoidHom :=

104 { toFun := S.map hij

105 map_one' := InverseSystems.IsGroupSystem.map_one (S := S) hij

106 map_mul' := InverseSystems.IsGroupSystem.map_mul (S := S) hij }

107 continuous_toFun := S.continuous_map hij }).map_mul x y

108 map_inv := by

109 intro i j hij x

110 exact (TopologicalAbelianization.map

111 { toMonoidHom :=

112 { toFun := S.map hij

113 map_one' := InverseSystems.IsGroupSystem.map_one (S := S) hij

114 map_mul' := InverseSystems.IsGroupSystem.map_mul (S := S) hij }

115 continuous_toFun := S.continuous_map hij }).map_inv x

116

117/--

118The stagewise quotient maps assemble into a morphism from an inverse system to its stagewise

119topological abelianization.

120-/

121def toAbelianizationInverseSystem

122 {I : Type u} [Preorder I]

123 (S : InverseSystems.InverseSystem (I := I))

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

125 [∀ i, IsTopologicalGroup (S.X i)] :

126 S.Morphism (abelianizationInverseSystem S) where

127 map := fun i => TopologicalAbelianization.mk (S.X i)

128 continuous_map := fun _ => continuous_quotient_mk'

129 comm := by

130 intro i j hij

131 funext x

132 rfl

133

134/--

135The stagewise closed commutator subgroups form a compatible closed-normal family in any

136group-valued inverse system of topological groups.

137-/

138noncomputable def closedCommutatorCompatibleClosedNormalSubgroups

139 {I : Type u} [Preorder I]

140 (S : InverseSystems.InverseSystem (I := I))

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

142 [∀ i, IsTopologicalGroup (S.X i)] :

143 S.CompatibleClosedNormalSubgroups where

144 N := fun i => Subgroup.closedCommutator (S.X i)

145 normal := fun i => by infer_instance

146 closed := fun i => Subgroup.isClosed_closedCommutator (S.X i)

147 map_le := by

148 intro i j hij x hx

149 let f : S.X j →ₜ* S.X i :=

150 { toMonoidHom := S.transitionHom hij

151 continuous_toFun :=

152 InverseSystems.InverseSystem.continuous_transitionHom (S := S) hij }

153 have hxmap :

154 S.transitionHom hij x ∈

155 (Subgroup.closedCommutator (S.X j)).map f.toMonoidHom :=

156 Subgroup.mem_map_of_mem f.toMonoidHom hx

157 exact Subgroup.closedCommutator_map_le f hxmap

158

159/--

160The canonical comparison map from the abelianization of an inverse limit to the inverse limit of

161the stagewise abelianizations.

162-/

163noncomputable def topologicalAbelianizationInverseLimitComparison

164 {I : Type u} [Preorder I]

165 (S : InverseSystems.InverseSystem (I := I))

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

167 [∀ i, IsTopologicalGroup (S.X i)] :

168 TopologicalAbelianization S.inverseLimit →ₜ*

169 (abelianizationInverseSystem S).inverseLimit := by

170 let T := abelianizationInverseSystem S

171 let ψ : ∀ i, TopologicalAbelianization S.inverseLimit →ₜ* T.X i := fun i =>

172 TopologicalAbelianization.map

173 { toMonoidHom :=

174 { toFun := S.projection i

175 map_one' := rfl

176 map_mul' := by intro x y; rfl }

177 continuous_toFun := S.continuous_projection i }

178 let ψFun : ∀ i, TopologicalAbelianization S.inverseLimit → T.X i := fun i => ψ i

179 have hψ : ∀ i, Continuous (ψFun i) := by

180 intro i

181 exact (ψ i).continuous_toFun

182 have hcompat : T.CompatibleMaps ψFun := by

183 intro i j hij

184 funext x

185 refine Quotient.inductionOn' x ?_

186 intro a

187 change

188 QuotientGroup.mk'

189 (Subgroup.topologicalClosure (commutator (S.X i)))

190 (S.map hij (S.projection j a)) =

191 QuotientGroup.mk'

192 (Subgroup.topologicalClosure (commutator (S.X i)))

193 (S.projection i a)

194 simpa using congrArg

195 (QuotientGroup.mk' (Subgroup.topologicalClosure (commutator (S.X i))))

196 (S.projection_compatible a i j hij)

197 refine

198 { toMonoidHom :=

199 { toFun := T.inverseLimitLift ψFun hcompat

200 map_one' := by

201 apply T.ext

202 intro i

203 change ψFun i 1 = 1

204 exact (ψ i).map_one

205 map_mul' := by

206 intro x y

207 apply T.ext

208 intro i

209 change ψFun i (x * y) = ψFun i x * ψFun i y

210 exact (ψ i).map_mul x y }

211 continuous_toFun := T.continuous_inverseLimitLift ψFun hψ hcompat }

212

213/--

214The projection from the topological abelianization inverse-limit comparison to a finite stage.

215-/

216@[simp 900] theorem π_topologicalAbelianizationInverseLimitComparison

217 {I : Type u} [Preorder I]

218 (S : InverseSystems.InverseSystem (I := I))

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

220 [∀ i, IsTopologicalGroup (S.X i)]

221 (i : I) :

222 (abelianizationInverseSystem S).projection i ∘

223 topologicalAbelianizationInverseLimitComparison S =

224 TopologicalAbelianization.map

225 { toMonoidHom :=

226 { toFun := S.projection i

227 map_one' := rfl

228 map_mul' := by intro x y; rfl }

229 continuous_toFun := S.continuous_projection i } := by

230 let T := abelianizationInverseSystem S

231 let ψ : ∀ i, TopologicalAbelianization S.inverseLimit →ₜ* T.X i := fun i =>

232 TopologicalAbelianization.map

233 { toMonoidHom :=

234 { toFun := S.projection i

235 map_one' := rfl

236 map_mul' := by intro x y; rfl }

237 continuous_toFun := S.continuous_projection i }

238 let ψFun : ∀ i, TopologicalAbelianization S.inverseLimit → T.X i := fun i => ψ i

239 have hcompat : T.CompatibleMaps ψFun := by

240 intro i j hij

241 funext x

242 refine Quotient.inductionOn' x ?_

243 intro a

244 change

245 QuotientGroup.mk'

246 (Subgroup.topologicalClosure (commutator (S.X i)))

247 (S.map hij (S.projection j a)) =

248 QuotientGroup.mk'

249 (Subgroup.topologicalClosure (commutator (S.X i)))

250 (S.projection i a)

251 simpa using congrArg

252 (QuotientGroup.mk' (Subgroup.topologicalClosure (commutator (S.X i))))

253 (S.projection_compatible a i j hij)

254 funext x

255 change T.projection i (T.inverseLimitLift ψFun hcompat x) = ψFun i x

256 rfl

257

258/--

259The finite-stage projection of the topological abelianization comparison has the stated value on

260representatives.

261-/

262@[simp 900] theorem π_topologicalAbelianizationInverseLimitComparison_mk

263 {I : Type u} [Preorder I]

264 (S : InverseSystems.InverseSystem (I := I))

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

266 [∀ i, IsTopologicalGroup (S.X i)]

267 (i : I) (x : S.inverseLimit) :

268 (abelianizationInverseSystem S).projection i

269 (topologicalAbelianizationInverseLimitComparison S

270 (QuotientGroup.mk' (Subgroup.closedCommutator S.inverseLimit) x)) =

271 QuotientGroup.mk' (Subgroup.closedCommutator (S.X i)) (S.projection i x) := by

272 rfl

273

274/--

275The inverse-limit map induced by stagewise abelianization factors as the limit quotient map

276followed by the abelianization comparison map.

277-/

278@[simp 900] theorem limMap_toAbelianizationInverseSystem_apply

279 {I : Type u} [Preorder I]

280 (S : InverseSystems.InverseSystem (I := I))

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

282 [∀ i, IsTopologicalGroup (S.X i)]

283 (x : S.inverseLimit) :

284 S.limMap (toAbelianizationInverseSystem S) x =

285 topologicalAbelianizationInverseLimitComparison S

286 (TopologicalAbelianization.mk S.inverseLimit x) := by

287 change S.limMap (toAbelianizationInverseSystem S) x =

288 topologicalAbelianizationInverseLimitComparison S

289 (QuotientGroup.mk' (Subgroup.closedCommutator S.inverseLimit) x)

290 apply (abelianizationInverseSystem S).ext

291 intro i

292 rw [S.π_limMap_apply (toAbelianizationInverseSystem S) i]

293 exact (π_topologicalAbelianizationInverseLimitComparison_mk (S := S) i x).symm

294

295/--

296Auxiliary injectivity of the canonical comparison map used to build the continuous equivalence;

297the main formulation is \(injective_topologicalAbelianizationInverseLimitComparison\).

298-/

299private theorem inj_topologicalAbelianizationInverseLimitComparison_of_profinite_inverse_system

300 {I : Type u} [Preorder I] [Nonempty I]

301 (S : InverseSystems.InverseSystem (I := I))

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

303 [∀ i, IsTopologicalGroup (S.X i)]

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

305 [∀ i, TotallyDisconnectedSpace (S.X i)]

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

307 Function.Injective (topologicalAbelianizationInverseLimitComparison S) := by

308 let f := topologicalAbelianizationInverseLimitComparison S

309 letI : CompactSpace S.inverseLimit := inferInstance

310 letI : T2Space S.inverseLimit := S.t2Space_inverseLimit

311 letI : TotallyDisconnectedSpace S.inverseLimit := S.totallyDisconnectedSpace_inverseLimit

312 let N : Subgroup S.inverseLimit :=

313 Subgroup.topologicalClosure (commutator S.inverseLimit)

314 letI : N.Normal := by dsimp [N]; infer_instance

315 have hNclosed : IsClosed (N : Set S.inverseLimit) := by

316 simp [N]

317 letI : IsClosed (N : Set S.inverseLimit) := hNclosed

318 letI : CompactSpace (TopologicalAbelianization S.inverseLimit) :=

319 by simpa [TopologicalAbelianization, N] using

320 (inferInstance : CompactSpace (S.inverseLimit ⧸ N))

321 letI : T2Space (TopologicalAbelianization S.inverseLimit) :=

322 by simpa [TopologicalAbelianization, N] using

323 (inferInstance : T2Space (S.inverseLimit ⧸ N))

324 letI : TotallyDisconnectedSpace (TopologicalAbelianization S.inverseLimit) :=

325 by simpa [TopologicalAbelianization, N] using

326 (ProCGroups.totallyDisconnectedSpace_quotient_closedNormal N hNclosed)

327 have hkerbot : f.toMonoidHom.ker = ⊥ := by

328 ext a

329 constructor

330 · intro ha

331 by_contra hane

332 rcases ProCGroups.ProC.exists_openNormalSubgroup_not_mem

333 (G := TopologicalAbelianization S.inverseLimit) (x := a) hane with ⟨U, haU⟩

334 let Q := TopologicalAbelianization S.inverseLimit ⧸

335 (U : Subgroup (TopologicalAbelianization S.inverseLimit))

336 letI : Finite Q := openNormalSubgroup_finiteQuotient

337 (G := TopologicalAbelianization S.inverseLimit) U

338 letI : DiscreteTopology Q :=

339 QuotientGroup.discreteTopology

340 (openNormalSubgroup_isOpen (G := TopologicalAbelianization S.inverseLimit) U)

341 let qInv : S.inverseLimit →ₜ* TopologicalAbelianization S.inverseLimit :=

342 { toMonoidHom := TopologicalAbelianization.mk S.inverseLimit

343 continuous_toFun := continuous_quotient_mk' }

344 let β : S.inverseLimit →ₜ* Q :=

345 { toMonoidHom :=

346 (QuotientGroup.mk' (U : Subgroup (TopologicalAbelianization S.inverseLimit))).comp

347 qInv.toMonoidHom

348 continuous_toFun := continuous_quotient_mk'.comp qInv.continuous_toFun

349 }

350 rcases InverseSystems.InverseSystem.factors_through_projection_finite_group_hom

351 (S := S) hdir β.toMonoidHom β.continuous_toFun with ⟨i, βi, hβi_continuous, hβfac⟩

352 let βiCont : S.X i →ₜ* Q :=

353 { toMonoidHom := βi

354 continuous_toFun := hβi_continuous }

355 have hq : QuotientGroup.mk' (U : Subgroup (TopologicalAbelianization S.inverseLimit)) a =

356 1 := by

357 rcases QuotientGroup.mk'_surjective

358 (Subgroup.topologicalClosure (commutator S.inverseLimit)) a with ⟨x, rfl⟩

359 calc

360 QuotientGroup.mk'

361 (U : Subgroup (TopologicalAbelianization S.inverseLimit))

362 (TopologicalAbelianization.mk S.inverseLimit x)

363 = β x := rfl

364 _ = βi (S.projection i x) := by

365 simpa [Function.comp] using

366 congrArg

367 (fun g : S.inverseLimit → Q => g x)

368 hβfac

369 _ = TopologicalAbelianization.lift βiCont

370 (TopologicalAbelianization.mk (S.X i) (S.projection i x)) := by

371 symm

372 exact TopologicalAbelianization.lift_apply_mk βiCont (S.projection i x)

373 _ = TopologicalAbelianization.lift βiCont

374 ((abelianizationInverseSystem S).projection i

375 (topologicalAbelianizationInverseLimitComparison S

376 (QuotientGroup.mk'

377 (Subgroup.closedCommutator S.inverseLimit) x))) := by

378 exact congrArg (TopologicalAbelianization.lift βiCont)

379 (π_topologicalAbelianizationInverseLimitComparison_mk (S := S) i x).symm

380 _ = TopologicalAbelianization.lift βiCont

381 ((abelianizationInverseSystem S).projection i 1) := by

382 rw [show topologicalAbelianizationInverseLimitComparison S

383 (QuotientGroup.mk' (Subgroup.closedCommutator S.inverseLimit) x) = 1 by

384 simpa [MonoidHom.mem_ker, f] using ha]

385 _ = TopologicalAbelianization.lift βiCont (1 : TopologicalAbelianization (S.X i)) := by

386 rfl

387 _ = 1 := by simp only [map_one]

388 exact haU <| (QuotientGroup.eq_one_iff

389 (N := (U : Subgroup (TopologicalAbelianization S.inverseLimit))) a).1 hq

390 · intro hx

391 rw [Subgroup.mem_bot] at hx

392 rw [MonoidHom.mem_ker]

393 simp only [ContinuousMonoidHom.coe_toMonoidHom, hx, map_one]

394 exact (MonoidHom.ker_eq_bot_iff (f := f.toMonoidHom)).mp hkerbot

395

396/--

397Membership in the inverse-limit closed commutator subgroup is equivalent to the displayed

398coordinate condition.

399-/

400theorem mem_closedCommutator_inverseLimit_iff

401 {I : Type u} [Preorder I] [Nonempty I]

402 {S : InverseSystems.InverseSystem (I := I)}

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

404 [∀ i, IsTopologicalGroup (S.X i)]

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

406 [∀ i, TotallyDisconnectedSpace (S.X i)]

407 (hdir : Directed (· ≤ ·) (id : I → I)) {x : S.inverseLimit} :

408 x ∈ Subgroup.closedCommutator S.inverseLimit ↔

409 ∀ i, S.projection i x ∈ Subgroup.closedCommutator (S.X i) := by

410 constructor

411 · intro hx i

412 have hxmk :

413 QuotientGroup.mk' (Subgroup.closedCommutator S.inverseLimit) x = 1 :=

414 (TopologicalAbelianization.mk_eq_one_iff (G := S.inverseLimit) (x := x)).2 hx

415 have hcoord :=

416 π_topologicalAbelianizationInverseLimitComparison_mk (S := S) i x

417 have hcoord' :

418 (abelianizationInverseSystem S).projection i

419 ((topologicalAbelianizationInverseLimitComparison S)

420 (QuotientGroup.mk' (Subgroup.closedCommutator S.inverseLimit) x)) =

421 QuotientGroup.mk' (Subgroup.closedCommutator (S.X i)) (S.projection i x) := by

422 exact hcoord

423 rw [hxmk] at hcoord'

424 have hmk :

425 QuotientGroup.mk' (Subgroup.closedCommutator (S.X i)) (S.projection i x) = 1 := by

426 exact hcoord'.symm.trans

427 (InverseSystems.projection_one (S := abelianizationInverseSystem S) i)

428 exact (TopologicalAbelianization.mk_eq_one_iff

429 (G := S.X i) (x := S.projection i x)).1 hmk

430 · intro hxcoord

431 let f := topologicalAbelianizationInverseLimitComparison S

432 have hf :

433 f (QuotientGroup.mk' (Subgroup.closedCommutator S.inverseLimit) x) = 1 := by

434 apply (abelianizationInverseSystem S).ext

435 intro i

436 have hmk :

437 QuotientGroup.mk' (Subgroup.closedCommutator (S.X i)) (S.projection i x) = 1 :=

438 (TopologicalAbelianization.mk_eq_one_iff

439 (G := S.X i) (x := S.projection i x)).2 (hxcoord i)

440 change (abelianizationInverseSystem S).projection i

441 (topologicalAbelianizationInverseLimitComparison S

442 (QuotientGroup.mk' (Subgroup.closedCommutator S.inverseLimit) x)) =

443 (abelianizationInverseSystem S).projection i 1

444 exact (π_topologicalAbelianizationInverseLimitComparison_mk (S := S) i x).trans

445 (hmk.trans

446 (InverseSystems.projection_one (S := abelianizationInverseSystem S) i).symm)

447 have hxmk :

448 QuotientGroup.mk' (Subgroup.closedCommutator S.inverseLimit) x = 1 := by

449 apply inj_topologicalAbelianizationInverseLimitComparison_of_profinite_inverse_system (S

450 := S) hdir

451 simpa only [f, map_one] using hf

452 exact (TopologicalAbelianization.mk_eq_one_iff (G := S.inverseLimit) (x := x)).1 hxmk

453

454/--

455The closed commutator subgroup of a profinite inverse limit is the infimum of the pullbacks of

456the stagewise closed commutator subgroups.

457-/

458theorem closedCommutator_inverseLimit_eq_iInf_comap

459 {I : Type u} [Preorder I] [Nonempty I]

460 (S : InverseSystems.InverseSystem (I := I))

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

462 [∀ i, IsTopologicalGroup (S.X i)]

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

464 [∀ i, TotallyDisconnectedSpace (S.X i)]

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

466 Subgroup.closedCommutator S.inverseLimit =

467 ⨅ i, (Subgroup.closedCommutator (S.X i)).comap

468 ({ toFun := S.projection i

469 map_one' := rfl

470 map_mul' := by intro x y; rfl } : S.inverseLimit →* S.X i) := by

471 ext x

472 rw [mem_closedCommutator_inverseLimit_iff (S := S) hdir (x := x)]

473 simp only [InverseSystems.InverseSystem.projection_apply, Subgroup.mem_iInf, Subgroup.mem_comap,

474 MonoidHom.coe_mk, OneHom.coe_mk]

475

476/--

477For the closed-commutator compatible family, the generic quotient-limit kernel is the closed

478commutator subgroup of the inverse limit.

479-/

480theorem closedCommutatorCompatibleClosedNormalSubgroups_inverseLimitKernel

481 {I : Type u} [Preorder I] [Nonempty I]

482 (S : InverseSystems.InverseSystem (I := I))

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

484 [∀ i, IsTopologicalGroup (S.X i)]

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

486 [∀ i, TotallyDisconnectedSpace (S.X i)]

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

488 (closedCommutatorCompatibleClosedNormalSubgroups S).inverseLimitKernel =

489 Subgroup.closedCommutator S.inverseLimit := by

490 symm

491 simpa [closedCommutatorCompatibleClosedNormalSubgroups,

492 InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.inverseLimitKernel,

493 InverseSystems.projectionHom]

494 using closedCommutator_inverseLimit_eq_iInf_comap (S := S) hdir

495

496/-- The generic quotient inverse-limit theorem specialized to the closed commutator family. -/

497noncomputable def closedCommutatorQuotientInverseLimitContinuousMulEquiv

498 {I : Type u} [Preorder I] [Nonempty I]

499 (S : InverseSystems.InverseSystem (I := I))

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

501 [∀ i, IsTopologicalGroup (S.X i)]

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

503 [∀ i, TotallyDisconnectedSpace (S.X i)]

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

505 TopologicalAbelianization S.inverseLimit ≃ₜ*

506 (closedCommutatorCompatibleClosedNormalSubgroups S).quotientInverseSystem.inverseLimit := by

507 let Q := closedCommutatorCompatibleClosedNormalSubgroups S

508 have hkernel :

509 (Subgroup.closedCommutator S.inverseLimit).map

510 (ContinuousMulEquiv.refl S.inverseLimit).toMulEquiv.toMonoidHom =

511 Q.inverseLimitKernel := by

512 rw [closedCommutatorCompatibleClosedNormalSubgroups_inverseLimitKernel (S := S) hdir]

513 ext x

514 constructor

515 · intro hx

516 rcases hx with ⟨y, hy, hyx⟩

517 simpa using hyx ▸ hy

518 · intro hx

519 exact ⟨x, hx, rfl⟩

520 exact (QuotientGroup.congrₜ

521 (Subgroup.closedCommutator S.inverseLimit) Q.inverseLimitKernel

522 (ContinuousMulEquiv.refl S.inverseLimit) hkernel).trans

523 (Q.quotientInverseLimitContinuousMulEquiv hdir)

524

525/--

526The projection closed commutator quotient inverse limit continuous multiplicative equivalence mk

527is compatible with the profinite topology and gives the continuous map or equivalence determined

528by the finite-quotient data.

529-/

530@[simp 900] theorem projection_closedCommutatorQuotientInverseLimitContinuousMulEquiv_mk

531 {I : Type u} [Preorder I] [Nonempty I]

532 (S : InverseSystems.InverseSystem (I := I))

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

534 [∀ i, IsTopologicalGroup (S.X i)]

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

536 [∀ i, TotallyDisconnectedSpace (S.X i)]

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

538 (i : I) (x : S.inverseLimit) :

539 (closedCommutatorCompatibleClosedNormalSubgroups S).quotientInverseSystem.projection i

540 (closedCommutatorQuotientInverseLimitContinuousMulEquiv (S := S) hdir

541 (QuotientGroup.mk' (Subgroup.closedCommutator S.inverseLimit) x)) =

542 QuotientGroup.mk'

543 ((closedCommutatorCompatibleClosedNormalSubgroups S).N i)

544 (S.projection i x) := by

545 let Q := closedCommutatorCompatibleClosedNormalSubgroups S

546 unfold closedCommutatorQuotientInverseLimitContinuousMulEquiv

547 dsimp

548 change Q.quotientInverseSystem.projection i

549 (Q.quotientInverseLimitContinuousMulEquiv hdir

550 (QuotientGroup.mk' Q.inverseLimitKernel x)) =

551 QuotientGroup.mk' (Q.N i) (S.projection i x)

552 unfold quotientInverseLimitContinuousMulEquiv

553 change Q.quotientInverseSystem.projection i

554 (Q.quotientInverseLimitComparison (QuotientGroup.mk' Q.inverseLimitKernel x)) =

555 QuotientGroup.mk' (Q.N i) (S.projection i x)

556 exact Q.projection_quotientInverseLimitComparison_mk i x

557

558/--

559Topological abelianization commutes with profinite inverse limits as a topological-group

560isomorphism.

561-/

562noncomputable def topologicalAbelianizationInverseLimitContinuousMulEquiv

563 {I : Type u} [Preorder I] [Nonempty I]

564 (S : InverseSystems.InverseSystem (I := I))

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

566 [∀ i, IsTopologicalGroup (S.X i)]

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

568 [∀ i, TotallyDisconnectedSpace (S.X i)]

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

570 TopologicalAbelianization S.inverseLimit ≃ₜ*

571 (abelianizationInverseSystem S).inverseLimit := by

572 let Q := closedCommutatorCompatibleClosedNormalSubgroups S

573 let E : InverseSystems.InverseSystem.InverseSystemIso Q.quotientInverseSystem

574 (abelianizationInverseSystem S) :=

575 { stageEquiv := fun _ => ContinuousMulEquiv.refl _

576 comm := by intro i j hij x; rfl }

577 exact (closedCommutatorQuotientInverseLimitContinuousMulEquiv (S := S) hdir).trans

578 E.inverseLimitContinuousMulEquiv

579

580/-- The inverse-limit comparison for topological abelianization evaluates coordinatewise. -/

581@[simp 900] theorem topologicalAbelianizationInverseLimitContinuousMulEquiv_apply

582 {I : Type u} [Preorder I] [Nonempty I]

583 (S : InverseSystems.InverseSystem (I := I))

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

585 [∀ i, IsTopologicalGroup (S.X i)]

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

587 [∀ i, TotallyDisconnectedSpace (S.X i)]

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

589 (x : TopologicalAbelianization S.inverseLimit) :

590 topologicalAbelianizationInverseLimitContinuousMulEquiv (S := S) hdir x =

591 topologicalAbelianizationInverseLimitComparison S x := by

592 refine Quotient.inductionOn' x ?_

593 intro g

594 apply (abelianizationInverseSystem S).ext

595 intro i

596 let Q := closedCommutatorCompatibleClosedNormalSubgroups S

597 let E : InverseSystems.InverseSystem.InverseSystemIso Q.quotientInverseSystem

598 (abelianizationInverseSystem S) :=

599 { stageEquiv := fun _ => ContinuousMulEquiv.refl _

600 comm := by intro i j hij x; rfl }

601 change (abelianizationInverseSystem S).projection i

602 (E.inverseLimitContinuousMulEquiv

603 ((closedCommutatorQuotientInverseLimitContinuousMulEquiv (S := S) hdir)

604 (QuotientGroup.mk'

605 (Subgroup.topologicalClosure (commutator S.inverseLimit)) g))) =

606 (abelianizationInverseSystem S).projection i

607 (topologicalAbelianizationInverseLimitComparison S

608 (QuotientGroup.mk'

609 (Subgroup.topologicalClosure (commutator S.inverseLimit)) g))

610 change (abelianizationInverseSystem S).projection i

611 (Q.quotientInverseSystem.limMap E.toMorphism

612 ((closedCommutatorQuotientInverseLimitContinuousMulEquiv (S := S) hdir)

613 (QuotientGroup.mk'

614 (Subgroup.topologicalClosure (commutator S.inverseLimit)) g))) =

615 (abelianizationInverseSystem S).projection i

616 (topologicalAbelianizationInverseLimitComparison S

617 (QuotientGroup.mk'

618 (Subgroup.topologicalClosure (commutator S.inverseLimit)) g))

619 rw [Q.quotientInverseSystem.π_limMap_apply E.toMorphism i]

620 change Q.quotientInverseSystem.projection i

621 ((closedCommutatorQuotientInverseLimitContinuousMulEquiv (S := S) hdir)

622 (QuotientGroup.mk'

623 (Subgroup.topologicalClosure (commutator S.inverseLimit)) g)) =

624 (abelianizationInverseSystem S).projection i

625 (topologicalAbelianizationInverseLimitComparison S

626 (QuotientGroup.mk'

627 (Subgroup.topologicalClosure (commutator S.inverseLimit)) g))

628 rw [projection_closedCommutatorQuotientInverseLimitContinuousMulEquiv_mk]

629 rw [π_topologicalAbelianizationInverseLimitComparison_mk]

630 rfl

631

632/-- The inverse-limit comparison is injective, as a corollary of the continuous equivalence. -/

633theorem injective_topologicalAbelianizationInverseLimitComparison

634 {I : Type u} [Preorder I] [Nonempty I]

635 (S : InverseSystems.InverseSystem (I := I))

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

637 [∀ i, IsTopologicalGroup (S.X i)]

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

639 [∀ i, TotallyDisconnectedSpace (S.X i)]

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

641 Function.Injective (topologicalAbelianizationInverseLimitComparison S) := by

642 let e := topologicalAbelianizationInverseLimitContinuousMulEquiv (S := S) hdir

643 intro x y hxy

644 apply e.injective

645 simpa [e] using hxy

646

647/-- The inverse-limit comparison is surjective, as a corollary of the continuous equivalence. -/

648theorem surjective_topologicalAbelianizationInverseLimitComparison

649 {I : Type u} [Preorder I] [Nonempty I]

650 (S : InverseSystems.InverseSystem (I := I))

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

652 [∀ i, IsTopologicalGroup (S.X i)]

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

654 [∀ i, TotallyDisconnectedSpace (S.X i)]

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

656 Function.Surjective (topologicalAbelianizationInverseLimitComparison S) := by

657 let e := topologicalAbelianizationInverseLimitContinuousMulEquiv (S := S) hdir

658 intro y

659 rcases e.surjective y with ⟨x, hx⟩

660 refine ⟨x, ?_⟩

661 simpa [e] using hx

662

663end ProCGroups.Abelian