Source: ProCGroups.CompletedGroupAlgebra.UniversalProperty.Basic

1import ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteComparison

2import ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.GroupLike

3import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

5/-!

6# Completed Group Algebra / Universal Property / Basic

8This module packages canonical completed-group-algebra models by their finite-stage cone and

9inverse-limit universal property, derives comparison equivalences, and develops the continuous

10group-like map and its spanning properties.

11-/

13open scoped Topology

15namespace CompletedGroupAlgebra

17noncomputable section

19open ProCGroups

20open ProCGroups.ProC

21open ProCGroups.InverseSystems

22open ProCGroups.Completion

24universe u v w z

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

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

29/-- Certificate that a profinite ring realizes the inverse limit of the finite group algebras

30`R[G/U]` for bundled profinite coefficients and group.

32The data are the bundled finite-stage ring homomorphisms, their compatibility with the specified

33algebraic map, and the inverse-limit universal property. Continuity and transition compatibility

34of the projections are contained in `isInverseLimit`. In particular, no comparison with the

35canonical carrier is assumed: the comparison homeomorphism and ring equivalence below are derived

36from the universal property. Profiniteness is inherited from the three bundled objects rather

37than repeated as certificate fields. -/

38structure CanonicalCompletedGroupAlgebraModel

39 (R : ProfiniteCommRing.{u}) (G : ProfiniteGrp.{v}) (RG : ProfiniteRing.{w})

40 (algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG) where

41 /-- The projection from the candidate model to each finite group-algebra stage. -/

42 stageProjection : ∀ U : CompletedGroupAlgebraIndex G,

43 RG →+* CompletedGroupAlgebraStage R G U

44 /-- Each stage projection agrees with the canonical stage map on the algebraic source. -/

45 stageProjection_comp_algebraicMap : ∀ U : CompletedGroupAlgebraIndex G,

46 (stageProjection U).comp algebraicMap = completedGroupAlgebraNaturalSourceStageMap R G U

47 /-- The stage projections exhibit the candidate carrier as the inverse limit. -/

48 isInverseLimit :

49 (completedGroupAlgebraSystem R G).IsInverseLimit

50 (fun U x => stageProjection U x)

52namespace CanonicalCompletedGroupAlgebraModel

54variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}

55variable {RG : ProfiniteRing.{w}}

56variable {algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* RG}

58/-- Each model projection is continuous, as a consequence of the inverse-limit witness. -/

59theorem stageProjection_continuous

60 (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap)

61 (U : CompletedGroupAlgebraIndex G) :

62 letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=

63 (completedGroupAlgebraSystem R G).topologicalSpace U

64 Continuous (h.stageProjection U) := by

65 letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=

66 (completedGroupAlgebraSystem R G).topologicalSpace U

67 exact h.isInverseLimit.continuous_proj U

69/-- Model projections commute with finite-stage transition ring homomorphisms. -/

70theorem stageProjection_compatible

71 (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap)

72 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :

73 (completedGroupAlgebraTransition R G hUV).comp (h.stageProjection V) =

74 h.stageProjection U := by

75 apply RingHom.ext

76 intro x

77 change

78 (completedGroupAlgebraSystem R G).map hUV (h.stageProjection V x) =

79 h.stageProjection U x

80 exact congrFun (h.isInverseLimit.compatible U V hUV) x

82/-- The comparison homeomorphism with the concrete inverse-limit carrier, derived solely from

83the two inverse-limit universal properties. -/

84noncomputable def comparisonHomeomorph

