Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.Augmentation

1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.CompletionMap

2

3/-!

4# Fox differential: completed — coefficient rings — mod-\(n\) completed group algebra — augmentation

5

6The principal declarations in this module are:

7

8- `modNCompletedGroupAlgebraStageAugmentation`

9 The augmentation on one residue-coefficient finite stage.

10- `modNCompletedGroupAlgebraAugmentationAt`

11 The augmentation value of a residue-coefficient completed point, read at one finite stage.

12- `modNCompletedGroupAlgebraStageAugmentation_of`

13 The finite-stage \(n\)-modular augmentation sends every group-like basis element to \(1\).

14- `modNCompletedGroupAlgebraStageAugmentation_compatible`

15 Finite-stage \(n\)-modular augmentations are compatible with group-quotient transition maps.

16-/

17

18namespace FoxDifferential

19

20noncomputable section

21

22open ProCGroups.InverseSystems

23open ProCGroups.ProC

24

25universe u

26

27

28variable (n : ℕ) [Fact (0 < n)]

29variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

30

31/-- The augmentation on one residue-coefficient finite stage. -/

32def modNCompletedGroupAlgebraStageAugmentation (U :

33 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :

34 ModNCompletedGroupAlgebraStage n G U →+* ModNCompletedCoeff n :=

35 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)

36 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U)

37 (1 : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U →* ModNCompletedCoeff n)

38

39omit [Fact (0 < n)] in

40/-- The finite-stage \(n\)-modular augmentation sends every group-like basis element to \(1\). -/

41@[simp]

42theorem modNCompletedGroupAlgebraStageAugmentation_of

43 (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (q :

44 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U) :

45 modNCompletedGroupAlgebraStageAugmentation n G U

46 (MonoidAlgebra.of (ModNCompletedCoeff n) _ q) = 1 := by

47 change

48 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)

49 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U)

50 (1 : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U →*

51 ModNCompletedCoeff n)

52 (MonoidAlgebra.of (ModNCompletedCoeff n) _ q) = 1

53 rw [MonoidAlgebra.lift_of]

54 exact MonoidHom.one_apply q

55

56omit [Fact (0 < n)] in

57/-- Finite-stage \(n\)-modular augmentations are compatible with group-quotient transition maps. -/

58@[simp 900]

59theorem modNCompletedGroupAlgebraStageAugmentation_compatible

60 {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :

61 (modNCompletedGroupAlgebraStageAugmentation n G U).comp

62 (modNCompletedGroupAlgebraTransition n G hUV) =

63 modNCompletedGroupAlgebraStageAugmentation n G V := by

64 apply RingHom.ext

65 intro x

66 refine MonoidAlgebra.induction_on

67 (p := fun x =>

68 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp

69 (modNCompletedGroupAlgebraTransition n G hUV)) x =

70 modNCompletedGroupAlgebraStageAugmentation n G V x)

71 x ?_ ?_ ?_

72 · intro q

73 rw [RingHom.comp_apply, modNCompletedGroupAlgebraTransition_of]

74 change

75 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)

76 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U)

77 (1 : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U →*

78 ModNCompletedCoeff n)

79 (MonoidAlgebra.single

80 ((OpenNormalSubgroupInClass.map

81 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)

82 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) 1) =

83 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)

84 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G V)

85 (1 : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G V →*

86 ModNCompletedCoeff n)

87 (MonoidAlgebra.of (ModNCompletedCoeff n) _ q)

88 rw [MonoidAlgebra.lift_single, MonoidAlgebra.lift_of]

89 simp only [MonoidHom.one_apply, one_smul]

90 · intro x y hx hy

91 simp only [RingHom.map_add, hx, hy]

92 · intro a x hx

93 rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]

94 have hcoeff :

95 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp

96 (modNCompletedGroupAlgebraTransition n G hUV))

97 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupAlgebraStage n G V) a) =

98 (modNCompletedGroupAlgebraStageAugmentation n G V)

99 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupAlgebraStage n G V) a) := by

100 rw [RingHom.comp_apply]

101 change

102 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)

103 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U)

104 (1 : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U →*

105 ModNCompletedCoeff n)

106 (MonoidAlgebra.mapDomain _

107 (algebraMap (ModNCompletedCoeff n)

108 (ModNCompletedGroupAlgebraStage n G V) a)) =

109 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)

