Source: ProCGroups.FoxDifferential.Discrete.KernelBoundary.IdentityAugmentation

1import ProCGroups.FoxDifferential.Discrete.GroupRing

2import Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

3import Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro

5/-!

6# Fox differential: discrete — kernel boundary — identity augmentation

8The principal declarations in this module are:

10- `coinvariantsLEquivOfSubsingleton`

11 For a representation of a subsingleton monoid, taking coinvariants does not change the underlying

12 module.

13- `rightRegularRepresentation`

14 The right-regular \(\mathbb{Z}\)-linear representation on \(\mathbb{Z}[H]\), given by right

15 multiplication by \(g^{-1}\). This is the representation whose low-degree group homology matches

16 the identity-case Crowell relations.

17- `rightRegularRepresentation_apply_single`

18 The right-regular representation sends a single group element to the corresponding basis action.

19- `rightRegularRepresentation_apply_of`

20 The right-regular representation has the displayed value on a representative.

21-/

23namespace FoxDifferential

25noncomputable section

27open CategoryTheory Limits Representation Rep TensorProduct

28open scoped TensorProduct

31variable (H : Type) [Group H] [DecidableEq H]

33/--

34For a representation of a subsingleton monoid, taking coinvariants does not change the

35underlying module.

36-/

37def coinvariantsLEquivOfSubsingleton

38 {k G V : Type*} [CommRing k] [Monoid G] [Subsingleton G]

39 [AddCommGroup V] [Module k V] (ρ : Representation k G V) :

40 Representation.Coinvariants ρ ≃ₗ[k] V := by

41 refine LinearEquiv.ofLinear

42 (Representation.Coinvariants.lift ρ LinearMap.id ?_)

43 (Representation.Coinvariants.mk ρ)

44 ?_ ?_

45 · intro g

46 ext x

47 have : g = (1 : G) := Subsingleton.elim _ _

48 subst this

49 simp only [map_one, LinearMap.id_comp, Module.End.one_apply, LinearMap.id_coe, id_eq]

50 · ext x

51 simp only [Coinvariants.lift_comp_mk, LinearMap.id_coe, id_eq]

52 · apply Representation.Coinvariants.hom_ext

53 ext x

54 simp only [LinearMap.coe_comp, Function.comp_apply, Coinvariants.lift_mk, LinearMap.id_coe,

55 id_eq,

56 LinearMap.id_comp]

58/--

59The right-regular \(\mathbb{Z}\)-linear representation on \(\mathbb{Z}[H]\), given by right

60multiplication by \(g^{-1}\). This is the representation whose low-degree group homology matches

61the identity-case Crowell relations.

62-/

63def rightRegularRepresentation : Representation ℤ H (GroupRing H) where

64 toFun g :=

65 { toFun := fun x => x * MonoidAlgebra.of ℤ H g⁻¹

66 map_add' := by

67 intro x y

68 simp only [MonoidAlgebra.of_apply, add_mul]

69 map_smul' := by

70 intro n x

71 simpa using smul_mul_assoc n x (MonoidAlgebra.of ℤ H g⁻¹) }

72 map_one' := by

73 ext x

74 simp only [inv_one, MonoidAlgebra.of_apply, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk,

75 Function.comp_apply, MonoidAlgebra.lsingle_apply, MonoidAlgebra.single_mul_single, mul_one,

76 Module.End.one_apply]

77 map_mul' g₁ g₂ := by

78 ext x

79 simp only [mul_inv_rev, MonoidAlgebra.of_apply, LinearMap.coe_comp, LinearMap.coe_mk,

80 AddHom.coe_mk,

81 Function.comp_apply, MonoidAlgebra.lsingle_apply, MonoidAlgebra.single_mul_single, mul_one,

82 Module.End.mul_apply,

83 mul_assoc]

85omit [DecidableEq H] in

86/--

87The right-regular representation sends a single group element to the corresponding basis action.

88-/

89@[simp]

90theorem rightRegularRepresentation_apply_single (g h : H) (n : ℤ) :

91 rightRegularRepresentation H g (MonoidAlgebra.single h n) =

92 MonoidAlgebra.single (h * g⁻¹) n := by

93 ext a

94 simp only [rightRegularRepresentation, MonoidAlgebra.of_apply, MonoidHom.coe_mk, OneHom.coe_mk,

95 LinearMap.coe_mk, AddHom.coe_mk, MonoidAlgebra.single_mul_single, mul_one]

