Source: ProCGroups.CompletedGroupAlgebra.Basic.ClassComparison

1import ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Topology

2import ProCGroups.CompletedGroupAlgebra.Basic.InClass.Topology

4/-!

5# Completed Group Algebra / Basic / Class Comparison

7This module compares the all-finite and \(C\)-indexed named completed carriers through their

8canonical projections, and bundles the resulting inverse maps as ring, algebra, and topological

9equivalences for pro-\(C\) groups.

10-/

12open scoped Topology

14namespace CompletedGroupAlgebra

16noncomputable section

18open ProCGroups

19open ProCGroups.ProC

20open ProCGroups.InverseSystems

21open ProCGroups.Completion

23universe u v w

25variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

26variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

28/-- The projection from the all-finite completion to a stage indexed by a finite quotient class

29\(C\), bundled as a ring homomorphism. -/

30def completedGroupAlgebraProjectionToStageInClass

31 (C : ProCGroups.FiniteGroupClass.{v})

32 (U : CompletedGroupAlgebraIndexInClass G C) :

33 CompletedGroupAlgebraCarrier R G →+* CompletedGroupAlgebraStageInClass C R G U :=

34 completedGroupAlgebraProjection R G

35 (completedGroupAlgebraIndexInClassToAllFinite G C U)

37/--

38The all-finite projection to a \(C\)-indexed stage is compatible with the transition maps of the

39\(C\)-indexed tower.

40-/

41theorem completedGroupAlgebraProjectionToStageInClass_compatible

42 (C : ProCGroups.FiniteGroupClass.{v})

43 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)

44 (x : CompletedGroupAlgebraCarrier R G) :

45 completedGroupAlgebraTransitionInClass C R G hUV

46 (completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C V x) =

47 completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C U x := by

48 change completedGroupAlgebraTransition R G

49 (completedGroupAlgebraIndexInClassToAllFinite_le (G := G) C hUV)

50 (completedGroupAlgebraProjection R G

51 (completedGroupAlgebraIndexInClassToAllFinite G C V) x) =

52 completedGroupAlgebraProjection R G

53 (completedGroupAlgebraIndexInClassToAllFinite G C U) x

54 exact completedGroupAlgebraProjection_compatible (R := R) (G := G) x

55 (completedGroupAlgebraIndexInClassToAllFinite_le (G := G) C hUV)

57/--

58The comparison map from the ordinary all-finite completed group algebra to the inverse limit

59over any finite-quotient class.

60-/

61def completedGroupAlgebraToInClass

62 (C : ProCGroups.FiniteGroupClass.{v}) :

63 CompletedGroupAlgebraCarrier R G → CompletedGroupAlgebraInClass C R G :=

64 fun x =>

65 (completedGroupAlgebraInClassCompatibleFamilyEquiv

66 (R := R) (G := G) C).symm

67 ((completedGroupAlgebraSystemInClass C R G).inverseLimitLift

68 (fun U =>

69 completedGroupAlgebraProjectionToStageInClass

70 (R := R) (G := G) C U)

71 (by

72 intro U V hUV

73 funext x

74 exact completedGroupAlgebraProjectionToStageInClass_compatible

75 (R := R) (G := G) C hUV x) x)

77/--

78Projecting the comparison map \(\widehat{R[G]}\to\widehat{R[G]}_{C}\) to a \(C\)-indexed finite

79stage recovers the corresponding all-finite projection.

80-/

81@[simp]

82theorem completedGroupAlgebraToInClass_projection

83 (C : ProCGroups.FiniteGroupClass.{v})

84 (U : CompletedGroupAlgebraIndexInClass G C) (x : CompletedGroupAlgebraCarrier R G) :

85 completedGroupAlgebraProjectionInClass C R G U

86 (completedGroupAlgebraToInClass (R := R) (G := G) C x) =

87 completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C U x :=

88 rfl

90/--

