Source: ProCGroups.CompletedGroupAlgebra.UniversalProperty.ProfiniteModule

1import ProCGroups.CompletedGroupAlgebra.UniversalProperty.OpenSubmoduleQuotient

3/-!

4# Lifts to profinite modules

6Compatible lifts to all open-submodule quotients are assembled by compactness into a continuous

7linear map to a profinite module. This file proves existence and uniqueness and applies it to the

8free profinite-module property of completed group algebras.

9-/

11open scoped Topology

13namespace CompletedGroupAlgebra

15noncomputable section

17open ProCGroups

18open ProCGroups.ProC

19open ProCGroups.InverseSystems

20open ProCGroups.Completion

22universe u v w

24variable (R : ProfiniteCommRing.{u})

25variable (G : ProfiniteGrp.{v})

27local instance (N : ProfiniteModule.{u, w} R.toProfiniteRing) : Module R N :=

28 N.module

30local instance (N : ProfiniteModule.{u, w} R.toProfiniteRing) :

31 ContinuousSMul R N :=

32 N.continuousSMul

34/--

35The closed fiber in a profinite target determined by the quotient-valued extension modulo one

36open submodule.

37-/

38private def completedGroupAlgebraLiftFiberSet

39 (N : ProfiniteModule.{u, w} R.toProfiniteRing)

40 (f : G → N) (hf : Continuous f)

41 (x : CompletedGroupAlgebraCarrier R G)

42 (W : ProfiniteModuleOpenSubmodule (R := R) N) : Set N :=

43 {y | Submodule.mkQ W.1 y =

44 completedGroupAlgebraLiftToOpenSubmoduleQuotient

45 (R := R) (G := G) N f hf W.1 W.2 x}

47/-- The quotient fiber attached to an open submodule is closed. -/

48private theorem completedGroupAlgebraLiftFiberSet_isClosed

49 (N : ProfiniteModule.{u, w} R.toProfiniteRing)

50 (f : G → N) (hf : Continuous f)

51 (x : CompletedGroupAlgebraCarrier R G)

52 (W : ProfiniteModuleOpenSubmodule (R := R) N) :

53 IsClosed (completedGroupAlgebraLiftFiberSet

54 (R := R) (G := G) N f hf x W) := by

55 let hdisc : IsDiscreteModule R (N ⧸ W.1) :=

56 quotient_openSubmodule_isDiscreteModule R N W.1 W.2

57 letI : DiscreteTopology (N ⧸ W.1) := hdisc.2

58 have hqcont : Continuous (Submodule.mkQ W.1 : N → N ⧸ W.1) := by

59 change Continuous (Submodule.Quotient.mk (p := W.1))

60 exact continuous_quotient_mk'

61 change IsClosed ((Submodule.mkQ W.1 : N → N ⧸ W.1) ⁻¹'

62 ({completedGroupAlgebraLiftToOpenSubmoduleQuotient

63 (R := R) (G := G) N f hf W.1 W.2 x} : Set (N ⧸ W.1)))

64 exact (isClosed_discrete _).preimage hqcont

66/-- Finite intersection property for the fibers used to assemble the profinite-target lift. -/

67private theorem completedGroupAlgebraLiftFiberSet_finite_inter_nonempty

68 (N : ProfiniteModule.{u, w} R.toProfiniteRing)

69 (f : G → N) (hf : Continuous f)

70 (x : CompletedGroupAlgebraCarrier R G)

71 (s : Finset (ProfiniteModuleOpenSubmodule (R := R) N)) :

72 (⋂ W ∈ s, completedGroupAlgebraLiftFiberSet

73 (R := R) (G := G) N f hf x W).Nonempty := by

74 classical

75 rcases exists_openSubmodule_le_finset (R := R) N s with ⟨K, hK⟩

76 rcases Submodule.mkQ_surjective K.1

77 (completedGroupAlgebraLiftToOpenSubmoduleQuotient

78 (R := R) (G := G) N f hf K.1 K.2 x) with

79 ⟨z, hz⟩

80 refine ⟨z, ?_⟩

81 simp only [Set.mem_iInter]

82 intro W hWs

83 dsimp [completedGroupAlgebraLiftFiberSet]

84 calc

85 Submodule.mkQ W.1 z = Submodule.factor (hK W hWs) (Submodule.mkQ K.1 z) := by

86 rw [Submodule.factor_mk]