85 (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :

86 RG ≃ₜ CompletedGroupAlgebraCarrier R G :=

87 h.isInverseLimit.homeomorphToInverseLimit

89/-- The derived comparison is characterized by every finite-stage projection. -/

90@[simp]

91theorem completedGroupAlgebraProjection_comparisonHomeomorph

92 (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap)

93 (U : CompletedGroupAlgebraIndex G) (x : RG) :

94 completedGroupAlgebraProjection R G U (h.comparisonHomeomorph x) =

95 h.stageProjection U x := by

96 rfl

98/-- The comparison homeomorphism preserves the ring operations because all model projections are

99ring homomorphisms. -/

100noncomputable def comparisonRingEquiv

101 (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :

102 RG ≃+* CompletedGroupAlgebraCarrier R G where

103 toEquiv := h.comparisonHomeomorph.toEquiv

104 map_add' x y := by

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

106 intro U

107 change completedGroupAlgebraProjection R G U (h.comparisonHomeomorph (x + y)) =

108 completedGroupAlgebraProjection R G U

109 (h.comparisonHomeomorph x + h.comparisonHomeomorph y)

110 calc

111 completedGroupAlgebraProjection R G U (h.comparisonHomeomorph (x + y)) =

112 h.stageProjection U (x + y) :=

113 h.completedGroupAlgebraProjection_comparisonHomeomorph U (x + y)

114 _ = h.stageProjection U x + h.stageProjection U y := map_add _ x y

115 _ = completedGroupAlgebraProjection R G U (h.comparisonHomeomorph x) +

116 completedGroupAlgebraProjection R G U (h.comparisonHomeomorph y) :=

117 congrArg₂ (· + ·)

118 (h.completedGroupAlgebraProjection_comparisonHomeomorph U x).symm

119 (h.completedGroupAlgebraProjection_comparisonHomeomorph U y).symm

120 _ = completedGroupAlgebraProjection R G U

121 (h.comparisonHomeomorph x + h.comparisonHomeomorph y) :=

122 (map_add (completedGroupAlgebraProjection R G U) _ _).symm

123 map_mul' x y := by

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

125 intro U

126 change completedGroupAlgebraProjection R G U (h.comparisonHomeomorph (x * y)) =

127 completedGroupAlgebraProjection R G U

128 (h.comparisonHomeomorph x * h.comparisonHomeomorph y)

129 calc

130 completedGroupAlgebraProjection R G U (h.comparisonHomeomorph (x * y)) =

131 h.stageProjection U (x * y) :=

132 h.completedGroupAlgebraProjection_comparisonHomeomorph U (x * y)

133 _ = h.stageProjection U x * h.stageProjection U y := map_mul _ x y

134 _ = completedGroupAlgebraProjection R G U (h.comparisonHomeomorph x) *

135 completedGroupAlgebraProjection R G U (h.comparisonHomeomorph y) :=

136 congrArg₂ (· * ·)

137 (h.completedGroupAlgebraProjection_comparisonHomeomorph U x).symm

138 (h.completedGroupAlgebraProjection_comparisonHomeomorph U y).symm

139 _ = completedGroupAlgebraProjection R G U

140 (h.comparisonHomeomorph x * h.comparisonHomeomorph y) :=

141 (map_mul (completedGroupAlgebraProjection R G U) _ _).symm

142

143/-- Ring-equivalence form of the finite-stage characterization. -/

144@[simp]

145theorem completedGroupAlgebraProjection_comparisonRingEquiv

146 (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap)

147 (U : CompletedGroupAlgebraIndex G) (x : RG) :

148 completedGroupAlgebraProjection R G U (h.comparisonRingEquiv x) =

149 h.stageProjection U x :=

150 h.completedGroupAlgebraProjection_comparisonHomeomorph U x

151

152/-- The derived comparison ring equivalence is continuous. -/

153theorem comparisonRingEquiv_continuous

154 (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :

155 Continuous h.comparisonRingEquiv := by

156 change Continuous h.comparisonHomeomorph

157 exact h.comparisonHomeomorph.continuous

158

159/-- The inverse of the derived comparison ring equivalence is continuous. -/

160theorem comparisonRingEquiv_symm_continuous

161 (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :

162 Continuous h.comparisonRingEquiv.symm := by

163 change Continuous h.comparisonHomeomorph.symm

164 exact h.comparisonHomeomorph.symm.continuous

165

166/-- The derived comparison extends the specified algebraic map. -/

167@[simp]

168theorem comparisonRingEquiv_algebraicMap

169 (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap)

170 (x : CompletedGroupAlgebraNaturalSource R G) :

171 h.comparisonRingEquiv (algebraicMap x) =

172 toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G) x := by

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

174 intro U

175 calc

176 completedGroupAlgebraProjection R G U

177 (h.comparisonRingEquiv (algebraicMap x)) =

178 h.stageProjection U (algebraicMap x) :=

179 h.completedGroupAlgebraProjection_comparisonRingEquiv U (algebraicMap x)

180 _ = completedGroupAlgebraNaturalSourceStageMap R G U x :=

181 congrFun (congrArg DFunLike.coe (h.stageProjection_comp_algebraicMap U)) x

182 _ = completedGroupAlgebraProjection R G U

183 (toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G) x) := by

184 rw [completedGroupAlgebraNaturalSourceStageMap_apply]

185 change completedGroupAlgebraStageMap R G U x.toMonoidAlgebra =

186 completedGroupAlgebraProjection R G U

187 (toCompletedGroupAlgebra R G x.toMonoidAlgebra)

188 exact

189 (completedGroupAlgebraProjection_toCompletedGroupAlgebra

190 (R := R) (G := G) U x.toMonoidAlgebra).symm

191

192/-- Bundled ring-homomorphism form of algebraic-map compatibility. -/

193theorem comparisonRingEquiv_comp_algebraicMap

194 (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :

195 h.comparisonRingEquiv.toRingHom.comp algebraicMap =

196 toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G) := by

197 apply RingHom.ext

198 intro x

199 exact h.comparisonRingEquiv_algebraicMap x

200

201/-- The specified algebraic map is forced by the finite-stage cone: it is the canonical map

202followed by the inverse comparison equivalence. -/

203theorem algebraicMap_eq_comparisonRingEquiv_symm_comp

204 (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :

205 algebraicMap = h.comparisonRingEquiv.symm.toRingHom.comp

206 (toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G)) := by

207 apply RingHom.ext

208 intro x

209 apply h.comparisonRingEquiv.injective

210 change h.comparisonRingEquiv (algebraicMap x) =

211 h.comparisonRingEquiv

212 (h.comparisonRingEquiv.symm

213 (toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G) x))

214 calc

215 h.comparisonRingEquiv (algebraicMap x) =

216 toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G) x :=

