Source: ProCGroups.CompletedGroupAlgebra.Basic.InClass.LimitAlgebra

1import ProCGroups.CompletedGroupAlgebra.Basic.InClass.System

3/-!

4# Completed Group Algebra / Basic / Within a Class / Limit Algebra

6This module gives the \(C\)-indexed completion the same opaque-carrier API as the all-finite

7completion. Its inverse-limit representation is exchanged explicitly, while projections,

8compatibility, and extensionality are the ordinary public interface. Algebraic structures are

9inherited from the generic ring and module inverse limits.

10-/

12open scoped Topology

14namespace CompletedGroupAlgebra

16noncomputable section

18open ProCGroups

19open ProCGroups.ProC

20open ProCGroups.InverseSystems

22universe u v w

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

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

27/-- The \(C\)-indexed completed group algebra, kept opaque from its compatible-family

28inverse-limit realization. -/

29def CompletedGroupAlgebraInClass

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

31 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

32 [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :

33 Type (max u v) :=

34 (completedGroupAlgebraSystemInClass C R G).inverseLimit

36/-- The \(C\)-indexed completion carries its inverse-limit topology. -/

37instance instTopologicalSpaceCompletedGroupAlgebraInClass

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

39 TopologicalSpace (CompletedGroupAlgebraInClass C R G) :=

40 inferInstanceAs

41 (TopologicalSpace (completedGroupAlgebraSystemInClass C R G).inverseLimit)

43/-- Explicit exchange between the named \(C\)-indexed carrier and its concrete compatible-family

44realization. Ordinary code should use finite-stage projections instead. -/

45def completedGroupAlgebraInClassCompatibleFamilyEquiv

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

47 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]

48 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :

49 CompletedGroupAlgebraInClass C R G ≃

50 (completedGroupAlgebraSystemInClass C R G).inverseLimit :=

51 Equiv.refl _

53local instance

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

55 (U : CompletedGroupAlgebraIndexInClass G C) :

56 Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by

57 change Ring (CompletedGroupAlgebraStageInClass C R G U)

58 infer_instance

60local instance

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

62 (U : CompletedGroupAlgebraIndexInClass G C) :

63 Module R ((completedGroupAlgebraSystemInClass C R G).X U) := by

64 change Module R (CompletedGroupAlgebraStageInClass C R G U)

65 infer_instance

67/-- The \(C\)-indexed ring structure is inherited from the generic ring inverse limit. -/

68instance instRingCompletedGroupAlgebraInClass

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

70 Ring (CompletedGroupAlgebraInClass C R G) :=

71 inferInstanceAs (Ring (completedGroupAlgebraSystemInClass C R G).inverseLimit)

73/-- The canonical \(C\)-indexed finite-stage projection, bundled at its source as a ring

74homomorphism. -/

75def completedGroupAlgebraProjectionInClass

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

77 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]

78 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

79 (U : CompletedGroupAlgebraIndexInClass G C) :

80 CompletedGroupAlgebraInClass C R G →+*

81 CompletedGroupAlgebraStageInClass C R G U :=

82 projectionRingHom (S := completedGroupAlgebraSystemInClass C R G) U

84/-- The \(C\)-indexed bundled projections satisfy the transition compatibility equations. -/

85theorem completedGroupAlgebraProjectionInClass_compatible

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

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

88 (x : CompletedGroupAlgebraInClass C R G) :

89 completedGroupAlgebraTransitionInClass C R G hUV

90 (completedGroupAlgebraProjectionInClass C R G V x) =

91 completedGroupAlgebraProjectionInClass C R G U x :=

92 (completedGroupAlgebraSystemInClass C R G).projection_compatible

93 (completedGroupAlgebraInClassCompatibleFamilyEquiv

94 (R := R) (G := G) C x) U V hUV

96/-- \(C\)-indexed completed elements are equal when all bundled stage projections agree. -/

97@[ext]

98theorem completedGroupAlgebraInClass_ext

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

100 {x y : CompletedGroupAlgebraInClass C R G}

101 (h : ∀ U, completedGroupAlgebraProjectionInClass C R G U x =

102 completedGroupAlgebraProjectionInClass C R G U y) :

103 x = y := by

104 apply (completedGroupAlgebraInClassCompatibleFamilyEquiv

105 (R := R) (G := G) C).injective

106 apply (completedGroupAlgebraSystemInClass C R G).ext

107 exact h

108

109/-- The \(C\)-indexed tower is a module-valued inverse system over the coefficient ring. -/

110instance instIsModuleSystemCompletedGroupAlgebraSystemInClass

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

112 IsModuleSystem R (completedGroupAlgebraSystemInClass C R G) where

113 map_smul := completedGroupAlgebraTransitionInClass_smul

114 (R := R) (G := G) C

115

116/-- The \(C\)-indexed module structure is inherited from the generic module inverse limit. -/

117instance instModuleCoeffCompletedGroupAlgebraInClass

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

119 Module R (CompletedGroupAlgebraInClass C R G) :=