91The comparison from the all-finite completed group algebra to the \(C\)-indexed inverse limit is

92bundled as a ring homomorphism.

93-/

94def completedGroupAlgebraToInClassRingHom

95 (C : ProCGroups.FiniteGroupClass.{v}) :

96 CompletedGroupAlgebraCarrier R G →+* CompletedGroupAlgebraInClass C R G where

97 toFun := completedGroupAlgebraToInClass (R := R) (G := G) C

98 map_zero' := by

99 apply completedGroupAlgebraInClass_ext (R := R) (G := G) C

100 intro U

101 rfl

102 map_one' := by

103 apply completedGroupAlgebraInClass_ext (R := R) (G := G) C

104 intro U

105 rfl

106 map_add' x y := by

107 apply completedGroupAlgebraInClass_ext (R := R) (G := G) C

108 intro U

109 rfl

110 map_mul' x y := by

111 apply completedGroupAlgebraInClass_ext (R := R) (G := G) C

112 intro U

113 rfl

114

115/--

116The comparison map from the all-finite completed group algebra to the \(C\)-indexed model is

117evaluated by reading the corresponding finite-stage coordinate.

118-/

119@[simp]

120theorem completedGroupAlgebraToInClassRingHom_apply

121 (C : ProCGroups.FiniteGroupClass.{v})

122 (x : CompletedGroupAlgebraCarrier R G) :

123 completedGroupAlgebraToInClassRingHom (R := R) (G := G) C x =

124 completedGroupAlgebraToInClass (R := R) (G := G) C x :=

125 rfl

126

127/--

128The comparison from the all-finite completed group algebra to the \(C\)-indexed inverse limit,

129as an \(R\)-algebra homomorphism.

130-/

131def completedGroupAlgebraToInClassAlgHom

132 (C : ProCGroups.FiniteGroupClass.{v}) :

133 CompletedGroupAlgebraCarrier R G →ₐ[R] CompletedGroupAlgebraInClass C R G where

134 toRingHom := completedGroupAlgebraToInClassRingHom (R := R) (G := G) C

135 commutes' := by

136 intro r

137 apply completedGroupAlgebraInClass_ext (R := R) (G := G) C

138 intro U

139 rfl

140

141/--

142The comparison map from the all-finite completed group algebra to the \(C\)-indexed model is

143evaluated by reading the corresponding finite-stage coordinate.

144-/

145@[simp]

146theorem completedGroupAlgebraToInClassAlgHom_apply

147 (C : ProCGroups.FiniteGroupClass.{v})

148 (x : CompletedGroupAlgebraCarrier R G) :

149 completedGroupAlgebraToInClassAlgHom (R := R) (G := G) C x =

150 completedGroupAlgebraToInClass (R := R) (G := G) C x :=

151 rfl

152

153/--

154The comparison map from the all-finite completed group algebra to the \(C\)-indexed completed

155group algebra is continuous for the inverse-limit topology.

156-/

157theorem continuous_completedGroupAlgebraToInClass

158 (C : ProCGroups.FiniteGroupClass.{v}) :

159 Continuous (completedGroupAlgebraToInClass (R := R) (G := G) C ) := by

160 let S := completedGroupAlgebraSystemInClass C R G

161 letI : ∀ U, TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=

162 fun U => (completedGroupAlgebraSystemInClass C R G).topologicalSpace U

163 let π : ∀ U : CompletedGroupAlgebraIndexInClass G C,

164 CompletedGroupAlgebraCarrier R G →

165 CompletedGroupAlgebraStageInClass C R G U :=

166 fun U => completedGroupAlgebraProjectionToStageInClass

167 (R := R) (G := G) C U

168 have hπ : ∀ U, Continuous (π U) := by

169 intro U

170 change Continuous ((completedGroupAlgebraSystem R G).projection

171 (completedGroupAlgebraIndexInClassToAllFinite G C U))