217 h.comparisonRingEquiv_algebraicMap x

218 _ = h.comparisonRingEquiv

219 (h.comparisonRingEquiv.symm

220 (toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G) x)) :=

221 (h.comparisonRingEquiv.apply_symm_apply _).symm

222

223/-- Continuity of the specified algebraic map is derived from the inverse-limit comparison. -/

224theorem algebraicMap_continuous

225 (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :

226 Continuous algebraicMap := by

227 rw [h.algebraicMap_eq_comparisonRingEquiv_symm_comp]

228 exact h.comparisonRingEquiv_symm_continuous.comp

229 (continuous_toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G))

230

231/-- Density of the specified algebraic map is likewise forced by the canonical inverse-limit

232model; it is not independent structure data. -/

233theorem algebraicMap_dense

234 (h : CanonicalCompletedGroupAlgebraModel R G RG algebraicMap) :

235 DenseRange algebraicMap := by

236 rw [h.algebraicMap_eq_comparisonRingEquiv_symm_comp]

237 exact h.comparisonRingEquiv.symm.surjective.denseRange.comp

238 (denseRange_toCompletedGroupAlgebraNaturalSourceRingHom

239 (R := R) (G := G))

240 h.comparisonRingEquiv_symm_continuous

241

242variable {RG₁ : ProfiniteRing.{w}} {RG₂ : ProfiniteRing.{z}}

243variable {algebraicMap₁ : CompletedGroupAlgebraNaturalSource R G →+* RG₁}

244variable {algebraicMap₂ : CompletedGroupAlgebraNaturalSource R G →+* RG₂}

245

246/-- The canonical homeomorphism between two finite-stage inverse-limit models. -/

247noncomputable def modelToModelHomeomorph

248 (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)

249 (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂) :

250 RG₁ ≃ₜ RG₂ :=

251 h₁.comparisonHomeomorph.trans h₂.comparisonHomeomorph.symm

252

253/-- The canonical ring equivalence between two finite-stage inverse-limit models. -/

254noncomputable def modelToModelRingEquiv

255 (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)

256 (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂) :

257 RG₁ ≃+* RG₂ :=

258 h₁.comparisonRingEquiv.trans h₂.comparisonRingEquiv.symm

259

260/-- The model-to-model equivalence commutes with every finite-stage projection. -/

261@[simp]

262theorem stageProjection_modelToModelRingEquiv

263 (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)

264 (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂)

265 (U : CompletedGroupAlgebraIndex G) (x : RG₁) :

266 h₂.stageProjection U (h₁.modelToModelRingEquiv h₂ x) =

267 h₁.stageProjection U x := by

268 change h₂.stageProjection U

269 (h₂.comparisonRingEquiv.symm (h₁.comparisonRingEquiv x)) =

270 h₁.stageProjection U x

271 calc

272 h₂.stageProjection U

273 (h₂.comparisonRingEquiv.symm (h₁.comparisonRingEquiv x)) =

274 completedGroupAlgebraProjection R G U

275 (h₂.comparisonRingEquiv

276 (h₂.comparisonRingEquiv.symm (h₁.comparisonRingEquiv x))) :=

277 (h₂.completedGroupAlgebraProjection_comparisonRingEquiv U

278 (h₂.comparisonRingEquiv.symm (h₁.comparisonRingEquiv x))).symm

279 _ = completedGroupAlgebraProjection R G U (h₁.comparisonRingEquiv x) := by

280 rw [RingEquiv.apply_symm_apply]

281 _ = h₁.stageProjection U x :=

282 h₁.completedGroupAlgebraProjection_comparisonRingEquiv U x

283

284/-- The canonical model-to-model ring equivalence is continuous. -/

285theorem modelToModelRingEquiv_continuous

286 (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)

287 (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂) :

