Yamaguchi Lean 4 Library
FoxDifferential/Discrete/KernelBoundary/Homology.lean
FoxDifferential/Discrete/KernelBoundary/Homology/Source

FoxDifferential/Discrete/KernelBoundary/Homology.lean

1import Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
2import FoxDifferential.Discrete.KernelBoundary.Basic
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Discrete/KernelBoundary/Homology.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Kernel augmentation and coinvariants
15The kernel action on the augmentation ideal is compared with right-regular group homology.
16The resulting coinvariant map is the homological input for the Magnus-kernel theorem.
17-/
19namespace FoxDifferential
21noncomputable section
23open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
25variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
27section KernelGroupRing
29variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
31variable (ψ : G →* H) (hψ : Function.Surjective ψ)
33instance instMulActionKernelCodomainTrivial : MulAction ↥(ψ.ker) H where
34 smul _ h := h
35 one_smul _ := rfl
36 mul_smul _ _ _ := rfl
38/-- The left-multiplication representation of `ker ψ` on `ℤ[G]`. -/
39abbrev kernelGroupRingRep : Rep ℤ ↥(ψ.ker) :=
40 Rep.ofMulAction ℤ ↥(ψ.ker) G
42/-- A section-based decomposition `G ≃ ker ψ × H`. -/
43def kernelSplitEquiv : G ≃ ↥(ψ.ker) × H where
44 toFun g :=
45 (⟨g * (Function.surjInv hψ (ψ g))⁻¹, by
46 simp only [MonoidHom.mem_ker, map_mul, map_inv, Function.surjInv_eq hψ (ψ g), mul_inv_cancel]⟩, ψ g)
47 invFun x := x.1.1 * Function.surjInv hψ x.2
48 left_inv g := by
49 simp only [mul_assoc, inv_mul_cancel, mul_one]
50 right_inv x := by
51 rcases x with ⟨n, h⟩
52 apply Prod.ext
53 · apply Subtype.ext
54 change
55 n.1 * Function.surjInv hψ h *
56 (Function.surjInv hψ (ψ (n.1 * Function.surjInv hψ h)))⁻¹ = n.1
57 rw [map_mul, n.2, Function.surjInv_eq hψ h]
58 simp only [one_mul, mul_assoc, mul_inv_cancel, mul_one]
59 · change ψ (n.1 * Function.surjInv hψ h) = h
60 rw [map_mul, n.2, one_mul, Function.surjInv_eq hψ h]
62omit [DecidableEq H] [DecidableEq G] in
63@[simp]
64theorem kernelSplitEquiv_smul (n : ↥(ψ.ker)) (g : G) :
65 kernelSplitEquiv ψ hψ (n • g) = n • kernelSplitEquiv ψ hψ g := by
66 apply Prod.ext
67 · apply Subtype.ext
68 change
69 n.1 * g * (Function.surjInv hψ (ψ (n.1 * g)))⁻¹ =
70 n.1 * (g * (Function.surjInv hψ (ψ g))⁻¹)
71 rw [map_mul, n.2, one_mul]
72 simp only [mul_assoc]
73 · change ψ (n.1 * g) = ψ g
74 rw [map_mul, n.2, one_mul]
76/-- The `ker ψ`-representation on `ℤ[ker ψ] ⊗ ℤ[H]` whose first factor is right-regular and whose
77second factor is trivial. -/
78abbrev kernelRightTensorRep : Rep ℤ ↥(ψ.ker) :=
79 rightRegularRep ↥(ψ.ker) ⊗ Rep.trivial ℤ ↥(ψ.ker) (H →₀ ℤ)
81/-- The section decomposition, rewritten as a representation isomorphism to a right-regular tensor
82model. -/
84 kernelGroupRingRep (ψ := ψ) ≅ kernelRightTensorRep (H := H) (ψ := ψ) := by
85 let e₁ :
86 (G →₀ ℤ) ≃ₗ[ℤ] ((↥(ψ.ker) × H) →₀ ℤ) :=
87 Finsupp.domLCongr (kernelSplitEquiv ψ hψ)
88 let e₂ :
89 ((↥(ψ.ker) × H) →₀ ℤ) ≃ₗ[ℤ] (GroupRing ↥(ψ.ker)) ⊗[ℤ] (H →₀ ℤ) :=
90 (finsuppTensorFinsupp' ℤ ↥(ψ.ker) H).symm.trans
91 (TensorProduct.congr
92 (Finsupp.domLCongr (Equiv.inv ↥(ψ.ker)))
93 (LinearEquiv.refl ℤ (H →₀ ℤ)))
94 refine Action.mkIso ((e₁.trans e₂).toModuleIso) ?_
95 intro n
96 refine ModuleCat.hom_ext <| Finsupp.lhom_ext fun g r => ?_
97 have hcalc :
98 e₂ (Finsupp.single (n • kernelSplitEquiv ψ hψ g) r) =
99 ((kernelRightTensorRep (ψ := ψ) (H := H)).ρ n)
100 (e₂ (Finsupp.single (kernelSplitEquiv ψ hψ g) r)) := by
101 change e₂ (Finsupp.single (n • kernelSplitEquiv ψ hψ g) r) =
102 TensorProduct.map ((rightRegularRepresentation ↥(ψ.ker)) n) LinearMap.id
103 (e₂ (Finsupp.single (kernelSplitEquiv ψ hψ g) r))
104 cases hkg : kernelSplitEquiv ψ hψ g with
105 | mk m h =>
106 simp only [e₂, LinearEquiv.trans_apply,
107 finsuppTensorFinsupp'_symm_single_eq_single_one_tmul, TensorProduct.congr_tmul,
108 TensorProduct.map_tmul, LinearEquiv.refl_apply]
109 have hnm :
110 ((Finsupp.domLCongr (Equiv.inv ↥(ψ.ker)) :
111 GroupRing ↥(ψ.ker) ≃ₗ[ℤ] GroupRing ↥(ψ.ker))
112 (Finsupp.single (n * m) (1 : ℤ))) =
113 (Finsupp.single ((n * m)⁻¹) (1 : ℤ) : GroupRing ↥(ψ.ker)) := by
114 ext x
115 simp only [Finsupp.domLCongr_apply, Finsupp.domCongr_apply, Finsupp.equivMapDomain_single, Equiv.inv_apply,
116 mul_inv_rev]
117 have hm :
118 ((Finsupp.domLCongr (Equiv.inv ↥(ψ.ker)) :
119 GroupRing ↥(ψ.ker) ≃ₗ[ℤ] GroupRing ↥(ψ.ker))
120 (Finsupp.single m (1 : ℤ))) =
121 (Finsupp.single m⁻¹ (1 : ℤ) : GroupRing ↥(ψ.ker)) := by
122 ext x
123 simp only [Finsupp.domLCongr_apply, Finsupp.domCongr_apply, Finsupp.equivMapDomain_single, Equiv.inv_apply]
124 change
125 ((Finsupp.domLCongr (Equiv.inv ↥(ψ.ker)) :
126 GroupRing ↥(ψ.ker) ≃ₗ[ℤ] GroupRing ↥(ψ.ker))
127 (Finsupp.single (n * m) (1 : ℤ))) ⊗ₜ[ℤ] Finsupp.single h r =
129 (((Finsupp.domLCongr (Equiv.inv ↥(ψ.ker)) :
130 GroupRing ↥(ψ.ker) ≃ₗ[ℤ] GroupRing ↥(ψ.ker))
131 (Finsupp.single m (1 : ℤ)))) ⊗ₜ[ℤ] Finsupp.single h r
132 rw [hnm, hm]
134 change
135 e₂
136 (e₁
137 (((kernelGroupRingRep (ψ := ψ)).ρ n) (Finsupp.single g r))) =
138 ((kernelRightTensorRep (ψ := ψ) (H := H)).ρ n)
139 (e₂ (e₁ (Finsupp.single g r)))
140 simpa [kernelGroupRingRep, kernelRightTensorRep, e₁, LinearEquiv.trans_apply,
141 kernelSplitEquiv_smul, Representation.ofMulAction_single, Rep.tensor_ρ] using hcalc
143/-- The trivial representation of the trivial subgroup of `ker ψ` on the free `ℤ`-module `ℤ[H]`.
144-/
146 Representation.IndV (⊥ : Subgroup ↥(ψ.ker)).subtype
147 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ
148 ≃ₗ[ℤ] (GroupRing ↥(ψ.ker)) ⊗[ℤ] (H →₀ ℤ) := by
149 let ρt :
150 Representation ℤ (⊥ : Subgroup ↥(ψ.ker))
151 (TensorProduct ℤ (GroupRing ↥(ψ.ker)) (H →₀ ℤ)) :=
152 Representation.tprod
153 (((Rep.leftRegular ℤ ↥(ψ.ker)).ρ.comp (⊥ : Subgroup ↥(ψ.ker)).subtype))
154 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ
157omit [DecidableEq H] [DecidableEq G] in
158@[simp 900]
159theorem indBottomKernelUnderlyingEquiv_mk (g : ↥(ψ.ker)) (a : H →₀ ℤ) :
161 (Representation.IndV.mk (⊥ : Subgroup ↥(ψ.ker)).subtype
162 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ g a) =
163 (Finsupp.single g 1 : GroupRing ↥(ψ.ker)) ⊗ₜ[ℤ] a := by
164 change
165 (Representation.Coinvariants.lift
166 (Representation.tprod
167 (((Rep.leftRegular ℤ ↥(ψ.ker)).ρ.comp (⊥ : Subgroup ↥(ψ.ker)).subtype))
168 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ)
169 LinearMap.id
170 (fun x => by
171 ext y
172 have : x = (1 : (⊥ : Subgroup ↥(ψ.ker))) := Subsingleton.elim _ _
173 subst this
174 simp only [of_ρ, Function.comp_apply,
175 map_one, LinearMap.id_comp, LinearMap.coe_comp, Finsupp.lsingle_apply,
176 AlgebraTensorModule.curry_apply, LinearMap.restrictScalars_self, curry_apply, Module.End.one_apply,
177 LinearMap.id_coe, id_eq]))
178 (Representation.Coinvariants.mk _
179 ((Finsupp.single g 1 : GroupRing ↥(ψ.ker)) ⊗ₜ[ℤ] a)) = _
180 rw [Representation.Coinvariants.lift_mk]
181 rfl
183/-- `Ind_{1}^{ker ψ}(ℤ[H])` is the right-regular tensor model. -/
185 Rep.ind (⊥ : Subgroup ↥(ψ.ker)).subtype
186 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)) ≅
187 kernelRightTensorRep (ψ := ψ) (H := H) :=
188 Action.mkIso ((indBottomKernelUnderlyingEquiv (H := H) (ψ := ψ)).toModuleIso) fun g => by
189 refine ModuleCat.hom_ext <|
190 Representation.IndV.hom_ext (φ := (⊥ : Subgroup ↥(ψ.ker)).subtype)
191 (ρ := (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ) ?_
192 intro h
193 apply LinearMap.ext
194 intro a
195 change
197 (((Rep.ind (⊥ : Subgroup ↥(ψ.ker)).subtype
198 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ))).ρ g)
199 ((Representation.IndV.mk (⊥ : Subgroup ↥(ψ.ker)).subtype
200 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ h) a)) =
201 ((kernelRightTensorRep (ψ := ψ) (H := H)).ρ g)
202 (indBottomKernelUnderlyingEquiv (H := H) (ψ := ψ)
203 ((Representation.IndV.mk (⊥ : Subgroup ↥(ψ.ker)).subtype
204 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ h) a))
205 have hind :
206 (((Rep.ind (⊥ : Subgroup ↥(ψ.ker)).subtype
207 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ))).ρ g)
208 ((Representation.IndV.mk (⊥ : Subgroup ↥(ψ.ker)).subtype
209 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ h) a)) =
210 (Representation.IndV.mk (⊥ : Subgroup ↥(ψ.ker)).subtype
211 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ (h * g⁻¹)) a := by
212 simp only [Rep.ind, of_ρ, ind_apply, LinearMap.coe_comp, Function.comp_apply, mk_apply, Coinvariants.map_mk,
213 LinearMap.rTensor_tmul, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single]
215 change Finsupp.single (h * g⁻¹) 1 ⊗ₜ[ℤ] a =
216 TensorProduct.map ((rightRegularRepresentation ↥(ψ.ker)) g) LinearMap.id
217 (Finsupp.single h 1 ⊗ₜ[ℤ] a)
218 simp only [map_tmul, rightRegularRepresentation_apply_single, LinearMap.id_coe, id_eq]
220end KernelGroupRing
222section KernelAugmentation
224variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
226variable (ψ : G →* H)
228abbrev groupRingRep : Rep ℤ G :=
229 Rep.ofMulAction ℤ G G
231omit [DecidableEq G] in
232@[simp]
233theorem groupRingRep_apply_single (g h : G) (m : ℤ) :
234 ((groupRingRep (G := G)).ρ g) (Finsupp.single h m) =
235 Finsupp.single (g * h) m := by
236 exact Representation.ofMulAction_single (k := ℤ) (G := G) (H := G) g h m
238omit [DecidableEq H] [DecidableEq G] in
239@[simp]
240theorem kernelGroupRingRep_apply_single (n : ψ.ker) (g : G) (m : ℤ) :
241 ((kernelGroupRingRep (ψ := ψ)).ρ n) (Finsupp.single g m) =
242 Finsupp.single (n • g) m := by
243 exact Representation.ofMulAction_single (k := ℤ) (G := ↥(ψ.ker)) (H := G) n g m
245omit [DecidableEq H] [DecidableEq G] in
247 (n : ψ.ker) (x : GroupRing G) :
248 augmentation G (((kernelGroupRingRep (ψ := ψ)).ρ n) x) = augmentation G x := by
249 let F : GroupRing G →ₗ[ℤ] ℤ :=
250 ((augmentation G).toAddMonoidHom.toIntLinearMap).comp ((kernelGroupRingRep (ψ := ψ)).ρ n)
251 have hF : F = (augmentation G).toAddMonoidHom.toIntLinearMap := by
252 apply Finsupp.lhom_ext
253 intro g m
254 change augmentation G (((kernelGroupRingRep (ψ := ψ)).ρ n) (Finsupp.single g m)) =
255 augmentation G (Finsupp.single g m)
256 simp only [augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe, kernelGroupRingRep, of_ρ,
257 ofMulAction_single, RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply, Int.zsmul_eq_mul, mul_one]
258 exact LinearMap.congr_fun hF x
260omit [DecidableEq G] in
261/-- Left multiplication by `g : G` preserves the group-ring augmentation. -/
263 (g : G) (x : GroupRing G) :
264 augmentation G (((groupRingRep (G := G)).ρ g) x) = augmentation G x := by
265 let F : GroupRing G →ₗ[ℤ] ℤ :=
266 ((augmentation G).toAddMonoidHom.toIntLinearMap).comp ((groupRingRep (G := G)).ρ g)
267 have hF : F = (augmentation G).toAddMonoidHom.toIntLinearMap := by
268 apply Finsupp.lhom_ext
269 intro h m
270 change augmentation G (((groupRingRep (G := G)).ρ g) (Finsupp.single h m)) =
271 augmentation G (Finsupp.single h m)
272 simp only [augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe, groupRingRep, of_ρ, ofMulAction_single,
273 smul_eq_mul, RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply, mul_one]
274 exact LinearMap.congr_fun hF x
276/-- The left-regular `G`-action preserves the augmentation ideal `I(ℤ[G])`. -/
277abbrev groupAugmentationIdealRep : Rep ℤ G :=
278 Rep.of (V := augmentationIdeal G)
279 { toFun := fun g =>
280 { toFun := fun x =>
281 ⟨((groupRingRep (G := G)).ρ g) x.1, by
283 rw [augmentation_groupRingRep (G := G) g x.1]
284 exact (mem_augmentationIdeal_iff (H := G) (x := x.1)).1 x.2⟩
285 map_add' := by
286 intro x y
287 apply Subtype.ext
288 exact map_add ((groupRingRep (G := G)).ρ g) x.1 y.1
289 map_smul' := by
290 intro m x
291 apply Subtype.ext
292 exact map_smul ((groupRingRep (G := G)).ρ g) m x.1 }
293 map_one' := by
294 ext x h
295 simp only [groupRingRep, of_ρ, map_one, Module.End.one_apply, Subtype.coe_eta, LinearMap.coe_mk,
296 AddHom.coe_mk]
297 map_mul' := by
298 intro g₁ g₂
299 ext x h
300 simp only [groupRingRep, of_ρ, map_mul, Module.End.mul_apply, LinearMap.coe_mk, AddHom.coe_mk,
301 ofMulAction_apply, smul_eq_mul]}
303/-- The kernel-restricted action of `ker ψ` on the augmentation ideal `I(ℤ[G])`. -/
304abbrev kernelAugmentationIdealRep : Rep ℤ ↥(ψ.ker) :=
305 Rep.of (V := augmentationIdeal G)
306 { toFun := fun n =>
307 { toFun := fun x =>
308 ⟨((kernelGroupRingRep (ψ := ψ)).ρ n) x.1, by
310 rw [augmentation_kernelGroupRingRep (ψ := ψ) n x.1]
311 exact (mem_augmentationIdeal_iff (H := G) (x := x.1)).1 x.2⟩
312 map_add' := by
313 intro x y
314 apply Subtype.ext
315 exact map_add ((kernelGroupRingRep (ψ := ψ)).ρ n) x.1 y.1
316 map_smul' := by
317 intro m x
318 apply Subtype.ext
319 exact map_smul ((kernelGroupRingRep (ψ := ψ)).ρ n) m x.1 }
320 map_one' := by
321 ext x g
322 simp only [kernelGroupRingRep, of_ρ, map_one, Module.End.one_apply, Subtype.coe_eta, LinearMap.coe_mk,
323 AddHom.coe_mk]
324 map_mul' := by
325 intro n₁ n₂
326 ext x g
327 simp only [kernelGroupRingRep, of_ρ, map_mul, Module.End.mul_apply, LinearMap.coe_mk, AddHom.coe_mk,
328 ofMulAction_apply]}
330/-- The inclusion `I(ℤ[G]) ↪ ℤ[G]` as a morphism of `ker ψ`-representations. -/
333 Action.Hom.mk (ModuleCat.ofHom ((augmentationIdeal G).subtype.restrictScalars ℤ)) fun _ => rfl
335/-- The augmentation map `ℤ[G] → ℤ` as a morphism of `ker ψ`-representations. -/
337 kernelGroupRingRep (ψ := ψ) ⟶ Rep.trivial ℤ ↥(ψ.ker) ℤ :=
338 Action.Hom.mk
339 (ModuleCat.ofHom ((augmentation G).toAddMonoidHom.toIntLinearMap)) fun n => by
340 refine ModuleCat.hom_ext <| Finsupp.lhom_ext fun g m => ?_
341 change augmentation G (((kernelGroupRingRep (ψ := ψ)).ρ n) (Finsupp.single g m)) =
342 ((Rep.trivial ℤ ↥(ψ.ker) ℤ).ρ n) (augmentation G (Finsupp.single g m))
343 simp only [augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe, of_ρ, ofMulAction_single,
344 RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply, Int.zsmul_eq_mul, mul_one, isTrivial_def,
345 LinearMap.id_coe, id_eq]
347/-- The short complex `0 → I(ℤ[G]) → ℤ[G] → ℤ → 0` of `ker ψ`-representations. -/
349 CategoryTheory.ShortComplex (Rep ℤ ↥(ψ.ker)) :=
350 CategoryTheory.ShortComplex.mk
353 (by
354 ext x
355 exact x.2)
357omit [DecidableEq H] [DecidableEq G] in
359 (kernelAugmentationShortComplex (ψ := ψ)).Exact := by
360 refine Functor.reflects_exact_of_faithful (F := forget₂ (Rep ℤ ↥(ψ.ker)) (ModuleCat ℤ))
361 (S := kernelAugmentationShortComplex (ψ := ψ)) ?_
362 rw [CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker]
363 ext x
364 constructor
365 · rintro ⟨y, rfl⟩
366 exact y.2
367 · intro hx
368 refine ⟨⟨x, ?_⟩, rfl⟩
370 simpa [LinearMap.mem_ker] using hx
372/-- The kernel-augmentation short complex is short exact. -/
374 (kernelAugmentationShortComplex (ψ := ψ)).ShortExact := by
375 haveI : Mono (kernelAugmentationShortComplex (ψ := ψ)).f := by
376 change Mono (kernelAugmentationIdealInclusion (ψ := ψ))
377 exact (Rep.mono_iff_injective _).2 fun x y h => Subtype.ext h
378 haveI : Epi (kernelAugmentationShortComplex (ψ := ψ)).g := by
379 change Epi (kernelGroupRingAugmentation (ψ := ψ))
380 exact (Rep.epi_iff_surjective _).2 <| by
381 intro m
382 exact ⟨(m : GroupRing G), by simp only [kernelGroupRingAugmentation, RingHom.toAddMonoidHom_eq_coe, ModuleCat.hom_ofHom,
383 AddMonoidHom.coe_toIntLinearMap, AddMonoidHom.coe_coe, map_intCast, Int.cast_eq]⟩
384 refine CategoryTheory.ShortComplex.ShortExact.mk
388/-- The trivial `ker ψ`-representation on `ℤ`. -/
389abbrev kernelTrivialIntRep : Rep ℤ ↥(ψ.ker) :=
390 Rep.trivial ℤ ↥(ψ.ker) ℤ
392/-- The connecting homomorphism
393`H₁(ker ψ, ℤ) → H₀(ker ψ, I(ℤ[G]))`
394attached to the short exact sequence
395`0 → I(ℤ[G]) → ℤ[G] → ℤ → 0`
396of `ker ψ`-representations. -/
398 groupHomology (kernelTrivialIntRep (ψ := ψ)) 1 ⟶
399 groupHomology (kernelAugmentationIdealRep (ψ := ψ)) 0 :=
400 groupHomology.δ
403 1 0 rfl
405/-- The standard low-degree identification
406`H₁(ker ψ, ℤ) ≃ (ker ψ)^ab`. -/
408 groupHomology (kernelTrivialIntRep (ψ := ψ)) 1 ≃+
409 Additive (Abelianization ψ.ker) :=
410 (groupHomology.H1AddEquivOfIsTrivial (kernelTrivialIntRep (ψ := ψ))).trans
411 (TensorProduct.rid ℤ (Additive (Abelianization ψ.ker))).toAddEquiv
413omit [DecidableEq H] [DecidableEq G] in
414@[simp]
417 (Additive.ofMul (Abelianization.of n)) =
418 groupHomology.H1π (kernelTrivialIntRep (ψ := ψ))
419 ((groupHomology.cycles₁IsoOfIsTrivial (kernelTrivialIntRep (ψ := ψ))).inv
420 (Finsupp.single n 1)) := by
422 rw [AddEquiv.symm_trans_apply]
423 simpa [TensorProduct.rid_symm_apply] using
424 (groupHomology.H1AddEquivOfIsTrivial_symm_tmul
425 (A := kernelTrivialIntRep (ψ := ψ)) n (1 : ℤ))
427omit [DecidableEq H] [DecidableEq G] in
429 Finsupp.mapRange.linearMap (ModuleCat.Hom.hom (kernelAugmentationShortComplex (ψ := ψ)).g.hom)
430 (Finsupp.single n (Finsupp.single n.1 (1 : ℤ))) =
431 ((groupHomology.cycles₁IsoOfIsTrivial (kernelTrivialIntRep (ψ := ψ))).inv
432 (Finsupp.single n 1)).1 := by
433 change
434 Finsupp.mapRange.linearMap (ModuleCat.Hom.hom (kernelGroupRingAugmentation (ψ := ψ)).hom)
435 (Finsupp.single n (Finsupp.single n.1 (1 : ℤ))) =
436 (Finsupp.single n (1 : ℤ))
437 rw [show
438 (Finsupp.mapRange.linearMap (ModuleCat.Hom.hom (kernelGroupRingAugmentation (ψ := ψ)).hom))
439 (Finsupp.single n (Finsupp.single n.1 (1 : ℤ))) =
440 Finsupp.mapRange (ModuleCat.Hom.hom (kernelGroupRingAugmentation (ψ := ψ)).hom)
441 ((ModuleCat.Hom.hom (kernelGroupRingAugmentation (ψ := ψ)).hom).map_zero)
442 (Finsupp.single n (Finsupp.single n.1 (1 : ℤ))) by
443 rfl]
444 rw [Finsupp.mapRange_single]
445 have hcoeff :
446 (ModuleCat.Hom.hom (kernelGroupRingAugmentation (ψ := ψ)).hom)
447 (Finsupp.single n.1 (1 : ℤ)) = 1 := by
448 change augmentation G (Finsupp.single n.1 (1 : ℤ)) = 1
449 simp only [augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
450 MonoidAlgebra.lift_single, MonoidHom.one_apply, Int.zsmul_eq_mul, mul_one]
451 simpa using congrArg (Finsupp.single n) hcoeff
453omit [DecidableEq H] [DecidableEq G] in
456 (-(augmentationGeneratorSubtype (H := G) n.1)) =
457 groupHomology.d₁₀ (kernelGroupRingRep (ψ := ψ))
458 (Finsupp.single n (Finsupp.single n.1 (1 : ℤ))) := by
459 have hn : (n⁻¹ : ψ.ker) • n.1 = (1 : G) := by
460 change n.1⁻¹ * n.1 = 1
461 simp only [inv_mul_cancel]
462 change (-(augmentationGenerator (H := G) n.1) : GroupRing G) =
463 groupHomology.d₁₀ (kernelGroupRingRep (ψ := ψ))
464 (Finsupp.single n (Finsupp.single n.1 (1 : ℤ)))
465 rw [groupHomology.d₁₀_single, kernelGroupRingRep_apply_single, hn]
467 change (-( (Finsupp.single n.1 (1 : ℤ) : GroupRing G) -
468 (Finsupp.single (1 : G) (1 : ℤ) : GroupRing G)) : GroupRing G) =
469 Finsupp.single (1 : G) (1 : ℤ) - Finsupp.single n.1 (1 : ℤ)
470 simp only [sub_eq_add_neg]
471 rw [neg_add, neg_neg]
472 change -Finsupp.single n.1 (1 : ℤ) + Finsupp.single (1 : G) (1 : ℤ) =
473 Finsupp.single (1 : G) (1 : ℤ) + -Finsupp.single n.1 (1 : ℤ)
474 abel_nf
476omit [DecidableEq H] [DecidableEq G] in
478 (groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
481 (Additive.ofMul (Abelianization.of n)))) =
482 -Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
483 (augmentationGeneratorSubtype (H := G) n.1) := by
485 have hδ :
486 (groupHomology.δ (hX := kernelAugmentationShortExact (ψ := ψ)) 1 0 rfl).hom
487 ((groupHomology.H1π (kernelTrivialIntRep (ψ := ψ))).hom
488 ((groupHomology.cycles₁IsoOfIsTrivial (kernelTrivialIntRep (ψ := ψ))).inv
489 (Finsupp.single n 1))) =
490 (groupHomology.H0π (kernelAugmentationIdealRep (ψ := ψ))).hom
491 (-(augmentationGeneratorSubtype (H := G) n.1)) := by
492 exact
493 groupHomology.δ₀_apply
495 (z := (groupHomology.cycles₁IsoOfIsTrivial (kernelTrivialIntRep (ψ := ψ))).inv
496 (Finsupp.single n 1))
497 (y := Finsupp.single n (Finsupp.single n.1 (1 : ℤ)))
498 (x := -(augmentationGeneratorSubtype (H := G) n.1))
501 have hδ' := congrArg
502 ((groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom) hδ
503 have hδ'' :
504 (groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
506 ((groupHomology.H1π (kernelTrivialIntRep (ψ := ψ))).hom
507 ((groupHomology.cycles₁IsoOfIsTrivial (kernelTrivialIntRep (ψ := ψ))).inv
508 (Finsupp.single n 1)))) =
509 (groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
510 ((groupHomology.H0π (kernelAugmentationIdealRep (ψ := ψ))).hom
511 (-(augmentationGeneratorSubtype (H := G) n.1))) := by
513 calc
514 (groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
516 ((groupHomology.H1π (kernelTrivialIntRep (ψ := ψ))).hom
517 ((groupHomology.cycles₁IsoOfIsTrivial (kernelTrivialIntRep (ψ := ψ))).inv
518 (Finsupp.single n 1))))
519 =
520 (groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
521 ((groupHomology.H0π (kernelAugmentationIdealRep (ψ := ψ))).hom
522 (-(augmentationGeneratorSubtype (H := G) n.1))) := hδ''
523 _ = ((coinvariantsMk ℤ ↥ψ.ker).app (kernelAugmentationIdealRep (ψ := ψ)))
524 (-(augmentationGeneratorSubtype (H := G) n.1)) := by
525 exact
526 (groupHomology.H0π_comp_H0Iso_hom_apply
528 (x := -(augmentationGeneratorSubtype (H := G) n.1)))
529 _ = -Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
530 (augmentationGeneratorSubtype (H := G) n.1) := by
531 rfl
533omit [DecidableEq H] [DecidableEq G] in
535 (hψ : Function.Surjective ψ) :
536 Function.Injective (kernelAugmentationConnecting (ψ := ψ)).hom := by
537 letI : Mono (kernelAugmentationConnecting (ψ := ψ)) := by
538 let hH1 : Limits.IsZero (groupHomology (kernelGroupRingRep (ψ := ψ)) 1) := by
539 classical
540 let hrt : Limits.IsZero (groupHomology (kernelRightTensorRep (ψ := ψ) (H := H)) 1) :=
541 let hbot : Limits.IsZero
542 (groupHomology (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)) 1) := by
543 simpa using
544 (isZero_groupHomology_succ_of_subsingleton
545 (A := Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)) 0)
546 hbot.of_iso <|
547 (groupHomologyIsoOfRepIso (H := ↥(ψ.ker))
548 (indBottomKernelIsoRightTensor (H := H) (ψ := ψ)).symm 1) ≪≫
549 groupHomology.indIso (⊥ : Subgroup ↥(ψ.ker))
550 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)) 1
551 exact hrt.of_iso
552 (groupHomologyIsoOfRepIso (H := ↥(ψ.ker))
553 (kernelGroupRingRepIsoRightTensor (H := H) (ψ := ψ) hψ) 1)
554 exact groupHomology.mono_δ_of_isZero
557 0
558 hH1
559 exact (ModuleCat.mono_iff_injective _).1 inferInstance
561/-- The `ker ψ`-coinvariants of `I(ℤ[G])`. -/
562abbrev KernelAugmentationIdealCoinvariants (ψ : G →* H) : Type _ :=
563 Representation.Coinvariants ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
565omit [DecidableEq H] [DecidableEq G] in
566@[simp 900]
568 (n : ψ.ker) :
569 (kernelAugmentationIdealRep (ψ := ψ)).ρ n =
570 (groupAugmentationIdealRep (G := G)).ρ n.1 := by
571 ext x
572 rfl
574section CoinvariantsAction
576/-- The `H`-action on `H₀(ker ψ, I(ℤ[G]))`, built from a surjective section. -/
578 (hψ : Function.Surjective ψ) (h : H) :
581 Representation.Coinvariants.lift ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
582 ((Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)).comp
583 ((groupAugmentationIdealRep (G := G)).ρ (Function.surjInv hψ h)))
584 (by
585 intro n
586 ext x
587 let s : G := Function.surjInv hψ h
588 have hs : ψ s = h := by
589 simpa [s] using Function.surjInv_eq hψ h
590 let n' : ψ.ker := ⟨s * n.1 * s⁻¹, by
591 change ψ (s * n.1 * s⁻¹) = 1
592 rw [map_mul, map_mul, n.2, map_inv, hs]
593 simp only [mul_one, mul_inv_cancel]⟩
594 have hs_mul :
595 ((groupAugmentationIdealRep (G := G)).ρ s)
596 (((groupAugmentationIdealRep (G := G)).ρ n.1) x) =
597 ((groupAugmentationIdealRep (G := G)).ρ (s * n.1)) x := by
598 exact congrArg
599 (fun f : augmentationIdeal G →ₗ[ℤ] augmentationIdeal G => f x)
600 (((groupAugmentationIdealRep (G := G)).ρ).map_mul s n.1).symm
601 have hs'_mul :
602 ((groupAugmentationIdealRep (G := G)).ρ n'.1)
603 (((groupAugmentationIdealRep (G := G)).ρ s) x) =
604 ((groupAugmentationIdealRep (G := G)).ρ (n'.1 * s)) x := by
605 exact congrArg
606 (fun f : augmentationIdeal G →ₗ[ℤ] augmentationIdeal G => f x)
607 (((groupAugmentationIdealRep (G := G)).ρ).map_mul n'.1 s).symm
608 calc
609 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
610 (((groupAugmentationIdealRep (G := G)).ρ s)
611 (((kernelAugmentationIdealRep (ψ := ψ)).ρ n) x))
612 = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
613 (((groupAugmentationIdealRep (G := G)).ρ s)
614 (((groupAugmentationIdealRep (G := G)).ρ n.1) x)) := by
616 (ψ := ψ) n]
617 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
618 (((groupAugmentationIdealRep (G := G)).ρ (s * n.1)) x) := by
619 rw [hs_mul]
620 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
621 (((groupAugmentationIdealRep (G := G)).ρ (n'.1 * s)) x) := by
622 congr 1
623 simp only [of_ρ, MonoidHom.coe_mk, OneHom.coe_mk, map_mul, Module.End.mul_apply, LinearMap.coe_mk,
624 AddHom.coe_mk, mul_assoc, inv_mul_cancel, mul_one, s, n']
625 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
626 (((groupAugmentationIdealRep (G := G)).ρ n'.1)
627 (((groupAugmentationIdealRep (G := G)).ρ s) x)) := by
628 rw [hs'_mul]
629 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
630 (((kernelAugmentationIdealRep (ψ := ψ)).ρ n')
631 (((groupAugmentationIdealRep (G := G)).ρ s) x)) := by
633 (ψ := ψ) n']
634 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
635 (((groupAugmentationIdealRep (G := G)).ρ s) x) := by
636 exact Representation.Coinvariants.mk_self_apply
637 ((kernelAugmentationIdealRep (ψ := ψ)).ρ) n'
638 (((groupAugmentationIdealRep (G := G)).ρ s) x))
640omit [DecidableEq H] [DecidableEq G] in
641@[simp 900]
643 (hψ : Function.Surjective ψ) (h : H) (x : augmentationIdeal G) :
645 (Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ) x) =
646 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
647 (((groupAugmentationIdealRep (G := G)).ρ (Function.surjInv hψ h)) x) := by
648 rfl
650/-- The surjective-case `H`-action on `H₀(ker ψ, I(ℤ[G]))` as linear endomorphisms. -/
652 (hψ : Function.Surjective ψ) :
653 H →* Module.End ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) where
655 map_one' := by
656 apply Representation.Coinvariants.hom_ext
657 ext x
658 rw [LinearMap.comp_apply]
660 let n : ψ.ker := ⟨Function.surjInv hψ (1 : H), by
661 simpa using Function.surjInv_eq hψ (1 : H)⟩
663 (ψ := ψ) n]
664 simpa [n] using
665 (Representation.Coinvariants.mk_self_apply ((kernelAugmentationIdealRep (ψ := ψ)).ρ) n x)
666 map_mul' h₁ h₂ := by
667 apply Representation.Coinvariants.hom_ext
668 ext x
669 let s₁ : G := Function.surjInv hψ h₁
670 let s₂ : G := Function.surjInv hψ h₂
671 let s₁₂ : G := Function.surjInv hψ (h₁ * h₂)
672 have hs₁ : ψ s₁ = h₁ := by
673 simpa [s₁] using Function.surjInv_eq hψ h₁
674 have hs₂ : ψ s₂ = h₂ := by
675 simpa [s₂] using Function.surjInv_eq hψ h₂
676 have hs₁₂ : ψ s₁₂ = h₁ * h₂ := by
677 simpa [s₁₂] using Function.surjInv_eq hψ (h₁ * h₂)
678 let n : ψ.ker := ⟨s₁ * s₂ * s₁₂⁻¹, by
679 change ψ (s₁ * s₂ * s₁₂⁻¹) = 1
680 rw [map_mul, map_mul, hs₁, hs₂, map_inv, hs₁₂]
681 simp only [mul_inv_rev, mul_assoc, mul_inv_cancel_left, mul_inv_cancel]⟩
682 have hs :
683 ((groupAugmentationIdealRep (G := G)).ρ s₁)
684 (((groupAugmentationIdealRep (G := G)).ρ s₂) x) =
685 ((groupAugmentationIdealRep (G := G)).ρ (s₁ * s₂)) x := by
686 exact congrArg
687 (fun f : augmentationIdeal G →ₗ[ℤ] augmentationIdeal G => f x)
688 (((groupAugmentationIdealRep (G := G)).ρ).map_mul s₁ s₂).symm
689 rw [LinearMap.comp_apply, LinearMap.comp_apply]
690 change
691 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
692 (((groupAugmentationIdealRep (G := G)).ρ s₁₂) x) =
695 (Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ) x))
698 calc
699 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
700 (((groupAugmentationIdealRep (G := G)).ρ s₁₂) x)
701 =
702 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
703 (((kernelAugmentationIdealRep (ψ := ψ)).ρ n)
704 (((groupAugmentationIdealRep (G := G)).ρ s₁₂) x)) := by
705 rw [Representation.Coinvariants.mk_self_apply]
706 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
707 (((groupAugmentationIdealRep (G := G)).ρ n.1)
708 (((groupAugmentationIdealRep (G := G)).ρ s₁₂) x)) := by
710 (ψ := ψ) n]
711 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
712 (((groupAugmentationIdealRep (G := G)).ρ (n.1 * s₁₂)) x) := by
713 have hs' :
714 ((groupAugmentationIdealRep (G := G)).ρ n.1)
715 (((groupAugmentationIdealRep (G := G)).ρ s₁₂) x) =
716 ((groupAugmentationIdealRep (G := G)).ρ (n.1 * s₁₂)) x := by
717 exact congrArg
718 (fun f : augmentationIdeal G →ₗ[ℤ] augmentationIdeal G => f x)
719 (((groupAugmentationIdealRep (G := G)).ρ).map_mul n.1 s₁₂).symm
720 rw [hs']
721 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
722 (((groupAugmentationIdealRep (G := G)).ρ (s₁ * s₂)) x) := by
723 congr 1
724 simp only [of_ρ, mul_assoc, inv_mul_cancel, mul_one, MonoidHom.coe_mk, OneHom.coe_mk, map_mul,
725 Module.End.mul_apply, LinearMap.coe_mk, AddHom.coe_mk, s₁, s₂, s₁₂, n]
726 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
727 (((groupAugmentationIdealRep (G := G)).ρ s₁)
728 (((groupAugmentationIdealRep (G := G)).ρ s₂) x)) := by
729 rw [hs]
731/-- The ring action of `ℤ[H]` on `H₀(ker ψ, I(ℤ[G]))` induced by a surjective section. -/
733 (hψ : Function.Surjective ψ) :
734 GroupRing H →+* Module.End ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
735 MonoidAlgebra.liftNCRingHom
736 (Int.castRingHom (Module.End ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ))))
738 (by
739 intro z h
740 apply LinearMap.ext
741 intro x
742 change z •
745 rw [map_zsmul])
747omit [DecidableEq H] [DecidableEq G] in
748@[simp]
750 (hψ : Function.Surjective ψ) (h : H) :
752 (MonoidAlgebra.of ℤ H h) =
754 ext x
755 simp only [of_ρ, kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective, MonoidAlgebra.of_apply,
756 MonoidAlgebra.liftNCRingHom_single, eq_intCast, Int.cast_one, one_mul, LinearMap.coe_comp, Function.comp_apply]
758/-- The induced `ℤ[H]`-module structure on `H₀(ker ψ, I(ℤ[G]))`. -/
760 (hψ : Function.Surjective ψ) :
762 Module.compHom _
765omit [DecidableEq G] in
766/-- The additive generator identity
767`(g₁ g₂ - 1) = (g₁ - 1) + g₁ (g₂ - 1)` inside `I(ℤ[G])`. -/
768@[simp]
769theorem augmentationGeneratorSubtype_mul (g₁ g₂ : G) :
770 augmentationGeneratorSubtype (H := G) (g₁ * g₂) =
772 ((groupAugmentationIdealRep (G := G)).ρ g₁)
773 (augmentationGeneratorSubtype (H := G) g₂) := by
774 let ρg : GroupRing G →ₗ[ℤ] GroupRing G := (groupRingRep (G := G)).ρ g₁
775 apply Subtype.ext
776 change (augmentationGenerator G (g₁ * g₂) : GroupRing G) =
779 have hρ :
780 ρg (augmentationGenerator G g₂) =
781 (MonoidAlgebra.of ℤ G (g₁ * g₂) : GroupRing G) - MonoidAlgebra.of ℤ G g₁ := by
782 change ((groupRingRep (G := G)).ρ g₁)
783 ((Finsupp.single g₂ 1 : GroupRing G) - Finsupp.single (1 : G) 1) =
784 (MonoidAlgebra.of ℤ G (g₁ * g₂) : GroupRing G) - MonoidAlgebra.of ℤ G g₁
786 simp only [mul_one, MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk]
788 abel_nf
790/-- The kernel elements map to `H₀(ker ψ, I(ℤ[G]))` by `n ↦ [n - 1]`. -/
791def kernelCoinvariantsBoundary (ψ : G →* H) :
792 ψ.ker →* Multiplicative (KernelAugmentationIdealCoinvariants (ψ := ψ)) where
793 toFun n := Multiplicative.ofAdd <|
794 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
796 map_one' := by
797 apply Multiplicative.toAdd.injective
798 have hzero : augmentationGeneratorSubtype (H := G) (1 : G) = 0 := by
799 apply Subtype.ext
801 ZeroMemClass.coe_zero]
802 simp only [of_ρ, OneMemClass.coe_one, hzero, map_zero, ofAdd_zero, toAdd_one]
803 map_mul' n₁ n₂ := by
804 apply Multiplicative.toAdd.injective
805 change
806 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
807 (augmentationGeneratorSubtype (H := G) (n₁.1 * n₂.1)) =
808 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
809 (augmentationGeneratorSubtype (H := G) n₁.1) +
810 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
813 congr 1
814 calc
815 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
816 (((groupAugmentationIdealRep (G := G)).ρ n₁.1)
818 = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
819 (((kernelAugmentationIdealRep (ψ := ψ)).ρ n₁)
820 (augmentationGeneratorSubtype (H := G) n₂.1)) := by
822 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
823 (augmentationGeneratorSubtype (H := G) n₂.1) := by
824 exact Representation.Coinvariants.mk_self_apply
825 ((kernelAugmentationIdealRep (ψ := ψ)).ρ) n₁
828/-- The map `n ↦ [n - 1]` factors through `(ker ψ)^ab`. -/
830 Abelianization ψ.ker →* Multiplicative (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
831 Abelianization.lift (kernelCoinvariantsBoundary (ψ := ψ))
833/-- Additive form of the map `(ker ψ)^ab → H₀(ker ψ, I(ℤ[G]))`. -/
836 toFun x := Multiplicative.toAdd (kernelAbelianizationToCoinvariants (ψ := ψ) (Additive.toMul x))
837 map_zero' := by
838 simp only [of_ρ, toMul_zero, map_one, toAdd_one]
839 map_add' x y := by
840 simp only [of_ρ, toMul_add, map_mul, toAdd_mul]
842omit [DecidableEq H] [DecidableEq G] in
843@[simp]
846 (Additive.ofMul (Abelianization.of n)) =
847 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
848 (augmentationGeneratorSubtype (H := G) n.1) := by
850 kernelCoinvariantsBoundary, AddMonoidHom.coe_mk, ZeroHom.coe_mk, toMul_ofMul, Abelianization.lift_apply_of,
851 MonoidHom.coe_mk, OneHom.coe_mk, toAdd_ofAdd]
853/-- `ℤ`-linear form of `(ker ψ)^ab → H₀(ker ψ, I(ℤ[G]))`. -/
856 (kernelAbelianizationToCoinvariantsAdd (ψ := ψ)).toIntLinearMap
858/-- The low-degree homology comparison
859`(ker ψ)^ab → H₀(ker ψ, I(ℤ[G]))`
860obtained from the connecting morphism
861`H₁(ker ψ, ℤ) → H₀(ker ψ, I(ℤ[G]))`. Our convention for `δ₀`
862introduces a minus sign on generators. -/
865 toFun x :=
866 -((groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
869 map_zero' := by
870 simp only [coinvariantsFunctor_obj_carrier, of_ρ, map_zero, neg_zero]
871 map_add' x y := by
872 rw [(kernelTrivialH1AddEquivAbelianization (ψ := ψ)).symm.map_add]
873 simp only [coinvariantsFunctor_obj_carrier, of_ρ, map_add, neg_add_rev]
874 abel_nf
876/-- `ℤ`-linear form of the connecting-morphism comparison
877`(ker ψ)^ab → H₀(ker ψ, I(ℤ[G]))`. -/
882omit [DecidableEq H] [DecidableEq G] in
883@[simp]
886 (Additive.ofMul (Abelianization.of n)) =
887 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
888 (augmentationGeneratorSubtype (H := G) n.1) := by
889 change
890 -((groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
893 (Additive.ofMul (Abelianization.of n))))) =
894 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
897 simp only [coinvariantsFunctor_obj_carrier, of_ρ, neg_neg]
899omit [DecidableEq H] [DecidableEq G] in
900@[simp]
903 (Additive.ofMul (Abelianization.of n)) =
904 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
905 (augmentationGeneratorSubtype (H := G) n.1) := by
906 simp only [of_ρ, kernelAbelianizationToCoinvariantsViaConnectingLinear, AddMonoidHom.coe_toIntLinearMap,
909omit [DecidableEq H] [DecidableEq G] in
911 (ψ : G →* H) :
914 apply LinearMap.ext
915 intro x
916 change
917 (fun y : Abelianization ψ.ker =>
918 kernelAbelianizationToCoinvariantsLinear (ψ := ψ) (Additive.ofMul y) =
920 (Additive.toMul x)
921 refine QuotientGroup.induction_on (Additive.toMul x) ?_
922 intro n
923 calc
924 kernelAbelianizationToCoinvariantsLinear (ψ := ψ) (Additive.ofMul (Abelianization.of n))
926 (Additive.ofMul (Abelianization.of n)) := by
927 rfl
928 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
929 (augmentationGeneratorSubtype (H := G) n.1) := by
932 (Additive.ofMul (Abelianization.of n)) := by
935omit [DecidableEq H] [DecidableEq G] in
937 (hψ : Function.Surjective ψ) :
938 Function.Injective (kernelAbelianizationToCoinvariantsLinear (ψ := ψ)) := by
940 intro x y hxy
941 have hxy' :
944 simpa [hEq] using hxy
945 have hxy'' :
948 simpa [kernelAbelianizationToCoinvariantsViaConnectingLinear, AddMonoidHom.coe_toIntLinearMap]
949 using hxy'
950 have hxy''' : ((groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
952 ((kernelTrivialH1AddEquivAbelianization (ψ := ψ)).symm x))) =
953 ((groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
955 ((kernelTrivialH1AddEquivAbelianization (ψ := ψ)).symm y))) := by
956 simpa [kernelAbelianizationToCoinvariantsViaConnectingAdd] using congrArg Neg.neg hxy''
957 have hH0Iso :
958 Function.Injective
959 ((groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom) := by
960 exact (ModuleCat.mono_iff_injective _).1 inferInstance
961 apply (kernelTrivialH1AddEquivAbelianization (ψ := ψ)).symm.injective
962 apply kernelAugmentationConnecting_injective (H := H) (ψ := ψ) hψ
963 exact hH0Iso hxy'''
965omit [DecidableEq H] [DecidableEq G] in
966@[simp]
968 (hψ : Function.Surjective ψ) (h : H) (x : augmentationIdeal G) :
970 (MonoidAlgebra.of ℤ H h : GroupRing H) •
971 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ) x =
972 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
973 (((groupAugmentationIdealRep (G := G)).ρ (Function.surjInv hψ h)) x) := by
975 rw [show (MonoidAlgebra.of ℤ H h : GroupRing H) •
976 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ) x =
978 (MonoidAlgebra.of ℤ H h)
979 (Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ) x) by
980 rfl]
985omit [DecidableEq H] [DecidableEq G] in
987 {g₁ g₂ : G} (h : ψ g₁ = ψ g₂) (x : augmentationIdeal G) :
988 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
989 (((groupAugmentationIdealRep (G := G)).ρ g₁) x) =
990 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
991 (((groupAugmentationIdealRep (G := G)).ρ g₂) x) := by
992 let n : ψ.ker := ⟨g₁ * g₂⁻¹, by
993 simp only [MonoidHom.mem_ker, map_mul, h, map_inv, mul_inv_cancel]⟩
994 calc
995 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
996 (((groupAugmentationIdealRep (G := G)).ρ g₁) x)
997 = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
998 (((groupAugmentationIdealRep (G := G)).ρ (n.1 * g₂)) x) := by
999 congr 1
1000 simp only [of_ρ, MonoidHom.coe_mk, OneHom.coe_mk, LinearMap.coe_mk, AddHom.coe_mk, mul_assoc, inv_mul_cancel,
1001 mul_one, n]
1002 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1003 (((groupAugmentationIdealRep (G := G)).ρ n.1)
1004 (((groupAugmentationIdealRep (G := G)).ρ g₂) x)) := by
1005 congr 1
1006 exact congrArg
1007 (fun f : augmentationIdeal G →ₗ[ℤ] augmentationIdeal G => f x)
1008 (((groupAugmentationIdealRep (G := G)).ρ).map_mul n.1 g₂)
1009 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1010 (((kernelAugmentationIdealRep (ψ := ψ)).ρ n)
1011 (((groupAugmentationIdealRep (G := G)).ρ g₂) x)) := by
1013 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1014 (((groupAugmentationIdealRep (G := G)).ρ g₂) x) := by
1015 exact Representation.Coinvariants.mk_self_apply
1016 ((kernelAugmentationIdealRep (ψ := ψ)).ρ) n
1017 (((groupAugmentationIdealRep (G := G)).ρ g₂) x)
1019/-- The canonical differential generator `g ↦ [g - 1]` in `H₀(ker ψ, I(ℤ[G]))`. -/
1021 (g : G) :
1023 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1026omit [DecidableEq H] [DecidableEq G] in
1028 (hψ : Function.Surjective ψ) :
1033 intro g₁ g₂
1037 congr 1
1038 calc
1039 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1040 (((groupAugmentationIdealRep (G := G)).ρ g₁)
1042 = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1044 (Function.surjInv hψ (ψ g₁)))
1045 (augmentationGeneratorSubtype (H := G) g₂)) := by
1047 simpa using (Function.surjInv_eq hψ (ψ g₁)).symm
1048 _ = (MonoidAlgebra.of ℤ H (ψ g₁) : GroupRing H) •
1050 symm
1052 (ψ := ψ) hψ (ψ g₁) (augmentationGeneratorSubtype (H := G) g₂)
1054/-- The canonical linear map `A_ψ → H₀(ker ψ, I(ℤ[G]))` sending `d(g)` to `[g - 1]`. -/
1056 (hψ : Function.Surjective ψ) :
1060 exact
1061 lift ψ
1064 (ψ := ψ) hψ)
1066omit [DecidableEq H] [DecidableEq G] in
1067@[simp]
1069 (hψ : Function.Surjective ψ) (g : G) :
1072 (ψ := ψ) hψ (universalDifferential ψ g) =
1078 ψ
1081 (ψ := ψ) hψ)
1084omit [DecidableEq H] [DecidableEq G] in
1085@[simp 900]
1087 (hψ : Function.Surjective ψ) (x : KernelAbelianizationAdd ψ) :
1095 change
1096 (fun y : Abelianization ψ.ker =>
1098 (kernelAbelianizationBoundaryAdd ψ (Additive.ofMul y)) =
1099 kernelAbelianizationToCoinvariantsAdd (ψ := ψ) (Additive.ofMul y))
1100 (Additive.toMul x)
1101 refine QuotientGroup.induction_on (Additive.toMul x) ?_
1102 intro n
1103 calc
1105 ((kernelAbelianizationBoundaryAdd ψ) (Additive.ofMul (Abelianization.of n))) =
1108 exact congrArg
1110 (ψ := ψ) hψ)
1114 (ψ := ψ) hψ n.1
1115 _ = kernelAbelianizationToCoinvariantsAdd (ψ := ψ) (Additive.ofMul (Abelianization.of n)) := by
1116 symm
1120end CoinvariantsAction
1122end KernelAugmentation
1124end
1126end FoxDifferential