Source: ProCGroups.FoxDifferential.Common.CrossedDifferentialModule

1import ProCGroups.FoxDifferential.Common.CrossedDifferential

2import Mathlib.Algebra.MonoidAlgebra.Basic

3import Mathlib.LinearAlgebra.Finsupp.LinearCombination

4import Mathlib.LinearAlgebra.Quotient.Basic

6/-!

7# Fox differential: common — crossed differential module

9The principal declarations in this module are:

11- `CrossedDifferentialPreModule`

12 The free \(R\)-module on the underlying set of a group \(G\).

13- `crossedDifferentialRelationElement`

14 The universal crossed-differential relation \(d(g_1g_2) = d(g_1) + \mathrm{coeff}(g_1) \cdot

15 d(g_2)\) in the free pre-module.

16- `crossedDifferentialRelationElement_mem`

17 Every defining crossed-differential relation belongs to the relation submodule.

18- `universalCrossedDifferential_mul`

19 The universal crossed differential satisfies the crossed product rule.

20-/

22namespace FoxDifferential

24noncomputable section

26variable {R G : Type*} [Ring R] [Group G]

28/-- The free \(R\)-module on the underlying set of a group \(G\). -/

29abbrev CrossedDifferentialPreModule (R G : Type*) [Ring R] : Type _ :=

30 G →₀ R

32/--

33The universal crossed-differential relation \(d(g_1g_2) = d(g_1) + \mathrm{coeff}(g_1) \cdot

34d(g_2)\) in the free pre-module.

35-/

36def crossedDifferentialRelationElement (coeff : G →* R) (g₁ g₂ : G) :

37 CrossedDifferentialPreModule R G :=

38 Finsupp.single (g₁ * g₂) 1 -

39 (Finsupp.single g₁ 1 + coeff g₁ • Finsupp.single g₂ 1)

41/-- The submodule generated by all universal crossed-differential relations. -/

42def crossedDifferentialRelationSubmodule (coeff : G →* R) :

43 Submodule R (CrossedDifferentialPreModule R G) :=

44 Submodule.span R (Set.range fun p : G × G =>

45 crossedDifferentialRelationElement coeff p.1 p.2)

47/--

48The universal module representing crossed differentials with coefficient homomorphism

49\(\mathrm{coeff}:G\to R\), viewed multiplicatively.

50-/

51abbrev CrossedDifferentialModule (coeff : G →* R) : Type _ :=

52 CrossedDifferentialPreModule R G ⧸ crossedDifferentialRelationSubmodule coeff

54/-- The universal crossed differential `d_coeff : G -> CrossedDifferentialModule coeff`. -/

55def universalCrossedDifferential (coeff : G →* R) (g : G) :

56 CrossedDifferentialModule coeff :=

57 (crossedDifferentialRelationSubmodule coeff).mkQ (Finsupp.single g 1)

59/-- Every defining crossed-differential relation belongs to the relation submodule. -/

60theorem crossedDifferentialRelationElement_mem (coeff : G →* R) (g₁ g₂ : G) :

61 crossedDifferentialRelationElement coeff g₁ g₂ ∈

62 crossedDifferentialRelationSubmodule coeff := by

63 exact Submodule.subset_span ⟨(g₁, g₂), rfl⟩

65/-- The universal crossed differential satisfies the crossed product rule. -/

66theorem universalCrossedDifferential_mul (coeff : G →* R) (g₁ g₂ : G) :

67 universalCrossedDifferential coeff (g₁ * g₂) =

68 universalCrossedDifferential coeff g₁ +

69 coeff g₁ • universalCrossedDifferential coeff g₂ := by

70 have hzero :

71 (crossedDifferentialRelationSubmodule coeff).mkQ

72 (crossedDifferentialRelationElement coeff g₁ g₂) = 0 := by

73 exact

74 (Submodule.Quotient.mk_eq_zero

75 (p := crossedDifferentialRelationSubmodule coeff)

76 (x := crossedDifferentialRelationElement coeff g₁ g₂)).2

77 (crossedDifferentialRelationElement_mem coeff g₁ g₂)

78 have hzero' :

79 universalCrossedDifferential coeff (g₁ * g₂) -