172 exact (completedGroupAlgebraSystem R G).continuous_projection

173 (completedGroupAlgebraIndexInClassToAllFinite G C U)

174 have hcompat : S.CompatibleMaps π := by

175 intro U V hUV

176 funext x

177 exact completedGroupAlgebraProjectionToStageInClass_compatible

178 (R := R) (G := G) C hUV x

179 change Continuous (S.inverseLimitLift π hcompat)

180 exact S.continuous_inverseLimitLift π hπ hcompat

181

182/--

183For a pro-\(C\) group, the \(C\)-indexed inverse limit maps back to the ordinary all-finite

184completed group algebra by reading the same open-normal quotient stages.

185-/

186def completedGroupAlgebraFromInClass

187 (C : ProCGroups.FiniteGroupClass.{v})

188 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :

189 CompletedGroupAlgebraInClass C R G → CompletedGroupAlgebraCarrier R G :=

190 fun x =>

191 (completedGroupAlgebraCompatibleFamilyEquiv (R := R) (G := G)).symm

192 ((completedGroupAlgebraSystem R G).inverseLimitLift

193 (fun U : CompletedGroupAlgebraIndex G =>

194 completedGroupAlgebraProjectionInClass C R G

195 (completedGroupAlgebraIndexToInClass G C hForm hG U))

196 (by

197 intro U V hUV

198 funext x

199 change completedGroupAlgebraTransitionInClass C R G

200 (completedGroupAlgebraIndexToInClass_le

201 (G := G) C hForm hG hUV)

202 (completedGroupAlgebraProjectionInClass C R G

203 (completedGroupAlgebraIndexToInClass G C hForm hG V) x) =

204 completedGroupAlgebraProjectionInClass C R G

205 (completedGroupAlgebraIndexToInClass G C hForm hG U) x

206 exact completedGroupAlgebraProjectionInClass_compatible

207 (R := R) (G := G) C

208 (completedGroupAlgebraIndexToInClass_le

209 (G := G) C hForm hG hUV) x) x)

210

211/--

212Projecting the comparison map \(\widehat{R[G]}_{C}\to\widehat{R[G]}\) to an all-finite stage

213recovers the matching \(C\)-indexed projection.

214-/

215@[simp]

216theorem completedGroupAlgebraFromInClass_projection

217 (C : ProCGroups.FiniteGroupClass.{v})

218 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (U :

219 CompletedGroupAlgebraIndex G)

220 (x : CompletedGroupAlgebraInClass C R G) :

221 completedGroupAlgebraProjection R G U

222 (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x) =

223 completedGroupAlgebraProjectionInClass C R G

224 (completedGroupAlgebraIndexToInClass G C hForm hG U) x :=

225 rfl

226

227/--

228The ring-homomorphism form of the comparison map is the bundled ring map determined by the

229underlying coordinate formula for the completed group algebra.

230-/

231def completedGroupAlgebraFromInClassRingHom

232 (C : ProCGroups.FiniteGroupClass.{v})

233 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :

234 CompletedGroupAlgebraInClass C R G →+* CompletedGroupAlgebraCarrier R G where

235 toFun := completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG

236 map_zero' := by

237 apply completedGroupAlgebra_ext (R := R) (G := G)

238 intro U

239 change completedGroupAlgebraProjection R G U

240 (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG 0) =

241 completedGroupAlgebraProjection R G U (0 : CompletedGroupAlgebraCarrier R G)

242 rw [completedGroupAlgebraFromInClass_projection]

243 exact map_zero (completedGroupAlgebraProjectionInClass C R G

244 (completedGroupAlgebraIndexToInClass G C hForm hG U))

245 map_one' := by

246 apply completedGroupAlgebra_ext (R := R) (G := G)

247 intro U

248 change completedGroupAlgebraProjection R G U

249 (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG 1) =

250 completedGroupAlgebraProjection R G U (1 : CompletedGroupAlgebraCarrier R G)

