FoxDifferential/Discrete/KernelBoundary/IdentityAugmentation.lean
1import FoxDifferential.Discrete.GroupRing
2import Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
3import Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FoxDifferential/Discrete/KernelBoundary/IdentityAugmentation.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Identity differential module and right-regular chains
16For the identity homomorphism, the universal differential module is identified with the
17augmentation ideal through the right-regular bar complex.
19This file identifies the identity differential module with the augmentation ideal through
20right-regular chains.
22The low-degree right-regular formulas give the algebraic bridge for the identification
23`A_id ≃ I(ℤ[H])`.
24-/
26namespace FoxDifferential
28noncomputable section
30open CategoryTheory Limits Representation Rep TensorProduct
31open scoped TensorProduct
34variable (H : Type) [Group H] [DecidableEq H]
36/-- For a representation of a subsingleton monoid, taking coinvariants does not change the
37underlying module. -/
39 {k G V : Type*} [CommRing k] [Monoid G] [Subsingleton G]
40 [AddCommGroup V] [Module k V] (ρ : Representation k G V) :
41 Representation.Coinvariants ρ ≃ₗ[k] V := by
42 refine LinearEquiv.ofLinear
43 (Representation.Coinvariants.lift ρ LinearMap.id ?_)
44 (Representation.Coinvariants.mk ρ)
45 ?_ ?_
46 · intro g
47 ext x
48 have : g = (1 : G) := Subsingleton.elim _ _
49 subst this
51 · ext x
52 simp only [Coinvariants.lift_comp_mk, LinearMap.id_coe, id_eq]
53 · apply Representation.Coinvariants.hom_ext
54 ext x
55 simp only [LinearMap.coe_comp, Function.comp_apply, Coinvariants.lift_mk, LinearMap.id_coe, id_eq,
56 LinearMap.id_comp]
58/-- The right-regular `ℤ`-linear representation on `ℤ[H]`, given by right multiplication by
59`g⁻¹`. This is the representation whose low-degree group homology matches the identity-case
60Crowell relations. -/
61def rightRegularRepresentation : Representation ℤ H (GroupRing H) where
62 toFun g :=
63 { toFun := fun x => x * MonoidAlgebra.of ℤ H g⁻¹
64 map_add' := by
65 intro x y
66 simp only [MonoidAlgebra.of_apply, add_mul]
67 map_smul' := by
68 intro n x
69 simpa using smul_mul_assoc n x (MonoidAlgebra.of ℤ H g⁻¹) }
70 map_one' := by
71 ext x
72 simp only [inv_one, MonoidAlgebra.of_apply, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk,
73 Function.comp_apply, MonoidAlgebra.lsingle_apply, MonoidAlgebra.single_mul_single, mul_one, Module.End.one_apply]
74 map_mul' g₁ g₂ := by
75 ext x
76 simp only [mul_inv_rev, MonoidAlgebra.of_apply, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk,
77 Function.comp_apply, MonoidAlgebra.lsingle_apply, MonoidAlgebra.single_mul_single, mul_one, Module.End.mul_apply,
78 mul_assoc]
80omit [DecidableEq H] in
81@[simp]
82theorem rightRegularRepresentation_apply_single (g h : H) (n : ℤ) :
83 rightRegularRepresentation H g (Finsupp.single h n) =
84 Finsupp.single (h * g⁻¹) n := by
85 ext a
86 simp only [rightRegularRepresentation, MonoidAlgebra.of_apply, MonoidHom.coe_mk, OneHom.coe_mk,
87 LinearMap.coe_mk, AddHom.coe_mk, MonoidAlgebra.single_mul_single, mul_one]
89omit [DecidableEq H] in
90@[simp]
91theorem rightRegularRepresentation_apply_of (g h : H) :
92 rightRegularRepresentation H g (MonoidAlgebra.of ℤ H h : GroupRing H) =
93 MonoidAlgebra.of ℤ H (h * g⁻¹) := by
94 exact rightRegularRepresentation_apply_single (H := H) g h (1 : ℤ)
96/-- The right-regular representation as an object of `Rep ℤ H`. -/
97abbrev rightRegularRep : Rep ℤ H := Rep.of (rightRegularRepresentation H)
99omit [DecidableEq H] in
100/-- The Crowell identity relations are precisely the `d₂₁`-images of the right-regular
101representation, on basis elements. -/
102theorem rightRegular_d₂₁_single (g₁ g₂ : H) (r : GroupRing H) :
103 groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single (g₁, g₂) r) =
104 (-r) • relationElement (MonoidHom.id H) g₁ g₂ := by
105 rw [groupHomology.d₂₁_single]
106 simp only [of_ρ, rightRegularRepresentation, MonoidAlgebra.of_apply, MonoidHom.coe_mk, OneHom.coe_mk, inv_inv,
107 LinearMap.coe_mk, AddHom.coe_mk, sub_eq_add_neg, add_comm, relationElement, MonoidHom.id_apply, Finsupp.smul_single,
108 smul_eq_mul, mul_one, neg_add_rev, add_left_comm, smul_add, smul_neg, neg_smul, neg_neg, add_assoc]
110omit [DecidableEq H] in
111/-- Rewriting the right-regular boundary identity in the Crowell direction. -/
112theorem relationElement_eq_rightRegular_d₂₁_single (g₁ g₂ : H) (r : GroupRing H) :
113 r • relationElement (MonoidHom.id H) g₁ g₂ =
114 groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single (g₁, g₂) (-r)) := by
116 simp only [relationElement_eq_crossedDifferentialRelationElement, neg_neg]
118omit [DecidableEq H] in
119/-- Every right-regular 1-boundary is a Crowell relation in the identity differential module. -/
120theorem rightRegular_d₂₁_mem_relationSubmodule (x : H × H →₀ GroupRing H) :
121 groupHomology.d₂₁ (rightRegularRep H) x ∈ relationSubmodule (MonoidHom.id H) := by
122 induction x using Finsupp.induction with
124 simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, map_zero, zero_mem]
125 | single_add g r x hg hx ih =>
126 have hs :
127 groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single g r) ∈
128 relationSubmodule (MonoidHom.id H) := by
130 exact (relationSubmodule (MonoidHom.id H)).smul_mem _
131 (relationElement_mem (MonoidHom.id H) g.1 g.2)
132 simpa [map_add] using (relationSubmodule (MonoidHom.id H)).add_mem hs ih
134omit [DecidableEq H] in
135@[simp]
136theorem rightRegular_d₂₁_smul_single (r : GroupRing H) (g : H × H) (a : GroupRing H) :
137 groupHomology.d₂₁ (rightRegularRep H) (r • Finsupp.single g a) =
138 r • groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single g a) := by
139 calc
140 groupHomology.d₂₁ (rightRegularRep H) (r • Finsupp.single g a)
141 = groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single g (r * a)) := by
142 simp only [Finsupp.smul_single, smul_eq_mul]
143 _ = (-(r * a)) • relationElement (MonoidHom.id H) g.1 g.2 := by
145 _ = r • ((-a) • relationElement (MonoidHom.id H) g.1 g.2) := by
146 simp only [relationElement_eq_crossedDifferentialRelationElement, neg_smul, smul_neg, smul_smul]
147 _ = r • groupHomology.d₂₁ (rightRegularRep H) (Finsupp.single g a) := by
150omit [DecidableEq H] in
151theorem rightRegular_d₂₁_smul (r : GroupRing H) (x : H × H →₀ GroupRing H) :
152 groupHomology.d₂₁ (rightRegularRep H) (r • x) =
153 r • groupHomology.d₂₁ (rightRegularRep H) x := by
154 induction x using Finsupp.induction with
157 | single_add g a x hg hx ih =>
158 rw [smul_add, map_add, ih, rightRegular_d₂₁_smul_single]
161/-- The degree-1 boundaries for the right-regular representation, regarded as a
162`ℤ[H]`-submodule of the free pre-module. -/
163def rightRegularBoundariesSubmodule : Submodule (GroupRing H) (DifferentialPreModule H H) where
164 carrier := groupHomology.boundaries₁ (rightRegularRep H)
165 zero_mem' := by
167 add_mem' := by
168 intro x y hx hy
169 exact (groupHomology.boundaries₁ (rightRegularRep H)).add_mem hx hy
170 smul_mem' := by
171 intro r x hx
172 rcases hx with ⟨y, rfl⟩
173 exact ⟨r • y, rightRegular_d₂₁_smul (H := H) r y⟩
175variable {H} in
176omit [DecidableEq H] in
177@[simp]
178theorem mem_rightRegularBoundariesSubmodule {x : DifferentialPreModule H H} :
179 x ∈ rightRegularBoundariesSubmodule H ↔ x ∈ groupHomology.boundaries₁ (rightRegularRep H) :=
180 Iff.rfl
182omit [DecidableEq H] in
183/-- Each identity-Crowell relation already lies in the right-regular boundary submodule. -/
184theorem relationElement_mem_rightRegularBoundariesSubmodule (g₁ g₂ : H) :
185 relationElement (MonoidHom.id H) g₁ g₂ ∈ rightRegularBoundariesSubmodule H := by
186 refine ⟨Finsupp.single (g₁, g₂) (-1), ?_⟩
187 simpa using
188 (relationElement_eq_rightRegular_d₂₁_single (H := H) g₁ g₂ (1 : GroupRing H)).symm
190omit [DecidableEq H] in
191/-- The identity Crowell relation submodule is contained in the right-regular boundary submodule. -/
193 relationSubmodule (MonoidHom.id H) ≤ rightRegularBoundariesSubmodule H := by
194 rw [relationSubmodule]
195 refine Submodule.span_le.2 ?_
196 rintro _ ⟨⟨g₁, g₂⟩, rfl⟩
197 exact relationElement_mem_rightRegularBoundariesSubmodule (H := H) g₁ g₂
199omit [DecidableEq H] in
200/-- The degree-1 boundaries for the right-regular representation lie in the Crowell relation
201submodule. -/
203 groupHomology.boundaries₁ (rightRegularRep H) ≤
204 (relationSubmodule (MonoidHom.id H)).restrictScalars ℤ := by
205 intro x hx
206 rcases hx with ⟨y, rfl⟩
207 exact rightRegular_d₂₁_mem_relationSubmodule (H := H) y
209omit [DecidableEq H] in
211 rightRegularBoundariesSubmodule H ≤ relationSubmodule (MonoidHom.id H) := by
212 intro x hx
213 exact rightRegular_boundaries₁_le_relationSubmodule (H := H) hx
215omit [DecidableEq H] in
216/-- The identity Crowell relations are exactly the right-regular degree-1 boundaries. -/
218 relationSubmodule (MonoidHom.id H) = rightRegularBoundariesSubmodule H := by
219 exact le_antisymm
223omit [DecidableEq H] in
224@[simp]
225theorem liftLinear_groupRingBoundary_id_single (g : H) (r : GroupRing H) :
226 liftLinear (H := H) (G := H) (A := GroupRing H)
227 (groupRingBoundary (MonoidHom.id H)) (Finsupp.single g r) =
228 r * augmentationGenerator H g := by
229 simp only [liftLinear, Finsupp.linearCombination_single, groupRingBoundary, MonoidHom.id_apply,
230 MonoidAlgebra.of_apply, smul_eq_mul, mul_sub, mul_one, augmentationGenerator]
232omit [DecidableEq H] in
233/-- The pre-boundary map for the identity case lands in the augmentation ideal. -/
234theorem liftLinear_groupRingBoundary_id_mem_augmentationIdeal (x : DifferentialPreModule H H) :
235 liftLinear (H := H) (G := H) (A := GroupRing H)
236 (groupRingBoundary (MonoidHom.id H)) x ∈ augmentationIdeal H := by
237 rw [liftLinear, Finsupp.linearCombination_apply]
238 exact Submodule.sum_mem (augmentationIdeal H) fun g _ =>
239 (augmentationIdeal H).smul_mem _ <|
240 groupRingBoundary_mem_augmentationIdeal (H := H) (MonoidHom.id H) g
242omit [DecidableEq H] in
243/-- The standard generator `h - 1` of the augmentation ideal lies in the image of the identity
244pre-boundary map. -/
245theorem augmentationGenerator_mem_range_liftLinear_groupRingBoundary_id (h : H) :
246 augmentationGenerator H h ∈
247 LinearMap.range (liftLinear (H := H) (G := H) (A := GroupRing H)
248 (groupRingBoundary (MonoidHom.id H))) := by
249 refine ⟨Finsupp.single h 1, ?_⟩
250 simp only [liftLinear_single, groupRingBoundary, MonoidHom.id_apply, MonoidAlgebra.of_apply, smul_eq_mul,
251 one_mul, augmentationGenerator]
253omit [DecidableEq H] in
254/-- The augmentation ideal is generated by the image of the identity pre-boundary map. -/
256 (augmentationIdeal H : Submodule (GroupRing H) (GroupRing H)) ≤
257 LinearMap.range (liftLinear (H := H) (G := H) (A := GroupRing H)
258 (groupRingBoundary (MonoidHom.id H))) := by
259 have hgen :
260 (augmentationGeneratorIdeal H : Submodule (GroupRing H) (GroupRing H)) ≤
261 LinearMap.range (liftLinear (H := H) (G := H) (A := GroupRing H)
262 (groupRingBoundary (MonoidHom.id H))) := by
263 refine Ideal.span_le.2 ?_
264 rintro _ ⟨h, rfl⟩
265 exact augmentationGenerator_mem_range_liftLinear_groupRingBoundary_id (H := H) h
266 simpa [congrArg
268 (augmentationGeneratorIdeal_eq_augmentationIdeal (H := H))] using hgen
270omit [DecidableEq H] in
271/-- On the identity homomorphism, the pre-boundary map agrees with the degree-1 differential
272for the right-regular representation. -/
274 (liftLinear (H := H) (G := H) (A := GroupRing H)
275 (groupRingBoundary (MonoidHom.id H))).restrictScalars ℤ =
276 (groupHomology.d₁₀ (rightRegularRep H)).hom := by
277 apply Finsupp.lhom_ext
278 intro g r
279 rw [groupHomology.d₁₀_single]
280 simp only [liftLinear, LinearMap.coe_restrictScalars, Finsupp.linearCombination_single, groupRingBoundary,
281 MonoidHom.id_apply, MonoidAlgebra.of_apply, sub_eq_add_neg, smul_eq_mul, mul_add, mul_neg, mul_one, of_ρ,
282 rightRegularRepresentation, MonoidHom.coe_mk, OneHom.coe_mk, inv_inv, LinearMap.coe_mk, AddHom.coe_mk]
284omit [DecidableEq H] in
285theorem liftLinear_groupRingBoundary_id_apply (x : DifferentialPreModule H H) :
286 liftLinear (H := H) (G := H) (A := GroupRing H)
287 (groupRingBoundary (MonoidHom.id H)) x =
288 groupHomology.d₁₀ (rightRegularRep H) x := by
289 exact congrArg (fun f : DifferentialPreModule H H →ₗ[ℤ] GroupRing H => f x)
292omit [DecidableEq H] in
293/-- The right-regular degree-0 differential lands in the augmentation ideal. -/
294theorem rightRegular_d₁₀_mem_augmentationIdeal (x : DifferentialPreModule H H) :
295 groupHomology.d₁₀ (rightRegularRep H) x ∈ augmentationIdeal H := by
296 simpa [liftLinear_groupRingBoundary_id_apply] using
299omit [DecidableEq H] in
300/-- The image of the right-regular degree-0 differential is exactly the augmentation ideal. -/
302 LinearMap.range (groupHomology.d₁₀ (rightRegularRep H)).hom =
303 (augmentationIdeal H).restrictScalars ℤ := by
304 ext y
305 constructor
306 · rintro ⟨x, rfl⟩
307 exact rightRegular_d₁₀_mem_augmentationIdeal (H := H) x
308 · intro hy
309 rcases augmentationIdeal_le_range_liftLinear_groupRingBoundary_id (H := H) hy with ⟨x, hx⟩
310 refine ⟨x, ?_⟩
311 rw [← LinearMap.congr_fun (liftLinear_groupRingBoundary_id_eq_d₁₀ (H := H)) x]
312 exact hx
314/-- The trivial representation of the trivial subgroup of `H`. Shapiro identifies its induced
315representation with the right-regular representation. -/
316abbrev bottomTrivialRep : Rep ℤ (⊥ : Subgroup H) :=
317 Rep.trivial ℤ (⊥ : Subgroup H) ℤ
319/-- The induced module from the trivial subgroup is just the group ring. -/
321 Representation.IndV (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ ≃ₗ[ℤ] GroupRing H := by
323 Representation.tprod
325 (bottomTrivialRep H).ρ
330omit [DecidableEq H] in
331@[simp 900]
332theorem indBottomTrivialUnderlyingEquiv_mk (h : H) (n : ℤ) :
334 (Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ h n) =
335 Finsupp.single h n := by
337 ((Representation.Coinvariants.lift
339 (bottomTrivialRep H).ρ)
340 LinearMap.id
341 (fun x => by
342 ext y
343 have : x = (1 : (⊥ : Subgroup H)) := Subsingleton.elim _ _
344 subst this
346 Finsupp.lsingle_apply, AlgebraTensorModule.curry_apply, LinearMap.restrictScalars_self, curry_apply,
347 Module.End.one_apply, LinearMap.id_coe, id_eq]))
348 (Representation.Coinvariants.mk _ (Finsupp.single h 1 ⊗ₜ[ℤ] n))) = _
349 rw [Representation.Coinvariants.lift_mk]
350 simp only [LinearMap.id_coe, id_eq, rid_tmul, MonoidAlgebra.smul_single, Int.zsmul_eq_mul, mul_one]
352/-- Shapiro's lemma identifies the induced trivial representation of the trivial subgroup with the
353right-regular representation. -/
355 Rep.ind (⊥ : Subgroup H).subtype (bottomTrivialRep H) ≅ rightRegularRep H :=
356 Action.mkIso (indBottomTrivialUnderlyingEquiv H).toModuleIso fun g => by
358 (ρ := (bottomTrivialRep H).ρ) ?_
359 intro h
360 ext n
361 change (indBottomTrivialUnderlyingEquiv H)
362 (((Rep.ind (⊥ : Subgroup H).subtype (bottomTrivialRep H)).ρ g)
363 ((Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ h) (1 : ℤ))) n =
366 ((Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ h) (1 : ℤ)))) n
367 have hind :
368 (((Rep.ind (⊥ : Subgroup H).subtype (bottomTrivialRep H)).ρ g)
369 ((Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ h) (1 : ℤ))) =
370 (Representation.IndV.mk (⊥ : Subgroup H).subtype (bottomTrivialRep H).ρ (h * g⁻¹))
371 (1 : ℤ) := by
372 simp only [Rep.ind, of_ρ, ind_apply, LinearMap.coe_comp, Function.comp_apply, mk_apply, Coinvariants.map_mk,
373 LinearMap.rTensor_tmul, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single]
375 simp only [rightRegularRepresentation_apply_single]
377/-- Group homology respects isomorphic representations. -/
378def groupHomologyIsoOfRepIso {A B : Rep ℤ H} (e : A ≅ B) (n : ℕ) :
379 groupHomology A n ≅ groupHomology B n where
380 hom := groupHomology.map (MonoidHom.id H) e.hom n
381 inv := groupHomology.map (MonoidHom.id H) e.inv n
382 hom_inv_id := by
383 have h := groupHomology.map_id_comp (φ := e.hom) (ψ := e.inv) (n := n)
384 rw [e.hom_inv_id, groupHomology.map_id] at h
385 simpa using h.symm
386 inv_hom_id := by
387 have h := groupHomology.map_id_comp (φ := e.inv) (ψ := e.hom) (n := n)
388 rw [e.inv_hom_id, groupHomology.map_id] at h
389 simpa using h.symm
391/-- The first homology of the right-regular representation is identified with the first homology
392of the trivial subgroup. -/
394 groupHomology (rightRegularRep H) 1 ≅ groupHomology (bottomTrivialRep H) 1 := by
395 exact (groupHomologyIsoOfRepIso H (indBottomTrivialIsoRightRegular H).symm 1) ≪≫
396 groupHomology.indIso (⊥ : Subgroup H) (bottomTrivialRep H) 1
398omit [DecidableEq H] in
399/-- The first homology of the right-regular representation vanishes. -/
400theorem rightRegular_H1_isZero : Limits.IsZero (groupHomology (rightRegularRep H) 1) := by
401 classical
402 let hbot : Limits.IsZero (groupHomology (bottomTrivialRep H) 1) := by
403 simpa using (isZero_groupHomology_succ_of_subsingleton (A := bottomTrivialRep H) 0)
404 exact hbot.of_iso (rightRegularH1IsoBottom H)
406omit [DecidableEq H] in
407/-- In degree 1, right-regular cycles are exactly right-regular boundaries. -/
408theorem rightRegular_cycles₁_eq_boundaries₁ :
409 groupHomology.cycles₁ (rightRegularRep H) = groupHomology.boundaries₁ (rightRegularRep H) := by
410 classical
411 apply le_antisymm
412 · intro x hx
413 let hzero := rightRegular_H1_isZero H
414 haveI : Subsingleton (groupHomology (rightRegularRep H) 1) :=
415 ModuleCat.subsingleton_of_isZero hzero
416 let z : groupHomology.cycles₁ (rightRegularRep H) := ⟨x, hx⟩
417 exact (groupHomology.H1π_eq_zero_iff (A := rightRegularRep H) z).1 (Subsingleton.elim _ _)
418 · exact groupHomology.boundaries₁_le_cycles₁ (rightRegularRep H)
420/-- For the right-regular representation, a 1-chain is a boundary exactly when its degree-0
421differential vanishes. -/
423 {H : Type} [Group H] {x : DifferentialPreModule H H} :
424 x ∈ rightRegularBoundariesSubmodule H ↔ groupHomology.d₁₀ (rightRegularRep H) x = 0 := by
425 constructor
426 · intro hx
427 have hx' : x ∈ groupHomology.boundaries₁ (rightRegularRep H) := hx
428 have hcycle := groupHomology.mem_cycles₁_of_mem_boundaries₁ (A := rightRegularRep H) x hx'
429 simpa [groupHomology.cycles₁, LinearMap.mem_ker] using hcycle
430 · intro hx
431 have hcycle : x ∈ groupHomology.cycles₁ (rightRegularRep H) := by
432 simpa [groupHomology.cycles₁, LinearMap.mem_ker] using hx
433 have hbound : x ∈ groupHomology.boundaries₁ (rightRegularRep H) := by
434 simpa [rightRegular_cycles₁_eq_boundaries₁ (H := H)] using hcycle
435 exact hbound
437/-- The quotient of the free pre-module by right-regular degree-1 boundaries is the identity
438Crowell differential module. -/
440 (DifferentialPreModule H H ⧸ (rightRegularBoundariesSubmodule H)) ≃ₗ[GroupRing H]
441 DifferentialModule (MonoidHom.id H) :=
442 Submodule.quotEquivOfEq (rightRegularBoundariesSubmodule H)
443 (relationSubmodule (MonoidHom.id H))
444 (relationSubmodule_eq_rightRegularBoundariesSubmodule (H := H)).symm
446omit [DecidableEq H] in
447@[simp]
449 (x : DifferentialPreModule H H) :
451 (Submodule.Quotient.mk x) =
452 (relationSubmodule (MonoidHom.id H)).mkQ x := by
454 Submodule.quotEquivOfEq_mk]
455 rfl
457/-- The quotient by right-regular boundaries maps onto the augmentation ideal. -/
459 (DifferentialPreModule H H ⧸ (rightRegularBoundariesSubmodule H)) →ₗ[GroupRing H]
460 augmentationIdeal H :=
461 { toFun := fun x =>
462 toAugmentationIdeal (H := H) (MonoidHom.id H)
464 map_add' := by
465 intro x y
467 map_smul' := by
468 intro r x
469 simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, map_smul, RingHom.id_apply]}
471omit [DecidableEq H] in
472@[simp]
473theorem rightRegularBoundariesQuotientToAugmentationIdeal_mk_single (h : H) :
475 (Submodule.Quotient.mk (Finsupp.single h 1)) =
476 augmentationGeneratorSubtype (H := H) h := by
477 apply Subtype.ext
481 using toGroupRing_d (MonoidHom.id H) h
483omit [DecidableEq H] in
484/-- The quotient by right-regular boundaries surjects onto the augmentation ideal. -/
486 Function.Surjective (rightRegularBoundariesQuotientToAugmentationIdeal H) := by
487 intro y
488 rcases toAugmentationIdeal_surjective (H := H) (MonoidHom.id H) (fun h => ⟨h, rfl⟩) y with
489 ⟨x, hx⟩
490 refine ⟨(rightRegularBoundariesQuotientEquivIdentityDifferentialModule H).symm x, ?_⟩
491 simpa [rightRegularBoundariesQuotientToAugmentationIdeal] using hx
493/-- The quotient-to-augmentation map has trivial kernel. -/
495 {H : Type} [Group H]
496 {q : DifferentialPreModule H H ⧸ (rightRegularBoundariesSubmodule H)} :
497 rightRegularBoundariesQuotientToAugmentationIdeal H q = 0 ↔ q = 0 := by
498 refine Submodule.Quotient.induction_on _ q ?_
499 intro x
500 constructor
501 · intro hx
502 have hx' : groupHomology.d₁₀ (rightRegularRep H) x = 0 := by
503 have hxval := congrArg Subtype.val hx
504 change toGroupRing (MonoidHom.id H)
506 (Submodule.Quotient.mk x)) = 0 at hxval
508 change liftLinear (H := H) (G := H) (A := GroupRing H)
509 (groupRingBoundary (MonoidHom.id H)) x = 0 at hxval
510 simpa [liftLinear_groupRingBoundary_id_apply] using hxval
511 have hmem : x ∈ rightRegularBoundariesSubmodule H := by
512 exact (mem_rightRegularBoundariesSubmodule_iff_d₁₀_eq_zero (H := H) (x := x)).2 hx'
513 exact (Submodule.Quotient.mk_eq_zero (p := rightRegularBoundariesSubmodule H) (x := x)).2 hmem
514 · intro hq
517omit [DecidableEq H] in
518/-- The quotient-to-augmentation map is injective. -/
520 Function.Injective (rightRegularBoundariesQuotientToAugmentationIdeal H) := by
521 intro x y hxy
522 apply sub_eq_zero.mp
523 refine (rightRegularBoundariesQuotientToAugmentationIdeal_eq_zero_iff (H := H) (q := x - y)).1 ?_
524 simpa [LinearMap.map_sub] using sub_eq_zero.mpr hxy
526/-- The right-regular boundary quotient is exactly the augmentation ideal. -/
528 (DifferentialPreModule H H ⧸ (rightRegularBoundariesSubmodule H)) ≃ₗ[GroupRing H]
529 augmentationIdeal H :=
530 LinearEquiv.ofBijective (rightRegularBoundariesQuotientToAugmentationIdeal H)
534omit [DecidableEq H] in
535@[simp]
536theorem identityDifferentialModuleEquivAugmentationIdeal_d (h : H) :
538 (universalDifferential (MonoidHom.id H) h) =
539 augmentationGeneratorSubtype (H := H) h := by
540 change
541 (identityDifferentialModuleEquivAugmentationIdeal (H := H)).toLinearMap
542 (universalDifferential (MonoidHom.id H) h) =
543 augmentationGeneratorSubtype (H := H) h
545 rw [toAugmentationIdeal_d]
546 apply Subtype.ext
547 rfl
550end
552end FoxDifferential