80 (universalCrossedDifferential coeff g₁ +

81 (crossedDifferentialRelationSubmodule coeff).mkQ

82 (coeff g₁ • Finsupp.single g₂ 1)) = 0 := by

83 simpa [universalCrossedDifferential, crossedDifferentialRelationElement] using hzero

84 have hsmul :

85 (crossedDifferentialRelationSubmodule coeff).mkQ

86 (coeff g₁ • Finsupp.single g₂ 1) =

87 coeff g₁ • universalCrossedDifferential coeff g₂ := by

88 simpa [universalCrossedDifferential, Submodule.mkQ_apply] using

89 (Submodule.Quotient.mk_smul (p := crossedDifferentialRelationSubmodule coeff)

90 (r := coeff g₁) (x := Finsupp.single g₂ 1))

91 have hzero'' :

92 universalCrossedDifferential coeff (g₁ * g₂) -

93 (universalCrossedDifferential coeff g₁ +

94 coeff g₁ • universalCrossedDifferential coeff g₂) = 0 := by

95 rw [hsmul] at hzero'

96 exact hzero'

97 exact sub_eq_zero.mp hzero''

99/--

100The universal crossed differential \(d_{\mathrm{coeff}} : G \to

101\mathrm{CrossedDifferentialModule}(\mathrm{coeff})\).

102-/

103def universalCrossedHom (coeff : G →* R) :

104 ScalarCrossedHom coeff (CrossedDifferentialModule coeff) where

105 toFun := universalCrossedDifferential coeff

106 map_mul' := by

107 intro g₁ g₂

108 change universalCrossedDifferential coeff (g₁ * g₂) =

109 universalCrossedDifferential coeff g₁ +

110 coeff g₁ • universalCrossedDifferential coeff g₂

111 exact universalCrossedDifferential_mul coeff g₁ g₂

112

113/-- The universal crossed differential vanishes at the identity. -/

114@[simp]

115theorem universalCrossedDifferential_one (coeff : G →* R) :

116 universalCrossedDifferential coeff (1 : G) = 0 :=

117 ScalarCrossedHom.map_one (universalCrossedHom coeff)

118

119section UniversalProperty

120

121variable {A : Type*} [AddCommGroup A] [Module R A]

122

123/-- The linear extension of a map out of G to the free crossed-differential pre-module. -/

124def crossedDifferentialModuleLiftLinear (delta : G → A) :

125 CrossedDifferentialPreModule R G →ₗ[R] A :=

126 Finsupp.linearCombination R delta

127

128omit [Group G] in

129/-- The linear extension of a map evaluates on a single basis vector by scalar multiplication. -/

130@[simp]

131theorem crossedDifferentialModuleLiftLinear_single (delta : G → A) (g : G) (r : R) :

132 crossedDifferentialModuleLiftLinear (R := R) delta (Finsupp.single g r) = r • delta g := by

133 simp only [crossedDifferentialModuleLiftLinear, Finsupp.linearCombination_single]

134

135/-- A crossed differential kills each defining universal relation. -/

136theorem crossedHomModuleLiftLinear_relationElement

137 (coeff : G →* R) (delta : ScalarCrossedHom coeff A) (g₁ g₂ : G) :

138 crossedDifferentialModuleLiftLinear (R := R) delta

139 (crossedDifferentialRelationElement coeff g₁ g₂) = 0 := by

140 simp only [crossedDifferentialModuleLiftLinear, crossedDifferentialRelationElement,

141 Finsupp.smul_single, smul_eq_mul, mul_one, map_sub,

142 Finsupp.linearCombination_single, ScalarCrossedHom.map_mul, smul_add, one_smul,

143 map_add, sub_self]

144

145/--

146The relation submodule is contained in the kernel of the linear extension of a crossed

147differential.

148-/

149theorem crossedHomRelationSubmodule_le_ker

150 (coeff : G →* R) (delta : ScalarCrossedHom coeff A) :

151 crossedDifferentialRelationSubmodule coeff ≤

152 LinearMap.ker (crossedDifferentialModuleLiftLinear (R := R) delta) := by

153 refine Submodule.span_le.2 ?_

154 rintro _ ⟨⟨g₁, g₂⟩, rfl⟩

155 simpa [LinearMap.mem_ker] using