110 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G V)

111 (1 : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G V →*

112 ModNCompletedCoeff n)

113 (algebraMap (ModNCompletedCoeff n)

114 (ModNCompletedGroupAlgebraStage n G V) a)

115 rw [MonoidAlgebra.mapDomain_algebraMap]

116 exact

117 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)

118 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U)

119 (1 : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U →*

120 ModNCompletedCoeff n)).commutes a |>.trans

121 ((MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)

122 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G V)

123 (1 : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G V →*

124 ModNCompletedCoeff n)).commutes a).symm

125 rw [hcoeff]

126

127omit [Fact (0 < n)] in

128/--

129Composing the finite-stage \(n\)-modular augmentation with the dense stage map gives the

130ordinary \(n\)-modular group-algebra augmentation.

131-/

132@[simp 900]

133theorem modNCompletedGroupAlgebraStageAugmentation_comp_stageMap

134 (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :

135 (modNCompletedGroupAlgebraStageAugmentation n G U).comp

136 (modNCompletedGroupAlgebraStageMap n G U) =

137 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G

138 (1 : G →* ModNCompletedCoeff n) := by

139 apply RingHom.ext

140 intro x

141 refine MonoidAlgebra.induction_on

142 (p := fun x =>

143 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp

144 (modNCompletedGroupAlgebraStageMap n G U)) x =

145 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G

146 (1 : G →* ModNCompletedCoeff n)) x)

147 x ?_ ?_ ?_

148 · intro g

149 rw [RingHom.comp_apply, modNCompletedGroupAlgebraStageMap_of]

150 change

151 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)

152 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U)

153 (1 : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U →*

154 ModNCompletedCoeff n)

155 (MonoidAlgebra.single

156 (openNormalSubgroupInClassProj

157 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) 1) =

158 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G

159 (1 : G →* ModNCompletedCoeff n)

160 (MonoidAlgebra.of (ModNCompletedCoeff n) G g)

161 rw [MonoidAlgebra.lift_single, MonoidAlgebra.lift_of]

162 simp only [MonoidHom.one_apply, one_smul]

163 · intro x y hx hy

164 simp only [hx, hy, map_add]

165 · intro a x hx

166 have hcoeff :

167 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp

168 (modNCompletedGroupAlgebraStageMap n G U))

169 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) = a := by

170 rw [RingHom.comp_apply]

171 change

172 modNCompletedGroupAlgebraStageAugmentation n G U

173 (MonoidAlgebra.mapDomain _

174 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a)) = a

175 rw [MonoidAlgebra.mapDomain_algebraMap]

176 change

177 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)

178 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U)

179 (1 : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U →*

180 ModNCompletedCoeff n)

181 (algebraMap (ModNCompletedCoeff n)

182 (ModNCompletedGroupAlgebraStage n G U) a) = a

183 simpa only [Algebra.algebraMap_self, RingHom.id_apply] using

184 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n)

185 (_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U)

186 (1 : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient G U →*

187 ModNCompletedCoeff n)).commutes a

188 have hcoeff' :

189 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp

190 (modNCompletedGroupAlgebraStageMap n G U))

191 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) =

192 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G

193 (1 : G →* ModNCompletedCoeff n))

194 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) := by

195 rw [hcoeff]

196 simp only [MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id,

197 Function.comp_apply, id_eq,

198 MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul, mul_one]

199 rw [Algebra.smul_def]

200 calc

201 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp

202 (modNCompletedGroupAlgebraStageMap n G U))

203 ((algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) * x)

204 =

205 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp

206 (modNCompletedGroupAlgebraStageMap n G U))

207 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) *

208 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp

209 (modNCompletedGroupAlgebraStageMap n G U)) x := by

210 rw [RingHom.map_mul]

211 _ =

212 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp

213 (modNCompletedGroupAlgebraStageMap n G U))

214 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) *

215 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G

216 (1 : G →* ModNCompletedCoeff n)) x := by

217 rw [hx]

218 _ =

219 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G

220 (1 : G →* ModNCompletedCoeff n))

221 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) *

222 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G

223 (1 : G →* ModNCompletedCoeff n)) x := by

224 rw [hcoeff']

225 _ =

226 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G

227 (1 : G →* ModNCompletedCoeff n))

228 ((algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) * x) := by

229 exact