288 Continuous (h₁.modelToModelRingEquiv h₂) := by

289 change Continuous (h₁.modelToModelHomeomorph h₂)

290 exact (h₁.modelToModelHomeomorph h₂).continuous

291

292/-- The inverse of the canonical model-to-model ring equivalence is continuous. -/

293theorem modelToModelRingEquiv_symm_continuous

294 (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)

295 (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂) :

296 Continuous (h₁.modelToModelRingEquiv h₂).symm := by

297 change Continuous (h₁.modelToModelHomeomorph h₂).symm

298 exact (h₁.modelToModelHomeomorph h₂).symm.continuous

299

300/-- The canonical model-to-model equivalence carries one specified algebraic map to the other. -/

301@[simp]

302theorem modelToModelRingEquiv_algebraicMap

303 (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)

304 (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂)

305 (x : CompletedGroupAlgebraNaturalSource R G) :

306 h₁.modelToModelRingEquiv h₂ (algebraicMap₁ x) = algebraicMap₂ x := by

307 apply h₂.comparisonRingEquiv.injective

308 change h₂.comparisonRingEquiv

309 (h₂.comparisonRingEquiv.symm

310 (h₁.comparisonRingEquiv (algebraicMap₁ x))) =

311 h₂.comparisonRingEquiv (algebraicMap₂ x)

312 rw [RingEquiv.apply_symm_apply, h₁.comparisonRingEquiv_algebraicMap,

313 h₂.comparisonRingEquiv_algebraicMap]

314

315/-- Bundled ring-homomorphism form of model-to-model algebraic-map compatibility. -/

316theorem modelToModelRingEquiv_comp_algebraicMap

317 (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)

318 (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂) :

319 (h₁.modelToModelRingEquiv h₂).toRingHom.comp algebraicMap₁ = algebraicMap₂ := by

320 apply RingHom.ext

321 intro x

322 exact h₁.modelToModelRingEquiv_algebraicMap h₂ x

323

324/-- A ring equivalence commuting with all finite-stage projections is the canonical

325model-to-model equivalence. Joint injectivity of the canonical stage projections makes a

326separate continuity hypothesis unnecessary. -/

327theorem modelToModelRingEquiv_unique

328 (h₁ : CanonicalCompletedGroupAlgebraModel R G RG₁ algebraicMap₁)

329 (h₂ : CanonicalCompletedGroupAlgebraModel R G RG₂ algebraicMap₂)

330 (e : RG₁ ≃+* RG₂)

331 (hstage : ∀ U : CompletedGroupAlgebraIndex G,

332 (h₂.stageProjection U).comp e.toRingHom = h₁.stageProjection U) :

333 e = h₁.modelToModelRingEquiv h₂ := by

334 apply RingEquiv.ext

335 intro x

336 apply h₂.comparisonRingEquiv.injective

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

338 intro U

339 calc

340 completedGroupAlgebraProjection R G U (h₂.comparisonRingEquiv (e x)) =

341 h₂.stageProjection U (e x) :=

342 h₂.completedGroupAlgebraProjection_comparisonRingEquiv U (e x)

343 _ = h₁.stageProjection U x :=

344 congrFun (congrArg DFunLike.coe (hstage U)) x

345 _ = h₂.stageProjection U (h₁.modelToModelRingEquiv h₂ x) :=

346 (h₁.stageProjection_modelToModelRingEquiv h₂ U x).symm

347 _ = completedGroupAlgebraProjection R G U

348 (h₂.comparisonRingEquiv (h₁.modelToModelRingEquiv h₂ x)) :=

349 (h₂.completedGroupAlgebraProjection_comparisonRingEquiv U

350 (h₁.modelToModelRingEquiv h₂ x)).symm

351

352end CanonicalCompletedGroupAlgebraModel

353

354/-- A completed group algebra model whose coefficient ring, profinite carrier, and group are

355genuine bundled objects.

356

357The data fields contain the algebraic map and the finite-stage cone with its universal property.

358Continuity, density, and carrier profiniteness are theorems forced by comparison with the concrete

359inverse limit; they are not stored as independent witnesses. Likewise, all input profiniteness

360structure is inherited from the objects. `CompletedGroupAlgebraModel.certificate` reconstructs

361the finite-stage certificate when needed. -/

362structure CompletedGroupAlgebraModel

363 (R : ProfiniteCommRing.{u}) (G : ProfiniteGrp.{v}) where

364 /-- The profinite ring underlying the completed group-algebra model. -/

365 carrier : ProfiniteRing.{w}

366 /-- The canonical map from the algebraic group algebra into the model. -/

367 algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* carrier

368 /-- The projection from the model to each finite group-algebra stage. -/

369 stageProjection : ∀ U : CompletedGroupAlgebraIndex G,