251 rw [completedGroupAlgebraFromInClass_projection]

252 exact map_one (completedGroupAlgebraProjectionInClass C R G

253 (completedGroupAlgebraIndexToInClass G C hForm hG U))

254 map_add' x y := by

255 apply completedGroupAlgebra_ext (R := R) (G := G)

256 intro U

257 change completedGroupAlgebraProjection R G U

258 (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG (x + y)) =

259 completedGroupAlgebraProjection R G U

260 (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x +

261 completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG y)

262 rw [completedGroupAlgebraFromInClass_projection]

263 exact map_add (completedGroupAlgebraProjectionInClass C R G

264 (completedGroupAlgebraIndexToInClass G C hForm hG U)) x y

265 map_mul' x y := by

266 apply completedGroupAlgebra_ext (R := R) (G := G)

267 intro U

268 change completedGroupAlgebraProjection R G U

269 (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG (x * y)) =

270 completedGroupAlgebraProjection R G U

271 (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x *

272 completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG y)

273 rw [completedGroupAlgebraFromInClass_projection]

274 exact map_mul (completedGroupAlgebraProjectionInClass C R G

275 (completedGroupAlgebraIndexToInClass G C hForm hG U)) x y

276

277/--

278The comparison map from the \(C\)-indexed completed group algebra to the all-finite model is

279evaluated by reading the corresponding finite-stage coordinate.

280-/

281@[simp]

282theorem completedGroupAlgebraFromInClassRingHom_apply

283 (C : ProCGroups.FiniteGroupClass.{v})

284 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :

285 CompletedGroupAlgebraInClass C R G) :

286 completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG x =

287 completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x :=

288 rfl

289

290/--

291The algebra homomorphism form of the comparison map is the bundled algebra map determined by the

292underlying coordinate formula for the completed group algebra.

293-/

294def completedGroupAlgebraFromInClassAlgHom

295 (C : ProCGroups.FiniteGroupClass.{v})

296 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :

297 CompletedGroupAlgebraInClass C R G →ₐ[R] CompletedGroupAlgebraCarrier R G where

298 toRingHom := completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG

299 commutes' := by

300 intro r

301 apply completedGroupAlgebra_ext (R := R) (G := G)

302 intro U

303 change completedGroupAlgebraProjection R G U

304 (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG

305 (algebraMap R (CompletedGroupAlgebraInClass C R G) r)) =

306 completedGroupAlgebraProjection R G U (algebraMap R (CompletedGroupAlgebraCarrier R G) r)

307 rw [completedGroupAlgebraFromInClass_projection]

308 change completedGroupAlgebraProjectionInClass C R G

309 (completedGroupAlgebraIndexToInClass G C hForm hG U)

310 (algebraMap R (CompletedGroupAlgebraInClass C R G) r) =

311 algebraMap R (CompletedGroupAlgebraStage R G U) r

312 exact completedGroupAlgebraProjectionInClass_algebraMap (R := R) (G := G) C

313 (completedGroupAlgebraIndexToInClass G C hForm hG U) r

314

315/--

316The comparison map from the \(C\)-indexed completed group algebra to the all-finite model is

317evaluated by reading the corresponding finite-stage coordinate.

318-/

319@[simp]

320theorem completedGroupAlgebraFromInClassAlgHom_apply

321 (C : ProCGroups.FiniteGroupClass.{v})

322 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :

323 CompletedGroupAlgebraInClass C R G) :

324 completedGroupAlgebraFromInClassAlgHom (R := R) (G := G) C hForm hG x =

325 completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x :=

326 rfl

327

328/--

329The comparison map from the \(C\)-indexed completed group algebra to the all-finite completed

330group algebra is continuous for the inverse-limit topology.

331-/

332theorem continuous_completedGroupAlgebraFromInClass

333 (C : ProCGroups.FiniteGroupClass.{v})

334 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :

335 Continuous (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG) := by

336 let S := completedGroupAlgebraSystem R G

337 letI : ∀ U, TopologicalSpace (CompletedGroupAlgebraStage R G U) :=

338 fun U => (completedGroupAlgebraSystem R G).topologicalSpace U

339 let π : ∀ U : CompletedGroupAlgebraIndex G,

340 CompletedGroupAlgebraInClass C R G →

341 CompletedGroupAlgebraStage R G U :=

342 fun U => completedGroupAlgebraProjectionInClass C R G

343 (completedGroupAlgebraIndexToInClass G C hForm hG U)

344 have hπ : ∀ U, Continuous (π U) := by

345 intro U

346 letI : TopologicalSpace

347 (CompletedGroupAlgebraStageInClass C R G (completedGroupAlgebraIndexToInClass G C hForm

348 hG U)) :=

349 (completedGroupAlgebraSystemInClass C R G).topologicalSpace

350 (completedGroupAlgebraIndexToInClass G C hForm hG U)

351 change Continuous (completedGroupAlgebraProjectionInClass C R G

352 (completedGroupAlgebraIndexToInClass G C hForm hG U))

353 simpa using continuous_completedGroupAlgebraProjectionInClass

354 (R := R) (G := G) C (completedGroupAlgebraIndexToInClass G C hForm hG U)

355 have hcompat : S.CompatibleMaps π := by

356 intro U V hUV

357 funext x

358 change completedGroupAlgebraTransitionInClass C R G

359 (completedGroupAlgebraIndexToInClass_le

360 (G := G) C hForm hG hUV)

361 (completedGroupAlgebraProjectionInClass C R G

362 (completedGroupAlgebraIndexToInClass G C hForm hG V) x) =

363 completedGroupAlgebraProjectionInClass C R G

364 (completedGroupAlgebraIndexToInClass G C hForm hG U) x

365 exact completedGroupAlgebraProjectionInClass_compatible

366 (R := R) (G := G) C

367 (completedGroupAlgebraIndexToInClass_le

368 (G := G) C hForm hG hUV) x

369 change Continuous (S.inverseLimitLift π hcompat)

370 exact S.continuous_inverseLimitLift π hπ hcompat

371

372/--

373The composite from a \(C\)-indexed completion to the all-finite completion and back is the

374identity on the \(C\)-indexed completion.

375-/

376@[simp]

377theorem completedGroupAlgebraFromInClass_toInClass

378 (C : ProCGroups.FiniteGroupClass.{v})

379 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :

380 CompletedGroupAlgebraCarrier R G) :

381 completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG

382 (completedGroupAlgebraToInClass (R := R) (G := G) C x) = x := by

383 apply completedGroupAlgebra_ext (R := R) (G := G)

384 intro U

385 rw [completedGroupAlgebraFromInClass_projection, completedGroupAlgebraToInClass_projection]

386 change completedGroupAlgebraProjection R G

387 (completedGroupAlgebraIndexInClassToAllFinite G C

388 (completedGroupAlgebraIndexToInClass G C hForm hG U)) x =

389 completedGroupAlgebraProjection R G U x

390 cases U

391 rfl

392

393/--

394The composite from the all-finite completion to the \(C\)-indexed completion and back is the

395identity on the all-finite completion.

396-/

397@[simp]

398theorem completedGroupAlgebraToInClass_fromInClass

399 (C : ProCGroups.FiniteGroupClass.{v})

400 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :

401 CompletedGroupAlgebraInClass C R G) :

402 completedGroupAlgebraToInClass (R := R) (G := G) C

403 (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x) = x := by

404 apply completedGroupAlgebraInClass_ext (R := R) (G := G) C

405 intro U

406 rw [completedGroupAlgebraToInClass_projection]

407 change completedGroupAlgebraProjection R G

408 (completedGroupAlgebraIndexInClassToAllFinite G C U)

409 (completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x) =