87 _ = Submodule.factor (hK W hWs)

88 (completedGroupAlgebraLiftToOpenSubmoduleQuotient

89 (R := R) (G := G) N f hf K.1 K.2 x) := by

90 rw [hz]

91 _ = completedGroupAlgebraLiftToOpenSubmoduleQuotient

92 (R := R) (G := G) N f hf W.1 W.2 x := by

93 exact completedGroupAlgebraLiftToOpenSubmoduleQuotient_factor

94 (R := R) (G := G) N f hf (hK W hWs) K.2 W.2 x

96/--

97Compactness of the profinite target gives a simultaneous lift of the compatible quotient values.

98-/

99private theorem completedGroupAlgebraLiftFiberSet_iInter_nonempty

100 (N : ProfiniteModule.{u, w} R.toProfiniteRing)

101 (f : G → N) (hf : Continuous f)

102 (x : CompletedGroupAlgebraCarrier R G) :

103 (⋂ W : ProfiniteModuleOpenSubmodule (R := R) N,

104 completedGroupAlgebraLiftFiberSet

105 (R := R) (G := G) N f hf x W).Nonempty := by

106 exact CompactSpace.iInter_nonempty

107 (t := fun W : ProfiniteModuleOpenSubmodule (R := R) N =>

108 completedGroupAlgebraLiftFiberSet

109 (R := R) (G := G) N f hf x W)

110 (fun W => completedGroupAlgebraLiftFiberSet_isClosed

111 (R := R) (G := G) N f hf x W)

112 (fun s => completedGroupAlgebraLiftFiberSet_finite_inter_nonempty

113 (R := R) (G := G) N f hf x s)

114

115/-- The assembled pointwise lift from \(\widehat{R[G]}\) to a profinite target module. -/

116private def completedGroupAlgebraLiftToProfiniteModuleFun

117 (N : ProfiniteModule.{u, w} R.toProfiniteRing)

118 (f : G → N) (hf : Continuous f) :

119 CompletedGroupAlgebraCarrier R G → N :=

120 fun x => Classical.choose

121 (completedGroupAlgebraLiftFiberSet_iInter_nonempty

122 (R := R) (G := G) N f hf x)

123

124/--

125The assembled point maps to the prescribed quotient-valued extension modulo every open

126submodule.

127-/

128private theorem completedGroupAlgebraLiftToProfiniteModuleFun_quotient

129 (N : ProfiniteModule.{u, w} R.toProfiniteRing)

130 (f : G → N) (hf : Continuous f)

131 (W : ProfiniteModuleOpenSubmodule (R := R) N)

132 (x : CompletedGroupAlgebraCarrier R G) :

133 Submodule.mkQ W.1

134 (completedGroupAlgebraLiftToProfiniteModuleFun

135 (R := R) (G := G) N f hf x) =

136 completedGroupAlgebraLiftToOpenSubmoduleQuotient

137 (R := R) (G := G) N f hf W.1 W.2 x := by

138 have hmem := Classical.choose_spec

139 (completedGroupAlgebraLiftFiberSet_iInter_nonempty

140 (R := R) (G := G) N f hf x)

141 exact (Set.mem_iInter.1 hmem W : _)

142

143/-- The assembled lift has the prescribed values on the completed group-like elements. -/

144@[simp]

145private theorem completedGroupAlgebraLiftToProfiniteModuleFun_apply_of

146 (N : ProfiniteModule.{u, w} R.toProfiniteRing)

147 (f : G → N) (hf : Continuous f)

148 (g : G) :

149 completedGroupAlgebraLiftToProfiniteModuleFun

150 (R := R) (G := G) N f hf (completedGroupAlgebraOf R G g) = f g := by

151 apply profiniteModule_ext_of_openSubmoduleQuotients (R := R) N

152 intro W hW

153 rw [completedGroupAlgebraLiftToProfiniteModuleFun_quotient

154 (R := R) (G := G) N f hf ⟨W, hW⟩,

155 completedGroupAlgebraLiftToOpenSubmoduleQuotient_apply_of]

156

157/--

158Additivity of the assembled profinite-target lift, checked after all open-submodule quotients.

159-/

160private theorem completedGroupAlgebraLiftToProfiniteModuleFun_add

161 (N : ProfiniteModule.{u, w} R.toProfiniteRing)

162 (f : G → N) (hf : Continuous f)

163 (x y : CompletedGroupAlgebraCarrier R G) :