370 carrier →+* CompletedGroupAlgebraStage R G U

371 /-- Each stage projection agrees with the canonical stage map on the algebraic source. -/

372 stageProjection_comp_algebraicMap : ∀ U : CompletedGroupAlgebraIndex G,

373 (stageProjection U).comp algebraicMap = completedGroupAlgebraNaturalSourceStageMap R G U

374 /-- The stage projections exhibit the model carrier as the inverse limit. -/

375 isInverseLimit :

376 (completedGroupAlgebraSystem R G).IsInverseLimit

377 (fun U x => stageProjection U x)

378

379namespace CompletedGroupAlgebraModel

380

381variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}

382

383/-- Expose the bundled model's finite-stage inverse-limit certificate. -/

384def certificate (M : CompletedGroupAlgebraModel R G) :

385 CanonicalCompletedGroupAlgebraModel R G M.carrier M.algebraicMap where

386 stageProjection := M.stageProjection

387 stageProjection_comp_algebraicMap := M.stageProjection_comp_algebraicMap

388 isInverseLimit := M.isInverseLimit

389

390/-- Package a finite-stage certificate as a completed-group-algebra model. -/

391def ofCertificate (carrier : ProfiniteRing.{w})

392 (algebraicMap : CompletedGroupAlgebraNaturalSource R G →+* carrier)

393 (h : CanonicalCompletedGroupAlgebraModel R G carrier algebraicMap) :

394 CompletedGroupAlgebraModel R G where

395 carrier := carrier

396 algebraicMap := algebraicMap

397 stageProjection := h.stageProjection

398 stageProjection_comp_algebraicMap := h.stageProjection_comp_algebraicMap

399 isInverseLimit := h.isInverseLimit

400

401/-- The bundled model's specified algebraic map is continuous; this is derived, not stored. -/

402theorem algebraicMap_continuous (M : CompletedGroupAlgebraModel R G) :

403 Continuous M.algebraicMap :=

404 M.certificate.algebraicMap_continuous

405

406/-- The bundled model's specified algebraic map has dense range; this is derived, not stored. -/

407theorem algebraicMap_dense (M : CompletedGroupAlgebraModel R G) :

408 DenseRange M.algebraicMap :=

409 M.certificate.algebraicMap_dense

410

411/-- Restriction of the algebraic map to the coefficient ring. -/

412def coefficientMap (M : CompletedGroupAlgebraModel R G) : R →+* M.carrier :=

413 M.algebraicMap.comp

414 (completedGroupAlgebraNaturalSourceCoefficientRingHom (R := R) (G := G))

415

416/-- Restriction of the algebraic map to group-like elements. -/

417def groupMap (M : CompletedGroupAlgebraModel R G) : G →* M.carrier :=

418 M.algebraicMap.toMonoidHom.comp

419 (completedGroupAlgebraNaturalSourceGroupMonoidHom (R := R) (G := G))

420

421/-- Group-like elements land in units; this is the object-level unit representation of a model. -/

422def groupUnitsMap (M : CompletedGroupAlgebraModel R G) : G →* M.carrierˣ :=

423 M.groupMap.toHomUnits

424

425/-- Forgetting the unit structure from a model's group map recovers its underlying group-like

426element. -/

427@[simp]

428theorem groupUnitsMap_coe (M : CompletedGroupAlgebraModel R G) (g : G) :

429 ((M.groupUnitsMap g : M.carrierˣ) : M.carrier) = M.groupMap g :=

430 rfl

431

432/-- The derived comparison with the concrete compatible-family model. -/

433noncomputable def comparisonRingEquiv (M : CompletedGroupAlgebraModel R G) :

434 M.carrier ≃+* CompletedGroupAlgebraCarrier R G :=

435 M.certificate.comparisonRingEquiv

436

437/-- The derived comparison is a homeomorphism. -/

438noncomputable def comparisonHomeomorph (M : CompletedGroupAlgebraModel R G) :

439 M.carrier ≃ₜ CompletedGroupAlgebraCarrier R G :=

440 M.certificate.comparisonHomeomorph

441

442/-- The bundled comparison is characterized by every finite-stage projection. -/

443@[simp]

444theorem completedGroupAlgebraProjection_comparisonRingEquiv

445 (M : CompletedGroupAlgebraModel R G) (U : CompletedGroupAlgebraIndex G) (x : M.carrier) :

446 completedGroupAlgebraProjection R G U (M.comparisonRingEquiv x) =

447 M.stageProjection U x :=

448 M.certificate.completedGroupAlgebraProjection_comparisonRingEquiv U x

449

450/-- The bundled comparison extends the model's full algebraic map. -/

451@[simp]

