Source: ProCGroups.FoxDifferential.Discrete.KernelBoundary.Basic
1import ProCGroups.FoxDifferential.Discrete.KernelBoundary.IdentityAugmentation
3/-!
4# Fox differential: discrete — kernel boundary — basic
6The principal declarations in this module are:
8- `KernelAbelianizationAdd`
9 Additive form of the kernel abelianization map.
10- `kernelBoundary`
11 The kernel of \(\psi\) maps multiplicatively into the additive differential module via d.
12- `augmentation_toGroupRing_eq_zero`
13 The Crowell boundary map lands in the kernel of the augmentation map.
14- `augmentation_surjective`
15 The augmentation map \(\mathbb{Z}[H] \to \mathbb{Z}\) is surjective.
16-/
18namespace FoxDifferential
20noncomputable section
23variable {H G : Type*} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
25/-- Additive form of the kernel abelianization map. -/
26abbrev KernelAbelianizationAdd (ψ : G →* H) : Type _ :=
27 Additive (Abelianization ψ.ker)
29omit [DecidableEq H] [DecidableEq G] in
30/-- The Crowell boundary map lands in the kernel of the augmentation map. -/
31theorem augmentation_toGroupRing_eq_zero (ψ : G →* H) (x : DifferentialModule ψ) :
32 augmentation H (toGroupRing ψ x) = 0 := by
33 exact (mem_augmentationIdeal_iff (H := H) (x := toGroupRing ψ x)).1
34 (toGroupRing_mem_augmentationIdeal (H := H) ψ x)
36omit [DecidableEq H] in
37/-- The augmentation map \(\mathbb{Z}[H] \to \mathbb{Z}\) is surjective. -/
38theorem augmentation_surjective : Function.Surjective (augmentation H) := by
39 intro n
40 refine ⟨(n : GroupRing H), ?_⟩
41 simp only [augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe, map_intCast, Int.cast_eq]
43omit [DecidableEq H] [DecidableEq G] in
44/--
45Tail exactness of the discrete Crowell sequence: \(A_{\psi}\) \(\to\) \(\mathbb{Z}[H]\) \(\to\)
46\(\mathbb{Z}\) is used when \(\psi\) is surjective.
47-/
48theorem exact_toGroupRing_augmentation (ψ : G →* H) (hψ : Function.Surjective ψ) :
49 Function.Exact (fun x => toGroupRing ψ x) (augmentation H) := by
50 intro y
51 constructor
52 · intro hy
53 have hy_mem : y ∈ augmentationIdeal H := (mem_augmentationIdeal_iff (H := H) (x := y)).2 hy
54 let y' : augmentationIdeal H := ⟨y, hy_mem⟩
55 rcases toAugmentationIdeal_surjective (H := H) ψ hψ y' with ⟨x, hx⟩
56 refine ⟨x, ?_⟩
57 exact congrArg Subtype.val hx
58 · rintro ⟨x, rfl⟩
59 exact augmentation_toGroupRing_eq_zero (H := H) ψ x
61/-- The kernel of \(\psi\) maps multiplicatively into the additive differential module via d. -/
62def kernelBoundary (ψ : G →* H) : ψ.ker →* Multiplicative (DifferentialModule ψ) where
63 toFun g := Multiplicative.ofAdd (universalDifferential ψ g.1)
64 map_one' := by
65 apply congrArg Multiplicative.ofAdd
66 simp only [OneMemClass.coe_one, universalDifferential_one]
67 map_mul' g₁ g₂ := by
68 apply congrArg Multiplicative.ofAdd
69 have h := universalDifferential_mul ψ g₁.1 g₂.1
70 have hψ : (MonoidAlgebra.of ℤ H (ψ g₁.1) : GroupRing H) = 1 := by
71 rw [g₁.2, groupRing_of_one (H := H)]
72 rw [hψ, one_smul] at h
73 simpa using h
75/-- The kernel boundary factors through the abelianization of \(\ker \psi\). -/
76def kernelAbelianizationBoundary (ψ : G →* H) :
77 Abelianization ψ.ker →* Multiplicative (DifferentialModule ψ) :=
78 Abelianization.lift (kernelBoundary ψ)
80/-- The additive kernel-boundary map sends a kernel element to its abelianization boundary class. -/
81def kernelAbelianizationBoundaryAdd (ψ : G →* H) :
82 Additive (Abelianization ψ.ker) →+ DifferentialModule ψ where
83 toFun x := Multiplicative.toAdd (kernelAbelianizationBoundary ψ (Additive.toMul x))
84 map_zero' := by
85 simp only [toMul_zero, map_one, toAdd_one]
86 map_add' x y := by
87 simp only [toMul_add, map_mul, toAdd_mul]
89omit [DecidableEq H] [DecidableEq G] in
90/-- The additive kernel-boundary map has the stated value on a kernel element. -/
91@[simp 900]
92theorem kernelAbelianizationBoundaryAdd_of (ψ : G →* H) (g : ψ.ker) :
93 kernelAbelianizationBoundaryAdd ψ (Additive.ofMul (Abelianization.of g)) =
94 universalDifferential ψ g.1 := by
95 change Multiplicative.toAdd (Multiplicative.ofAdd (universalDifferential ψ g.1)) =
96 universalDifferential ψ g.1
97 rfl
99/-- Conjugation by G on \(\ker \psi\), transported to the abelianization of \(\ker \psi\). -/
100def kernelAbelianizationConj (ψ : G →* H) :
101 G →* MulAut (Abelianization ψ.ker) where
102 toFun g := (MulAut.conjNormal (H := ψ.ker) g).abelianizationCongr
103 map_one' := by
104 ext x
105 refine QuotientGroup.induction_on x ?_
106 intro n
107 have hconj : MulAut.conjNormal (H := ψ.ker) (1 : G) = 1 := by
108 ext m
109 simp only [map_one, MulAut.one_apply]
110 rw [hconj]
111 rfl
112 map_mul' g₁ g₂ := by
113 ext x
114 refine QuotientGroup.induction_on x ?_
115 intro n
116 let e₁ : MulAut ψ.ker := MulAut.conjNormal (H := ψ.ker) g₁
117 let e₂ : MulAut ψ.ker := MulAut.conjNormal (H := ψ.ker) g₂
118 have hconj : MulAut.conjNormal (H := ψ.ker) (g₁ * g₂) = e₁ * e₂ := by
119 ext m
120 simp only [map_mul, MulAut.mul_apply, MulAut.conjNormal_apply, mul_assoc, e₁, e₂]
121 rw [hconj]
122 calc
123 (e₁ * e₂).abelianizationCongr (Abelianization.of n)
124 = Abelianization.of ((e₁ * e₂) n) := by
125 exact abelianizationCongr_of (e := e₁ * e₂) n
126 _ = e₁.abelianizationCongr (Abelianization.of (e₂ n)) := by
127 exact (abelianizationCongr_of (e := e₁) (e₂ n)).symm
128 _ = e₁.abelianizationCongr (e₂.abelianizationCongr (Abelianization.of n)) := by
129 rw [abelianizationCongr_of (e := e₂) n]
130 _ = (e₁.abelianizationCongr * e₂.abelianizationCongr) (Abelianization.of n) := by
131 rfl
133omit [DecidableEq H] [DecidableEq G] in
134/--
135The conjugation action on kernel abelianization is computed by the displayed representative
136formula.
137-/
138@[simp]
139theorem kernelAbelianizationConj_of (ψ : G →* H) (g : G) (n : ψ.ker) :
140 kernelAbelianizationConj ψ g (Abelianization.of n) =
141 Abelianization.of (MulAut.conjNormal (H := ψ.ker) g n) := by
142 rfl
144omit [DecidableEq H] [DecidableEq G] in
145/-- Conjugation by a kernel element becomes trivial in the kernel abelianization. -/
146@[simp]
147theorem kernelAbelianizationConj_eq_one_of_mem_ker (ψ : G →* H) (n : ψ.ker) :
148 kernelAbelianizationConj ψ n = 1 := by
149 ext x
150 refine QuotientGroup.induction_on x ?_
151 intro k
152 calc
153 kernelAbelianizationConj ψ n (Abelianization.of k)
154 = Abelianization.of ((MulAut.conjNormal (H := ψ.ker) (n : G)) k) := by
155 exact abelianizationCongr_of (e := MulAut.conjNormal (H := ψ.ker) (n : G)) k
156 _ = Abelianization.of (n * k * n⁻¹) := by
157 congr 1
158 _ = Abelianization.of k := by
159 simp only [mul_assoc, map_mul, map_inv, mul_inv_cancel_comm_assoc]
161omit [DecidableEq H] [DecidableEq G] in
162/--
163Elements in the kernel of \(\psi\) act trivially after passing to the kernel abelianization
164action.
165-/
166theorem ker_le_kernelAbelianizationConj_ker (ψ : G →* H) :
167 ψ.ker ≤ (kernelAbelianizationConj ψ).ker := by
168 intro n hn
169 change kernelAbelianizationConj ψ n = 1
170 simpa using kernelAbelianizationConj_eq_one_of_mem_ker (ψ := ψ) ⟨n, hn⟩
172/--
173The conjugation action on the abelianization of \(\ker \psi\) factors through \(G/\ker \psi\).
174-/
175def quotientKernelAbelianizationConj (ψ : G →* H) :
176 G ⧸ ψ.ker →* MulAut (Abelianization ψ.ker) :=
177 QuotientGroup.lift ψ.ker (kernelAbelianizationConj ψ) (ker_le_kernelAbelianizationConj_ker ψ)
179omit [DecidableEq H] [DecidableEq G] in
180/--
181If \(\psi\) is surjective, the conjugation action on the abelianization of \(\ker \psi\) is
182expressed directly as an action of H.
183-/
184def kernelAbelianizationConjOfSurjective
185 (ψ : G →* H) (hψ : Function.Surjective ψ) :
186 H →* MulAut (Abelianization ψ.ker) :=
187 (quotientKernelAbelianizationConj ψ).comp
188 (QuotientGroup.quotientKerEquivOfSurjective (φ := ψ) hψ).symm.toMonoidHom
190omit [DecidableEq H] [DecidableEq G] in
191/--
192For a surjective \(\psi\), the induced action on the kernel abelianization agrees with
193conjugation by a chosen preimage.
194-/
195@[simp 900]
196theorem kernelAbelianizationConjOfSurjective_eq_surjInv
197 (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) :
198 kernelAbelianizationConjOfSurjective ψ hψ h =
199 kernelAbelianizationConj ψ (Function.surjInv hψ h) := by
200 let g₁ : G := hψ.hasRightInverse.choose h
201 let g₂ : G := Function.surjInv hψ h
202 have hg₁ : ψ g₁ = h := hψ.hasRightInverse.choose_spec h
203 have hg₂ : ψ g₂ = h := Function.surjInv_eq hψ h
204 have hker : ψ (g₁ * g₂⁻¹) = 1 := by
205 simp only [map_mul, hg₁, map_inv, hg₂, mul_inv_cancel]
206 have htriv :
207 kernelAbelianizationConj ψ (g₁ * g₂⁻¹) = 1 := by
208 simpa using kernelAbelianizationConj_eq_one_of_mem_ker (ψ := ψ) ⟨g₁ * g₂⁻¹, hker⟩
209 have hsame :
210 kernelAbelianizationConj ψ g₁ = kernelAbelianizationConj ψ g₂ := by
211 have hmul :
212 kernelAbelianizationConj ψ g₁ *
213 (kernelAbelianizationConj ψ g₂)⁻¹ = 1 := by
214 simpa [map_mul] using htriv
215 have hmul' := congrArg (fun u : MulAut (Abelianization ψ.ker) =>
216 u * kernelAbelianizationConj ψ g₂) hmul
217 simpa [mul_assoc] using hmul'
218 unfold kernelAbelianizationConjOfSurjective QuotientGroup.quotientKerEquivOfSurjective
219 QuotientGroup.quotientKerEquivOfRightInverse
220 simpa [g₁, g₂, quotientKernelAbelianizationConj] using hsame
222/--
223For a surjective homomorphism, the conjugation action on the kernel abelianization is rewritten
224as an additive automorphism action.
225-/
226def kernelAbelianizationAddAutOfSurjective
227 (ψ : G →* H) (hψ : Function.Surjective ψ) :
228 H →* Multiplicative (AddAut (KernelAbelianizationAdd ψ)) :=
229 (AddAutAdditive (Abelianization ψ.ker)).symm.toAddMonoidHom.toMultiplicativeRight.comp
230 (kernelAbelianizationConjOfSurjective ψ hψ)
232omit [DecidableEq H] [DecidableEq G] in
233/--
234An additive automorphism of the kernel abelianization determines its underlying
235\(\mathbb{Z}\)-linear endomorphism.
236-/
237def kernelAbelianizationAddAutToModuleEnd (ψ : G →* H) :
238 Multiplicative (AddAut (KernelAbelianizationAdd ψ)) →*
239 Module.End ℤ (KernelAbelianizationAdd ψ) where
240 toFun e := e.toAdd.toIntLinearEquiv.toLinearMap
241 map_one' := by
242 ext x
243 change (0 : AddAut (KernelAbelianizationAdd ψ)) x = x
244 rfl
245 map_mul' e₁ e₂ := by
246 ext x
247 change (e₁.toAdd + e₂.toAdd) x = e₁.toAdd (e₂.toAdd x)
248 rfl
250/-- The surjective-case action as a hom into \(\mathbb{Z}\)-linear endomorphisms. -/
251def kernelAbelianizationModuleEndOfSurjective
252 (ψ : G →* H) (hψ : Function.Surjective ψ) :
253 H →* Module.End ℤ (KernelAbelianizationAdd ψ) where
254 toFun h := kernelAbelianizationAddAutToModuleEnd (ψ := ψ)
255 (kernelAbelianizationAddAutOfSurjective ψ hψ h)
256 map_one' := by
257 rw [(kernelAbelianizationAddAutOfSurjective ψ hψ).map_one]
258 ext x
259 rfl
260 map_mul' h₁ h₂ := by
261 rw [(kernelAbelianizationAddAutOfSurjective ψ hψ).map_mul]
262 ext x
263 rfl
265omit [DecidableEq H] [DecidableEq G] in
266/--
267The module endomorphism associated to `h` acts by the conjugation automorphism obtained from a
268chosen lift of `h`.
269-/
270@[simp]
271theorem kernelAbelianizationModuleEndOfSurjective_apply
272 (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) (x : KernelAbelianizationAdd ψ) :
273 kernelAbelianizationModuleEndOfSurjective ψ hψ h x =
274 Additive.ofMul (kernelAbelianizationConjOfSurjective ψ hψ h (Additive.toMul x)) := by
275 rfl
277/--
278The induced \(\mathbb{Z}[H]\)-action on \((\ker \psi)^{\mathrm{ab}}\), written in additive form.
279-/
280def kernelAbelianizationActionRingHomOfSurjective
281 (ψ : G →* H) (hψ : Function.Surjective ψ) :
282 GroupRing H →+* Module.End ℤ (KernelAbelianizationAdd ψ) :=
283 MonoidAlgebra.liftNCRingHom (Int.castRingHom (Module.End ℤ (KernelAbelianizationAdd ψ)))
284 (kernelAbelianizationModuleEndOfSurjective ψ hψ) (by
285 intro z h
286 ext x
287 simp only [eq_intCast, Module.End.mul_apply, kernelAbelianizationModuleEndOfSurjective_apply,
288 kernelAbelianizationConjOfSurjective_eq_surjInv, Module.End.intCast_apply, toMul_zsmul,
289 toMul_ofMul, map_smul])
291omit [DecidableEq H] [DecidableEq G] in
292/--
293The surjective-case group-ring action on kernel abelianization has the displayed value on
294representatives.
295-/
296@[simp]
297theorem kernelAbelianizationActionRingHomOfSurjective_of
298 (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) :
299 kernelAbelianizationActionRingHomOfSurjective ψ hψ (MonoidAlgebra.of ℤ H h) =
300 kernelAbelianizationModuleEndOfSurjective ψ hψ h := by
301 ext x
302 simp only [kernelAbelianizationActionRingHomOfSurjective, MonoidAlgebra.of_apply,
303 MonoidAlgebra.liftNCRingHom_single, eq_intCast, Int.cast_one, one_mul,
304 kernelAbelianizationModuleEndOfSurjective_apply,
305 kernelAbelianizationConjOfSurjective_eq_surjInv, toMul_ofMul]
307/--
308The \(\mathbb{Z}[H]\)-module structure on \(\ker(\psi)^{\mathrm{ab}}\) induced by surjective
309conjugation.
310-/
311@[reducible]
312def kernelAbelianizationModuleOfSurjective
313 (ψ : G →* H) (hψ : Function.Surjective ψ) :
314 Module (GroupRing H) (KernelAbelianizationAdd ψ) :=
315 Module.compHom _ (kernelAbelianizationActionRingHomOfSurjective ψ hψ)
317omit [DecidableEq H] [DecidableEq G] in
318/--
319For a surjective \(\psi\), the additive kernel-boundary map intertwines the induced conjugation
320action with scalar multiplication by the corresponding group-ring basis element.
321-/
322@[simp]
323theorem kernelAbelianizationBoundaryAdd_conjOfSurjective
324 (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) (x : Abelianization ψ.ker) :
325 kernelAbelianizationBoundaryAdd ψ
326 (Additive.ofMul (kernelAbelianizationConjOfSurjective ψ hψ h x)) =
327 (MonoidAlgebra.of ℤ H h : GroupRing H) •
328 kernelAbelianizationBoundaryAdd ψ (Additive.ofMul x) := by
329 let g : G := Function.surjInv hψ h
330 have hg : ψ g = h := Function.surjInv_eq hψ h
331 refine QuotientGroup.induction_on x ?_
332 intro n
333 rw [kernelAbelianizationConjOfSurjective_eq_surjInv]
334 change kernelAbelianizationBoundaryAdd ψ
335 (Additive.ofMul (kernelAbelianizationConj ψ g (Abelianization.of n))) =
336 (MonoidAlgebra.of ℤ H h : GroupRing H) •
337 kernelAbelianizationBoundaryAdd ψ (Additive.ofMul (Abelianization.of n))
338 rw [kernelAbelianizationConj_of, kernelAbelianizationBoundaryAdd_of,
339 kernelAbelianizationBoundaryAdd_of]
340 simpa [g, hg, MulAut.conjNormal_apply, mul_assoc] using universalDifferential_conj_of_mem_ker
341 ψ g n.1 n.2
343omit [DecidableEq H] [DecidableEq G] in
344/-- The kernel-boundary additive map is compatible with the surjective-case group-ring action. -/
345@[simp]
346theorem kernelAbelianizationBoundaryAdd_commOfSurjective
347 (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) (x : KernelAbelianizationAdd ψ) :
348 letI := kernelAbelianizationModuleOfSurjective ψ hψ
349 kernelAbelianizationBoundaryAdd ψ ((MonoidAlgebra.of ℤ H h : GroupRing H) • x) =
350 (MonoidAlgebra.of ℤ H h : GroupRing H) • kernelAbelianizationBoundaryAdd ψ x := by
351 letI := kernelAbelianizationModuleOfSurjective ψ hψ
352 change kernelAbelianizationBoundaryAdd ψ
353 ((kernelAbelianizationActionRingHomOfSurjective ψ hψ (MonoidAlgebra.of ℤ H h)) x) =
354 (MonoidAlgebra.of ℤ H h : GroupRing H) • kernelAbelianizationBoundaryAdd ψ x
355 rw [kernelAbelianizationActionRingHomOfSurjective_of,
356 kernelAbelianizationModuleEndOfSurjective_apply]
357 simpa using
358 kernelAbelianizationBoundaryAdd_conjOfSurjective ψ hψ h (Additive.toMul x)
360/--
361The head map of the discrete Crowell sequence, in \(\mathbb{Z}[H]\)-linear form when \(\psi\) is
362surjective.
363-/
364def kernelAbelianizationBoundaryLinearOfSurjective
365 (ψ : G →* H) (hψ : Function.Surjective ψ) :
366 letI := kernelAbelianizationModuleOfSurjective ψ hψ
367 KernelAbelianizationAdd ψ →ₗ[GroupRing H] DifferentialModule ψ := by
368 letI := kernelAbelianizationModuleOfSurjective ψ hψ
369 let f : KernelAbelianizationAdd ψ →ₗ[ℤ] DifferentialModule ψ :=
370 (kernelAbelianizationBoundaryAdd ψ).toIntLinearMap
371 exact MonoidAlgebra.equivariantOfLinearOfComm f
372 (fun h x => by
373 exact kernelAbelianizationBoundaryAdd_commOfSurjective (ψ := ψ) hψ h x)
375omit [DecidableEq H] [DecidableEq G] in
376/--
377The linear kernel-boundary map in the surjective case has the stated value on a kernel element.
378-/
379@[simp]
380theorem kernelAbelianizationBoundaryLinearOfSurjective_of
381 (ψ : G →* H) (hψ : Function.Surjective ψ) (n : ψ.ker) :
382 kernelAbelianizationBoundaryLinearOfSurjective ψ hψ
383 (Additive.ofMul (Abelianization.of n)) = universalDifferential ψ n.1 := by
384 letI := kernelAbelianizationModuleOfSurjective ψ hψ
385 change kernelAbelianizationBoundaryAdd ψ (Additive.ofMul (Abelianization.of n)) =
386 universalDifferential ψ n.1
387 exact kernelAbelianizationBoundaryAdd_of ψ n
389omit [DecidableEq H] [DecidableEq G] in
390/--
391The kernel-abelianization boundary map is evaluated on canonical generators and then extended
392linearly.
393-/
394@[simp]
395theorem kernelAbelianizationBoundaryLinearOfSurjective_apply
396 (ψ : G →* H) (hψ : Function.Surjective ψ) (x : KernelAbelianizationAdd ψ) :
397 kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x =
398 kernelAbelianizationBoundaryAdd ψ x := by
399 letI := kernelAbelianizationModuleOfSurjective ψ hψ
400 rfl
402omit [DecidableEq H] [DecidableEq G] in
403/--
404Composing the surjective-case kernel-boundary map with the group-ring map gives the expected
405group-ring boundary.
406-/
407@[simp]
408theorem toGroupRing_kernelAbelianizationBoundaryLinearOfSurjective
409 (ψ : G →* H) (hψ : Function.Surjective ψ) (x : KernelAbelianizationAdd ψ) :
410 toGroupRing ψ (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x) = 0 := by
411 rw [kernelAbelianizationBoundaryLinearOfSurjective_apply]
412 change toGroupRing ψ
413 (Multiplicative.toAdd (kernelAbelianizationBoundary ψ (Additive.toMul x))) = 0
414 refine QuotientGroup.induction_on (Additive.toMul x) ?_
415 intro n
416 change toGroupRing ψ (universalDifferential ψ n.1) = 0
419/-- The \(A_{\psi}\)-submodule generated by the head map in the surjective case. -/
420abbrev kernelAbelianizationBoundaryRangeOfSurjective
421 (ψ : G →* H) (hψ : Function.Surjective ψ) :
422 Submodule (GroupRing H) (DifferentialModule ψ) := by
423 letI := kernelAbelianizationModuleOfSurjective ψ hψ
424 exact LinearMap.range (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ)
427end
429end FoxDifferential