Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Discrete.KernelBoundary.Homology
ProCGroups/FoxDifferential/Discrete/KernelBoundary/Homology/Source

Source: ProCGroups.FoxDifferential.Discrete.KernelBoundary.Homology

1import Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
2import ProCGroups.FoxDifferential.Discrete.KernelBoundary.Basic
4/-!
5# Fox differential: discrete — kernel boundary — homology
7The principal declarations in this module are:
9- `kernelGroupRingRep`
10 The left-multiplication representation of \(\ker \psi\) on \(\mathbb{Z}[G]\).
11- `kernelSplitEquiv`
12 A section-based decomposition G \(\simeq\) \(\ker \psi\) \(\times\) H.
13- `kernelSplitEquiv_smul`
14 The kernel-splitting equivalence is equivariant for the left action of \(\ker\psi\): acting by
15 \(n\) before applying the equivalence is the same as acting by \(n\) afterward.
16- `indBottomKernelUnderlyingEquiv_mk`
17 The bottom-kernel induced-module equivalence sends the representative indexed by \(g\in\ker\psi\)
18 and \(a\in \mathbb{Z}[H]\) to the tensor of the singleton at \(g\) with \(a\).
19-/
21namespace FoxDifferential
23noncomputable section
25open CategoryTheory Limits Representation Rep TensorProduct MonoidalCategory
27variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
29section KernelGroupRing
31variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
33variable (ψ : G →* H) (hψ : Function.Surjective ψ)
35/-- The kernel-boundary codomain carries the trivial multiplication action. -/
36instance instMulActionKernelCodomainTrivial : MulAction ↥(ψ.ker) H where
37 smul _ h := h
38 one_smul _ := rfl
39 mul_smul _ _ _ := rfl
41/-- The left-multiplication representation of \(\ker \psi\) on \(\mathbb{Z}[G]\). -/
42abbrev kernelGroupRingRep : Rep ℤ ↥(ψ.ker) :=
43 Rep.ofMulAction ℤ ↥(ψ.ker) G
45/-- A section-based decomposition G \(\simeq\) \(\ker \psi\) \(\times\) H. -/
46def kernelSplitEquiv : G ≃ ↥(ψ.ker) × H where
47 toFun g :=
48 (⟨g * (Function.surjInv hψ (ψ g))⁻¹, by
49 simp only [MonoidHom.mem_ker, map_mul, map_inv, Function.surjInv_eq hψ (ψ g),
50 mul_inv_cancel]⟩, ψ g)
51 invFun x := x.1.1 * Function.surjInv hψ x.2
52 left_inv g := by
53 simp only [mul_assoc, inv_mul_cancel, mul_one]
54 right_inv x := by
55 rcases x with ⟨n, h⟩
56 apply Prod.ext
57 · apply Subtype.ext
58 change
59 n.1 * Function.surjInv hψ h *
60 (Function.surjInv hψ (ψ (n.1 * Function.surjInv hψ h)))⁻¹ = n.1
61 rw [map_mul, n.2, Function.surjInv_eq hψ h]
62 simp only [one_mul, mul_assoc, mul_inv_cancel, mul_one]
63 · change ψ (n.1 * Function.surjInv hψ h) = h
64 rw [map_mul, n.2, one_mul, Function.surjInv_eq hψ h]
66omit [DecidableEq H] [DecidableEq G] in
67/--
68The kernel-splitting equivalence is equivariant for the left action of \(\ker\psi\): acting by
69\(n\) before applying the equivalence is the same as acting by \(n\) afterward.
70-/
71@[simp]
72theorem kernelSplitEquiv_smul (n : ↥(ψ.ker)) (g : G) :
73 kernelSplitEquiv ψ hψ (n • g) = n • kernelSplitEquiv ψ hψ g := by
74 apply Prod.ext
75 · apply Subtype.ext
76 change
77 n.1 * g * (Function.surjInv hψ (ψ (n.1 * g)))⁻¹ =
78 n.1 * (g * (Function.surjInv hψ (ψ g))⁻¹)
79 rw [map_mul, n.2, one_mul]
80 simp only [mul_assoc]
81 · change ψ (n.1 * g) = ψ g
82 rw [map_mul, n.2, one_mul]
84/--
85The \(\ker \psi\)-representation on \(\mathbb{Z}[\ker \psi\] \otimes \mathbb{Z}[H]\) whose first
86factor is right-regular and whose second factor is trivial.
87-/
88abbrev kernelRightTensorRep : Rep ℤ ↥(ψ.ker) :=
89 rightRegularRep ↥(ψ.ker) ⊗ Rep.trivial ℤ ↥(ψ.ker) (H →₀ ℤ)
91/--
92The section decomposition, rewritten as a representation isomorphism to a right-regular tensor
93model.
94-/
95def kernelGroupRingRepIsoRightTensor :
96 kernelGroupRingRep (ψ := ψ) ≅ kernelRightTensorRep (H := H) (ψ := ψ) := by
97 let e₁ :
98 GroupRing G ≃ₗ[ℤ] ((↥(ψ.ker) × H) →₀ ℤ) :=
99 (MonoidAlgebra.coeffLinearEquiv ℤ).trans
100 (Finsupp.domLCongr (kernelSplitEquiv ψ hψ))
101 let e₂ :
102 ((↥(ψ.ker) × H) →₀ ℤ) ≃ₗ[ℤ] (GroupRing ↥(ψ.ker)) ⊗[ℤ] (H →₀ ℤ) :=
103 (finsuppTensorFinsupp' ℤ ↥(ψ.ker) H).symm.trans
104 (TensorProduct.congr
105 ((Finsupp.domLCongr (Equiv.inv ↥(ψ.ker))).trans
106 (MonoidAlgebra.coeffLinearEquiv ℤ).symm)
107 (LinearEquiv.refl ℤ (H →₀ ℤ)))
108 refine Rep.mkIso (Representation.Equiv.mk (e₁.trans e₂) ?_)
109 intro n
110 apply LinearMap.toAddMonoidHom_injective
111 apply MonoidAlgebra.addMonoidHom_ext
112 intro g r
113 have hcalc :
114 e₂ (Finsupp.single (n • kernelSplitEquiv ψ hψ g) r) =
115 ((kernelRightTensorRep (ψ := ψ) (H := H)).ρ n)
116 (e₂ (Finsupp.single (kernelSplitEquiv ψ hψ g) r)) := by
117 change e₂ (Finsupp.single (n • kernelSplitEquiv ψ hψ g) r) =
118 TensorProduct.map ((rightRegularRepresentation ↥(ψ.ker)) n) LinearMap.id
119 (e₂ (Finsupp.single (kernelSplitEquiv ψ hψ g) r))
120 cases hkg : kernelSplitEquiv ψ hψ g with
121 | mk m h =>
122 simp only [e₂, LinearEquiv.trans_apply,
123 finsuppTensorFinsupp'_symm_single_eq_single_one_tmul, TensorProduct.congr_tmul,
124 TensorProduct.map_tmul, LinearEquiv.refl_apply]
125 have hnm :
126 (((Finsupp.domLCongr (Equiv.inv ↥(ψ.ker))).trans
127 (MonoidAlgebra.coeffLinearEquiv ℤ).symm)
128 (Finsupp.single (n * m) (1 : ℤ))) =
129 MonoidAlgebra.single ((n * m)⁻¹) (1 : ℤ) := by
130 ext x
131 simp only [LinearEquiv.trans_apply, Finsupp.domLCongr_apply, Finsupp.domCongr_apply,
132 Finsupp.equivMapDomain_single, Equiv.inv_apply, mul_inv_rev,
133 MonoidAlgebra.coeffLinearEquiv_symm_apply, MonoidAlgebra.coeff_single]
134 have hm :
135 (((Finsupp.domLCongr (Equiv.inv ↥(ψ.ker))).trans
136 (MonoidAlgebra.coeffLinearEquiv ℤ).symm)
137 (Finsupp.single m (1 : ℤ))) =
138 MonoidAlgebra.single m⁻¹ (1 : ℤ) := by
139 ext x
140 simp only [LinearEquiv.trans_apply, Finsupp.domLCongr_apply, Finsupp.domCongr_apply,
141 Finsupp.equivMapDomain_single, Equiv.inv_apply,
142 MonoidAlgebra.coeffLinearEquiv_symm_apply, MonoidAlgebra.coeff_single]
143 change
144 (((Finsupp.domLCongr (Equiv.inv ↥(ψ.ker))).trans
145 (MonoidAlgebra.coeffLinearEquiv ℤ).symm)
146 (Finsupp.single (n * m) (1 : ℤ))) ⊗ₜ[ℤ] Finsupp.single h r =
147 ((rightRegularRepresentation ↥(ψ.ker)) n)
148 ((((Finsupp.domLCongr (Equiv.inv ↥(ψ.ker))).trans
149 (MonoidAlgebra.coeffLinearEquiv ℤ).symm)
150 (Finsupp.single m (1 : ℤ)))) ⊗ₜ[ℤ] Finsupp.single h r
151 rw [hnm, hm]
152 simp only [mul_inv_rev, rightRegularRepresentation_apply_single]
153 change
154 e₂
155 (e₁
156 (((kernelGroupRingRep (ψ := ψ)).ρ n) (MonoidAlgebra.single g r))) =
157 ((kernelRightTensorRep (ψ := ψ) (H := H)).ρ n)
158 (e₂ (e₁ (MonoidAlgebra.single g r)))
159 simpa [kernelGroupRingRep, kernelRightTensorRep, e₁,
160 LinearEquiv.trans_apply, kernelSplitEquiv_smul, MonoidAlgebra.coeffLinearEquiv_apply,
161 Representation.ofMulAction_single, Rep.tensor_ρ] using hcalc
163/--
164The trivial representation of the trivial subgroup of \(\ker \psi\) on the free
165\(\mathbb{Z}\)-module \(\mathbb{Z}[H]\).
166-/
167def indBottomKernelUnderlyingEquiv :
168 Representation.IndV (⊥ : Subgroup ↥(ψ.ker)).subtype
169 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ
170 ≃ₗ[ℤ] (GroupRing ↥(ψ.ker)) ⊗[ℤ] (H →₀ ℤ) := by
171 let ρt :
172 Representation ℤ (⊥ : Subgroup ↥(ψ.ker))
173 (TensorProduct ℤ (GroupRing ↥(ψ.ker)) (H →₀ ℤ)) :=
174 Representation.tprod
175 (((Rep.leftRegular ℤ ↥(ψ.ker)).ρ.comp (⊥ : Subgroup ↥(ψ.ker)).subtype))
176 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ
177 exact coinvariantsLEquivOfSubsingleton ρt
179omit [DecidableEq H] [DecidableEq G] in
180/--
181The bottom-kernel induced-module equivalence sends the representative indexed by
182\(g\in\ker\psi\) and \(a\in \mathbb{Z}[H]\) to the tensor of the singleton at \(g\) with \(a\).
183-/
184@[simp 900]
185theorem indBottomKernelUnderlyingEquiv_mk (g : ↥(ψ.ker)) (a : H →₀ ℤ) :
186 indBottomKernelUnderlyingEquiv (H := H) (ψ := ψ)
187 (Representation.IndV.mk (⊥ : Subgroup ↥(ψ.ker)).subtype
188 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ g a) =
189 MonoidAlgebra.single g 1 ⊗ₜ[ℤ] a := by
190 change
191 (Representation.Coinvariants.lift
192 (Representation.tprod
193 (((Rep.leftRegular ℤ ↥(ψ.ker)).ρ.comp (⊥ : Subgroup ↥(ψ.ker)).subtype))
194 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ)
195 LinearMap.id
196 (fun x => by
197 ext y
198 have : x = (1 : (⊥ : Subgroup ↥(ψ.ker))) := Subsingleton.elim _ _
199 subst this
200 simp only [Function.comp_apply,
201 map_one, LinearMap.id_comp, LinearMap.coe_comp, Finsupp.lsingle_apply,
202 AlgebraTensorModule.curry_apply, LinearMap.restrictScalars_self, curry_apply,
203 Module.End.one_apply,
204 LinearMap.id_coe, id_eq]))
205 (Representation.Coinvariants.mk _
206 ((MonoidAlgebra.single g 1 : GroupRing ↥(ψ.ker)) ⊗ₜ[ℤ] a)) = _
207 rw [Representation.Coinvariants.lift_mk]
208 rfl
210/-- \(\operatorname{Ind}_{1}^{\ker \psi}(\mathbb{Z}[H])\) is the right-regular tensor model. -/
211def indBottomKernelIsoRightTensor :
212 Rep.ind (⊥ : Subgroup ↥(ψ.ker)).subtype
213 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)) ≅
214 kernelRightTensorRep (ψ := ψ) (H := H) := by
215 refine Rep.mkIso (Representation.Equiv.mk
216 (indBottomKernelUnderlyingEquiv (H := H) (ψ := ψ)) ?_)
217 intro g
218 apply Representation.IndV.hom_ext (φ := (⊥ : Subgroup ↥(ψ.ker)).subtype)
219 (ρ := (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ)
220 · intro h
221 apply LinearMap.ext
222 intro a
223 change
224 indBottomKernelUnderlyingEquiv (H := H) (ψ := ψ)
225 (((Rep.ind (⊥ : Subgroup ↥(ψ.ker)).subtype
226 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ))).ρ g)
227 ((Representation.IndV.mk (⊥ : Subgroup ↥(ψ.ker)).subtype
228 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ h) a)) =
229 ((kernelRightTensorRep (ψ := ψ) (H := H)).ρ g)
230 (indBottomKernelUnderlyingEquiv (H := H) (ψ := ψ)
231 ((Representation.IndV.mk (⊥ : Subgroup ↥(ψ.ker)).subtype
232 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ h) a))
233 have hind :
234 (((Rep.ind (⊥ : Subgroup ↥(ψ.ker)).subtype
235 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ))).ρ g)
236 ((Representation.IndV.mk (⊥ : Subgroup ↥(ψ.ker)).subtype
237 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ h) a)) =
238 (Representation.IndV.mk (⊥ : Subgroup ↥(ψ.ker)).subtype
239 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ (h * g⁻¹)) a := by
240 exact Representation.ind_mk
241 (φ := (⊥ : Subgroup ↥(ψ.ker)).subtype)
242 (ρ := (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)).ρ) g h a
243 rw [hind, indBottomKernelUnderlyingEquiv_mk, indBottomKernelUnderlyingEquiv_mk]
244 change MonoidAlgebra.single (h * g⁻¹) 1 ⊗ₜ[ℤ] a =
245 TensorProduct.map ((rightRegularRepresentation ↥(ψ.ker)) g) LinearMap.id
246 (MonoidAlgebra.single h 1 ⊗ₜ[ℤ] a)
247 simp only [map_tmul, rightRegularRepresentation_apply_single, LinearMap.id_coe, id_eq]
249end KernelGroupRing
251section KernelAugmentation
253variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
255variable (ψ : G →* H)
257/-- The left-regular representation of \(G\) on \(\mathbb{Z}[G]\). -/
258abbrev groupRingRep : Rep ℤ G :=
259 Rep.ofMulAction ℤ G G
261omit [DecidableEq G] in
262/--
263The group-ring representation sends a singleton basis element to the singleton at the product.
264-/
265@[simp]
266theorem groupRingRep_apply_single (g h : G) (m : ℤ) :
267 ((groupRingRep (G := G)).ρ g) (MonoidAlgebra.single h m) =
268 MonoidAlgebra.single (g * h) m := by
269 exact Representation.ofMulAction_single (k := ℤ) (G := G) (H := G) g h m
271omit [DecidableEq H] [DecidableEq G] in
272/--
273The kernel group-ring representation sends a singleton basis element to the singleton at the
274product.
275-/
276@[simp]
277theorem kernelGroupRingRep_apply_single (n : ψ.ker) (g : G) (m : ℤ) :
278 ((kernelGroupRingRep (ψ := ψ)).ρ n) (MonoidAlgebra.single g m) =
279 MonoidAlgebra.single (n • g) m := by
280 exact Representation.ofMulAction_single (k := ℤ) (G := ↥(ψ.ker)) (H := G) n g m
282omit [DecidableEq H] [DecidableEq G] in
283/-- The left-regular group-ring representation preserves the augmentation-kernel condition. -/
284theorem augmentation_kernelGroupRingRep
285 (n : ψ.ker) (x : GroupRing G) :
286 augmentation G (((kernelGroupRingRep (ψ := ψ)).ρ n) x) = augmentation G x := by
287 let F : GroupRing G →ₗ[ℤ] ℤ :=
288 ((augmentation G).toAddMonoidHom.toIntLinearMap).comp ((kernelGroupRingRep (ψ := ψ)).ρ n)
289 have hF : F = (augmentation G).toAddMonoidHom.toIntLinearMap := by
290 apply LinearMap.toAddMonoidHom_injective
291 apply MonoidAlgebra.addMonoidHom_ext
292 intro g m
293 change augmentation G (((kernelGroupRingRep (ψ := ψ)).ρ n)
294 (MonoidAlgebra.single g m)) = augmentation G (MonoidAlgebra.single g m)
295 rw [kernelGroupRingRep_apply_single]
296 simp only [augmentation, augmentationAlgHom,
297 AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MonoidAlgebra.lift_single,
298 MonoidHom.one_apply, Int.zsmul_eq_mul, mul_one]
299 exact LinearMap.congr_fun hF x
301omit [DecidableEq G] in
302/-- Left multiplication by \(g : G\) preserves the group-ring augmentation. -/
303theorem augmentation_groupRingRep
304 (g : G) (x : GroupRing G) :
305 augmentation G (((groupRingRep (G := G)).ρ g) x) = augmentation G x := by
306 let F : GroupRing G →ₗ[ℤ] ℤ :=
307 ((augmentation G).toAddMonoidHom.toIntLinearMap).comp ((groupRingRep (G := G)).ρ g)
308 have hF : F = (augmentation G).toAddMonoidHom.toIntLinearMap := by
309 apply LinearMap.toAddMonoidHom_injective
310 apply MonoidAlgebra.addMonoidHom_ext
311 intro h m
312 change augmentation G (((groupRingRep (G := G)).ρ g)
313 (MonoidAlgebra.single h m)) = augmentation G (MonoidAlgebra.single h m)
314 rw [groupRingRep_apply_single]
315 simp only [augmentation, augmentationAlgHom,
316 AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MonoidAlgebra.lift_single,
317 MonoidHom.one_apply, Int.zsmul_eq_mul, mul_one]
318 exact LinearMap.congr_fun hF x
320/-- The left-regular G-action preserves the augmentation ideal \(I(\mathbb{Z}[G])\). -/
321abbrev groupAugmentationIdealRep : Rep ℤ G :=
322 Rep.of (X := augmentationIdeal G)
323 { toFun := fun g =>
324 { toFun := fun x =>
325 ⟨((groupRingRep (G := G)).ρ g) x.1, by
326 rw [mem_augmentationIdeal_iff]
327 rw [augmentation_groupRingRep (G := G) g x.1]
328 exact (mem_augmentationIdeal_iff (H := G) (x := x.1)).1 x.2⟩
329 map_add' := by
330 intro x y
331 apply Subtype.ext
332 exact map_add ((groupRingRep (G := G)).ρ g) x.1 y.1
333 map_smul' := by
334 intro m x
335 apply Subtype.ext
336 exact map_smul ((groupRingRep (G := G)).ρ g) m x.1 }
337 map_one' := by
338 ext x h
339 simp only [groupRingRep, map_one, Module.End.one_apply, Subtype.coe_eta,
340 LinearMap.coe_mk, AddHom.coe_mk]
341 map_mul' := by
342 intro g₁ g₂
343 ext x h
344 simp only [groupRingRep, map_mul, Module.End.mul_apply, LinearMap.coe_mk,
345 AddHom.coe_mk]}
347/-- The kernel-restricted action of \(\ker \psi\) on the augmentation ideal \(I(\mathbb{Z}[G])\). -/
348abbrev kernelAugmentationIdealRep : Rep ℤ ↥(ψ.ker) :=
349 Rep.of (X := augmentationIdeal G)
350 { toFun := fun n =>
351 { toFun := fun x =>
352 ⟨((kernelGroupRingRep (ψ := ψ)).ρ n) x.1, by
353 rw [mem_augmentationIdeal_iff]
354 rw [augmentation_kernelGroupRingRep (ψ := ψ) n x.1]
355 exact (mem_augmentationIdeal_iff (H := G) (x := x.1)).1 x.2⟩
356 map_add' := by
357 intro x y
358 apply Subtype.ext
359 exact map_add ((kernelGroupRingRep (ψ := ψ)).ρ n) x.1 y.1
360 map_smul' := by
361 intro m x
362 apply Subtype.ext
363 exact map_smul ((kernelGroupRingRep (ψ := ψ)).ρ n) m x.1 }
364 map_one' := by
365 ext x g
366 simp only [kernelGroupRingRep, map_one, Module.End.one_apply, Subtype.coe_eta,
367 LinearMap.coe_mk, AddHom.coe_mk]
368 map_mul' := by
369 intro n₁ n₂
370 ext x g
371 simp only [kernelGroupRingRep, map_mul, Module.End.mul_apply, LinearMap.coe_mk,
372 AddHom.coe_mk]}
374/--
375The inclusion \(I(\mathbb{Z}[G])\hookrightarrow \mathbb{Z}[G]\) as a morphism of \(\ker
376\psi\)-representations.
377-/
378def kernelAugmentationIdealInclusion :
379 kernelAugmentationIdealRep (ψ := ψ) ⟶ kernelGroupRingRep (ψ := ψ) :=
380 Rep.ofHom <| Representation.IntertwiningMap.mk
381 ((augmentationIdeal G).subtype.restrictScalars ℤ) fun _ => rfl
383/--
384The augmentation map \(\mathbb{Z}[G] \to \mathbb{Z}\) as a morphism of \(\ker
385\psi\)-representations.
386-/
387def kernelGroupRingAugmentation :
388 kernelGroupRingRep (ψ := ψ) ⟶ Rep.trivial ℤ ↥(ψ.ker) ℤ :=
389 Rep.ofHom <| Representation.IntertwiningMap.mk
390 ((augmentation G).toAddMonoidHom.toIntLinearMap) fun n => by
391 apply LinearMap.toAddMonoidHom_injective
392 apply MonoidAlgebra.addMonoidHom_ext
393 intro g m
394 change augmentation G (((kernelGroupRingRep (ψ := ψ)).ρ n)
395 (MonoidAlgebra.single g m)) =
396 ((Rep.trivial ℤ ↥(ψ.ker) ℤ).ρ n) (augmentation G (MonoidAlgebra.single g m))
397 rw [kernelGroupRingRep_apply_single]
398 simp only [augmentation, augmentationAlgHom,
399 AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MonoidAlgebra.lift_single,
400 MonoidHom.one_apply, Int.zsmul_eq_mul, mul_one, isTrivial_def, LinearMap.id_coe, id_eq]
402/--
403The augmentation ideal \(I(\mathbb{Z}[G])\), the group ring \(\mathbb{Z}[G]\), and the
404augmentation \(\mathbb{Z}[G]\to\mathbb{Z}\) form the short complex \(0\to
405I(\mathbb{Z}[G])\to\mathbb{Z}[G]\to\mathbb{Z}\to 0\) of \(\ker \psi\)-representations.
406-/
407def kernelAugmentationShortComplex :
408 CategoryTheory.ShortComplex (Rep ℤ ↥(ψ.ker)) :=
409 CategoryTheory.ShortComplex.mk
410 (kernelAugmentationIdealInclusion (ψ := ψ))
411 (kernelGroupRingAugmentation (ψ := ψ))
412 (by
413 ext x
414 exact x.2)
416omit [DecidableEq H] [DecidableEq G] in
417/--
418The kernel-augmentation short complex is exact: the augmentation ideal maps onto the kernel of
419the group-ring augmentation.
420-/
421theorem kernelAugmentationShortComplex_exact :
422 (kernelAugmentationShortComplex (ψ := ψ)).Exact := by
423 letI repIntModule (A : Rep.{0} ℤ ↥(ψ.ker)) : Module ℤ A := A.hV2
424 apply (forget₂ (Rep.{0} ℤ ↥(ψ.ker)) (ModuleCat ℤ)).reflects_exact_of_faithful
425 rw [CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker]
426 ext x
427 constructor
428 · rintro ⟨y, rfl⟩
429 exact y.2
430 · intro hx
431 change augmentation G x = 0 at hx
432 refine ⟨⟨x, ?_⟩, rfl⟩
433 rw [mem_augmentationIdeal_iff]
434 simpa [LinearMap.mem_ker] using hx
436omit [DecidableEq H] [DecidableEq G] in
437/--
438The canonical augmentation sequence with augmentation ideal as kernel is short exact: the
439inclusion is injective, its image is the kernel of augmentation, and the augmentation is
440surjective.
441-/
442theorem kernelAugmentationShortExact :
443 (kernelAugmentationShortComplex (ψ := ψ)).ShortExact := by
444 haveI : Mono (kernelAugmentationShortComplex (ψ := ψ)).f := by
445 change Mono (kernelAugmentationIdealInclusion (ψ := ψ))
446 exact (Rep.mono_iff_injective _).2 fun x y h => by
447 apply Subtype.ext
448 exact h
449 haveI : Epi (kernelAugmentationShortComplex (ψ := ψ)).g := by
450 change Epi (kernelGroupRingAugmentation (ψ := ψ))
451 exact (Rep.epi_iff_surjective _).2 <| by
452 intro m
453 refine ⟨(m : GroupRing G), ?_⟩
454 change augmentation G (m : GroupRing G) = m
455 rw [map_intCast]
456 rfl
457 refine CategoryTheory.ShortComplex.ShortExact.mk
458 (S := kernelAugmentationShortComplex (ψ := ψ))
459 (exact := kernelAugmentationShortComplex_exact (ψ := ψ))
461/-- The trivial integral representation of \(\ker\psi\). -/
462abbrev kernelTrivialIntRep : Rep ℤ ↥(ψ.ker) :=
463 Rep.trivial ℤ ↥(ψ.ker) ℤ
465/--
466The connecting homomorphism \(H_1(\ker \psi, \mathbb{Z})\) \(\to\) \(H_0(\ker \psi,
467I(\mathbb{Z}[G]))\) attached to the short exact sequence 0 \(\to\) \(I(\mathbb{Z}[G])\) \(\to\)
468\(\mathbb{Z}[G]\) \(\to\) \(\mathbb{Z}\) \(\to\) 0 of \(\ker \psi\)-representations.
469-/
470def kernelAugmentationConnecting :
471 groupHomology (kernelTrivialIntRep (ψ := ψ)) 1 ⟶
472 groupHomology (kernelAugmentationIdealRep (ψ := ψ)) 0 :=
473 groupHomology.δ
474 (X := kernelAugmentationShortComplex (ψ := ψ))
475 (kernelAugmentationShortExact (ψ := ψ))
476 1 0 rfl
478/--
479The standard low-degree identification \(H_1(\ker \psi, \mathbb{Z}) \simeq (\ker
480\psi)^{\mathrm{ab}}\).
481-/
482def kernelTrivialH1AddEquivAbelianization :
483 groupHomology (kernelTrivialIntRep (ψ := ψ)) 1 ≃+
484 Additive (Abelianization ψ.ker) :=
485 (groupHomology.H1AddEquivOfIsTrivial (kernelTrivialIntRep (ψ := ψ))).trans
486 (TensorProduct.rid ℤ (Additive (Abelianization ψ.ker))).toAddEquiv
488omit [DecidableEq H] [DecidableEq G] in
489/--
490The inverse of the \(H_1\)-abelianization equivalence sends the abelianization class of
491\(n\in\ker\psi\) to the degree-one homology class represented by the singleton cycle at \(n\).
492-/
493@[simp]
494theorem kernelTrivialH1AddEquivAbelianization_symm_of (n : ψ.ker) :
495 (kernelTrivialH1AddEquivAbelianization (ψ := ψ)).symm
496 (Additive.ofMul (Abelianization.of n)) =
497 groupHomology.H1π (kernelTrivialIntRep (ψ := ψ))
498 ((groupHomology.cycles₁IsoOfIsTrivial (kernelTrivialIntRep (ψ := ψ))).inv
499 (Finsupp.single n 1)) := by
500 unfold kernelTrivialH1AddEquivAbelianization
501 rw [AddEquiv.symm_trans_apply]
502 simpa [TensorProduct.rid_symm_apply] using
503 (groupHomology.H1AddEquivOfIsTrivial_symm_tmul
504 (A := kernelTrivialIntRep (ψ := ψ)) n (1 : ℤ))
506omit [DecidableEq H] [DecidableEq G] in
507/--
508The connecting morphism sends a boundary cycle to the corresponding augmentation-coinvariant
509class.
510-/
511theorem kernelAugmentationConnecting_boundaryCycle_of (n : ψ.ker) :
512 Finsupp.mapRange.linearMap (kernelAugmentationShortComplex (ψ := ψ)).g.hom.toLinearMap
513 (Finsupp.single n (MonoidAlgebra.single n.1 (1 : ℤ))) =
514 ((groupHomology.cycles₁IsoOfIsTrivial (kernelTrivialIntRep (ψ := ψ))).inv
515 (Finsupp.single n 1)).1 := by
516 change
517 Finsupp.mapRange.linearMap (kernelGroupRingAugmentation (ψ := ψ)).hom.toLinearMap
518 (Finsupp.single n (MonoidAlgebra.single n.1 (1 : ℤ))) =
519 (Finsupp.single n (1 : ℤ))
520 rw [show
521 (Finsupp.mapRange.linearMap (kernelGroupRingAugmentation (ψ := ψ)).hom.toLinearMap)
522 (Finsupp.single n (MonoidAlgebra.single n.1 (1 : ℤ))) =
523 Finsupp.mapRange (kernelGroupRingAugmentation (ψ := ψ)).hom.toLinearMap
524 ((kernelGroupRingAugmentation (ψ := ψ)).hom.toLinearMap.map_zero)
525 (Finsupp.single n (MonoidAlgebra.single n.1 (1 : ℤ))) by
526 rfl]
527 rw [Finsupp.mapRange_single]
528 have hcoeff :
529 (kernelGroupRingAugmentation (ψ := ψ)).hom.toLinearMap
530 (MonoidAlgebra.single n.1 (1 : ℤ)) = 1 := by
531 change augmentation G (MonoidAlgebra.single n.1 (1 : ℤ)) = 1
532 simp only [augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
533 MonoidAlgebra.lift_single, MonoidHom.one_apply, Int.zsmul_eq_mul, mul_one]
534 simpa using congrArg (Finsupp.single n) hcoeff
536omit [DecidableEq H] [DecidableEq G] in
537/-- The connecting morphism has the displayed representative on a boundary element. -/
538theorem kernelAugmentationConnecting_boundaryElement_of (n : ψ.ker) :
539 (kernelAugmentationShortComplex (ψ := ψ)).f.hom
540 (-(augmentationGeneratorSubtype (H := G) n.1)) =
541 groupHomology.d₁₀ (kernelGroupRingRep (ψ := ψ))
542 (Finsupp.single n (MonoidAlgebra.single n.1 (1 : ℤ))) := by
543 have hn : (n⁻¹ : ψ.ker) • n.1 = (1 : G) := by
544 change n.1⁻¹ * n.1 = 1
545 simp only [inv_mul_cancel]
546 change (-(augmentationGenerator (H := G) n.1) : GroupRing G) =
547 groupHomology.d₁₀ (kernelGroupRingRep (ψ := ψ))
548 (Finsupp.single n (MonoidAlgebra.single n.1 (1 : ℤ)))
549 rw [groupHomology.d₁₀_single, kernelGroupRingRep_apply_single, hn]
550 unfold augmentationGenerator
551 change (-(MonoidAlgebra.single n.1 (1 : ℤ) -
552 MonoidAlgebra.single (1 : G) (1 : ℤ)) : GroupRing G) =
553 MonoidAlgebra.single (1 : G) (1 : ℤ) - MonoidAlgebra.single n.1 (1 : ℤ)
554 simp only [sub_eq_add_neg]
555 rw [neg_add, neg_neg]
556 change -MonoidAlgebra.single n.1 (1 : ℤ) + MonoidAlgebra.single (1 : G) (1 : ℤ) =
557 MonoidAlgebra.single (1 : G) (1 : ℤ) + -MonoidAlgebra.single n.1 (1 : ℤ)
558 abel_nf
560omit [DecidableEq H] [DecidableEq G] in
561/-- The connecting morphism matches the corresponding degree-zero coinvariant class. -/
562theorem kernelAugmentationConnecting_H0Iso_of (n : ψ.ker) :
563 (groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
564 ((kernelAugmentationConnecting (ψ := ψ)).hom
565 ((kernelTrivialH1AddEquivAbelianization (ψ := ψ)).symm
566 (Additive.ofMul (Abelianization.of n)))) =
567 -Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
568 (augmentationGeneratorSubtype (H := G) n.1) := by
569 rw [kernelTrivialH1AddEquivAbelianization_symm_of (ψ := ψ) n]
570 have hδ :
571 (kernelAugmentationConnecting (ψ := ψ)).hom
572 ((groupHomology.H1π (kernelTrivialIntRep (ψ := ψ))).hom
573 ((groupHomology.cycles₁IsoOfIsTrivial (kernelTrivialIntRep (ψ := ψ))).inv
574 (Finsupp.single n 1))) =
575 (groupHomology.H0π (kernelAugmentationIdealRep (ψ := ψ))).hom
576 (-(augmentationGeneratorSubtype (H := G) n.1)) := by
577 exact
578 groupHomology.δ₀_apply
579 (hX := kernelAugmentationShortExact (ψ := ψ))
580 (z := (groupHomology.cycles₁IsoOfIsTrivial (kernelTrivialIntRep (ψ := ψ))).inv
581 (Finsupp.single n 1))
582 (y := Finsupp.single n (MonoidAlgebra.single n.1 (1 : ℤ)))
583 (x := -(augmentationGeneratorSubtype (H := G) n.1))
584 (kernelAugmentationConnecting_boundaryCycle_of (ψ := ψ) n)
585 (kernelAugmentationConnecting_boundaryElement_of (ψ := ψ) n)
586 have hδ' := congrArg
587 ((groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom) hδ
588 have hδ'' :
589 (groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
590 ((kernelAugmentationConnecting (ψ := ψ)).hom
591 ((groupHomology.H1π (kernelTrivialIntRep (ψ := ψ))).hom
592 ((groupHomology.cycles₁IsoOfIsTrivial (kernelTrivialIntRep (ψ := ψ))).inv
593 (Finsupp.single n 1)))) =
594 (groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
595 ((groupHomology.H0π (kernelAugmentationIdealRep (ψ := ψ))).hom
596 (-(augmentationGeneratorSubtype (H := G) n.1))) := by
597 exact hδ'
598 calc
599 (groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
600 ((kernelAugmentationConnecting (ψ := ψ)).hom
601 ((groupHomology.H1π (kernelTrivialIntRep (ψ := ψ))).hom
602 ((groupHomology.cycles₁IsoOfIsTrivial (kernelTrivialIntRep (ψ := ψ))).inv
603 (Finsupp.single n 1))))
604 =
605 (groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
606 ((groupHomology.H0π (kernelAugmentationIdealRep (ψ := ψ))).hom
607 (-(augmentationGeneratorSubtype (H := G) n.1))) := hδ''
608 _ = ((coinvariantsMk ℤ ↥ψ.ker).app (kernelAugmentationIdealRep (ψ := ψ)))
609 (-(augmentationGeneratorSubtype (H := G) n.1)) := by
610 exact
611 (groupHomology.H0π_comp_H0Iso_hom_apply
612 (A := kernelAugmentationIdealRep (ψ := ψ))
613 (x := -(augmentationGeneratorSubtype (H := G) n.1)))
614 _ = -Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
615 (augmentationGeneratorSubtype (H := G) n.1) := by
616 rfl
618omit [DecidableEq H] [DecidableEq G] in
619/-- The kernel-augmentation connecting map is injective. -/
620theorem kernelAugmentationConnecting_injective
621 (hψ : Function.Surjective ψ) :
622 Function.Injective (kernelAugmentationConnecting (ψ := ψ)).hom := by
623 letI : Mono (kernelAugmentationConnecting (ψ := ψ)) := by
624 let hH1 : Limits.IsZero (groupHomology (kernelGroupRingRep (ψ := ψ)) 1) := by
625 classical
626 let hrt : Limits.IsZero (groupHomology (kernelRightTensorRep (ψ := ψ) (H := H)) 1) :=
627 let hbot : Limits.IsZero
628 (groupHomology (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)) 1) := by
629 simpa using
630 (isZero_groupHomology_succ_of_subsingleton
631 (A := Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)) 0)
632 hbot.of_iso <|
633 (groupHomologyIsoOfRepIso (H := ↥(ψ.ker))
634 (indBottomKernelIsoRightTensor (H := H) (ψ := ψ)).symm 1) ≪≫
635 groupHomology.indIso (⊥ : Subgroup ↥(ψ.ker))
636 (Rep.trivial ℤ (⊥ : Subgroup ↥(ψ.ker)) (H →₀ ℤ)) 1
637 exact hrt.of_iso
638 (groupHomologyIsoOfRepIso (H := ↥(ψ.ker))
639 (kernelGroupRingRepIsoRightTensor (H := H) (ψ := ψ) hψ) 1)
640 exact groupHomology.mono_δ_of_isZero
641 (X := kernelAugmentationShortComplex (ψ := ψ))
642 (kernelAugmentationShortExact (ψ := ψ))
643 0
644 hH1
645 exact (ModuleCat.mono_iff_injective _).1 inferInstance
647/--
648The coinvariants of the kernel augmentation ideal are formed from the ordinary group-ring
649augmentation ideal.
650-/
651abbrev KernelAugmentationIdealCoinvariants (ψ : G →* H) : Type _ :=
652 Representation.Coinvariants ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
654local instance (priority := 2000) instKernelAugmentationIdealCoinvariantsIntModule :
655 Module ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
656 Representation.Coinvariants.instModule ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
658omit [DecidableEq H] [DecidableEq G] in
659/--
660The kernel augmentation-ideal representative agrees with the corresponding group
661augmentation-ideal representative.
662-/
663@[simp 900]
664theorem kernelAugmentationIdealRep_rho_eq_groupAugmentationIdealRep_rho
665 (n : ψ.ker) :
666 (kernelAugmentationIdealRep (ψ := ψ)).ρ n =
667 (groupAugmentationIdealRep (G := G)).ρ n.1 := by
668 ext x
669 rfl
671section CoinvariantsAction
673/-- The \(H\)-action on \(H_0(\ker \psi, I(\mathbb{Z}[G]))\), built from a surjective section. -/
674def kernelAugmentationIdealCoinvariantsEndOfSurjective
675 (hψ : Function.Surjective ψ) (h : H) :
676 KernelAugmentationIdealCoinvariants (ψ := ψ) →ₗ[ℤ]
677 KernelAugmentationIdealCoinvariants (ψ := ψ) :=
678 Representation.Coinvariants.lift ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
679 ((Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)).comp
680 ((groupAugmentationIdealRep (G := G)).ρ (Function.surjInv hψ h)))
681 (by
682 intro n
683 ext x
684 let s : G := Function.surjInv hψ h
685 have hs : ψ s = h := by
686 simpa [s] using Function.surjInv_eq hψ h
687 let n' : ψ.ker := ⟨s * n.1 * s⁻¹, by
688 change ψ (s * n.1 * s⁻¹) = 1
689 rw [map_mul, map_mul, n.2, map_inv, hs]
690 simp only [mul_one, mul_inv_cancel]⟩
691 have hs_mul :
692 ((groupAugmentationIdealRep (G := G)).ρ s)
693 (((groupAugmentationIdealRep (G := G)).ρ n.1) x) =
694 ((groupAugmentationIdealRep (G := G)).ρ (s * n.1)) x := by
695 exact congrArg
696 (fun f : augmentationIdeal G →ₗ[ℤ] augmentationIdeal G => f x)
697 (((groupAugmentationIdealRep (G := G)).ρ).map_mul s n.1).symm
698 have hs'_mul :
699 ((groupAugmentationIdealRep (G := G)).ρ n'.1)
700 (((groupAugmentationIdealRep (G := G)).ρ s) x) =
701 ((groupAugmentationIdealRep (G := G)).ρ (n'.1 * s)) x := by
702 exact congrArg
703 (fun f : augmentationIdeal G →ₗ[ℤ] augmentationIdeal G => f x)
704 (((groupAugmentationIdealRep (G := G)).ρ).map_mul n'.1 s).symm
705 calc
706 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
707 (((groupAugmentationIdealRep (G := G)).ρ s)
708 (((kernelAugmentationIdealRep (ψ := ψ)).ρ n) x))
709 = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
710 (((groupAugmentationIdealRep (G := G)).ρ s)
711 (((groupAugmentationIdealRep (G := G)).ρ n.1) x)) := by
712 rw [kernelAugmentationIdealRep_rho_eq_groupAugmentationIdealRep_rho
713 (ψ := ψ) n]
714 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
715 (((groupAugmentationIdealRep (G := G)).ρ (s * n.1)) x) := by
716 rw [hs_mul]
717 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
718 (((groupAugmentationIdealRep (G := G)).ρ (n'.1 * s)) x) := by
719 congr 1
720 simp only [MonoidHom.coe_mk, OneHom.coe_mk, map_mul, Module.End.mul_apply,
721 LinearMap.coe_mk,
722 AddHom.coe_mk, mul_assoc, inv_mul_cancel, mul_one, s, n']
723 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
724 (((groupAugmentationIdealRep (G := G)).ρ n'.1)
725 (((groupAugmentationIdealRep (G := G)).ρ s) x)) := by
726 rw [hs'_mul]
727 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
728 (((kernelAugmentationIdealRep (ψ := ψ)).ρ n')
729 (((groupAugmentationIdealRep (G := G)).ρ s) x)) := by
730 rw [kernelAugmentationIdealRep_rho_eq_groupAugmentationIdealRep_rho
731 (ψ := ψ) n']
732 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
733 (((groupAugmentationIdealRep (G := G)).ρ s) x) := by
734 exact Representation.Coinvariants.mk_self_apply
735 ((kernelAugmentationIdealRep (ψ := ψ)).ρ) n'
736 (((groupAugmentationIdealRep (G := G)).ρ s) x))
738omit [DecidableEq H] [DecidableEq G] in
739/--
740The surjective-case endomorphism of kernel augmentation coinvariants is evaluated on
741representatives.
742-/
743@[simp 900]
744theorem kernelAugmentationIdealCoinvariantsEndOfSurjective_mk
745 (hψ : Function.Surjective ψ) (h : H) (x : augmentationIdeal G) :
746 kernelAugmentationIdealCoinvariantsEndOfSurjective (ψ := ψ) hψ h
747 (Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ) x) =
748 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
749 (((groupAugmentationIdealRep (G := G)).ρ (Function.surjInv hψ h)) x) := by
750 rfl
752/--
753In the surjective case, the \(H\)-action on \(H_0(\ker\psi, I(\mathbb{Z}[G]))\) is bundled as
754linear endomorphisms.
755-/
756def kernelAugmentationIdealCoinvariantsModuleEndOfSurjective
757 (hψ : Function.Surjective ψ) :
758 H →* Module.End ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) where
759 toFun h := kernelAugmentationIdealCoinvariantsEndOfSurjective (ψ := ψ) hψ h
760 map_one' := by
761 apply Representation.Coinvariants.hom_ext
762 ext x
763 rw [LinearMap.comp_apply]
764 rw [kernelAugmentationIdealCoinvariantsEndOfSurjective_mk (ψ := ψ) hψ]
765 let n : ψ.ker := ⟨Function.surjInv hψ (1 : H), by
766 simpa using Function.surjInv_eq hψ (1 : H)⟩
767 rw [← kernelAugmentationIdealRep_rho_eq_groupAugmentationIdealRep_rho
768 (ψ := ψ) n]
769 simpa [n] using
770 (Representation.Coinvariants.mk_self_apply ((kernelAugmentationIdealRep (ψ := ψ)).ρ) n x)
771 map_mul' h₁ h₂ := by
772 apply Representation.Coinvariants.hom_ext
773 ext x
774 let s₁ : G := Function.surjInv hψ h₁
775 let s₂ : G := Function.surjInv hψ h₂
776 let s₁₂ : G := Function.surjInv hψ (h₁ * h₂)
777 have hs₁ : ψ s₁ = h₁ := by
778 simpa [s₁] using Function.surjInv_eq hψ h₁
779 have hs₂ : ψ s₂ = h₂ := by
780 simpa [s₂] using Function.surjInv_eq hψ h₂
781 have hs₁₂ : ψ s₁₂ = h₁ * h₂ := by
782 simpa [s₁₂] using Function.surjInv_eq hψ (h₁ * h₂)
783 let n : ψ.ker := ⟨s₁ * s₂ * s₁₂⁻¹, by
784 change ψ (s₁ * s₂ * s₁₂⁻¹) = 1
785 rw [map_mul, map_mul, hs₁, hs₂, map_inv, hs₁₂]
786 simp only [mul_inv_rev, mul_assoc, mul_inv_cancel_left, mul_inv_cancel]⟩
787 have hs :
788 ((groupAugmentationIdealRep (G := G)).ρ s₁)
789 (((groupAugmentationIdealRep (G := G)).ρ s₂) x) =
790 ((groupAugmentationIdealRep (G := G)).ρ (s₁ * s₂)) x := by
791 exact congrArg
792 (fun f : augmentationIdeal G →ₗ[ℤ] augmentationIdeal G => f x)
793 (((groupAugmentationIdealRep (G := G)).ρ).map_mul s₁ s₂).symm
794 rw [LinearMap.comp_apply, LinearMap.comp_apply]
795 change
796 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
797 (((groupAugmentationIdealRep (G := G)).ρ s₁₂) x) =
798 kernelAugmentationIdealCoinvariantsEndOfSurjective (ψ := ψ) hψ h₁
799 (kernelAugmentationIdealCoinvariantsEndOfSurjective (ψ := ψ) hψ h₂
800 (Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ) x))
801 rw [kernelAugmentationIdealCoinvariantsEndOfSurjective_mk (ψ := ψ) hψ,
802 kernelAugmentationIdealCoinvariantsEndOfSurjective_mk (ψ := ψ) hψ]
803 calc
804 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
805 (((groupAugmentationIdealRep (G := G)).ρ s₁₂) x)
806 =
807 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
808 (((kernelAugmentationIdealRep (ψ := ψ)).ρ n)
809 (((groupAugmentationIdealRep (G := G)).ρ s₁₂) x)) := by
810 rw [Representation.Coinvariants.mk_self_apply]
811 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
812 (((groupAugmentationIdealRep (G := G)).ρ n.1)
813 (((groupAugmentationIdealRep (G := G)).ρ s₁₂) x)) := by
814 rw [kernelAugmentationIdealRep_rho_eq_groupAugmentationIdealRep_rho
815 (ψ := ψ) n]
816 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
817 (((groupAugmentationIdealRep (G := G)).ρ (n.1 * s₁₂)) x) := by
818 have hs' :
819 ((groupAugmentationIdealRep (G := G)).ρ n.1)
820 (((groupAugmentationIdealRep (G := G)).ρ s₁₂) x) =
821 ((groupAugmentationIdealRep (G := G)).ρ (n.1 * s₁₂)) x := by
822 exact congrArg
823 (fun f : augmentationIdeal G →ₗ[ℤ] augmentationIdeal G => f x)
824 (((groupAugmentationIdealRep (G := G)).ρ).map_mul n.1 s₁₂).symm
825 rw [hs']
826 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
827 (((groupAugmentationIdealRep (G := G)).ρ (s₁ * s₂)) x) := by
828 congr 1
829 simp only [mul_assoc, inv_mul_cancel, mul_one, MonoidHom.coe_mk, OneHom.coe_mk,
830 map_mul,
831 Module.End.mul_apply, LinearMap.coe_mk, AddHom.coe_mk, s₁, s₂, s₁₂, n]
832 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
833 (((groupAugmentationIdealRep (G := G)).ρ s₁)
834 (((groupAugmentationIdealRep (G := G)).ρ s₂) x)) := by
835 rw [hs]
837/--
838The ring action of \(\mathbb{Z}[H]\) on \(H_0(\ker \psi, I(\mathbb{Z}[G]))\) induced by a
839surjective section.
840-/
841def kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective
842 (hψ : Function.Surjective ψ) :
843 GroupRing H →+* Module.End ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
844 MonoidAlgebra.liftNCRingHom
845 (Int.castRingHom (Module.End ℤ (KernelAugmentationIdealCoinvariants (ψ := ψ))))
846 (kernelAugmentationIdealCoinvariantsModuleEndOfSurjective (ψ := ψ) hψ)
847 (by
848 intro z h
849 apply LinearMap.ext
850 intro x
851 change z •
852 kernelAugmentationIdealCoinvariantsModuleEndOfSurjective (ψ := ψ) hψ h x =
853 kernelAugmentationIdealCoinvariantsModuleEndOfSurjective (ψ := ψ) hψ h (z • x)
854 rw [map_zsmul])
856omit [DecidableEq H] [DecidableEq G] in
857/--
858The surjective-case coefficient action on coinvariants has the displayed value on
859representatives.
860-/
861@[simp]
862theorem kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective_of
863 (hψ : Function.Surjective ψ) (h : H) :
864 kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective (ψ := ψ) hψ
865 (MonoidAlgebra.of ℤ H h) =
866 kernelAugmentationIdealCoinvariantsModuleEndOfSurjective (ψ := ψ) hψ h := by
867 ext x
868 simp only [kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective, MonoidAlgebra.of_apply,
869 MonoidAlgebra.liftNCRingHom_single, eq_intCast, Int.cast_one, one_mul, LinearMap.coe_comp,
870 Function.comp_apply]
872/-- The induced \(\mathbb{Z}[H]\)-module structure on \(H_0(\ker \psi, I(\mathbb{Z}[G]))\). -/
873@[reducible] def kernelAugmentationIdealCoinvariantsModuleOfSurjective
874 (hψ : Function.Surjective ψ) :
875 Module (GroupRing H) (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
876 Module.compHom _
877 (kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective (ψ := ψ) hψ)
879omit [DecidableEq G] in
880/--
881The augmentation-generator identity \((g_1g_2-1)=(g_1-1)+g_1(g_2-1)\) inside
882\(I(\mathbb{Z}[G])\).
883-/
884@[simp]
885theorem augmentationGeneratorSubtype_mul (g₁ g₂ : G) :
886 augmentationGeneratorSubtype (H := G) (g₁ * g₂) =
887 augmentationGeneratorSubtype (H := G) g₁ +
888 ((groupAugmentationIdealRep (G := G)).ρ g₁)
889 (augmentationGeneratorSubtype (H := G) g₂) := by
890 let ρg : GroupRing G →ₗ[ℤ] GroupRing G := (groupRingRep (G := G)).ρ g₁
891 apply Subtype.ext
892 change (augmentationGenerator G (g₁ * g₂) : GroupRing G) =
893 (augmentationGenerator G g₁ : GroupRing G) +
894 ρg (augmentationGenerator G g₂)
895 have hρ :
896 ρg (augmentationGenerator G g₂) =
897 (MonoidAlgebra.of ℤ G (g₁ * g₂) : GroupRing G) - MonoidAlgebra.of ℤ G g₁ := by
898 change ((groupRingRep (G := G)).ρ g₁)
899 (MonoidAlgebra.single g₂ 1 - MonoidAlgebra.single (1 : G) 1) =
900 (MonoidAlgebra.of ℤ G (g₁ * g₂) : GroupRing G) - MonoidAlgebra.of ℤ G g₁
901 rw [map_sub, groupRingRep_apply_single, groupRingRep_apply_single]
902 simp only [mul_one, MonoidAlgebra.of_apply]
903 rw [augmentationGenerator, augmentationGenerator, hρ]
904 abel_nf
906/-- Kernel elements map to \(H_0(\ker \psi, I(\mathbb{Z}[G]))\) by \(n \mapsto [n - 1]\). -/
907def kernelCoinvariantsBoundary (ψ : G →* H) :
908 ψ.ker →* Multiplicative (KernelAugmentationIdealCoinvariants (ψ := ψ)) where
909 toFun n := Multiplicative.ofAdd <|
910 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
911 (augmentationGeneratorSubtype (H := G) n.1)
912 map_one' := by
913 apply Multiplicative.toAdd.injective
914 have hzero : augmentationGeneratorSubtype (H := G) (1 : G) = 0 := by
915 apply Subtype.ext
916 simp only [augmentationGeneratorSubtype, augmentationGenerator, groupRing_of_one (H := G),
917 sub_self,
918 ZeroMemClass.coe_zero]
919 simp only [OneMemClass.coe_one, hzero, map_zero, ofAdd_zero, toAdd_one]
920 map_mul' n₁ n₂ := by
921 apply Multiplicative.toAdd.injective
922 change
923 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
924 (augmentationGeneratorSubtype (H := G) (n₁.1 * n₂.1)) =
925 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
926 (augmentationGeneratorSubtype (H := G) n₁.1) +
927 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
928 (augmentationGeneratorSubtype (H := G) n₂.1)
929 rw [augmentationGeneratorSubtype_mul, map_add]
930 congr 1
931 calc
932 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
933 (((groupAugmentationIdealRep (G := G)).ρ n₁.1)
934 (augmentationGeneratorSubtype (H := G) n₂.1))
935 = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
936 (((kernelAugmentationIdealRep (ψ := ψ)).ρ n₁)
937 (augmentationGeneratorSubtype (H := G) n₂.1)) := by
938 rw [kernelAugmentationIdealRep_rho_eq_groupAugmentationIdealRep_rho (ψ := ψ) n₁]
939 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
940 (augmentationGeneratorSubtype (H := G) n₂.1) := by
941 exact Representation.Coinvariants.mk_self_apply
942 ((kernelAugmentationIdealRep (ψ := ψ)).ρ) n₁
943 (augmentationGeneratorSubtype (H := G) n₂.1)
945/-- The map \(n \mapsto [n-1]\) factors through the abelianization of \(\ker \psi\). -/
946def kernelAbelianizationToCoinvariants (ψ : G →* H) :
947 Abelianization ψ.ker →* Multiplicative (KernelAugmentationIdealCoinvariants (ψ := ψ)) :=
948 Abelianization.lift (kernelCoinvariantsBoundary (ψ := ψ))
950/-- Additive form of the map \((\ker \psi)^{\mathrm{ab}} \to H_0(\ker \psi, I(\mathbb{Z}[G]))\). -/
951def kernelAbelianizationToCoinvariantsAdd (ψ : G →* H) :
952 KernelAbelianizationAdd ψ →+ KernelAugmentationIdealCoinvariants (ψ := ψ) where
953 toFun x := Multiplicative.toAdd (kernelAbelianizationToCoinvariants (ψ := ψ) (Additive.toMul x))
954 map_zero' := by
955 simp only [toMul_zero, map_one, toAdd_one]
956 map_add' x y := by
957 simp only [toMul_add, map_mul, toAdd_mul]
959omit [DecidableEq H] [DecidableEq G] in
960/--
961The additive kernel-abelianization map sends a kernel element to its augmentation-coinvariant
962class.
963-/
964@[simp]
965theorem kernelAbelianizationToCoinvariantsAdd_of (n : ψ.ker) :
966 kernelAbelianizationToCoinvariantsAdd (ψ := ψ)
967 (Additive.ofMul (Abelianization.of n)) =
968 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
969 (augmentationGeneratorSubtype (H := G) n.1) := by
970 simp only [kernelAbelianizationToCoinvariantsAdd, kernelAbelianizationToCoinvariants,
971 kernelCoinvariantsBoundary, AddMonoidHom.coe_mk, ZeroHom.coe_mk, toMul_ofMul,
972 Abelianization.lift_apply_of,
973 MonoidHom.coe_mk, OneHom.coe_mk, toAdd_ofAdd]
975/--
976\(\mathbb{Z}\)-linear form of the map \((\ker \psi)^{\mathrm{ab}} \to H_0(\ker \psi,
977I(\mathbb{Z}[G]))\).
978-/
979def kernelAbelianizationToCoinvariantsLinear (ψ : G →* H) :
980 KernelAbelianizationAdd ψ →ₗ[ℤ] KernelAugmentationIdealCoinvariants (ψ := ψ) :=
981 (kernelAbelianizationToCoinvariantsAdd (ψ := ψ)).toIntLinearMap
983/--
984The low-degree homology comparison \((\ker \psi)^{\mathrm{ab}} \to H_0(\ker \psi,
985I(\mathbb{Z}[G]))\) obtained from the connecting morphism \(H_1(\ker \psi, \mathbb{Z}) \to
986H_0(\ker \psi, I(\mathbb{Z}[G]))\). Our convention for \(\delta_0\) introduces a minus sign on
987generators.
988-/
989def kernelAbelianizationToCoinvariantsViaConnectingAdd (ψ : G →* H) :
990 KernelAbelianizationAdd ψ →+ KernelAugmentationIdealCoinvariants (ψ := ψ) where
991 toFun x :=
992 -((groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
993 ((kernelAugmentationConnecting (ψ := ψ)).hom
994 ((kernelTrivialH1AddEquivAbelianization (ψ := ψ)).symm x)))
995 map_zero' := by
996 simp only [coinvariantsFunctor_obj_carrier, map_zero, neg_zero]
997 map_add' x y := by
998 rw [(kernelTrivialH1AddEquivAbelianization (ψ := ψ)).symm.map_add]
999 simp only [coinvariantsFunctor_obj_carrier, map_add, neg_add_rev]
1000 abel_nf
1002/--
1003\(\mathbb{Z}\)-linear form of the connecting-morphism comparison \((\ker \psi)^{\mathrm{ab}} \to
1004H_0(\ker \psi, I(\mathbb{Z}[G]))\).
1006def kernelAbelianizationToCoinvariantsViaConnectingLinear (ψ : G →* H) :
1007 KernelAbelianizationAdd ψ →ₗ[ℤ] KernelAugmentationIdealCoinvariants (ψ := ψ) :=
1008 (kernelAbelianizationToCoinvariantsViaConnectingAdd (ψ := ψ)).toIntLinearMap
1010omit [DecidableEq H] [DecidableEq G] in
1011/--
1012The connecting-morphism comparison sends a kernel element to the corresponding
1013augmentation-coinvariant class.
1015@[simp]
1016theorem kernelAbelianizationToCoinvariantsViaConnectingAdd_of (n : ψ.ker) :
1017 kernelAbelianizationToCoinvariantsViaConnectingAdd (ψ := ψ)
1018 (Additive.ofMul (Abelianization.of n)) =
1019 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1020 (augmentationGeneratorSubtype (H := G) n.1) := by
1021 change
1022 -((groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
1023 ((kernelAugmentationConnecting (ψ := ψ)).hom
1024 ((kernelTrivialH1AddEquivAbelianization (ψ := ψ)).symm
1025 (Additive.ofMul (Abelianization.of n))))) =
1026 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1027 (augmentationGeneratorSubtype (H := G) n.1)
1028 rw [kernelAugmentationConnecting_H0Iso_of]
1029 simp only [coinvariantsFunctor_obj_carrier, neg_neg]
1031omit [DecidableEq H] [DecidableEq G] in
1032/-- The linear connecting-morphism comparison has the stated value on a kernel element. -/
1033@[simp]
1034theorem kernelAbelianizationToCoinvariantsViaConnectingLinear_of (n : ψ.ker) :
1035 kernelAbelianizationToCoinvariantsViaConnectingLinear (ψ := ψ)
1036 (Additive.ofMul (Abelianization.of n)) =
1037 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1038 (augmentationGeneratorSubtype (H := G) n.1) := by
1039 change kernelAbelianizationToCoinvariantsViaConnectingAdd (ψ := ψ)
1040 (Additive.ofMul (Abelianization.of n)) = _
1041 exact kernelAbelianizationToCoinvariantsViaConnectingAdd_of (ψ := ψ) n
1043omit [DecidableEq H] [DecidableEq G] in
1044/--
1045The linear abelianization-to-coinvariants map agrees with the map obtained from the connecting
1046morphism.
1048theorem kernelAbelianizationToCoinvariantsLinear_eq_viaConnecting
1049 (ψ : G →* H) :
1050 kernelAbelianizationToCoinvariantsLinear (ψ := ψ) =
1051 kernelAbelianizationToCoinvariantsViaConnectingLinear (ψ := ψ) := by
1052 apply LinearMap.ext
1053 intro x
1054 change
1055 (fun y : Abelianization ψ.ker =>
1056 kernelAbelianizationToCoinvariantsLinear (ψ := ψ) (Additive.ofMul y) =
1057 kernelAbelianizationToCoinvariantsViaConnectingLinear (ψ := ψ) (Additive.ofMul y))
1058 (Additive.toMul x)
1059 refine QuotientGroup.induction_on (Additive.toMul x) ?_
1060 intro n
1061 calc
1062 kernelAbelianizationToCoinvariantsLinear (ψ := ψ) (Additive.ofMul (Abelianization.of n))
1063 = kernelAbelianizationToCoinvariantsAdd (ψ := ψ)
1064 (Additive.ofMul (Abelianization.of n)) := by
1065 rfl
1066 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1067 (augmentationGeneratorSubtype (H := G) n.1) := by
1068 rw [kernelAbelianizationToCoinvariantsAdd_of]
1069 _ = kernelAbelianizationToCoinvariantsViaConnectingLinear (ψ := ψ)
1070 (Additive.ofMul (Abelianization.of n)) := by
1071 rw [kernelAbelianizationToCoinvariantsViaConnectingLinear_of]
1073omit [DecidableEq H] [DecidableEq G] in
1074/-- The abelianization-to-coinvariants map is injective. -/
1075theorem kernelAbelianizationToCoinvariantsLinear_injective
1076 (hψ : Function.Surjective ψ) :
1077 Function.Injective (kernelAbelianizationToCoinvariantsLinear (ψ := ψ)) := by
1078 have hEq := kernelAbelianizationToCoinvariantsLinear_eq_viaConnecting (ψ := ψ)
1079 intro x y hxy
1080 have hxy' :
1081 kernelAbelianizationToCoinvariantsViaConnectingLinear (ψ := ψ) x =
1082 kernelAbelianizationToCoinvariantsViaConnectingLinear (ψ := ψ) y := by
1083 simpa [hEq] using hxy
1084 have hxy'' :
1085 kernelAbelianizationToCoinvariantsViaConnectingAdd (ψ := ψ) x =
1086 kernelAbelianizationToCoinvariantsViaConnectingAdd (ψ := ψ) y := by
1087 change
1088 (kernelAbelianizationToCoinvariantsViaConnectingAdd (ψ := ψ)).toIntLinearMap x =
1089 (kernelAbelianizationToCoinvariantsViaConnectingAdd (ψ := ψ)).toIntLinearMap y
1090 exact hxy'
1091 have hxy''' : ((groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
1092 ((kernelAugmentationConnecting (ψ := ψ)).hom
1093 ((kernelTrivialH1AddEquivAbelianization (ψ := ψ)).symm x))) =
1094 ((groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom
1095 ((kernelAugmentationConnecting (ψ := ψ)).hom
1096 ((kernelTrivialH1AddEquivAbelianization (ψ := ψ)).symm y))) := by
1097 simpa [kernelAbelianizationToCoinvariantsViaConnectingAdd] using congrArg Neg.neg hxy''
1098 have hH0Iso :
1099 Function.Injective
1100 ((groupHomology.H0Iso (kernelAugmentationIdealRep (ψ := ψ))).hom.hom) := by
1101 exact (ModuleCat.mono_iff_injective _).1 inferInstance
1102 apply (kernelTrivialH1AddEquivAbelianization (ψ := ψ)).symm.injective
1103 apply kernelAugmentationConnecting_injective (H := H) (ψ := ψ) hψ
1104 exact hH0Iso hxy'''
1106omit [DecidableEq H] [DecidableEq G] in
1107/-- The induced \(H\)-action on kernel augmentation coinvariants is computed on representatives. -/
1108@[simp]
1109theorem kernelAugmentationIdealCoinvariants_smul_mk_ofSurjective
1110 (hψ : Function.Surjective ψ) (h : H) (x : augmentationIdeal G) :
1111 letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
1112 (MonoidAlgebra.of ℤ H h : GroupRing H) •
1113 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ) x =
1114 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1115 (((groupAugmentationIdealRep (G := G)).ρ (Function.surjInv hψ h)) x) := by
1116 letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
1117 rw [show (MonoidAlgebra.of ℤ H h : GroupRing H) •
1118 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ) x =
1119 kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective (ψ := ψ) hψ
1120 (MonoidAlgebra.of ℤ H h)
1121 (Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ) x) by
1122 rfl]
1123 rw [kernelAugmentationIdealCoinvariantsActionRingHomOfSurjective_of (ψ := ψ) hψ]
1124 simpa [kernelAugmentationIdealCoinvariantsModuleEndOfSurjective] using
1125 (kernelAugmentationIdealCoinvariantsEndOfSurjective_mk (ψ := ψ) hψ h x)
1127omit [DecidableEq H] [DecidableEq G] in
1128/--
1129The coinvariant representative in the augmentation-ideal kernel is compatible with the group
1130action whenever the underlying representatives are equal.
1132theorem kernelAugmentationIdealCoinvariants_mk_group_action_eq_of_eq
1133 {g₁ g₂ : G} (h : ψ g₁ = ψ g₂) (x : augmentationIdeal G) :
1134 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1135 (((groupAugmentationIdealRep (G := G)).ρ g₁) x) =
1136 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1137 (((groupAugmentationIdealRep (G := G)).ρ g₂) x) := by
1138 let n : ψ.ker := ⟨g₁ * g₂⁻¹, by
1139 simp only [MonoidHom.mem_ker, map_mul, h, map_inv, mul_inv_cancel]⟩
1140 calc
1141 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1142 (((groupAugmentationIdealRep (G := G)).ρ g₁) x)
1143 = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1144 (((groupAugmentationIdealRep (G := G)).ρ (n.1 * g₂)) x) := by
1145 congr 1
1146 simp only [MonoidHom.coe_mk, OneHom.coe_mk, LinearMap.coe_mk, AddHom.coe_mk,
1147 mul_assoc, inv_mul_cancel,
1148 mul_one, n]
1149 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1150 (((groupAugmentationIdealRep (G := G)).ρ n.1)
1151 (((groupAugmentationIdealRep (G := G)).ρ g₂) x)) := by
1152 congr 1
1153 exact congrArg
1154 (fun f : augmentationIdeal G →ₗ[ℤ] augmentationIdeal G => f x)
1155 (((groupAugmentationIdealRep (G := G)).ρ).map_mul n.1 g₂)
1156 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1157 (((kernelAugmentationIdealRep (ψ := ψ)).ρ n)
1158 (((groupAugmentationIdealRep (G := G)).ρ g₂) x)) := by
1159 rw [kernelAugmentationIdealRep_rho_eq_groupAugmentationIdealRep_rho (ψ := ψ) n]
1160 _ = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1161 (((groupAugmentationIdealRep (G := G)).ρ g₂) x) := by
1162 exact Representation.Coinvariants.mk_self_apply
1163 ((kernelAugmentationIdealRep (ψ := ψ)).ρ) n
1164 (((groupAugmentationIdealRep (G := G)).ρ g₂) x)
1166/--
1167The canonical differential generator \(g \mapsto [g - 1]\) in \(H_0(\ker \psi,
1168I(\mathbb{Z}[G]))\).
1170def kernelAugmentationIdealCoinvariantsGeneratorOfSurjective
1171 (g : G) :
1172 KernelAugmentationIdealCoinvariants (ψ := ψ) :=
1173 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1174 (augmentationGeneratorSubtype (H := G) g)
1176omit [DecidableEq H] [DecidableEq G] in
1177private theorem kernelAugmentationIdealCoinvariantsGeneratorOfSurjective_map_mul
1178 (hψ : Function.Surjective ψ) (g₁ g₂ : G) :
1179 letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
1180 kernelAugmentationIdealCoinvariantsGeneratorOfSurjective (ψ := ψ) (g₁ * g₂) =
1181 kernelAugmentationIdealCoinvariantsGeneratorOfSurjective (ψ := ψ) g₁ +
1182 groupRingScalar ψ g₁ •
1183 kernelAugmentationIdealCoinvariantsGeneratorOfSurjective (ψ := ψ) g₂ := by
1184 letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
1185 rw [kernelAugmentationIdealCoinvariantsGeneratorOfSurjective,
1186 augmentationGeneratorSubtype_mul]
1187 rw [map_add]
1188 congr 1
1189 calc
1190 Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1191 (((groupAugmentationIdealRep (G := G)).ρ g₁)
1192 (augmentationGeneratorSubtype (H := G) g₂))
1193 = Representation.Coinvariants.mk ((kernelAugmentationIdealRep (ψ := ψ)).ρ)
1194 (((groupAugmentationIdealRep (G := G)).ρ
1195 (Function.surjInv hψ (ψ g₁)))
1196 (augmentationGeneratorSubtype (H := G) g₂)) := by
1197 apply kernelAugmentationIdealCoinvariants_mk_group_action_eq_of_eq (ψ := ψ)
1198 simpa using (Function.surjInv_eq hψ (ψ g₁)).symm
1199 _ = (MonoidAlgebra.of ℤ H (ψ g₁) : GroupRing H) •
1200 kernelAugmentationIdealCoinvariantsGeneratorOfSurjective (ψ := ψ) g₂ := by
1201 symm
1202 exact kernelAugmentationIdealCoinvariants_smul_mk_ofSurjective
1203 (ψ := ψ) hψ (ψ g₁) (augmentationGeneratorSubtype (H := G) g₂)
1205/-- The canonical coinvariant generator is a crossed differential in the surjective case. -/
1206def kernelAugmentationIdealCoinvariantsGeneratorHomOfSurjective
1207 (hψ : Function.Surjective ψ) :
1208 letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
1209 DifferentialHom ψ (KernelAugmentationIdealCoinvariants (ψ := ψ)) := by
1210 letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
1211 exact
1212 { toFun := kernelAugmentationIdealCoinvariantsGeneratorOfSurjective (ψ := ψ)
1213 map_mul' := by
1214 intro g₁ g₂
1215 simpa only [scalarCrossedAction_apply] using
1216 kernelAugmentationIdealCoinvariantsGeneratorOfSurjective_map_mul
1217 (ψ := ψ) hψ g₁ g₂ }
1219/--
1220The canonical linear map \(A_{\psi}\to H_0(\ker \psi, I(\mathbb{Z}[G]))\) sending \(d(g)\) to
1221\([g-1]\).
1223def differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective
1224 (hψ : Function.Surjective ψ) :
1225 letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
1226 DifferentialModule ψ →ₗ[GroupRing H] KernelAugmentationIdealCoinvariants (ψ := ψ) := by
1227 letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
1228 exact
1229 differentialModuleLift ψ
1230 (kernelAugmentationIdealCoinvariantsGeneratorHomOfSurjective (ψ := ψ) hψ)
1232omit [DecidableEq H] [DecidableEq G] in
1233/--
1234The surjective-case differential-to-coinvariants map sends each universal differential generator
1235to the corresponding coinvariant class.
1237@[simp]
1238theorem differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_d
1239 (hψ : Function.Surjective ψ) (g : G) :
1240 letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
1241 differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective
1242 (ψ := ψ) hψ (universalDifferential ψ g) =
1243 kernelAugmentationIdealCoinvariantsGeneratorOfSurjective (ψ := ψ) g := by
1244 letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
1245 change
1246 differentialModuleLift ψ
1247 (kernelAugmentationIdealCoinvariantsGeneratorHomOfSurjective (ψ := ψ) hψ)
1248 (universalDifferential ψ g) =
1249 kernelAugmentationIdealCoinvariantsGeneratorOfSurjective (ψ := ψ) g
1250 exact
1251 differentialModuleLift_d
1252 (A := KernelAugmentationIdealCoinvariants (ψ := ψ))
1253 ψ
1254 (kernelAugmentationIdealCoinvariantsGeneratorHomOfSurjective (ψ := ψ) hψ)
1257omit [DecidableEq H] [DecidableEq G] in
1258/-- The surjective-case differential-to-coinvariants map is compatible with the boundary map. -/
1259@[simp 900]
1260theorem differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_boundary
1261 (hψ : Function.Surjective ψ) (x : KernelAbelianizationAdd ψ) :
1262 letI := kernelAbelianizationModuleOfSurjective ψ hψ
1263 letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
1264 differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective (ψ := ψ) hψ
1265 (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x) =
1266 kernelAbelianizationToCoinvariantsLinear (ψ := ψ) x := by
1267 letI := kernelAbelianizationModuleOfSurjective ψ hψ
1268 letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
1269 change
1270 (fun y : Abelianization ψ.ker =>
1271 differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective (ψ := ψ) hψ
1272 (kernelAbelianizationBoundaryAdd ψ (Additive.ofMul y)) =
1273 kernelAbelianizationToCoinvariantsAdd (ψ := ψ) (Additive.ofMul y))
1274 (Additive.toMul x)
1275 refine QuotientGroup.induction_on (Additive.toMul x) ?_
1276 intro n
1277 calc
1278 differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective (ψ := ψ) hψ
1279 ((kernelAbelianizationBoundaryAdd ψ) (Additive.ofMul (Abelianization.of n))) =
1280 differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective (ψ := ψ) hψ
1281 (universalDifferential ψ n.1) := by
1282 exact congrArg
1283 (differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective
1284 (ψ := ψ) hψ)
1285 (kernelAbelianizationBoundaryAdd_of (ψ := ψ) n)
1286 _ = kernelAugmentationIdealCoinvariantsGeneratorOfSurjective (ψ := ψ) n.1 := by
1287 exact differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_d
1288 (ψ := ψ) hψ n.1
1289 _ = kernelAbelianizationToCoinvariantsAdd (ψ := ψ) (Additive.ofMul (Abelianization.of n)) := by
1290 symm
1291 simp only [kernelAbelianizationToCoinvariantsAdd_of,
1292 kernelAugmentationIdealCoinvariantsGeneratorOfSurjective]
1294end CoinvariantsAction
1296end KernelAugmentation
1298end
1300end FoxDifferential