410 completedGroupAlgebraProjectionInClass C R G U x

411 rw [completedGroupAlgebraFromInClass_projection]

412 change completedGroupAlgebraProjectionInClass C R G

413 (completedGroupAlgebraIndexToInClass G C hForm hG

414 (completedGroupAlgebraIndexInClassToAllFinite G C U)) x =

415 completedGroupAlgebraProjectionInClass C R G U x

416 cases U

417 rfl

418

419/-- The two comparison ring homomorphisms are inverse to one another after composition. -/

420@[simp]

421theorem completedGroupAlgebraFromInClassRingHom_comp_toInClassRingHom

422 (C : ProCGroups.FiniteGroupClass.{v})

423 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :

424 (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG).comp

425 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ) =

426 RingHom.id (CompletedGroupAlgebraCarrier R G) := by

427 apply RingHom.ext

428 intro x

429 exact completedGroupAlgebraFromInClass_toInClass (R := R) (G := G) C hForm hG x

430

431/-- The two comparison ring homomorphisms are inverse to one another after composition. -/

432@[simp]

433theorem completedGroupAlgebraToInClassRingHom_comp_fromInClassRingHom

434 (C : ProCGroups.FiniteGroupClass.{v})

435 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :

436 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ).comp

437 (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG) =

438 RingHom.id (CompletedGroupAlgebraInClass C R G) := by

439 apply RingHom.ext

440 intro x

441 exact completedGroupAlgebraToInClass_fromInClass (R := R) (G := G) C hForm hG x

442

443/--

444For a pro-\(C\) group, the all-finite and \(C\)-indexed completed group algebras are the same

445ring, via the comparison maps.

446-/

447def completedGroupAlgebraInClassRingEquiv

448 (C : ProCGroups.FiniteGroupClass.{v})

449 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :

450 CompletedGroupAlgebraCarrier R G ≃+* CompletedGroupAlgebraInClass C R G where

451 toFun := completedGroupAlgebraToInClass (R := R) (G := G) C

452 invFun := completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG

453 left_inv := by

454 intro x

455 exact completedGroupAlgebraFromInClass_toInClass (R := R) (G := G) C hForm hG x

456 right_inv := by

457 intro x

458 exact completedGroupAlgebraToInClass_fromInClass (R := R) (G := G) C hForm hG x

459 map_mul' := by

460 intro x y

461 exact map_mul (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ) x y

462 map_add' := by

463 intro x y

464 exact map_add (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ) x y

465

466/--

467The comparison equivalence is evaluated by the underlying all-finite or \(C\)-indexed comparison

468map.

469-/

470@[simp]

471theorem completedGroupAlgebraInClassRingEquiv_apply

472 (C : ProCGroups.FiniteGroupClass.{v})

473 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :

474 CompletedGroupAlgebraCarrier R G) :

475 completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hForm hG x =

476 completedGroupAlgebraToInClass (R := R) (G := G) C x :=

477 rfl

478

479/--

480The comparison equivalence is evaluated by the underlying all-finite or \(C\)-indexed comparison

481map.

482-/

483@[simp]

484theorem completedGroupAlgebraInClassRingEquiv_symm_apply

485 (C : ProCGroups.FiniteGroupClass.{v})

486 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :

487 CompletedGroupAlgebraInClass C R G) :

488 (completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hForm hG).symm x =

489 completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x :=

490 rfl

491

492/--

493For a pro-\(C\) group, the all-finite and \(C\)-indexed completed group algebras are the same

494\(R\)-algebra.

495-/

496def completedGroupAlgebraInClassAlgEquiv

497 (C : ProCGroups.FiniteGroupClass.{v})

498 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :

499 CompletedGroupAlgebraCarrier R G ≃ₐ[R] CompletedGroupAlgebraInClass C R G :=

500 AlgEquiv.ofRingEquiv (f := completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hForm hG)

501 (by

502 intro r

503 rfl)

