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

1import ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.LimitEquiv

3/-!

4# Fox differential: completed — coefficient rings — prime-power augmentation ideal — augmentation

6The principal declarations in this module are:

8- `primePowerCompletedGroupAlgebraAugmentationAddHom`

9 The canonical prime-power augmentation as an additive homomorphism.

10- `primePowerCompletedGroupAlgebraAugmentationRingHom`

11 The prime-power completed augmentation bundled as a ring homomorphism.

12- `primePowerCompletedGroupAlgebraAugmentation_comp_coeffToGroupAlgebra`

13 The prime-power completed augmentation composed with the coefficient-to-group-algebra map is the

14 identity.

15- `mem_primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal_iff`

16 A prime-power completed group-algebra element lies in the augmentation ideal iff its prime-power

17 augmentation is zero.

18-/

20namespace FoxDifferential

22noncomputable section

24open ProCGroups.InverseSystems

26universe u

29variable (ℓ : ℕ) [Fact (0 < ℓ)]

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

32omit [Fact (0 < ℓ)] in

33/--

34The prime-power completed augmentation composed with the coefficient-to-group-algebra map is the

35identity.

36-/

37@[simp]

38theorem primePowerCompletedGroupAlgebraAugmentation_comp_coeffToGroupAlgebra

39 (x : PrimePowerCompletedCoeff ℓ G) :

40 primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G)

41 (primePowerCompletedCoeffToGroupAlgebra (ℓ := ℓ) (G := G) x) = x := by

42 apply (primePowerCompletedCoeffSystem ℓ G).ext

43 intro i

44 change modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2

45 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i

46 (primePowerCompletedCoeffToGroupAlgebra (ℓ := ℓ) (G := G) x)) = x.1 i

47 change modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2

48 (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i) (x.1 i)) = x.1 i

49 exact primePowerCompletedGroupAlgebraStageAugmentation_algebraMap (ℓ := ℓ) (G := G) i (x.1 i)

51/-- The canonical prime-power augmentation as an additive homomorphism. -/

52def primePowerCompletedGroupAlgebraAugmentationAddHom :

53 PrimePowerCompletedGroupAlgebra ℓ G →+ PrimePowerCompletedCoeff ℓ G where

54 toFun := primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G)

55 map_zero' := by

56 apply (primePowerCompletedCoeffSystem ℓ G).ext

57 intro i

58 change modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2

59 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i 0) = 0

60 rw [primePowerCompletedGroupAlgebraProjection_zero]

61 exact map_zero

62 (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2)

63 map_add' x y := by

64 apply (primePowerCompletedCoeffSystem ℓ G).ext

65 intro i

66 change modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2

67 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (x + y)) =

68 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2

69 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x) +

70 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2

71 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i y)

72 rw [primePowerCompletedGroupAlgebraProjection_add]

73 exact map_add

74 (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2)

75 _ _

77/-- The prime-power completed augmentation bundled as a ring homomorphism. -/

78def primePowerCompletedGroupAlgebraAugmentationRingHom :

79 PrimePowerCompletedGroupAlgebra ℓ G →+* PrimePowerCompletedCoeff ℓ G where

80 toFun := primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G)

81 map_one' := by

82 apply (primePowerCompletedCoeffSystem ℓ G).ext

83 intro i

84 change modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2

85 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i 1) =

86 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i 1

87 rw [primePowerCompletedGroupAlgebraProjection_one,

88 primePowerCompletedCoeffProjection_one]

89 exact map_one (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2)

90 map_mul' := by

91 intro x y

92 apply (primePowerCompletedCoeffSystem ℓ G).ext

93 intro i

94 change modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2

95 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (x * y)) =

96 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i

97 (primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) x *

98 primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) y)

99 rw [primePowerCompletedGroupAlgebraProjection_mul,

100 primePowerCompletedCoeffProjection_mul]

101 exact map_mul (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2)

102 _ _

103 map_zero' := by

104 exact map_zero (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G))

105 map_add' := by

106 intro x y

107 exact map_add (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G)) x y

108

109/-- The completed augmentation ideal is an ideal of the corresponding completed group algebra. -/

110abbrev primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal :

111 Ideal (PrimePowerCompletedGroupAlgebra ℓ G) :=

