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

Source: ProCGroups.FoxDifferential.Discrete.KernelBoundary.Quotient

1import ProCGroups.FoxDifferential.Discrete.KernelBoundary.Basic
3/-!
4# Fox differential: discrete — kernel boundary — quotient
6The principal declarations in this module are:
8- `HeadQuotientOfSurjective`
9 The quotient of \(A_{\psi}\) by the image of the head map.
10- `toIdentityDifferentialModule`
11 The canonical map from \(A_{\psi}\) to the derived module of the identity map on \(H\).
12- `toIdentityDifferentialModule_d`
13 The canonical map to the identity differential module sends the universal differential of \(g\) to
14 the universal differential of its image.
15- `toAugmentationIdeal_id_comp_toIdentityDifferentialModule`
16 For the identity map, composing the identity differential module with the augmentation-ideal map
17 gives the expected augmentation boundary.
18-/
20namespace FoxDifferential
22noncomputable section
24open FoxDifferential
26variable {H G : Type*} [Group H] [Group G]
28/-- The quotient of \(A_{\psi}\) by the image of the head map. -/
29abbrev HeadQuotientOfSurjective (ψ : G →* H) (hψ : Function.Surjective ψ) : Type _ :=
30 DifferentialModule ψ ⧸ kernelAbelianizationBoundaryRangeOfSurjective ψ hψ
32/-- The canonical map from \(A_{\psi}\) to the derived module of the identity map on \(H\). -/
33def toIdentityDifferentialModule (ψ : G →* H) :
34 DifferentialModule ψ →ₗ[GroupRing H] DifferentialModule (MonoidHom.id H) :=
35 differentialModuleLift ψ
36 { toFun := fun g => universalDifferential (MonoidHom.id H) (ψ g)
37 map_mul' := by
38 intro g₁ g₂
39 simpa [map_mul] using
40 universalDifferential_mul (MonoidHom.id H) (ψ g₁) (ψ g₂) }
42/--
43The canonical map to the identity differential module sends the universal differential of \(g\)
44to the universal differential of its image.
45-/
46@[simp]
47theorem toIdentityDifferentialModule_d (ψ : G →* H) (g : G) :
48 toIdentityDifferentialModule ψ (universalDifferential ψ g) = universalDifferential
49 (MonoidHom.id H) (ψ g) := by
50 rw [toIdentityDifferentialModule, differentialModuleLift_d]
51 rfl
53/--
54For the identity map, composing the identity differential module with the augmentation-ideal map
55gives the expected augmentation boundary.
56-/
57theorem toAugmentationIdeal_id_comp_toIdentityDifferentialModule
58 (ψ : G →* H) :
59 (toAugmentationIdeal (H := H) (MonoidHom.id H)).comp (toIdentityDifferentialModule ψ) =
60 toAugmentationIdeal (H := H) ψ := by
61 apply hom_ext ψ
62 intro g
63 change toAugmentationIdeal (H := H) (MonoidHom.id H)
64 (toIdentityDifferentialModule ψ (universalDifferential ψ g)) =
65 toAugmentationIdeal (H := H) ψ (universalDifferential ψ g)
66 rw [toIdentityDifferentialModule_d, toAugmentationIdeal_d,
67 toAugmentationIdeal_d]
68 rfl
70/--
71Composing the surjective-case kernel-boundary map with the identity differential-module map
72gives the corresponding identity-module boundary value.
73-/
74@[simp]
75theorem toIdentityDifferentialModule_kernelAbelianizationBoundaryLinearOfSurjective
76 (ψ : G →* H) (hψ : Function.Surjective ψ) (x : KernelAbelianizationAdd ψ) :
77 toIdentityDifferentialModule ψ
78 (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x) = 0 := by
79 letI := kernelAbelianizationModuleOfSurjective ψ hψ
80 rw [kernelAbelianizationBoundaryLinearOfSurjective_apply]
81 change
82 (fun y : Abelianization ψ.ker =>
83 toIdentityDifferentialModule ψ (kernelAbelianizationBoundaryAdd ψ (Additive.ofMul y)) = 0)
84 (Additive.toMul x)
85 refine QuotientGroup.induction_on (Additive.toMul x) ?_
86 intro n
87 change toIdentityDifferentialModule ψ
88 (kernelAbelianizationBoundaryAdd ψ (Additive.ofMul (Abelianization.of n))) = 0
89 have hinner :
90 toIdentityDifferentialModule ψ
91 (kernelAbelianizationBoundaryAdd ψ (Additive.ofMul (Abelianization.of n))) =
92 toIdentityDifferentialModule ψ (universalDifferential ψ n.1) := by
93 exact congrArg (toIdentityDifferentialModule ψ) (kernelAbelianizationBoundaryAdd_of ψ n)
94 rw [hinner, toIdentityDifferentialModule_d, n.2, universalDifferential_one]
96/--
97The surjective-case kernel-boundary range lies in the kernel of the map to the identity
98differential module.
99-/
100theorem kernelAbelianizationBoundaryRangeOfSurjective_le_ker_toIdentityDiffModule
101 (ψ : G →* H) (hψ : Function.Surjective ψ) :
102 kernelAbelianizationBoundaryRangeOfSurjective ψ hψ ≤
103 LinearMap.ker (toIdentityDifferentialModule ψ) := by
104 intro y hy
105 rcases hy with ⟨x, rfl⟩
106 simpa [LinearMap.mem_ker] using
107 toIdentityDifferentialModule_kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x
109/-- The quotient map \(A_{\psi} / \operatorname{im}(\mathrm{head}) \to A_{\mathrm{id}}\). -/
110def headQuotientToIdentityDifferentialModule
111 (ψ : G →* H) (hψ : Function.Surjective ψ) :
112 HeadQuotientOfSurjective ψ hψ →ₗ[GroupRing H] DifferentialModule (MonoidHom.id H) :=
113 (kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).liftQ
114 (toIdentityDifferentialModule ψ)
115 (kernelAbelianizationBoundaryRangeOfSurjective_le_ker_toIdentityDiffModule ψ hψ)
117/--
118The map from the head quotient to the identity differential module has the stated value on
119quotient classes.
120-/
121@[simp]
122theorem headQuotientToIdentityDifferentialModule_mkQ
123 (ψ : G →* H) (hψ : Function.Surjective ψ) (x : DifferentialModule ψ) :
124 headQuotientToIdentityDifferentialModule ψ hψ
125 ((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ x) =
126 toIdentityDifferentialModule ψ x := by
127 rfl
129/-- A section of \(\psi\) is viewed as a differential map into the head quotient. -/
130def headQuotientSectionOfSurjective
131 (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) :
132 HeadQuotientOfSurjective ψ hψ :=
133 (kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ
134 (universalDifferential ψ (Function.surjInv hψ h))
136private theorem headQuotientSectionOfSurjective_map_mul
137 (ψ : G →* H) (hψ : Function.Surjective ψ) (h₁ h₂ : H) :
138 headQuotientSectionOfSurjective ψ hψ (h₁ * h₂) =
139 headQuotientSectionOfSurjective ψ hψ h₁ +
140 groupRingScalar (MonoidHom.id H) h₁ •
141 headQuotientSectionOfSurjective ψ hψ h₂ := by
142 let s : H → G := Function.surjInv hψ
143 let q : Submodule (GroupRing H) (DifferentialModule ψ) :=
144 kernelAbelianizationBoundaryRangeOfSurjective ψ hψ
145 have hs12 : ψ (s (h₁ * h₂)) = h₁ * h₂ := by
146 simpa [s] using Function.surjInv_eq hψ (h₁ * h₂)
147 let n : ψ.ker := ⟨s (h₁ * h₂) * (s h₁ * s h₂)⁻¹, by
148 calc
149 ψ (s (h₁ * h₂) * (s h₁ * s h₂)⁻¹)
150 = ψ (s (h₁ * h₂)) * (ψ (s h₁ * s h₂))⁻¹ := by simp only [mul_inv_rev, map_mul, map_inv]
151 _ = (h₁ * h₂) * (h₂⁻¹ * h₁⁻¹) := by
152 rw [hs12]
153 simp only [map_mul, Function.surjInv_eq hψ h₁, Function.surjInv_eq hψ h₂,
154 mul_inv_rev, s]
155 _ = 1 := by simp only [mul_assoc, mul_inv_cancel_left, mul_inv_cancel]⟩
156 have hn_zero : q.mkQ (universalDifferential ψ n.1) = 0 := by
157 have hn_mem : universalDifferential ψ n.1 ∈ q := by
158 letI := kernelAbelianizationModuleOfSurjective ψ hψ
159 rw [← kernelAbelianizationBoundaryLinearOfSurjective_of (ψ := ψ) (hψ := hψ) n]
160 exact LinearMap.mem_range_self _ _
161 exact (Submodule.Quotient.mk_eq_zero (p := q) (x := universalDifferential ψ n.1)).2 hn_mem
162 have hs :
163 universalDifferential ψ (s (h₁ * h₂)) = universalDifferential ψ n.1 +
164 universalDifferential ψ (s h₁ * s h₂) := by
165 have hmul := universalDifferential_mul ψ n.1 (s h₁ * s h₂)
166 have hψn : (MonoidAlgebra.of ℤ H (ψ n.1) : GroupRing H) = 1 := by
167 rw [n.2, groupRing_of_one (H := H)]
168 rw [hψn, one_smul] at hmul
169 simpa [n, s, mul_assoc] using hmul
170 have hq :
171 q.mkQ (universalDifferential ψ (s (h₁ * h₂))) = q.mkQ (universalDifferential ψ (s h₁ * s
172 h₂)) := by
173 have hq' := congrArg q.mkQ hs
174 simpa [map_add, hn_zero] using hq'
175 calc
176 headQuotientSectionOfSurjective ψ hψ (h₁ * h₂)
177 = q.mkQ (universalDifferential ψ (s (h₁ * h₂))) := rfl
178 _ = q.mkQ (universalDifferential ψ (s h₁ * s h₂)) := hq
179 _ = q.mkQ (universalDifferential ψ (s h₁) + (MonoidAlgebra.of ℤ H (ψ (s h₁))) •
180 universalDifferential ψ (s h₂)) := by
181 rw [universalDifferential_mul]
182 _ = headQuotientSectionOfSurjective ψ hψ h₁ +
183 (MonoidAlgebra.of ℤ H h₁ : GroupRing H) •
184 headQuotientSectionOfSurjective ψ hψ h₂ := by
185 simp only [Function.surjInv_eq hψ h₁,
186 MonoidAlgebra.of_apply, Submodule.mkQ_apply, Submodule.Quotient.mk_add,
187 Submodule.Quotient.mk_smul,
188 headQuotientSectionOfSurjective, q, s]
190/-- The head-quotient section in the surjective case is a crossed differential. -/
191def headQuotientSectionHomOfSurjective
192 (ψ : G →* H) (hψ : Function.Surjective ψ) :
193 DifferentialHom (MonoidHom.id H) (HeadQuotientOfSurjective ψ hψ) where
194 toFun := headQuotientSectionOfSurjective ψ hψ
195 map_mul' := by
196 intro h₁ h₂
197 simpa only [scalarCrossedAction_apply] using
198 headQuotientSectionOfSurjective_map_mul ψ hψ h₁ h₂
200/--
201The inverse-direction map \(A_{\mathrm{id}} \to A_{\psi} / \operatorname{im}(\mathrm{head})\) is
202induced by a surjective section of \(\psi\).
203-/
204def fromIdentityDifferentialModuleOfSurjective
205 (ψ : G →* H) (hψ : Function.Surjective ψ) :
206 DifferentialModule (MonoidHom.id H) →ₗ[GroupRing H] HeadQuotientOfSurjective ψ hψ :=
207 differentialModuleLift (MonoidHom.id H) (headQuotientSectionHomOfSurjective ψ hψ)
209/--
210The surjective-case map from the identity differential module has the stated value on the
211differential generator.
212-/
213@[simp]
214theorem fromIdentityDifferentialModuleOfSurjective_d
215 (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) :
216 fromIdentityDifferentialModuleOfSurjective ψ hψ (universalDifferential (MonoidHom.id H) h) =
217 headQuotientSectionOfSurjective ψ hψ h := by
218 change
219 differentialModuleLift (MonoidHom.id H)
220 (headQuotientSectionHomOfSurjective ψ hψ)
221 (universalDifferential (MonoidHom.id H) h) =
222 headQuotientSectionOfSurjective ψ hψ h
223 exact
224 differentialModuleLift_d (A := HeadQuotientOfSurjective ψ hψ) (MonoidHom.id H)
225 (headQuotientSectionHomOfSurjective ψ hψ) h
227/--
228The maps between the head quotient and the identity differential module are inverse on the
229displayed side.
230-/
231theorem headQuotientToIdentityDiffModule_fromIdentityDiffModuleOfSurjective
232 (ψ : G →* H) (hψ : Function.Surjective ψ) :
233 (headQuotientToIdentityDifferentialModule ψ hψ).comp
234 (fromIdentityDifferentialModuleOfSurjective ψ hψ) =
235 LinearMap.id := by
236 apply hom_ext (ψ := MonoidHom.id H)
237 intro h
238 rw [LinearMap.comp_apply, fromIdentityDifferentialModuleOfSurjective_d,
239 headQuotientSectionOfSurjective, headQuotientToIdentityDifferentialModule_mkQ,
240 toIdentityDifferentialModule_d]
241 simp only [Function.surjInv_eq hψ h, LinearMap.id_coe, id_eq]
243/--
244The map from the identity differential module is a left inverse to the identity-differential
245quotient map in the surjective case.
246-/
247theorem fromIdentityDifferentialModuleOfSurjective_comp_toIdentityDifferentialModule
248 (ψ : G →* H) (hψ : Function.Surjective ψ) :
249 (fromIdentityDifferentialModuleOfSurjective ψ hψ).comp
250 (toIdentityDifferentialModule ψ) =
251 (kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ := by
252 apply hom_ext (ψ := ψ)
253 intro g
254 let s : H → G := Function.surjInv hψ
255 let q : Submodule (GroupRing H) (DifferentialModule ψ) :=
256 kernelAbelianizationBoundaryRangeOfSurjective ψ hψ
257 let n : ψ.ker := ⟨g * (s (ψ g))⁻¹, by
258 simp only [MonoidHom.mem_ker, map_mul, map_inv, Function.surjInv_eq hψ (ψ g),
259 mul_inv_cancel, s]⟩
260 have hn_zero : q.mkQ (universalDifferential ψ n.1) = 0 := by
261 have hn_mem : universalDifferential ψ n.1 ∈ q := by
262 letI := kernelAbelianizationModuleOfSurjective ψ hψ
263 rw [← kernelAbelianizationBoundaryLinearOfSurjective_of (ψ := ψ) (hψ := hψ) n]
264 exact LinearMap.mem_range_self _ _
265 exact (Submodule.Quotient.mk_eq_zero (p := q) (x := universalDifferential ψ n.1)).2 hn_mem
266 have hgdecomp : universalDifferential ψ g = universalDifferential ψ n.1 +
267 universalDifferential ψ (s (ψ g)) := by
268 have hmul := universalDifferential_mul ψ n.1 (s (ψ g))
269 have hψn : (MonoidAlgebra.of ℤ H (ψ n.1) : GroupRing H) = 1 := by
270 rw [n.2, groupRing_of_one (H := H)]
271 rw [hψn, one_smul] at hmul
272 simpa [n, s, mul_assoc] using hmul
273 have hq : q.mkQ (universalDifferential ψ g) = q.mkQ (universalDifferential ψ (s (ψ g))) := by
274 have hq' := congrArg q.mkQ hgdecomp
275 simpa [map_add, hn_zero] using hq'
276 calc
277 fromIdentityDifferentialModuleOfSurjective ψ hψ
278 (toIdentityDifferentialModule ψ (universalDifferential ψ g))
279 = q.mkQ (universalDifferential ψ (s (ψ g))) := by
280 rw [toIdentityDifferentialModule_d, fromIdentityDifferentialModuleOfSurjective_d,
281 headQuotientSectionOfSurjective]
282 _ = q.mkQ (universalDifferential ψ g) := hq.symm
284/--
285The quotient \(A_{\psi} / im(head)\) is canonically identified with the derived module of
286\(id_H\).
287-/
288def headQuotientEquivIdentityDifferentialModuleOfSurjective
289 (ψ : G →* H) (hψ : Function.Surjective ψ) :
290 HeadQuotientOfSurjective ψ hψ ≃ₗ[GroupRing H] DifferentialModule (MonoidHom.id H) where
291 toLinearMap := headQuotientToIdentityDifferentialModule ψ hψ
292 invFun := fromIdentityDifferentialModuleOfSurjective ψ hψ
293 left_inv := by
294 intro x
295 have hcomp :
296 (fromIdentityDifferentialModuleOfSurjective ψ hψ).comp
297 (headQuotientToIdentityDifferentialModule ψ hψ) =
298 LinearMap.id := by
299 apply Submodule.linearMap_qext _
300 apply LinearMap.ext
301 intro y
302 change fromIdentityDifferentialModuleOfSurjective ψ hψ
303 (headQuotientToIdentityDifferentialModule ψ hψ
304 ((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ y)) =
305 (kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ y
306 rw [headQuotientToIdentityDifferentialModule_mkQ]
307 exact LinearMap.congr_fun
308 (fromIdentityDifferentialModuleOfSurjective_comp_toIdentityDifferentialModule ψ hψ) y
309 exact LinearMap.congr_fun hcomp x
310 right_inv := by
311 intro x
312 exact LinearMap.congr_fun
313 (headQuotientToIdentityDiffModule_fromIdentityDiffModuleOfSurjective ψ hψ) x
315/-- For a surjective \(\psi\), the Crowell head quotient is the augmentation ideal. -/
316def headQuotientEquivAugmentationIdealOfSurjective
317 (ψ : G →* H) (hψ : Function.Surjective ψ) :
318 HeadQuotientOfSurjective ψ hψ ≃ₗ[GroupRing H] augmentationIdeal H :=
319 by
320 classical
321 exact
322 (headQuotientEquivIdentityDifferentialModuleOfSurjective ψ hψ).trans
325/--
326The head quotient is equivalent to the augmentation ideal and sends quotient classes to their
327augmentation representatives.
328-/
329@[simp]
330theorem headQuotientEquivAugmentationIdealOfSurjective_mkQ
331 (ψ : G →* H) (hψ : Function.Surjective ψ) (x : DifferentialModule ψ) :
332 headQuotientEquivAugmentationIdealOfSurjective ψ hψ
333 ((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ x) =
334 toAugmentationIdeal (H := H) ψ x := by
335 unfold headQuotientEquivAugmentationIdealOfSurjective
336 rw [LinearEquiv.trans_apply]
338 (headQuotientToIdentityDifferentialModule ψ hψ
339 ((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ x)) = _
340 rw [headQuotientToIdentityDifferentialModule_mkQ]
341 have hid := congrArg
342 (fun f : DifferentialModule (MonoidHom.id H) →ₗ[GroupRing H] augmentationIdeal H =>
343 f (toIdentityDifferentialModule ψ x))
345 exact hid.trans <|
346 LinearMap.congr_fun (toAugmentationIdeal_id_comp_toIdentityDifferentialModule (H := H) ψ) x
348/--
349The range of the surjective-case kernel-abelianization boundary is the kernel of the map to the
350augmentation ideal.
351-/
352theorem kernelAbelianizationBoundaryRangeOfSurjective_eq_ker_toAugmentationIdeal
353 (ψ : G →* H) (hψ : Function.Surjective ψ) :
354 kernelAbelianizationBoundaryRangeOfSurjective ψ hψ =
355 LinearMap.ker (toAugmentationIdeal (H := H) ψ) := by
356 apply le_antisymm
357 · intro y hy
358 rcases hy with ⟨x, rfl⟩
359 change toAugmentationIdeal (H := H) ψ
360 (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x) = 0
361 apply Subtype.ext
362 exact toGroupRing_kernelAbelianizationBoundaryLinearOfSurjective (H := H) ψ hψ x
363 · intro y hy
364 have hy0 : toAugmentationIdeal (H := H) ψ y = 0 := by
365 simpa [LinearMap.mem_ker] using hy
366 have hq0 :
367 headQuotientEquivAugmentationIdealOfSurjective ψ hψ
368 ((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ y) = 0 := by
369 rw [headQuotientEquivAugmentationIdealOfSurjective_mkQ]
370 exact hy0
371 have hq : ((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ y :
372 HeadQuotientOfSurjective ψ hψ) = 0 := by
373 exact (headQuotientEquivAugmentationIdealOfSurjective ψ hψ).injective
374 (by simpa using hq0)
375 exact (Submodule.Quotient.mk_eq_zero (p := kernelAbelianizationBoundaryRangeOfSurjective ψ hψ)
376 (x := y)).1 hq
378/-- Exactness at \(A_{\psi}\), formulated against the augmentation ideal. -/
379theorem exact_kernelAbelianizationBoundaryLinearOfSurjective_toAugmentationIdeal
380 (ψ : G →* H) (hψ : Function.Surjective ψ) :
381 Function.Exact
382 (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ)
383 (toAugmentationIdeal (H := H) ψ) := by
384 intro y
385 constructor
386 · intro hy
387 have hyker : y ∈ LinearMap.ker (toAugmentationIdeal (H := H) ψ) := by
388 simpa [LinearMap.mem_ker] using hy
389 rw [← kernelAbelianizationBoundaryRangeOfSurjective_eq_ker_toAugmentationIdeal
390 (H := H) (ψ := ψ) hψ] at hyker
391 exact hyker
392 · rintro ⟨x, rfl⟩
393 apply Subtype.ext
394 exact toGroupRing_kernelAbelianizationBoundaryLinearOfSurjective (H := H) ψ hψ x
396/-- Exactness at \(A_{\psi}\), against the usual map \(A_{\psi}\ \to \mathbb{Z}[H]\). -/
397theorem exact_kernelAbelianizationBoundaryLinearOfSurjective_toGroupRing
398 (ψ : G →* H) (hψ : Function.Surjective ψ) :
399 Function.Exact
400 (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ)
401 (toGroupRing ψ) := by
402 intro y
403 constructor
404 · intro hy
405 have hy' : toAugmentationIdeal (H := H) ψ y = 0 := by
406 apply Subtype.ext
407 exact hy
408 exact (exact_kernelAbelianizationBoundaryLinearOfSurjective_toAugmentationIdeal
409 (H := H) ψ hψ y).1 hy'
410 · rintro ⟨x, rfl⟩
411 exact toGroupRing_kernelAbelianizationBoundaryLinearOfSurjective (H := H) ψ hψ x
412end
414end FoxDifferential