452theorem comparisonRingEquiv_algebraicMap (M : CompletedGroupAlgebraModel R G)

453 (x : CompletedGroupAlgebraNaturalSource R G) :

454 M.comparisonRingEquiv (M.algebraicMap x) =

455 toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G) x :=

456 M.certificate.comparisonRingEquiv_algebraicMap x

457

458/-- The comparison therefore respects the coefficient-ring embedding. -/

459@[simp]

460theorem comparisonRingEquiv_coefficientMap (M : CompletedGroupAlgebraModel R G) (r : R) :

461 M.comparisonRingEquiv (M.coefficientMap r) =

462 algebraMap R (CompletedGroupAlgebraCarrier R G) r := by

463 change M.comparisonRingEquiv

464 (M.algebraicMap

465 (completedGroupAlgebraNaturalSourceCoefficientRingHom (R := R) (G := G) r)) =

466 algebraMap R (CompletedGroupAlgebraCarrier R G) r

467 exact

468 (M.comparisonRingEquiv_algebraicMap

469 (completedGroupAlgebraNaturalSourceCoefficientRingHom (R := R) (G := G) r)).trans

470 (toCompletedGroupAlgebraNaturalSourceRingHom_coefficient (R := R) (G := G) r)

471

472/-- Source-wrapper form of compatibility with the group-like map. The normalized

473`completedGroupAlgebraOf` form is stated after that canonical map is introduced below. -/

474@[simp]

475theorem comparisonRingEquiv_groupMap_source (M : CompletedGroupAlgebraModel R G) (g : G) :

476 M.comparisonRingEquiv (M.groupMap g) =

477 toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G)

478 (completedGroupAlgebraNaturalSourceGroupMonoidHom (R := R) (G := G) g) :=

479 M.comparisonRingEquiv_algebraicMap

480 (completedGroupAlgebraNaturalSourceGroupMonoidHom (R := R) (G := G) g)

481

482/-- Canonical equivalence between any two bundled models. -/

483noncomputable def modelEquiv (M : CompletedGroupAlgebraModel.{u, v, w} R G)

484 (N : CompletedGroupAlgebraModel.{u, v, z} R G) :

485 M.carrier ≃+* N.carrier :=

486 M.certificate.modelToModelRingEquiv N.certificate

487

488/-- The model equivalence carries the specified algebraic map to the specified algebraic map. -/

489@[simp]

490theorem modelEquiv_algebraicMap (M : CompletedGroupAlgebraModel.{u, v, w} R G)

491 (N : CompletedGroupAlgebraModel.{u, v, z} R G)

492 (x : CompletedGroupAlgebraNaturalSource R G) :

493 M.modelEquiv N (M.algebraicMap x) = N.algebraicMap x :=

494 M.certificate.modelToModelRingEquiv_algebraicMap N.certificate x

495

496/-- The canonical equivalence commutes with every finite-stage projection. -/

497@[simp]

498theorem stageProjection_modelEquiv (M : CompletedGroupAlgebraModel.{u, v, w} R G)

499 (N : CompletedGroupAlgebraModel.{u, v, z} R G)

500 (U : CompletedGroupAlgebraIndex G) (x : M.carrier) :

501 N.stageProjection U (M.modelEquiv N x) = M.stageProjection U x :=

502 M.certificate.stageProjection_modelToModelRingEquiv N.certificate U x

503

504/-- The canonical equivalence restricts to the identity on coefficient-ring data. -/

505@[simp]

506theorem modelEquiv_coefficientMap (M : CompletedGroupAlgebraModel.{u, v, w} R G)

507 (N : CompletedGroupAlgebraModel.{u, v, z} R G) (r : R) :

508 M.modelEquiv N (M.coefficientMap r) = N.coefficientMap r :=

509 M.modelEquiv_algebraicMap N

510 (completedGroupAlgebraNaturalSourceCoefficientRingHom (R := R) (G := G) r)

511

512/-- The canonical equivalence restricts to the identity on group-like data. -/

513@[simp]

514theorem modelEquiv_groupMap (M : CompletedGroupAlgebraModel.{u, v, w} R G)

515 (N : CompletedGroupAlgebraModel.{u, v, z} R G) (g : G) :

516 M.modelEquiv N (M.groupMap g) = N.groupMap g :=

517 M.modelEquiv_algebraicMap N

518 (completedGroupAlgebraNaturalSourceGroupMonoidHom (R := R) (G := G) g)

519

520/-- The canonical equivalence between bundled models is continuous. -/

521theorem modelEquiv_continuous (M : CompletedGroupAlgebraModel.{u, v, w} R G)

522 (N : CompletedGroupAlgebraModel.{u, v, z} R G) :

523 Continuous (M.modelEquiv N) :=