112 RingHom.ker (primePowerCompletedGroupAlgebraAugmentationRingHom (ℓ := ℓ) (G := G))

113

114variable {ℓ G} in

115omit [Fact (0 < ℓ)] in

116/--

117A prime-power completed group-algebra element lies in the augmentation ideal iff its prime-power

118augmentation is zero.

119-/

120@[simp]

121theorem mem_primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal_iff

122 {x : PrimePowerCompletedGroupAlgebra ℓ G} :

123 x ∈ primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal (ℓ := ℓ) (G := G) ↔

124 primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) x =

125 (0 : PrimePowerCompletedCoeff ℓ G) := by

126 rw [primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal, RingHom.mem_ker]

127 rfl

128

129variable {ℓ G} in

130omit [Fact (0 < ℓ)] in

131/--

132Membership in the prime-power completed augmentation ideal is equivalent to vanishing of every

133finite-stage augmentation projection.

134-/

135theorem mem_primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal_iff_forall

136 {x : PrimePowerCompletedGroupAlgebra ℓ G} :

137 x ∈ primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal (ℓ := ℓ) (G := G) ↔

138 ∀ i : PrimePowerCompletedGroupAlgebraIndex G,

139 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2

140 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x) = 0 := by

141 rw [mem_primePowerCompletedGroupAlgebraAugmentationIdealAsIdeal_iff,

142 ← mem_primePowerCompletedGroupAlgebraAugmentationKernel_iff_forall]

143 rfl

144

145/-- The additive kernel of the prime-power augmentation. -/

146def primePowerCompletedGroupAlgebraAugmentationAddSubgroup :

147 AddSubgroup (PrimePowerCompletedGroupAlgebra ℓ G) :=

148 { carrier := {x |

149 primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G) x = 0}

150 zero_mem' := by

151 exact map_zero (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G))

152 add_mem' := by

153 intro x y hx hy

154 change primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G) (x + y) = 0

155 rw [map_add, hx, hy]

156 simp only [add_zero]

157 neg_mem' := by

158 intro x hx

159 change primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G) (-x) = 0

160 rw [map_neg, hx]

161 simp only [neg_zero]}

162

163omit [Fact (0 < ℓ)] in

164/-- The prime-power completed augmentation is surjective. -/

165theorem primePowerCompletedGroupAlgebraAugmentation_surjective :

166 Function.Surjective (primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G)) := by

167 intro x

168 refine ⟨primePowerCompletedCoeffToGroupAlgebra (ℓ := ℓ) (G := G) x, ?_⟩

169 exact primePowerCompletedGroupAlgebraAugmentation_comp_coeffToGroupAlgebra

170 (ℓ := ℓ) (G := G) x

171

172omit [Fact (0 < ℓ)] in

173/-- The additive form of the prime-power completed augmentation is surjective. -/

174theorem primePowerCompletedGroupAlgebraAugmentationAddHom_surjective :

175 Function.Surjective (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G)) := by

176 simpa [primePowerCompletedGroupAlgebraAugmentationAddHom] using

177 primePowerCompletedGroupAlgebraAugmentation_surjective (ℓ := ℓ) (G := G)

178

179omit [Fact (0 < ℓ)] in

180/--

181The subtype map from the additive augmentation subgroup has image equal to the kernel of the

182prime-power augmentation add-hom.

183-/

184theorem exact_primePowerCompletedGroupAlgebraAugmentationAddSubgroup_subtype :

185 Function.Exact

186 (primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G)).subtype

187 (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G)) := by

188 intro x

189 constructor

190 · intro hx

191 exact ⟨⟨x, hx⟩, rfl⟩

192 · rintro ⟨y, rfl⟩

193 exact y.2

194

195omit [Fact (0 < ℓ)] in

196/--

197The subtype inclusion for the additive subgroup underlying the prime-power augmentation kernel

198is injective.

199-/

200theorem primePowerCompletedGroupAlgebraAugmentationAddSubgroup_subtype_injective :

201 Function.Injective

202 (primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G)).subtype := by

203 intro x y hxy

204 exact Subtype.ext hxy

205

206omit [Fact (0 < ℓ)] in

207/--