164 completedGroupAlgebraLiftToProfiniteModuleFun

165 (R := R) (G := G) N f hf (x + y) =

166 completedGroupAlgebraLiftToProfiniteModuleFun

167 (R := R) (G := G) N f hf x +

168 completedGroupAlgebraLiftToProfiniteModuleFun

169 (R := R) (G := G) N f hf y := by

170 apply profiniteModule_ext_of_openSubmoduleQuotients (R := R) N

171 intro W hW

172 rw [completedGroupAlgebraLiftToProfiniteModuleFun_quotient

173 (R := R) (G := G) N f hf ⟨W, hW⟩,

174 map_add,

175 ← completedGroupAlgebraLiftToProfiniteModuleFun_quotient

176 (R := R) (G := G) N f hf ⟨W, hW⟩ x,

177 ← completedGroupAlgebraLiftToProfiniteModuleFun_quotient

178 (R := R) (G := G) N f hf ⟨W, hW⟩ y]

179 rfl

180

181/--

182The assembled profinite-target lift is compatible with scalar multiplication after all

183open-submodule quotients.

184-/

185private theorem completedGroupAlgebraLiftToProfiniteModuleFun_smul

186 (N : ProfiniteModule.{u, w} R.toProfiniteRing)

187 (f : G → N) (hf : Continuous f)

188 (r : R) (x : CompletedGroupAlgebraCarrier R G) :

189 completedGroupAlgebraLiftToProfiniteModuleFun

190 (R := R) (G := G) N f hf (r • x) =

191 r • completedGroupAlgebraLiftToProfiniteModuleFun

192 (R := R) (G := G) N f hf x := by

193 apply profiniteModule_ext_of_openSubmoduleQuotients (R := R) N

194 intro W hW

195 rw [completedGroupAlgebraLiftToProfiniteModuleFun_quotient

196 (R := R) (G := G) N f hf ⟨W, hW⟩,

197 map_smul,

198 ← completedGroupAlgebraLiftToProfiniteModuleFun_quotient

199 (R := R) (G := G) N f hf ⟨W, hW⟩ x]

200 rfl

201

202/--

203Existence half of Lemma 5.3.5(d): a continuous map from the profinite group \(G\) to a profinite

204\(R\)-module extends to a continuous \(R\)-linear map out of \(\widehat{R[G]}\).

205-/

206private def completedGroupAlgebraLiftToProfiniteModule

207 (N : ProfiniteModule.{u, w} R.toProfiniteRing)

208 (f : G → N) (hf : Continuous f) :

209 CompletedGroupAlgebraCarrier R G →L[R] N where

210 toFun := completedGroupAlgebraLiftToProfiniteModuleFun (R := R) (G := G) N f hf

211 map_add' := completedGroupAlgebraLiftToProfiniteModuleFun_add

212 (R := R) (G := G) N f hf

213 map_smul' := completedGroupAlgebraLiftToProfiniteModuleFun_smul

214 (R := R) (G := G) N f hf

215 cont := by

216 apply continuous_of_forall_openSubmodule_quotient_continuous (R := R) N

217 intro W hW

218 have hEq : (fun x : CompletedGroupAlgebraCarrier R G =>

219 Submodule.mkQ W

220 (completedGroupAlgebraLiftToProfiniteModuleFun

221 (R := R) (G := G) N f hf x)) =

222 completedGroupAlgebraLiftToOpenSubmoduleQuotient

223 (R := R) (G := G) N f hf W hW := by

224 funext x

225 exact completedGroupAlgebraLiftToProfiniteModuleFun_quotient

226 (R := R) (G := G) N f hf ⟨W, hW⟩ x

227 rw [hEq]

228 exact (completedGroupAlgebraLiftToOpenSubmoduleQuotient

229 (R := R) (G := G) N f hf W hW).continuous

230

231/-- The profinite-target lift has the prescribed value on completed group-like elements. -/

232@[simp]

233private theorem completedGroupAlgebraLiftToProfiniteModule_apply_of

234 (N : ProfiniteModule.{u, w} R.toProfiniteRing)

235 (f : G → N) (hf : Continuous f)

236 (g : G) :

237 completedGroupAlgebraLiftToProfiniteModule

238 (R := R) (G := G) N f hf (completedGroupAlgebraOf R G g) = f g :=

239 completedGroupAlgebraLiftToProfiniteModuleFun_apply_of