97omit [DecidableEq H] in

98/-- The right-regular representation has the displayed value on a representative. -/

99@[simp]

100theorem rightRegularRepresentation_apply_of (g h : H) :

101 rightRegularRepresentation H g (MonoidAlgebra.of ℤ H h : GroupRing H) =

102 MonoidAlgebra.of ℤ H (h * g⁻¹) := by

103 exact rightRegularRepresentation_apply_single (H := H) g h (1 : ℤ)

104

105/-- The right-regular representation as an object of Rep \(\mathbb{Z}\) H. -/

106abbrev rightRegularRep : Rep ℤ H := Rep.of (rightRegularRepresentation H)

107

108omit [DecidableEq H] in

109/--

110The Crowell identity relations are precisely the \(d_{21}\)-images of the right-regular

111representation, on basis elements.

112-/

113theorem rightRegular_d₂₁_single (g₁ g₂ : H) (r : GroupRing H) :

114 groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single (g₁, g₂) r) =

115 (-r) • relationElement (MonoidHom.id H) g₁ g₂ := by

116 rw [groupHomology.d₂₁_single]

117 simp only [rightRegularRepresentation, MonoidAlgebra.of_apply, MonoidHom.coe_mk,

118 OneHom.coe_mk, inv_inv,

119 LinearMap.coe_mk, AddHom.coe_mk, sub_eq_add_neg, add_comm, relationElement,

120 MonoidHom.id_apply, Finsupp.smul_single,

121 smul_eq_mul, mul_one, neg_add_rev, add_left_comm, smul_add, smul_neg, neg_smul, neg_neg,

122 add_assoc]

123

124omit [DecidableEq H] in

125/-- Rewriting the right-regular boundary identity in the Crowell direction. -/

126theorem relationElement_eq_rightRegular_d₂₁_single (g₁ g₂ : H) (r : GroupRing H) :

127 r • relationElement (MonoidHom.id H) g₁ g₂ =

128 groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single (g₁, g₂) (-r)) := by

129 rw [rightRegular_d₂₁_single]

130 simp only [relationElement_eq_crossedDifferentialRelationElement, neg_neg]

131

132omit [DecidableEq H] in

133/-- Every right-regular 1-boundary is a Crowell relation in the identity differential module. -/

134theorem rightRegular_d₂₁_mem_relationSubmodule (x : H × H →₀ GroupRing H) :

135 groupHomology.d₂₁ (rightRegularRep H) x ∈ relationSubmodule (MonoidHom.id H) := by

136 induction x using Finsupp.induction with

137 | zero =>

138 simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, map_zero, zero_mem]

139 | single_add g r x hg hx ih =>

140 have hs :

141 groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single g r) ∈

142 relationSubmodule (MonoidHom.id H) := by

143 rw [rightRegular_d₂₁_single]

144 exact (relationSubmodule (MonoidHom.id H)).smul_mem _

145 (relationElement_mem (MonoidHom.id H) g.1 g.2)

146 simpa [map_add] using (relationSubmodule (MonoidHom.id H)).add_mem hs ih

147

148omit [DecidableEq H] in

149/-- The scalar-multiplication formula for \(d_{21}\) holds on singleton generators. -/

150@[simp]

151theorem rightRegular_d₂₁_smul_single (r : GroupRing H) (g : H × H) (a : GroupRing H) :

152 groupHomology.d₂₁ (rightRegularRep H) (r • Finsupp.single g a) =

153 r • groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single g a) := by

154 calc

155 groupHomology.d₂₁ (rightRegularRep H) (r • Finsupp.single g a)

156 = groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single g (r * a)) := by

157 simp only [Finsupp.smul_single, smul_eq_mul]

158 _ = (-(r * a)) • relationElement (MonoidHom.id H) g.1 g.2 := by

159 rw [rightRegular_d₂₁_single]

160 _ = r • ((-a) • relationElement (MonoidHom.id H) g.1 g.2) := by

161 simp only [relationElement_eq_crossedDifferentialRelationElement, neg_smul, smul_neg,

162 smul_smul]

163 _ = r • groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single g a) := by

164 rw [rightRegular_d₂₁_single]

165

166omit [DecidableEq H] in

167/-- The right-regular \(d_{21}\) map is compatible with scalar multiplication. -/