208The canonical augmentation sequence with augmentation ideal as kernel is short exact: the

209inclusion is injective, its image is the kernel of augmentation, and the augmentation is

210surjective.

211-/

212theorem primePowerCompletedGroupAlgebraAugmentationAdd_shortExact :

213 Function.Injective

214 (primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G)).subtype ∧

215 Function.Exact

216 (primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G)).subtype

217 (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G)) ∧

218 Function.Surjective

219 (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G)) := by

220 refine ⟨primePowerCompletedGroupAlgebraAugmentationAddSubgroup_subtype_injective

221 (ℓ := ℓ) (G := G), ?_, ?_⟩

222 · exact exact_primePowerCompletedGroupAlgebraAugmentationAddSubgroup_subtype

223 (ℓ := ℓ) (G := G)

224 · exact primePowerCompletedGroupAlgebraAugmentationAddHom_surjective (ℓ := ℓ) (G := G)

225

226/-- The canonical prime-power augmentation is viewed as a \(\mathbb{Z}\)-linear map. -/

227def primePowerCompletedGroupAlgebraAugmentationLinear :

228 PrimePowerCompletedGroupAlgebra ℓ G →ₗ[ℤ] PrimePowerCompletedCoeff ℓ G :=

229 (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G)).toIntLinearMap

230

231/--

232The canonical prime-power augmentation is viewed as a linear map over the prime-power completed

233coefficient ring.

234-/

235def primePowerCompletedGroupAlgebraAugmentationCoeffLinear :

236 PrimePowerCompletedGroupAlgebra ℓ G →ₗ[PrimePowerCompletedCoeff ℓ G]

237 PrimePowerCompletedCoeff ℓ G where

238 toFun := primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G)

239 map_add' := by

240 intro x y

241 exact map_add (primePowerCompletedGroupAlgebraAugmentationAddHom (ℓ := ℓ) (G := G)) x y

242 map_smul' := by

243 intro a x

244 apply (primePowerCompletedCoeffSystem ℓ G).ext

245 intro i

246 change modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2

247 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (a • x)) =

248 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a *

249 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2

250 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x)

251 rw [primePowerCompletedGroupAlgebraProjection_smul, Algebra.smul_def, map_mul,

252 primePowerCompletedGroupAlgebraStageAugmentation_algebraMap]

253

254/-- The coefficient-linear prime-power augmentation sends a group-like basis element to \(1\). -/

255@[simp]

256theorem primePowerCompletedGroupAlgebraAugmentationCoeffLinear_of

257 (ell : Nat)

258 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (h : H) :

259 primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ell) (G := H)

260 (primePowerCompletedGroupAlgebraOf (ell := ell) h) =

261 1 := by

262 apply (primePowerCompletedCoeffSystem ell H).ext

263 intro i

264 change modNCompletedGroupAlgebraStageAugmentation (ell ^ i.1) H i.2

265 (primePowerCompletedGroupAlgebraProjection (ℓ := ell) (G := H) i

266 (primePowerCompletedGroupAlgebraOf (ell := ell) h)) =

267 primePowerCompletedCoeffProjection (ℓ := ell) (G := H) i

268 (1 : PrimePowerCompletedCoeff ell H)

269 rw [primePowerCompletedGroupAlgebraProjection_of,

270 primePowerCompletedCoeffProjection_one]

271 exact modNCompletedGroupAlgebraStageAugmentation_of (n := ell ^ i.1) (G := H) i.2

272 (QuotientGroup.mk h)

273

274/-- The coefficient-linear prime-power completed augmentation sends the unit element to \(1\). -/

275@[simp]

276theorem primePowerCompletedGroupAlgebraAugmentationCoeffLinear_one

277 (ell : Nat)

278 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :

279 primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ell) (G := H)

280 (1 : PrimePowerCompletedGroupAlgebra ell H) =

281 1 := by

282 change primePowerCompletedGroupAlgebraAugmentation (ℓ := ell) (G := H)

283 (1 : PrimePowerCompletedGroupAlgebra ell H) = 1

284 exact map_one (primePowerCompletedGroupAlgebraAugmentationRingHom (ℓ := ell) (G := H))

285

286/-- The coefficient-linear prime-power augmentation is multiplicative on products. -/