240 (R := R) (G := G) N f hf g

241

242/--

243Lemma 5.3.5(d): the completed group algebra satisfies the full universal property for maps into

244profinite modules.

245-/

246private theorem completedGroupAlgebra_existsUnique_lift_to_profiniteModule

247 (N : ProfiniteModule.{u, w} R.toProfiniteRing)

248 (f : G → N) (hf : Continuous f) :

249 ∃! F : CompletedGroupAlgebraCarrier R G →L[R] N,

250 ∀ g : G, F (completedGroupAlgebraOf R G g) = f g := by

251 let F := completedGroupAlgebraLiftToProfiniteModule (R := R) (G := G) N f hf

252 refine ⟨F, ?_, ?_⟩

253 · intro g

254 exact completedGroupAlgebraLiftToProfiniteModule_apply_of

255 (R := R) (G := G) N f hf g

256 · intro K hK

257 apply completedGroupAlgebraContinuousLinearMap_ext_of_basis (R := R) (G := G)

258 intro g

259 rw [completedGroupAlgebraLiftToProfiniteModule_apply_of, hK]

260

261/-- The completed group algebra as an object in profinite modules over a bundled profinite

262coefficient ring. -/

263def completedGroupAlgebraProfiniteModule

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

265 ProfiniteModule Λ.toProfiniteRing := by

266 letI : CompactSpace (CompletedGroupAlgebraCarrier Λ P) :=

267 completedGroupAlgebra_compactSpace (R := Λ) (G := P)

268 letI : T2Space (CompletedGroupAlgebraCarrier Λ P) :=

269 completedGroupAlgebra_t2Space (R := Λ) (G := P)

270 letI : TotallyDisconnectedSpace (CompletedGroupAlgebraCarrier Λ P) :=

271 completedGroupAlgebra_totallyDisconnectedSpace (R := Λ) (G := P)

272 letI : Module Λ.toProfiniteRing (CompletedGroupAlgebraCarrier Λ P) :=

273 instModuleCoeffCompletedGroupAlgebra (R := Λ) (G := P)

274 letI : ContinuousSMul Λ.toProfiniteRing (CompletedGroupAlgebraCarrier Λ P) :=

275 instContinuousSMulCompletedGroupAlgebra (R := Λ) (G := P)

276 exact

277 { toProfinite := Profinite.of (CompletedGroupAlgebraCarrier Λ P)

278 addCommGroup := inferInstance

279 module := inferInstance

280 isTopologicalAddGroup := inferInstance

281 continuousSMul := inferInstance }

282

283/-- Cross-universe extension property for the bundled completed group algebra. -/

284theorem completedGroupAlgebraOf_hasFreeLiftTo

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

286 (N : ProfiniteModule.{u, w} Λ.toProfiniteRing) :

287 ProfiniteModule.HasFreeLiftTo

288 (completedGroupAlgebraProfiniteModule Λ P)

289 P.toProfinite (fun g => by

290 change CompletedGroupAlgebraCarrier Λ P

291 exact completedGroupAlgebraOf Λ P g) N := by

292 letI : Module Λ N := N.module

293 change ∀ f : P → N, Continuous f →

294 ∃! F : CompletedGroupAlgebraCarrier Λ P →L[Λ] N,

295 ∀ g : P, F (completedGroupAlgebraOf Λ P g) = f g

296 intro f hf

297 exact completedGroupAlgebra_existsUnique_lift_to_profiniteModule

298 (R := Λ) (G := P) N f hf

299

300/--

301Ribes--Zalesskii Lemma 5.3.5(d): \(\widehat{R[G]}\) is the free profinite \(R\)-module on the

302profinite space G, with basis map \(g\mapsto [g]\) inside the completed group algebra.

303-/

304theorem completedGroupAlgebraOf_freeProfiniteModule

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

306 (completedGroupAlgebraProfiniteModule Λ P).IsFreeOn

307 P.toProfinite (fun g => by

308 change CompletedGroupAlgebraCarrier Λ P

309 exact completedGroupAlgebraOf Λ P g) := by

310 refine ⟨continuous_completedGroupAlgebraOf (R := Λ) (G := P),

311 completedGroupAlgebraOf_dense_span Λ P, ?_⟩

312 intro N

313 exact completedGroupAlgebraOf_hasFreeLiftTo Λ P N

314

315end

316

317end CompletedGroupAlgebra