168theorem rightRegular_d₂₁_smul (r : GroupRing H) (x : H × H →₀ GroupRing H) :

169 groupHomology.d₂₁ (rightRegularRep H) (r • x) =

170 r • groupHomology.d₂₁ (rightRegularRep H) x := by

171 induction x using Finsupp.induction with

172 | zero =>

173 simp only [smul_zero, map_zero]

174 | single_add g a x hg hx ih =>

175 rw [smul_add, map_add, ih, rightRegular_d₂₁_smul_single]

176 simp only [map_add, smul_add]

177

178/--

179The degree-1 boundaries for the right-regular representation, regarded as a

180\(\mathbb{Z}[H]\)-submodule of the free pre-module.

181-/

182def rightRegularBoundariesSubmodule : Submodule (GroupRing H) (DifferentialPreModule H H) where

183 carrier := groupHomology.boundaries₁ (rightRegularRep H)

184 zero_mem' := by

185 exact ⟨0, by simp only [map_zero]⟩

186 add_mem' := by

187 intro x y hx hy

188 exact (groupHomology.boundaries₁ (rightRegularRep H)).add_mem hx hy

189 smul_mem' := by

190 intro r x hx

191 rcases hx with ⟨y, rfl⟩

192 exact ⟨r • y, rightRegular_d₂₁_smul (H := H) r y⟩

193

194variable {H} in

195omit [DecidableEq H] in

196/-- The displayed right-regular boundary lies in the right-regular boundary submodule. -/

197@[simp]

198theorem mem_rightRegularBoundariesSubmodule {x : DifferentialPreModule H H} :

199 x ∈ rightRegularBoundariesSubmodule H ↔ x ∈ groupHomology.boundaries₁ (rightRegularRep H) :=

200 Iff.rfl

201

202omit [DecidableEq H] in

203/-- Each identity-Crowell relation already lies in the right-regular boundary submodule. -/

204theorem relationElement_mem_rightRegularBoundariesSubmodule (g₁ g₂ : H) :

205 relationElement (MonoidHom.id H) g₁ g₂ ∈ rightRegularBoundariesSubmodule H := by

206 refine ⟨Finsupp.single (g₁, g₂) (-1), ?_⟩

207 simpa using

208 (relationElement_eq_rightRegular_d₂₁_single (H := H) g₁ g₂ (1 : GroupRing H)).symm

209

210omit [DecidableEq H] in

211/-- The identity Crowell relation submodule is contained in the right-regular boundary submodule. -/

212theorem relationSubmodule_le_rightRegularBoundariesSubmodule :

213 relationSubmodule (MonoidHom.id H) ≤ rightRegularBoundariesSubmodule H := by

214 rw [relationSubmodule]

215 refine Submodule.span_le.2 ?_

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

217 exact relationElement_mem_rightRegularBoundariesSubmodule (H := H) g₁ g₂

218

219omit [DecidableEq H] in

220/--

221The degree-1 boundaries for the right-regular representation lie in the Crowell relation

222submodule.

223-/

224theorem rightRegular_boundaries₁_le_relationSubmodule :

225 groupHomology.boundaries₁ (rightRegularRep H) ≤

226 (relationSubmodule (MonoidHom.id H)).restrictScalars ℤ := by

227 intro x hx

228 rcases hx with ⟨y, rfl⟩

229 exact rightRegular_d₂₁_mem_relationSubmodule (H := H) y

230

231omit [DecidableEq H] in

232/-- The right-regular boundary submodule is contained in the relation submodule. -/

233theorem rightRegularBoundariesSubmodule_le_relationSubmodule :

234 rightRegularBoundariesSubmodule H ≤ relationSubmodule (MonoidHom.id H) := by

235 intro x hx

236 exact rightRegular_boundaries₁_le_relationSubmodule (H := H) hx

237

238omit [DecidableEq H] in

239/-- The identity Crowell relations are exactly the right-regular degree-1 boundaries. -/

240theorem relationSubmodule_eq_rightRegularBoundariesSubmodule :

241 relationSubmodule (MonoidHom.id H) = rightRegularBoundariesSubmodule H := by

242 exact le_antisymm

243 (relationSubmodule_le_rightRegularBoundariesSubmodule (H := H))

244 (rightRegularBoundariesSubmodule_le_relationSubmodule (H := H))

245

246omit [DecidableEq H] in

247/--

248The lifted linear identity-boundary map has the stated value on a single group-ring generator.