120 inferInstanceAs

121 (Module R (completedGroupAlgebraSystemInClass C R G).inverseLimit)

122

123/-- Stagewise coefficient change on the \(C\)-indexed completion. -/

124def completedGroupAlgebraCoeffMapInClass

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

126 (S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]

127 (f : R →+* S) :

128 CompletedGroupAlgebraInClass C R G →+*

129 CompletedGroupAlgebraInClass C S G where

130 toFun x :=

131 (completedGroupAlgebraInClassCompatibleFamilyEquiv

132 (R := S) (G := G) C).symm

133 ((completedGroupAlgebraSystemInClass C S G).inverseLimitLift

134 (fun U x =>

135 completedGroupAlgebraStageCoeffMapInClass

136 (R := R) (G := G) C S f U

137 (completedGroupAlgebraProjectionInClass C R G U x))

138 (by

139 intro U V hUV

140 funext x

141 have hcompat := congrFun

142 (congrArg DFunLike.coe

143 (completedGroupAlgebraStageCoeffMapInClass_compatible

144 (R := R) (G := G) C S f hUV))

145 (completedGroupAlgebraProjectionInClass C R G V x)

146 calc

147 completedGroupAlgebraTransitionInClass C S G hUV

148 (completedGroupAlgebraStageCoeffMapInClass

149 (R := R) (G := G) C S f V

150 (completedGroupAlgebraProjectionInClass C R G V x))

151 =

152 completedGroupAlgebraStageCoeffMapInClass

153 (R := R) (G := G) C S f U

154 (completedGroupAlgebraTransitionInClass C R G hUV

155 (completedGroupAlgebraProjectionInClass C R G V x)) :=

156 hcompat.symm

157 _ =

158 completedGroupAlgebraStageCoeffMapInClass

159 (R := R) (G := G) C S f U

160 (completedGroupAlgebraProjectionInClass C R G U x) := by

161 rw [completedGroupAlgebraProjectionInClass_compatible]) x)

162 map_zero' := by

163 apply completedGroupAlgebraInClass_ext (R := S) (G := G) C

164 intro U

165 exact map_zero

166 (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U)

167 map_one' := by

168 apply completedGroupAlgebraInClass_ext (R := S) (G := G) C

169 intro U

170 exact map_one

171 (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U)

172 map_add' x y := by

173 apply completedGroupAlgebraInClass_ext (R := S) (G := G) C

174 intro U

175 exact map_add

176 (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U)

177 (completedGroupAlgebraProjectionInClass C R G U x)

178 (completedGroupAlgebraProjectionInClass C R G U y)

179 map_mul' x y := by

180 apply completedGroupAlgebraInClass_ext (R := S) (G := G) C

181 intro U

182 exact map_mul

183 (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U)

184 (completedGroupAlgebraProjectionInClass C R G U x)

185 (completedGroupAlgebraProjectionInClass C R G U y)

186

187/-- The coefficient-ring map is the inverse-limit lift of the \(C\)-indexed stage algebra maps. -/

188def completedGroupAlgebraAlgebraMapInClass

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

190 R →+* CompletedGroupAlgebraInClass C R G where

191 toFun r :=

192 (completedGroupAlgebraInClassCompatibleFamilyEquiv

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

194 ((completedGroupAlgebraSystemInClass C R G).inverseLimitLift

195 (fun U r => algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r)

196 (by

197 intro U V hUV

198 funext r

199 exact completedGroupAlgebraTransitionInClass_algebraMap

200 (R := R) (G := G) C hUV r) r)

201 map_zero' := by

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

203 intro U

204 exact map_zero (algebraMap R (CompletedGroupAlgebraStageInClass C R G U))

205 map_one' := by

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

207 intro U

208 exact map_one (algebraMap R (CompletedGroupAlgebraStageInClass C R G U))

209 map_add' r s := by

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

211 intro U

212 exact map_add

213 (algebraMap R (CompletedGroupAlgebraStageInClass C R G U)) r s

214 map_mul' r s := by

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

216 intro U

217 exact map_mul

218 (algebraMap R (CompletedGroupAlgebraStageInClass C R G U)) r s

219

220/-- The \(C\)-indexed completed group algebra is an algebra over its coefficient ring. -/

221instance instAlgebraCompletedGroupAlgebraInClass

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

223 Algebra R (CompletedGroupAlgebraInClass C R G) where

224 algebraMap := completedGroupAlgebraAlgebraMapInClass

225 (R := R) (G := G) C

226 commutes' := by

227 intro r x

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

229 intro U

230 exact Algebra.commutes r

231 (completedGroupAlgebraProjectionInClass C R G U x)

232 smul_def' := by

233 intro r x

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

235 intro U

236 change r • completedGroupAlgebraProjectionInClass C R G U x =

237 algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r *

238 completedGroupAlgebraProjectionInClass C R G U x

239 rw [Algebra.smul_def]

240

241end

242

243end CompletedGroupAlgebra