230 (map_mul

231 (MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G

232 (1 : G →* ModNCompletedCoeff n))

233 (algebraMap (ModNCompletedCoeff n) (ModNCompletedGroupRing n G) a) x).symm

234

235/-- The augmentation value of a residue-coefficient completed point, read at one finite stage. -/

236def modNCompletedGroupAlgebraAugmentationAt (U :

237 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :

238 ModNCompletedGroupAlgebra n G → ModNCompletedCoeff n :=

239 fun x => modNCompletedGroupAlgebraStageAugmentation n G U

240 (modNCompletedGroupAlgebraProjection n G U x)

241

242omit [Fact (0 < n)] in

243/--

244The finite coordinate used to compute the \(n\)-modular completed augmentation is independent of

245passing to a finer quotient stage.

246-/

247@[simp 900]

248theorem modNCompletedGroupAlgebraAugmentationAt_eq_of_le

249 {U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (x :

250 ModNCompletedGroupAlgebra n G) :

251 modNCompletedGroupAlgebraAugmentationAt n G U x =

252 modNCompletedGroupAlgebraAugmentationAt n G V x := by

253 unfold modNCompletedGroupAlgebraAugmentationAt

254 have hcomp := congrFun

255 (congrArg DFunLike.coe

256 (modNCompletedGroupAlgebraStageAugmentation_compatible

257 (n := n) (G := G) (U := U) (V := V) hUV))

258 (modNCompletedGroupAlgebraProjection n G V x)

259 calc

260 modNCompletedGroupAlgebraStageAugmentation n G U

261 (modNCompletedGroupAlgebraProjection n G U x)

262 =

263 modNCompletedGroupAlgebraStageAugmentation n G U

264 (modNCompletedGroupAlgebraTransition n G hUV

265 (modNCompletedGroupAlgebraProjection n G V x)) := by

266 have hx := x.2 U V hUV

267 change modNCompletedGroupAlgebraTransition n G hUV

268 (modNCompletedGroupAlgebraProjection n G V x) =

269 modNCompletedGroupAlgebraProjection n G U x at hx

270 exact congrArg

271 (modNCompletedGroupAlgebraStageAugmentation n G U) hx.symm

272 _ = modNCompletedGroupAlgebraStageAugmentation n G V

273 (modNCompletedGroupAlgebraProjection n G V x) := by

274 exact hcomp

275

276/-- The canonical augmentation on the residue-coefficient completed group algebra. -/

277def modNCompletedGroupAlgebraAugmentation :

278 ModNCompletedGroupAlgebra n G → ModNCompletedCoeff n :=

279 modNCompletedGroupAlgebraAugmentationAt n G

280 (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G)

281

282omit [Fact (0 < n)] in

283/-- The \(n\)-modular completed augmentation is computed at any finite quotient stage. -/

284@[simp]

285theorem modNCompletedGroupAlgebraAugmentation_eq_at

286 (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (x :

287 ModNCompletedGroupAlgebra n G) :

288 modNCompletedGroupAlgebraAugmentation n G x =

289 modNCompletedGroupAlgebraAugmentationAt n G U x := by

290 exact modNCompletedGroupAlgebraAugmentationAt_eq_of_le

291 (n := n) (G := G)

292 (U := _root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G) (V := U)

293 (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex_le (G := G) U) x

294

295omit [Fact (0 < n)] in

296/--

297The \(n\)-modular completed augmentation extends the abstract \(n\)-modular group-algebra

298augmentation through the dense map.

299-/

300@[simp]

301theorem modNCompletedGroupAlgebraAugmentation_toCompleted

302 (x : ModNCompletedGroupRing n G) :

303 modNCompletedGroupAlgebraAugmentation n G (toModNCompletedGroupAlgebra n G x) =

304 MonoidAlgebra.lift (ModNCompletedCoeff n) (ModNCompletedCoeff n) G

305 (1 : G →* ModNCompletedCoeff n) x := by

306 unfold modNCompletedGroupAlgebraAugmentation modNCompletedGroupAlgebraAugmentationAt

307 rw [modNCompletedGroupAlgebraProjection_toCompleted]

308 exact congrFun

309 (congrArg DFunLike.coe

310 (modNCompletedGroupAlgebraStageAugmentation_comp_stageMap

311 (n := n) (G := G) (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G)))

312 x

313

314end

315

316end FoxDifferential