249-/

250@[simp]

251theorem liftLinear_groupRingBoundary_id_single (g : H) (r : GroupRing H) :

252 liftLinear (H := H) (G := H) (A := GroupRing H)

253 (groupRingBoundary (MonoidHom.id H)) (Finsupp.single g r) =

254 r * augmentationGenerator H g := by

255 simp only [liftLinear, Finsupp.linearCombination_single, groupRingBoundary, MonoidHom.id_apply,

256 MonoidAlgebra.of_apply, smul_eq_mul, mul_sub, mul_one, augmentationGenerator]

257

258omit [DecidableEq H] in

259/-- The pre-boundary map for the identity case lands in the augmentation ideal. -/

260theorem liftLinear_groupRingBoundary_id_mem_augmentationIdeal (x : DifferentialPreModule H H) :

261 liftLinear (H := H) (G := H) (A := GroupRing H)

262 (groupRingBoundary (MonoidHom.id H)) x ∈ augmentationIdeal H := by

263 rw [liftLinear, Finsupp.linearCombination_apply]

264 exact Submodule.sum_mem (augmentationIdeal H) fun g _ =>

265 (augmentationIdeal H).smul_mem _ <|

266 groupRingBoundary_mem_augmentationIdeal (H := H) (MonoidHom.id H) g

267

268omit [DecidableEq H] in

269/--

270The standard generator \(h-1\) of the augmentation ideal lies in the image of the identity

271pre-boundary map.

272-/

273theorem augmentationGenerator_mem_range_liftLinear_groupRingBoundary_id (h : H) :

274 augmentationGenerator H h ∈

275 LinearMap.range (liftLinear (H := H) (G := H) (A := GroupRing H)

276 (groupRingBoundary (MonoidHom.id H))) := by

277 refine ⟨Finsupp.single h 1, ?_⟩

278 simp only [liftLinear_single, groupRingBoundary, MonoidHom.id_apply, MonoidAlgebra.of_apply,

279 smul_eq_mul,

280 one_mul, augmentationGenerator]

281

282omit [DecidableEq H] in

283/-- The augmentation ideal is generated by the image of the identity pre-boundary map. -/

284theorem augmentationIdeal_le_range_liftLinear_groupRingBoundary_id :

285 (augmentationIdeal H : Submodule (GroupRing H) (GroupRing H)) ≤

286 LinearMap.range (liftLinear (H := H) (G := H) (A := GroupRing H)

287 (groupRingBoundary (MonoidHom.id H))) := by

288 have hgen :

289 (augmentationGeneratorIdeal H : Submodule (GroupRing H) (GroupRing H)) ≤

290 LinearMap.range (liftLinear (H := H) (G := H) (A := GroupRing H)

291 (groupRingBoundary (MonoidHom.id H))) := by

292 refine Ideal.span_le.2 ?_

293 rintro _ ⟨h, rfl⟩

294 exact augmentationGenerator_mem_range_liftLinear_groupRingBoundary_id (H := H) h

295 simpa [congrArg

296 (fun I : Ideal (GroupRing H) => (I : Submodule (GroupRing H) (GroupRing H)))

297 (augmentationGeneratorIdeal_eq_augmentationIdeal (H := H))] using hgen

298

299omit [DecidableEq H] in

300/--

301For the identity homomorphism, the lifted group-ring boundary equals the degree-one differential

302for the right-regular representation.

303-/

304theorem liftLinear_groupRingBoundary_id_eq_d₁₀ :

305 (liftLinear (H := H) (G := H) (A := GroupRing H)

306 (groupRingBoundary (MonoidHom.id H))).restrictScalars ℤ =

307 (groupHomology.d₁₀ (rightRegularRep H)).hom := by

308 apply Finsupp.lhom_ext

309 intro g r

310 rw [groupHomology.d₁₀_single]

311 simp only [liftLinear, LinearMap.coe_restrictScalars, Finsupp.linearCombination_single,

312 groupRingBoundary,

313 MonoidHom.id_apply, MonoidAlgebra.of_apply, sub_eq_add_neg, smul_eq_mul, mul_add, mul_neg,

314 mul_one,

315 rightRegularRepresentation, MonoidHom.coe_mk, OneHom.coe_mk, inv_inv, LinearMap.coe_mk,

316 AddHom.coe_mk]

317

318omit [DecidableEq H] in

319/--

320The identity group-ring boundary lift is evaluated on canonical generators and then extended