156 crossedHomModuleLiftLinear_relationElement (A := A) coeff delta g₁ g₂

157

158/-- The universal linear map induced by a crossed differential. -/

159def crossedHomModuleLift

160 (coeff : G →* R) (delta : ScalarCrossedHom coeff A) :

161 CrossedDifferentialModule coeff →ₗ[R] A :=

162 (crossedDifferentialRelationSubmodule coeff).liftQ

163 (crossedDifferentialModuleLiftLinear (R := R) delta)

164 (crossedHomRelationSubmodule_le_ker (A := A) coeff delta)

165

166/--

167The universal lift evaluated on a quotient representative is the finite linear combination of

168the prescribed crossed differential on that representative.

169-/

170theorem crossedHomModuleLift_mkQ

171 (coeff : G →* R) (delta : ScalarCrossedHom coeff A)

172 (x : CrossedDifferentialPreModule R G) :

173 crossedHomModuleLift (A := A) coeff delta

174 ((crossedDifferentialRelationSubmodule coeff).mkQ x) =

175 crossedDifferentialModuleLiftLinear (R := R) delta x := by

176 rw [crossedHomModuleLift, Submodule.mkQ_apply, Submodule.liftQ_apply]

177

178/--

179The universal lift evaluates on \(d_{\mathrm{coeff}}(g)\) as the original crossed differential.

180-/

181@[simp]

182theorem crossedHomModuleLift_universal

183 (coeff : G →* R) (delta : ScalarCrossedHom coeff A) (g : G) :

184 crossedHomModuleLift (A := A) coeff delta (universalCrossedDifferential coeff g) = delta g := by

185 change

186 (crossedDifferentialRelationSubmodule coeff).liftQ

187 (crossedDifferentialModuleLiftLinear (R := R) delta)

188 (crossedHomRelationSubmodule_le_ker (A := A) coeff delta)

189 ((crossedDifferentialRelationSubmodule coeff).mkQ (Finsupp.single g 1)) = delta g

190 rw [Submodule.mkQ_apply, Submodule.liftQ_apply]

191 simp only [crossedDifferentialModuleLiftLinear_single, one_smul]

192

193/--

194Linear maps out of the universal crossed-differential module are equal when they agree on all

195universal differentials.

196-/

197@[ext]

198theorem crossedDifferentialModuleHom_ext

199 (coeff : G →* R) {f h : CrossedDifferentialModule coeff →ₗ[R] A}

200 (hfh : ∀ g, f (universalCrossedDifferential coeff g) =

201 h (universalCrossedDifferential coeff g)) :

202 f = h := by

203 apply Submodule.linearMap_qext _

204 apply Finsupp.lhom_ext

205 intro g r

206 have hsingle :

207 ((crossedDifferentialRelationSubmodule coeff).mkQ (Finsupp.single g r) :

208 CrossedDifferentialModule coeff) =

209 r • universalCrossedDifferential coeff g := by

210 rw [← Finsupp.smul_single_one]

211 rfl

212 change f ((crossedDifferentialRelationSubmodule coeff).mkQ (Finsupp.single g r)) =

213 h ((crossedDifferentialRelationSubmodule coeff).mkQ (Finsupp.single g r))

214 simpa [hsingle, map_smul] using congrArg (fun z => r • z) (hfh g)

215

216/--

217The universal lift is the unique linear map with prescribed values on universal differentials.

218-/

219theorem crossedHomModuleLift_unique

220 (coeff : G →* R) (delta : ScalarCrossedHom coeff A)

221 (f : CrossedDifferentialModule coeff →ₗ[R] A)

222 (hf : ∀ g, f (universalCrossedDifferential coeff g) = delta g) :

223 f = crossedHomModuleLift (A := A) coeff delta := by

224 apply crossedDifferentialModuleHom_ext coeff

225 intro g

226 rw [hf g, crossedHomModuleLift_universal]

227

228/-- Existence and uniqueness of the linear map representing a crossed differential. -/

229theorem existsUnique_crossedHomModuleLift

230 (coeff : G →* R) (delta : ScalarCrossedHom coeff A) :

231 ∃! f : CrossedDifferentialModule coeff →ₗ[R] A,