504

505/--

506The comparison equivalence is evaluated by the underlying all-finite or \(C\)-indexed comparison

507map.

508-/

509@[simp]

510theorem completedGroupAlgebraInClassAlgEquiv_apply

511 (C : ProCGroups.FiniteGroupClass.{v})

512 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :

513 CompletedGroupAlgebraCarrier R G) :

514 completedGroupAlgebraInClassAlgEquiv (R := R) (G := G) C hForm hG x =

515 completedGroupAlgebraToInClass (R := R) (G := G) C x :=

516 rfl

517

518/--

519The comparison equivalence is evaluated by the underlying all-finite or \(C\)-indexed comparison

520map.

521-/

522@[simp]

523theorem completedGroupAlgebraInClassAlgEquiv_symm_apply

524 (C : ProCGroups.FiniteGroupClass.{v})

525 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :

526 CompletedGroupAlgebraInClass C R G) :

527 (completedGroupAlgebraInClassAlgEquiv (R := R) (G := G) C hForm hG).symm x =

528 completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x :=

529 rfl

530

531/-- The comparison equivalence is an equivalence of topological spaces. -/

532def completedGroupAlgebraInClassHomeomorph

533 (C : ProCGroups.FiniteGroupClass.{v})

534 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :

535 CompletedGroupAlgebraCarrier R G ≃ₜ CompletedGroupAlgebraInClass C R G where

536 toEquiv := (completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hForm hG).toEquiv

537 continuous_toFun := continuous_completedGroupAlgebraToInClass (R := R) (G := G) C

538 continuous_invFun := continuous_completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG

539

540/--

541The comparison homeomorphism is evaluated by the underlying all-finite or \(C\)-indexed

542comparison map.

543-/

544@[simp]

545theorem completedGroupAlgebraInClassHomeomorph_apply

546 (C : ProCGroups.FiniteGroupClass.{v})

547 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :

548 CompletedGroupAlgebraCarrier R G) :

549 completedGroupAlgebraInClassHomeomorph (R := R) (G := G) C hForm hG x =

550 completedGroupAlgebraToInClass (R := R) (G := G) C x :=

551 rfl

552

553/--

554The comparison homeomorphism is evaluated by the underlying all-finite or \(C\)-indexed

555comparison map.

556-/

557@[simp]

558theorem completedGroupAlgebraInClassHomeomorph_symm_apply

559 (C : ProCGroups.FiniteGroupClass.{v})

560 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) (x :

561 CompletedGroupAlgebraInClass C R G) :

562 (completedGroupAlgebraInClassHomeomorph (R := R) (G := G) C hForm hG).symm x =

563 completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x :=

564 rfl

565

566/--

567Surjectivity of the induced map is obtained from surjectivity on the underlying quotient or

568dense algebraic model, together with closedness of the image in the completed target.

569-/

570theorem completedGroupAlgebraToInClass_surjective

571 (C : ProCGroups.FiniteGroupClass.{v})

572 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :

573 Function.Surjective (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ) := by

574 intro x

575 refine ⟨completedGroupAlgebraFromInClass (R := R) (G := G) C hForm hG x, ?_⟩

576 exact completedGroupAlgebraToInClass_fromInClass (R := R) (G := G) C hForm hG x

577

578/--

579Surjectivity of the induced map is obtained from surjectivity on the underlying quotient or

580dense algebraic model, together with closedness of the image in the completed target.

581-/

582theorem completedGroupAlgebraFromInClass_surjective

583 (C : ProCGroups.FiniteGroupClass.{v})

584 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :

585 Function.Surjective (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG) := by

586 intro x

587 refine ⟨completedGroupAlgebraToInClass (R := R) (G := G) C x, ?_⟩

588 exact completedGroupAlgebraFromInClass_toInClass (R := R) (G := G) C hForm hG x

589

590end

591

592end CompletedGroupAlgebra