321linearly.

322-/

323theorem liftLinear_groupRingBoundary_id_apply (x : DifferentialPreModule H H) :

324 liftLinear (H := H) (G := H) (A := GroupRing H)

325 (groupRingBoundary (MonoidHom.id H)) x =

326 groupHomology.d₁₀ (rightRegularRep H) x := by

327 exact congrArg (fun f : DifferentialPreModule H H →ₗ[ℤ] GroupRing H => f x)

328 (liftLinear_groupRingBoundary_id_eq_d₁₀ H)

329

330omit [DecidableEq H] in

331/-- The right-regular degree-0 differential lands in the augmentation ideal. -/

332theorem rightRegular_d₁₀_mem_augmentationIdeal (x : DifferentialPreModule H H) :

333 groupHomology.d₁₀ (rightRegularRep H) x ∈ augmentationIdeal H := by

334 simpa [liftLinear_groupRingBoundary_id_apply] using

335 liftLinear_groupRingBoundary_id_mem_augmentationIdeal (H := H) x

336

337omit [DecidableEq H] in

338/-- The canonical augmentation ideal is the kernel of the ordinary group-ring augmentation map. -/

339theorem rightRegular_d₁₀_range_eq_augmentationIdeal :

340 LinearMap.range (groupHomology.d₁₀ (rightRegularRep H)).hom =

341 (augmentationIdeal H).restrictScalars ℤ := by

342 ext y

343 constructor

344 · rintro ⟨x, rfl⟩

345 exact rightRegular_d₁₀_mem_augmentationIdeal (H := H) x

346 · intro hy

347 rcases augmentationIdeal_le_range_liftLinear_groupRingBoundary_id (H := H) hy with ⟨x, hx⟩

348 refine ⟨x, ?_⟩

349 rw [← LinearMap.congr_fun (liftLinear_groupRingBoundary_id_eq_d₁₀ (H := H)) x]

350 exact hx

351

352/--

353The trivial representation of the trivial subgroup of \(H\). Shapiro identifies its induced

354representation with the right-regular representation.

355-/

356abbrev bottomTrivialRep : Rep ℤ (⊥ : Subgroup H) :=

357 Rep.trivial ℤ (⊥ : Subgroup H) ℤ

358

359/-- The induced module from the trivial subgroup is just the group ring. -/

360def indBottomTrivialUnderlyingEquiv :