232 ∀ g, f (universalCrossedDifferential coeff g) = delta g := by

233 refine ⟨crossedHomModuleLift (A := A) coeff delta, ?_, ?_⟩

234 · intro g

235 exact crossedHomModuleLift_universal (A := A) coeff delta g

236 · intro f hf

237 exact crossedHomModuleLift_unique (A := A) coeff delta f hf

238

239/-- The crossed differential induced by a linear map out of the universal module. -/

240def crossedHomOfModuleLinearMap

241 (coeff : G →* R) (f : CrossedDifferentialModule coeff →ₗ[R] A) :

242 ScalarCrossedHom coeff A where

243 toFun g := f (universalCrossedDifferential coeff g)

244 map_mul' := by

245 intro g₁ g₂

246 change f (universalCrossedDifferential coeff (g₁ * g₂)) =

247 f (universalCrossedDifferential coeff g₁) +

248 coeff g₁ • f (universalCrossedDifferential coeff g₂)

249 rw [universalCrossedDifferential_mul, map_add, map_smul]

250

251/-- The crossed homomorphism induced by a linear map evaluates the map on the universal

252differential. -/

253@[simp]

254theorem crossedHomOfModuleLinearMap_apply

255 (coeff : G →* R) (f : CrossedDifferentialModule coeff →ₗ[R] A) (g : G) :

256 crossedHomOfModuleLinearMap (A := A) coeff f g =

257 f (universalCrossedDifferential coeff g) :=

258 rfl

259

260/--

261Crossed differentials \(G \to A\) with coefficient homomorphism \(\mathrm{coeff}:G \to R\) are

262represented by \(R\)-linear maps out of the universal module

263\(\mathrm{CrossedDifferentialModule}\,\mathrm{coeff}\).

264-/

265def crossedHomModuleEquivLinearMap (coeff : G →* R) :

266 ScalarCrossedHom coeff A ≃ (CrossedDifferentialModule coeff →ₗ[R] A) where

267 toFun delta := crossedHomModuleLift (A := A) coeff delta

268 invFun f := crossedHomOfModuleLinearMap (A := A) coeff f

269 left_inv delta := by

270 apply CrossedHom.ext

271 intro g

272 change crossedHomModuleLift (A := A) coeff delta

273 (universalCrossedDifferential coeff g) = delta g

274 exact crossedHomModuleLift_universal (A := A) coeff delta g

275 right_inv f := by

276 apply crossedDifferentialModuleHom_ext coeff

277 intro g

278 change crossedHomModuleLift (A := A) coeff

279 (crossedHomOfModuleLinearMap (A := A) coeff f)

280 (universalCrossedDifferential coeff g) =

281 f (universalCrossedDifferential coeff g)

282 exact crossedHomModuleLift_universal (A := A) coeff

283 (crossedHomOfModuleLinearMap (A := A) coeff f) g

284

285end UniversalProperty

286

287section MonoidAlgebraIdentityBoundary

288

289variable {S : Type*} [CommRing S]

290

291/--

292The S-linear map from a group algebra to the identity crossed-differential module sending

293\([g]\) to the universal differential d g.

294-/

295def monoidAlgebraToIdentityCrossedDifferentialModule :

296 MonoidAlgebra S G →ₗ[S]

297 CrossedDifferentialModule (MonoidAlgebra.of S G) :=

298 (Finsupp.linearCombination S

299 (fun g : G => universalCrossedDifferential (MonoidAlgebra.of S G) g)).comp

300 (MonoidAlgebra.coeffLinearEquiv S).toLinearMap

301

302/-- A group-algebra basis term maps to its coefficient times the corresponding universal

303differential. -/

304@[simp]

305theorem monoidAlgebraToIdentityCrossedDifferentialModule_single (g : G) (a : S) :

306 monoidAlgebraToIdentityCrossedDifferentialModule

307 (MonoidAlgebra.single g a : MonoidAlgebra S G) =

308 a • universalCrossedDifferential (MonoidAlgebra.of S G) g := by

309 change

310 (Finsupp.linearCombination S

311 (fun g : G => universalCrossedDifferential (MonoidAlgebra.of S G) g))

312 (Finsupp.single g a) =

313 a • universalCrossedDifferential (MonoidAlgebra.of S G) g