524 M.certificate.modelToModelRingEquiv_continuous N.certificate

525

526/-- Its inverse is continuous as well. -/

527theorem modelEquiv_symm_continuous (M : CompletedGroupAlgebraModel.{u, v, w} R G)

528 (N : CompletedGroupAlgebraModel.{u, v, z} R G) :

529 Continuous (M.modelEquiv N).symm :=

530 M.certificate.modelToModelRingEquiv_symm_continuous N.certificate

531

532/-- Public bundled uniqueness theorem: a ring equivalence commuting with all stage projections

533is the canonical model equivalence. -/

534theorem modelEquiv_unique (M : CompletedGroupAlgebraModel.{u, v, w} R G)

535 (N : CompletedGroupAlgebraModel.{u, v, z} R G)

536 (e : M.carrier ≃+* N.carrier)

537 (hstage : ∀ U : CompletedGroupAlgebraIndex G,

538 (N.stageProjection U).comp e.toRingHom = M.stageProjection U) :

539 e = M.modelEquiv N :=

540 M.certificate.modelToModelRingEquiv_unique N.certificate e hstage

541

542end CompletedGroupAlgebraModel

543

544/-- The concrete inverse-limit carrier as a profinite ring object. -/

545noncomputable def completedGroupAlgebraProfiniteRing

546 (R : ProfiniteCommRing.{u}) (G : ProfiniteGrp.{v}) : ProfiniteRing := by

547 letI : CompactSpace (CompletedGroupAlgebraCarrier R G) :=

548 completedGroupAlgebra_compactSpace (R := R) (G := G)

549 letI : T2Space (CompletedGroupAlgebraCarrier R G) :=

550 completedGroupAlgebra_t2Space (R := R) (G := G)

551 letI : TotallyDisconnectedSpace (CompletedGroupAlgebraCarrier R G) :=

552 completedGroupAlgebra_totallyDisconnectedSpace (R := R) (G := G)

553 exact

554 { toProfinite := Profinite.of (CompletedGroupAlgebraCarrier R G)

555 ring := inferInstance

556 isTopologicalRing := inferInstance }

557

558/-- The inverse-limit carrier with its canonical dense map is the canonical model. -/

559noncomputable def completedGroupAlgebraCanonicalModel

560 (R : ProfiniteCommRing.{u}) (G : ProfiniteGrp.{v}) :

561 CanonicalCompletedGroupAlgebraModel R G (completedGroupAlgebraProfiniteRing R G)

562 (toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G)) where

563 stageProjection := completedGroupAlgebraProjection R G

564 stageProjection_comp_algebraicMap := by

565 intro U

566 apply RingHom.ext

567 intro x

568 change completedGroupAlgebraProjection R G U

569 (toCompletedGroupAlgebraNaturalSourceRingHom (R := R) (G := G) x) =

570 completedGroupAlgebraNaturalSourceStageMap R G U x

571 rw [completedGroupAlgebraNaturalSourceStageMap_apply]

572 change completedGroupAlgebraProjection R G U

573 (toCompletedGroupAlgebra R G x.toMonoidAlgebra) =

574 completedGroupAlgebraStageMap R G U x.toMonoidAlgebra

575 exact completedGroupAlgebraProjection_toCompletedGroupAlgebra

576 (R := R) (G := G) U x.toMonoidAlgebra

577 isInverseLimit := by

578 change

579 (completedGroupAlgebraSystem R G).IsInverseLimit

580 (fun U x => (completedGroupAlgebraSystem R G).projection U x)

581 exact (completedGroupAlgebraSystem R G).isInverseLimit_projection

582

583/-- The concrete inverse limit packaged as the canonical bundled completed-group-algebra model.

584

585This is the object-level source of truth: the coefficient ring and group enter as standard

586profinite bundles, so their compactness and separation witnesses are not repeated in the API. -/

587noncomputable def completedGroupAlgebraModel

588 (Λ : ProfiniteCommRing.{u}) (P : ProfiniteGrp.{v}) :

589 CompletedGroupAlgebraModel Λ P :=

590 CompletedGroupAlgebraModel.ofCertificate

591 (completedGroupAlgebraProfiniteRing Λ P)

592 (toCompletedGroupAlgebraNaturalSourceRingHom (R := Λ) (G := P))

593 (completedGroupAlgebraCanonicalModel Λ P)

594

595namespace CompletedGroupAlgebraModel

596

597variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}

598

599/-- The model comparison sends its group-like map to the canonical completed group element. -/

600@[simp]

601theorem comparisonRingEquiv_groupMap (M : CompletedGroupAlgebraModel R G) (g : G) :

602 M.comparisonRingEquiv (M.groupMap g) = completedGroupAlgebraOf R G g := by