287@[simp]

288theorem primePowerCompletedGroupAlgebraAugmentationCoeffLinear_mul

289 (ell : Nat)

290 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

291 (x y : PrimePowerCompletedGroupAlgebra ell H) :

292 primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ell) (G := H) (x * y) =

293 primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ell) (G := H) x *

294 primePowerCompletedGroupAlgebraAugmentationCoeffLinear (ℓ := ell) (G := H) y := by

295 change primePowerCompletedGroupAlgebraAugmentation (ℓ := ell) (G := H) (x * y) =

296 primePowerCompletedGroupAlgebraAugmentation (ℓ := ell) (G := H) x *

297 primePowerCompletedGroupAlgebraAugmentation (ℓ := ell) (G := H) y

298 exact map_mul (primePowerCompletedGroupAlgebraAugmentationRingHom (ℓ := ell) (G := H)) x y

299

300/--

301The kernel inclusion of the prime-power augmentation is viewed as a \(\mathbb{Z}\)-linear map.

302-/

303def primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear :

304 primePowerCompletedGroupAlgebraAugmentationAddSubgroup (ℓ := ℓ) (G := G) →ₗ[ℤ]

305 PrimePowerCompletedGroupAlgebra ℓ G :=

306 (primePowerCompletedGroupAlgebraAugmentationAddSubgroup

307 (ℓ := ℓ) (G := G)).subtype.toIntLinearMap

308

309omit [Fact (0 < ℓ)] in

310/-- The linear form of the prime-power completed augmentation is surjective. -/

311theorem primePowerCompletedGroupAlgebraAugmentationLinear_surjective :

312 Function.Surjective

313 (primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G)) := by

314 simpa [primePowerCompletedGroupAlgebraAugmentationLinear, AddMonoidHom.coe_toIntLinearMap] using

315 primePowerCompletedGroupAlgebraAugmentationAddHom_surjective (ℓ := ℓ) (G := G)

316

317omit [Fact (0 < ℓ)] in

318/--

319The linear subtype inclusion for the additive subgroup underlying the prime-power augmentation

320kernel is injective.

321-/

322theorem primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear_injective :

323 Function.Injective

324 (primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear

325 (ℓ := ℓ) (G := G)) := by

326 exact primePowerCompletedGroupAlgebraAugmentationAddSubgroup_subtype_injective

327 (ℓ := ℓ) (G := G)

328

329omit [Fact (0 < ℓ)] in

330/--

331The linear subtype map from the additive augmentation subgroup has image equal to the kernel of

332the prime-power augmentation linear map.

333-/

334theorem exact_primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear :

335 Function.Exact

336 (primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear

337 (ℓ := ℓ) (G := G))

338 (primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G)) := by

339 simpa [primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear,

340 primePowerCompletedGroupAlgebraAugmentationLinear, AddMonoidHom.coe_toIntLinearMap] using

341 exact_primePowerCompletedGroupAlgebraAugmentationAddSubgroup_subtype

342 (ℓ := ℓ) (G := G)

343

344omit [Fact (0 < ℓ)] in

345/--

346The canonical augmentation sequence with augmentation ideal as kernel is short exact: the

347inclusion is injective, its image is the kernel of augmentation, and the augmentation is

348surjective.

349-/

350theorem primePowerCompletedGroupAlgebraAugmentationLinear_shortExact :

351 Function.Injective

352 (primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear

353 (ℓ := ℓ) (G := G)) ∧

354 Function.Exact

355 (primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear

356 (ℓ := ℓ) (G := G))

357 (primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G)) ∧

358 Function.Surjective

359 (primePowerCompletedGroupAlgebraAugmentationLinear (ℓ := ℓ) (G := G)) := by

360 refine ⟨primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear_injective

361 (ℓ := ℓ) (G := G), ?_, ?_⟩

362 · exact exact_primePowerCompletedGroupAlgebraAugmentationAddSubgroupSubtypeLinear

363 (ℓ := ℓ) (G := G)

364 · exact primePowerCompletedGroupAlgebraAugmentationLinear_surjective (ℓ := ℓ) (G := G)

365

366

367end

368

369end FoxDifferential