314 exact Finsupp.linearCombination_single

315 (R := S)

316 (v := fun g : G => universalCrossedDifferential (MonoidAlgebra.of S G) g)

317 (c := a) (a := g)

318

319/--

320The linear map from the group algebra to the identity crossed-differential module sends

321\(a([g]-1)\) to \(a\) acting on the universal differential of \(g\).

322-/

323theorem monoidAlgebraToIdentityCrossedDifferentialModule_mul_sub_one

324 (a : MonoidAlgebra S G) (g : G) :

325 monoidAlgebraToIdentityCrossedDifferentialModule

326 (a * (MonoidAlgebra.of S G g - 1)) =

327 a • universalCrossedDifferential (MonoidAlgebra.of S G) g := by

328 refine MonoidAlgebra.induction_linear a ?zero ?add ?single

329 · simp only [MonoidAlgebra.of_apply, zero_mul, map_zero, zero_smul]

330 · intro a b ha hb

331 rw [add_mul, map_add, ha, hb, add_smul]

332 · intro p c

333 rw [MonoidAlgebra.of_apply]

334 rw [mul_sub, mul_one, MonoidAlgebra.single_mul_single]

335 change

336 monoidAlgebraToIdentityCrossedDifferentialModule

337 (MonoidAlgebra.single (p * g) (c * 1) - MonoidAlgebra.single p c) =

338 (MonoidAlgebra.single p c : MonoidAlgebra S G) •

339 universalCrossedDifferential (MonoidAlgebra.of S G) g

340 rw [map_sub]

341 rw [monoidAlgebraToIdentityCrossedDifferentialModule_single,

342 monoidAlgebraToIdentityCrossedDifferentialModule_single]

343 simp only [mul_one]

344 rw [universalCrossedDifferential_mul]

345 rw [smul_add, add_sub_cancel_left]

346 rw [MonoidAlgebra.of_apply]

347 rw [show (MonoidAlgebra.single p c : MonoidAlgebra S G) =

348 c • MonoidAlgebra.single p 1 by

349 simp only [MonoidAlgebra.smul_single, smul_eq_mul, mul_one]]

350 exact (smul_assoc c (MonoidAlgebra.single p 1 : MonoidAlgebra S G)

351 (universalCrossedDifferential (MonoidAlgebra.of S G) g)).symm

352

353/-- The group-algebra boundary `g ↦ [g] - 1`, bundled as a scalar crossed homomorphism. -/

354def identityGroupAlgebraCrossedHom :

355 ScalarCrossedHom (MonoidAlgebra.of S G) (MonoidAlgebra S G) where

356 toFun g := MonoidAlgebra.of S G g - 1

357 map_mul' := by

358 intro g h

359 change MonoidAlgebra.of S G (g * h) - 1 =

360 (MonoidAlgebra.of S G g - 1) +

361 MonoidAlgebra.of S G g • (MonoidAlgebra.of S G h - 1)

362 simp only [map_mul, MonoidAlgebra.of_apply,

363 MonoidAlgebra.single_mul_single, mul_one, sub_eq_add_neg, smul_eq_mul, mul_add,

364 mul_neg, add_comm, add_assoc, neg_add_cancel_left]

365

366/-- The identity-coefficient crossed homomorphism sends a group element to its group-like term

367minus one. -/

368@[simp]

369theorem identityGroupAlgebraCrossedHom_apply (g : G) :

370 identityGroupAlgebraCrossedHom (S := S) (G := G) g =

371 MonoidAlgebra.of S G g - 1 :=

372 rfl

373

374/-- The identity crossed-differential boundary sends \(d g\) to \([g] - 1\) over a group algebra. -/

375def identityCrossedDifferentialBoundary :

376 CrossedDifferentialModule (MonoidAlgebra.of S G) →ₗ[MonoidAlgebra S G]

377 MonoidAlgebra S G :=

378 crossedHomModuleLift

379 (A := MonoidAlgebra S G) (MonoidAlgebra.of S G)

380 (identityGroupAlgebraCrossedHom (S := S) (G := G))

381

382/--

383The identity crossed-differential boundary sends the universal differential at \(g\) to the

384group-algebra element \([g]-1\).

385-/

386@[simp]