603 change M.comparisonRingEquiv (M.groupMap g) =

604 toCompletedGroupAlgebra R G (MonoidAlgebra.of R G g)

605 exact (M.comparisonRingEquiv_groupMap_source g).trans

606 (toCompletedGroupAlgebraNaturalSourceRingHom_group (R := R) (G := G) g)

607

608end CompletedGroupAlgebraModel

609

610/-- The dense abstract group-algebra map lands in the span of the completed group-like elements. -/

611theorem toCompletedGroupAlgebraRingHom_mem_span_completedGroupAlgebraOf

612 (x : MonoidAlgebra R G) :

613 toCompletedGroupAlgebraRingHom R G x ∈

614 Submodule.span R (Set.range (completedGroupAlgebraOf R G)) := by

615 classical

616 let P := fun y : MonoidAlgebra R G =>

617 toCompletedGroupAlgebraRingHom R G y ∈

618 Submodule.span R (Set.range (completedGroupAlgebraOf R G))

619 change P x

620 refine MonoidAlgebra.induction_on (p := P) x ?_ ?_ ?_

621 · intro g

622 dsimp [P]

623 change completedGroupAlgebraOf R G g ∈

624 Submodule.span R (Set.range (completedGroupAlgebraOf R G))

625 exact Submodule.subset_span ⟨g, rfl⟩

626 · intro a b ha hb

627 dsimp [P] at ha hb ⊢

628 rw [map_add]

629 exact Submodule.add_mem _ ha hb

630 · intro r y hy

631 dsimp [P] at hy ⊢

632 change toCompletedGroupAlgebra R G (r • y) ∈

633 Submodule.span R (Set.range (completedGroupAlgebraOf R G))

634 rw [toCompletedGroupAlgebra_smul]

635 exact Submodule.smul_mem _ r hy

636

637/-- The completed group-like elements have dense linear span in the completed group algebra. -/

638theorem completedGroupAlgebraOf_dense_span :

639 closure (Submodule.span R (Set.range (completedGroupAlgebraOf R G)) :

640 Set (CompletedGroupAlgebraCarrier R G)) = Set.univ := by

641 rw [Set.eq_univ_iff_forall]

642 intro y

643 have hy :

644 y ∈ closure (Set.range (toCompletedGroupAlgebraRingHom R G)) := by

645 rw [(denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := G)).closure_range]

646 exact Set.mem_univ y

647 exact closure_mono (by

648 intro z hz

649 rcases hz with ⟨x, rfl⟩

650 exact toCompletedGroupAlgebraRingHom_mem_span_completedGroupAlgebraOf

651 (R := R) (G := G) x) hy

652

653/--

654The uniqueness half of the universal property in Lemma 5.3.5(d): a continuous linear map out of

655\(\widehat{R[G]}\) is determined by its values on the completed group-like elements.

656-/

657theorem completedGroupAlgebraContinuousLinearMap_ext_of_basis

658 {N : Type w} [AddCommGroup N] [TopologicalSpace N] [Module R N] [T2Space N]

659 {F K : CompletedGroupAlgebraCarrier R G →L[R] N}

660 (hbasis : ∀ g : G, F (completedGroupAlgebraOf R G g) =

661 K (completedGroupAlgebraOf R G g)) :

662 F = K := by

663 apply ContinuousLinearMap.ext

664 intro x

665 have hclosed : IsClosed {x : CompletedGroupAlgebraCarrier R G | F x = K x} :=

666 isClosed_eq F.continuous K.continuous

667 have hspan :

668 (Submodule.span R (Set.range (completedGroupAlgebraOf R G)) :

669 Set (CompletedGroupAlgebraCarrier R G)) ⊆

670 {x : CompletedGroupAlgebraCarrier R G | F x = K x} := by

671 intro y hy

672 exact Submodule.span_induction

673 (fun z hz => by

674 rcases hz with ⟨g, rfl⟩

675 exact hbasis g)

676 (by simp only [Set.mem_setOf_eq, map_zero])

677 (fun z w _ _ hz hw => by

678 change F (z + w) = K (z + w)

679 rw [map_add, map_add, hz, hw])

680 (fun r z _ hz => by

681 change F (r • z) = K (r • z)

682 rw [map_smul, map_smul, hz])

683 hy

684 have hx :

685 x ∈ closure (Submodule.span R (Set.range (completedGroupAlgebraOf R G)) :

686 Set (CompletedGroupAlgebraCarrier R G)) := by

687 rw [completedGroupAlgebraOf_dense_span (R := R) (G := G)]

688 exact Set.mem_univ x

689 exact hclosed.closure_subset_iff.2 hspan hx

690end

691

692end CompletedGroupAlgebra