361 Representation.IndV (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ ≃ₗ[ℤ] GroupRing H := by

362 let ρt : Representation ℤ (⊥ : Subgroup H) (TensorProduct ℤ (GroupRing H) ℤ) :=

363 Representation.tprod

364 (((Rep.leftRegular ℤ H).ρ.comp (⊥ : Subgroup H).subtype))

365 (bottomTrivialRep H).ρ

366 let e1 : Representation.Coinvariants ρt ≃ₗ[ℤ] TensorProduct ℤ (GroupRing H) ℤ :=

367 coinvariantsLEquivOfSubsingleton ρt

368 exact e1.trans (TensorProduct.rid ℤ (GroupRing H))

369

370omit [DecidableEq H] in

371/--

372The bottom-trivial induced-module equivalence sends the induced representative with element

373\(h\) and coefficient \(n\) to the singleton group-ring element at \(h\) with coefficient \(n\).

374-/

375@[simp 900]

376theorem indBottomTrivialUnderlyingEquiv_mk (h : H) (n : ℤ) :

377 indBottomTrivialUnderlyingEquiv H

378 (Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ h n) =

379 MonoidAlgebra.single h n := by

380 change (TensorProduct.rid ℤ (GroupRing H))

381 ((Representation.Coinvariants.lift

382 (Representation.tprod (((Rep.leftRegular ℤ H).ρ.comp (⊥ : Subgroup H).subtype))

383 (bottomTrivialRep H).ρ)

384 LinearMap.id

385 (fun x => by

386 ext y

387 have : x = (1 : (⊥ : Subgroup H)) := Subsingleton.elim _ _

388 subst this

389 simp only [Function.comp_apply, map_one, LinearMap.id_comp, LinearMap.coe_comp,

390 AlgebraTensorModule.curry_apply, LinearMap.restrictScalars_self, curry_apply,

391 Module.End.one_apply, LinearMap.id_coe, id_eq]))

392 (Representation.Coinvariants.mk _ (MonoidAlgebra.single h 1 ⊗ₜ[ℤ] n))) = _

393 rw [Representation.Coinvariants.lift_mk]

394 simp only [LinearMap.id_coe, id_eq, rid_tmul, MonoidAlgebra.smul_single, Int.zsmul_eq_mul,

395 mul_one]

396

397/--

398Shapiro's lemma identifies the induced trivial representation of the trivial subgroup with the

399right-regular representation.

400-/

401def indBottomTrivialIsoRightRegular :

402 Rep.ind (⊥ : Subgroup H).subtype (bottomTrivialRep H) ≅ rightRegularRep H := by

403 refine Rep.mkIso

404 (Representation.Equiv.mk (indBottomTrivialUnderlyingEquiv H) ?_)

405 intro g

406 apply Representation.IndV.hom_ext

407 intro h

408 apply LinearMap.ext

409 intro n

410 change (indBottomTrivialUnderlyingEquiv H)

411 (((Rep.ind (⊥ : Subgroup H).subtype (bottomTrivialRep H)).ρ g)

412 ((Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ h) n)) =

413 (rightRegularRepresentation H g

414 (indBottomTrivialUnderlyingEquiv H

415 ((Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ h) n)))

416 have hind :

417 (((Rep.ind (⊥ : Subgroup H).subtype (bottomTrivialRep H)).ρ g)

418 ((Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ h) n)) =

419 (Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ (h * g⁻¹))

420 n := by

421 exact Representation.ind_mk

422 (φ := (⊥ : Subgroup H).subtype) (ρ := (bottomTrivialRep H).ρ) g h n

423 rw [hind, indBottomTrivialUnderlyingEquiv_mk, indBottomTrivialUnderlyingEquiv_mk]

424 simp only [rightRegularRepresentation_apply_single]

425

426/-- Group homology respects isomorphic representations. -/

427def groupHomologyIsoOfRepIso {A B : Rep ℤ H} (e : A ≅ B) (n : ℕ) :

428 groupHomology A n ≅ groupHomology B n where

429 hom := groupHomology.map (MonoidHom.id H) e.hom n

430 inv := groupHomology.map (MonoidHom.id H) e.inv n

431 hom_inv_id := by

432 have h := groupHomology.map_id_comp (φ := e.hom) (ψ := e.inv) (n := n)

433 rw [e.hom_inv_id, groupHomology.map_id] at h

434 simpa using h.symm

435 inv_hom_id := by

436 have h := groupHomology.map_id_comp (φ := e.inv) (ψ := e.hom) (n := n)

437 rw [e.inv_hom_id, groupHomology.map_id] at h

438 simpa using h.symm

439

440/--

441The first homology of the right-regular representation is identified with the first homology of

442the trivial subgroup.

443-/

444def rightRegularH1IsoBottom :

445 groupHomology (rightRegularRep H) 1 ≅ groupHomology (bottomTrivialRep H) 1 := by

446 exact (groupHomologyIsoOfRepIso H (indBottomTrivialIsoRightRegular H).symm 1) ≪≫

447 groupHomology.indIso (⊥ : Subgroup H) (bottomTrivialRep H) 1

448

449omit [DecidableEq H] in

450/-- The first homology of the right-regular representation vanishes. -/

451theorem rightRegular_H1_isZero : Limits.IsZero (groupHomology (rightRegularRep H) 1) := by

452 classical

453 let hbot : Limits.IsZero (groupHomology (bottomTrivialRep H) 1) := by

454 simpa using (isZero_groupHomology_succ_of_subsingleton (A := bottomTrivialRep H) 0)

455 exact hbot.of_iso (rightRegularH1IsoBottom H)

456

457omit [DecidableEq H] in

458/-- In degree 1, right-regular cycles are exactly right-regular boundaries. -/

459theorem rightRegular_cycles₁_eq_boundaries₁ :

460 groupHomology.cycles₁ (rightRegularRep H) = groupHomology.boundaries₁ (rightRegularRep H) := by

461 classical

462 apply le_antisymm

463 · intro x hx

464 let hzero := rightRegular_H1_isZero H

465 haveI : Subsingleton (groupHomology (rightRegularRep H) 1) :=

466 ModuleCat.subsingleton_of_isZero hzero

467 let z : groupHomology.cycles₁ (rightRegularRep H) := ⟨x, hx⟩

468 exact (groupHomology.H1π_eq_zero_iff (A := rightRegularRep H) z).1 (Subsingleton.elim _ _)

469 · exact groupHomology.boundaries₁_le_cycles₁ (rightRegularRep H)

470

471/--

472For the right-regular representation, a 1-chain is a boundary exactly when its degree-0

473differential vanishes.

474-/

475theorem mem_rightRegularBoundariesSubmodule_iff_d₁₀_eq_zero

476 {H : Type} [Group H] {x : DifferentialPreModule H H} :

477 x ∈ rightRegularBoundariesSubmodule H ↔ groupHomology.d₁₀ (rightRegularRep H) x = 0 := by

478 constructor

479 · intro hx

480 have hx' : x ∈ groupHomology.boundaries₁ (rightRegularRep H) := hx

481 have hcycle := groupHomology.mem_cycles₁_of_mem_boundaries₁ (A := rightRegularRep H) x hx'

482 simpa [groupHomology.cycles₁, LinearMap.mem_ker] using hcycle

483 · intro hx

484 have hcycle : x ∈ groupHomology.cycles₁ (rightRegularRep H) := by

485 simpa [groupHomology.cycles₁, LinearMap.mem_ker] using hx

486 have hbound : x ∈ groupHomology.boundaries₁ (rightRegularRep H) := by

487 simpa [rightRegular_cycles₁_eq_boundaries₁ (H := H)] using hcycle

488 exact hbound

489

490/--

491The quotient of the free pre-module by right-regular degree-1 boundaries is the identity Crowell

492differential module.

493-/

494def rightRegularBoundariesQuotientEquivIdentityDifferentialModule :

495 (DifferentialPreModule H H ⧸ (rightRegularBoundariesSubmodule H)) ≃ₗ[GroupRing H]

496 DifferentialModule (MonoidHom.id H) :=

497 Submodule.quotEquivOfEq (rightRegularBoundariesSubmodule H)

498 (relationSubmodule (MonoidHom.id H))

499 (relationSubmodule_eq_rightRegularBoundariesSubmodule (H := H)).symm

500

501omit [DecidableEq H] in

502/--

503The equivalence from the quotient by right-regular boundaries to the identity differential

504module sends a quotient class to the corresponding relation-submodule quotient class.

505-/

506@[simp]

507theorem rightRegularBoundariesQuotientEquivIdentityDifferentialModule_mk

508 (x : DifferentialPreModule H H) :

509 rightRegularBoundariesQuotientEquivIdentityDifferentialModule H

510 (Submodule.Quotient.mk x) =

511 (relationSubmodule (MonoidHom.id H)).mkQ x := by

512 rw [rightRegularBoundariesQuotientEquivIdentityDifferentialModule,

513 Submodule.quotEquivOfEq_mk]

514 rfl

515

516/-- The quotient by right-regular boundaries maps onto the augmentation ideal. -/

517def rightRegularBoundariesQuotientToAugmentationIdeal :

518 (DifferentialPreModule H H ⧸ (rightRegularBoundariesSubmodule H)) →ₗ[GroupRing H]

519 augmentationIdeal H :=

520 { toFun := fun x =>

521 toAugmentationIdeal (H := H) (MonoidHom.id H)

522 (rightRegularBoundariesQuotientEquivIdentityDifferentialModule H x)

523 map_add' := by

524 intro x y

525 simp only [map_add]

526 map_smul' := by

527 intro r x

528 simp only [map_smul, RingHom.id_apply]}

529

530omit [DecidableEq H] in

531/--

532The quotient map from right-regular boundaries to the augmentation ideal sends a single

533generator to the corresponding augmentation generator.

534-/

535@[simp]

536theorem rightRegularBoundariesQuotientToAugmentationIdeal_mk_single (h : H) :

537 rightRegularBoundariesQuotientToAugmentationIdeal H

538 (Submodule.Quotient.mk (Finsupp.single h 1)) =

539 augmentationGeneratorSubtype (H := H) h := by

540 change toAugmentationIdeal (H := H) (MonoidHom.id H)

541 ((relationSubmodule (MonoidHom.id H)).mkQ (Finsupp.single h 1)) =

542 augmentationGeneratorSubtype (H := H) h

543 exact toAugmentationIdeal_d (H := H) (MonoidHom.id H) h

544

545omit [DecidableEq H] in

546/-- The quotient by right-regular boundaries surjects onto the augmentation ideal. -/

547theorem rightRegularBoundariesQuotientToAugmentationIdeal_surjective :

548 Function.Surjective (rightRegularBoundariesQuotientToAugmentationIdeal H) := by

549 intro y

550 rcases toAugmentationIdeal_surjective (H := H) (MonoidHom.id H) (fun h => ⟨h, rfl⟩) y with

551 ⟨x, hx⟩

552 refine ⟨(rightRegularBoundariesQuotientEquivIdentityDifferentialModule H).symm x, ?_⟩

553 simpa [rightRegularBoundariesQuotientToAugmentationIdeal] using hx

554

555/-- The quotient-to-augmentation map has trivial kernel. -/

556theorem rightRegularBoundariesQuotientToAugmentationIdeal_eq_zero_iff

557 {H : Type} [Group H]

558 {q : DifferentialPreModule H H ⧸ (rightRegularBoundariesSubmodule H)} :

559 rightRegularBoundariesQuotientToAugmentationIdeal H q = 0 ↔ q = 0 := by

560 refine Submodule.Quotient.induction_on _ q ?_

561 intro x

562 constructor

563 · intro hx

564 have hx' : groupHomology.d₁₀ (rightRegularRep H) x = 0 := by

565 have hxval := congrArg Subtype.val hx

566 change toGroupRing (MonoidHom.id H)

567 ((rightRegularBoundariesQuotientEquivIdentityDifferentialModule H)

568 (Submodule.Quotient.mk x)) = 0 at hxval

569 rw [rightRegularBoundariesQuotientEquivIdentityDifferentialModule_mk] at hxval

570 change liftLinear (H := H) (G := H) (A := GroupRing H)

571 (groupRingBoundary (MonoidHom.id H)) x = 0 at hxval

572 simpa [liftLinear_groupRingBoundary_id_apply] using hxval

573 have hmem : x ∈ rightRegularBoundariesSubmodule H := by

574 exact (mem_rightRegularBoundariesSubmodule_iff_d₁₀_eq_zero (H := H) (x := x)).2 hx'

575 exact (Submodule.Quotient.mk_eq_zero (p := rightRegularBoundariesSubmodule H) (x := x)).2 hmem

576 · intro hq

577 simp only [hq, map_zero]

578

579omit [DecidableEq H] in

580/--

581The map from the quotient of right-regular boundaries to the ordinary augmentation ideal is

582injective.

583-/

584theorem rightRegularBoundariesQuotientToAugmentationIdeal_injective :

585 Function.Injective (rightRegularBoundariesQuotientToAugmentationIdeal H) := by

586 intro x y hxy

587 apply sub_eq_zero.mp

588 refine (rightRegularBoundariesQuotientToAugmentationIdeal_eq_zero_iff (H := H) (q := x - y)).1 ?_

589 simpa [LinearMap.map_sub] using sub_eq_zero.mpr hxy

590

591/-- The right-regular boundary quotient is exactly the augmentation ideal. -/

592def rightRegularBoundariesQuotientEquivAugmentationIdeal :

593 (DifferentialPreModule H H ⧸ (rightRegularBoundariesSubmodule H)) ≃ₗ[GroupRing H]

594 augmentationIdeal H :=

595 LinearEquiv.ofBijective (rightRegularBoundariesQuotientToAugmentationIdeal H)

596 ⟨rightRegularBoundariesQuotientToAugmentationIdeal_injective (H := H),

597 rightRegularBoundariesQuotientToAugmentationIdeal_surjective (H := H)⟩

598

599omit [DecidableEq H] in

600/--

601Under the identity differential module equivalence, the universal differential \(d(h)\)

602corresponds to the augmentation generator \(h-1\).

603-/

604@[simp]

605theorem identityDifferentialModuleEquivAugmentationIdeal_d (h : H) :

606 identityDifferentialModuleEquivAugmentationIdeal (H := H)

607 (universalDifferential (MonoidHom.id H) h) =

608 augmentationGeneratorSubtype (H := H) h := by

609 change

610 (identityDifferentialModuleEquivAugmentationIdeal (H := H)).toLinearMap

611 (universalDifferential (MonoidHom.id H) h) =

612 augmentationGeneratorSubtype (H := H) h

613 rw [identityDifferentialModuleEquivAugmentationIdeal_toLinearMap]

614 rw [toAugmentationIdeal_d]

615 apply Subtype.ext

616 rfl

617

618

619end

620

621end FoxDifferential