387theorem identityCrossedDifferentialBoundary_universal (g : G) :

388 identityCrossedDifferentialBoundary

389 (universalCrossedDifferential (MonoidAlgebra.of S G) g) =

390 MonoidAlgebra.of S G g - 1 := by

391 rw [identityCrossedDifferentialBoundary, crossedHomModuleLift_universal,

392 identityGroupAlgebraCrossedHom_apply]

393

394/--

395Composing the identity-boundary map with the monoid-algebra comparison has the stated value on

396quotient generators.

397-/

398theorem monoidAlgebraToIdentityCrossedDifferentialModule_comp_identityBoundary_mkQ

399 (x : CrossedDifferentialPreModule (MonoidAlgebra S G) G) :

400 monoidAlgebraToIdentityCrossedDifferentialModule

401 (crossedDifferentialModuleLiftLinear

402 (R := MonoidAlgebra S G)

403 (fun g : G => MonoidAlgebra.of S G g - 1) x) =

404 (crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ x := by

405 refine Finsupp.induction_linear x ?zero ?add ?single

406 · simp only [crossedDifferentialModuleLiftLinear, MonoidAlgebra.of_apply, map_zero]

407 · intro x y hx hy

408 rw [map_add, map_add]

409 exact congrArg₂ (· + ·)

410 (by simpa [MonoidAlgebra.of_apply] using hx)

411 (by simpa [MonoidAlgebra.of_apply] using hy)

412 · intro g a

413 rw [crossedDifferentialModuleLiftLinear_single]

414 change

415 monoidAlgebraToIdentityCrossedDifferentialModule

416 (a * (MonoidAlgebra.of S G g - 1)) =

417 (crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ

418 (Finsupp.single g a)

419 rw [monoidAlgebraToIdentityCrossedDifferentialModule_mul_sub_one]

420 rw [← Finsupp.smul_single_one]

421 exact

422 (Submodule.Quotient.mk_smul

423 (p := crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G))

424 (r := a) (x := Finsupp.single g 1)).symm

425

426/--

427The boundary of the additive lift \(\sum a_g [g] \mapsto \sum a_g d g\) is the augmentation-zero

428part of the group-algebra element.

429-/

430theorem idCrossedDiffBoundary_monoidAlgebraToModule

431 (a : MonoidAlgebra S G) :

432 identityCrossedDifferentialBoundary

433 (monoidAlgebraToIdentityCrossedDifferentialModule (S := S) (G := G) a) =

434 a -

435 MonoidAlgebra.single (1 : G)

436 ((MonoidAlgebra.lift S S G (1 : G →* S)) a) := by

437 refine MonoidAlgebra.induction_linear a ?zero ?add ?single

438 · simp only [map_zero, MonoidAlgebra.single_zero, sub_zero]

439 · intro x y hx hy

440 rw [show

441 monoidAlgebraToIdentityCrossedDifferentialModule (S := S) (G := G) (x + y) =

442 monoidAlgebraToIdentityCrossedDifferentialModule x +

443 monoidAlgebraToIdentityCrossedDifferentialModule y by

444 rw [map_add]]

445 rw [show

446 identityCrossedDifferentialBoundary

447 (monoidAlgebraToIdentityCrossedDifferentialModule x +

448 monoidAlgebraToIdentityCrossedDifferentialModule y) =

449 identityCrossedDifferentialBoundary

450 (monoidAlgebraToIdentityCrossedDifferentialModule x) +

451 identityCrossedDifferentialBoundary

452 (monoidAlgebraToIdentityCrossedDifferentialModule y) by

453 rw [map_add]]

454 rw [hx, hy]

455 have haug :

456 ((MonoidAlgebra.lift S S G (1 : G →* S)) (x + y : MonoidAlgebra S G)) =

457 ((MonoidAlgebra.lift S S G (1 : G →* S)) x) +

458 ((MonoidAlgebra.lift S S G (1 : G →* S)) y) := by

459 exact map_add (MonoidAlgebra.lift S S G (1 : G →* S)) x y

460 rw [haug]

461 simp only [sub_eq_add_neg, add_left_comm, add_assoc, MonoidAlgebra.single_add,

462 neg_add_rev, add_comm]

463 · intro g c

464 calc

465 identityCrossedDifferentialBoundary

466 (monoidAlgebraToIdentityCrossedDifferentialModule

467 (MonoidAlgebra.single g c)) =

468 identityCrossedDifferentialBoundary

469 (c • universalCrossedDifferential (MonoidAlgebra.of S G) g) := by

470 rw [monoidAlgebraToIdentityCrossedDifferentialModule_single]

471 _ =

472 (MonoidAlgebra.single g c : MonoidAlgebra S G) -

473 MonoidAlgebra.single (1 : G)

474 ((MonoidAlgebra.lift S S G (1 : G →* S))

475 (MonoidAlgebra.single g c : MonoidAlgebra S G)) := by

476 rw [LinearMap.map_smul_of_tower,

477 identityCrossedDifferentialBoundary_universal]

478 rw [Algebra.smul_def, MonoidAlgebra.of_apply]

479 rw [show (algebraMap S (MonoidAlgebra S G)) c =

480 MonoidAlgebra.single (1 : G) c by rfl]

481 rw [mul_sub, mul_one, MonoidAlgebra.single_mul_single]

482 simp only [one_mul, mul_one, MonoidAlgebra.lift_single, MonoidHom.one_apply,

483 smul_eq_mul]

484

485/--

486On the augmentation ideal, the additive lift \(\sum a_g [g] \mapsto \sum a_g d g\) is a right

487inverse to the identity crossed-differential boundary.

488-/

489theorem idCrossedDiffBoundary_monoidAlgebraToModule_of_augmentation_eq_zero

490 {a : MonoidAlgebra S G}

491 (ha : (MonoidAlgebra.lift S S G (1 : G →* S)) a = 0) :

492 identityCrossedDifferentialBoundary

493 (monoidAlgebraToIdentityCrossedDifferentialModule (S := S) (G := G) a) = a := by

494 rw [idCrossedDiffBoundary_monoidAlgebraToModule,

495 ha]

496 simp only [MonoidAlgebra.single_zero, sub_zero]

497

498/--

499For the identity coefficient map into a group algebra, the boundary map sending \(d g\) to \([g]

500- 1\) is injective.

501-/

502theorem identityCrossedDifferentialBoundary_injective :

503 Function.Injective (identityCrossedDifferentialBoundary (S := S) (G := G)) := by

504 intro x y hxy

505 revert y

506 refine Submodule.Quotient.induction_on

507 (p := crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)) x ?_

508 intro x y hxy'

509 revert hxy'

510 refine Submodule.Quotient.induction_on

511 (p := crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)) y ?_

512 intro y hxy'

513 apply (Submodule.Quotient.eq

514 (crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G))).2

515 have hdiff :

516 crossedDifferentialModuleLiftLinear

517 (R := MonoidAlgebra S G)

518 (fun g : G => MonoidAlgebra.of S G g - 1) (x - y) = 0 := by

519 have hboundary :

520 identityCrossedDifferentialBoundary

521 ((crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ (x - y)) =

522 0 := by

523 rw [show

524 (crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ (x - y) =

525 (crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ x -

526 (crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ y by

527 rw [map_sub]]

528 rw [map_sub]

529 have hxy'' :

530 identityCrossedDifferentialBoundary

531 ((crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ x) =

532 identityCrossedDifferentialBoundary

533 ((crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ y) := by

534 simpa [Submodule.mkQ_apply] using hxy'

535 rw [hxy'', sub_self]

536 rw [map_sub]

537 rw [identityCrossedDifferentialBoundary, crossedHomModuleLift_mkQ] at hboundary

538 rw [map_sub] at hboundary

539 exact hboundary

540 have hmk :

541 (crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ (x - y) =

542 0 := by

543 have happ :=

544 monoidAlgebraToIdentityCrossedDifferentialModule_comp_identityBoundary_mkQ

545 (S := S) (G := G) (x - y)

546 rw [hdiff, map_zero] at happ

547 exact happ.symm

548 exact

549 (Submodule.Quotient.mk_eq_zero

550 (p := crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G))

551 (x := x - y)).1 hmk

552

553end MonoidAlgebraIdentityBoundary

554

555end

556

557end FoxDifferential