Source: ProCGroups.FoxDifferential.Completed.Comparison.MagnusKernel
1import ProCGroups.FoxDifferential.Discrete.KernelBoundary.MagnusComparison
2import ProCGroups.FoxDifferential.Discrete.KernelBoundary.Quotient
3import ProCGroups.FoxDifferential.Discrete.FoxCalculus.Boundary
4import ProCGroups.FoxDifferential.Completed.Comparison.DiscreteCompletion
6/-!
7# Fox Differential / Completed / Comparison / Magnus Kernel
9This module transfers discrete Magnus-kernel criteria through finite algebraic stages and
10completed Fox differential coordinates.
11-/
13namespace CrowellExactSequence
15noncomputable section
17open FoxDifferential
19variable {X : Type} {H : Type}
20variable [Group H] [Finite X]
22local instance : Fintype X := Fintype.ofFinite X
23local instance : DecidableEq X := Classical.decEq X
25/--
26The finite-stage Magnus reverse inclusion in residue-universal form. For the finite quotient
27\(F/N\), vanishing of the residue universal Fox differential modulo \(n\) forces a kernel word
28into \([N,N]N^n\).
29-/
30theorem mem_foxCommutatorPowerSubgroup_of_residueUniversalDifferential_eq_zero
31 (N : Subgroup (FreeGroup X)) [N.Normal] {n : ℕ} (hn : 0 < n)
32 {w : FreeGroup X} (hwN : w ∈ N)
33 (hres :
34 FoxDifferential.residueUniversalDifferential n (QuotientGroup.mk' N) w = 0) :
36 (F := FreeGroup X) N n := by
37 let Hq := FoxDifferential.foxAlgebraicStageTargetQuotient (X := X) N
38 let ψ : FreeGroup X →* Hq := QuotientGroup.mk' N
39 have hψ : Function.Surjective ψ := by
40 intro q
41 rcases QuotientGroup.mk'_surjective N q with ⟨g, hg⟩
42 exact ⟨g, hg⟩
43 obtain ⟨y, hy⟩ :=
45 (X := X) N w hres
46 have hder :
47 FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := Hq) X ψ w = n • y :=
48 by simpa [Hq, ψ] using hy
49 have hwker : w ∈ ψ.ker := by
50 change ψ w = 1
51 exact (QuotientGroup.eq_one_iff (N := N) w).2 hwN
52 have hboundary_derivative :
53 FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ
54 (FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := Hq) X ψ w) = 0 := by
55 have hfund :=
57 (H := Hq) X ψ w
58 have hgb : groupRingBoundary ψ w = 0 :=
59 groupRingBoundary_eq_zero_of_mem_ker (ψ := ψ) hwker
60 rw [hgb] at hfund
61 simpa [FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary] using hfund.symm
62 have hboundary_map_nsmul_all :
63 ∀ m : ℕ,
64 FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ (m • y) =
65 m • FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ y := by
66 intro m
67 induction m with
68 | zero =>
69 simp only [zero_nsmul, map_zero]
70 | succ m ih =>
71 rw [succ_nsmul, map_add, ih, succ_nsmul]
72 have hboundary_map_nsmul := hboundary_map_nsmul_all n
73 have hboundary_nsmul :
74 n • FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ y = 0 := by
75 calc
76 n • FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ y =
77 FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ (n • y) := by
78 exact hboundary_map_nsmul.symm
79 _ = FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ
80 (FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := Hq) X ψ w) := by
81 rw [← hder]
82 _ = 0 := hboundary_derivative
83 have hboundary_y :
84 FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ y = 0 :=
86 (FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ y)
87 hboundary_nsmul
88 let Y : DifferentialModule ψ :=
89 FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap (H := Hq) X ψ y
90 have hYker : toGroupRing ψ Y = 0 := by
91 have hcomp :=
92 LinearMap.congr_fun
94 (H := Hq) X ψ) y
95 change
96 toGroupRing ψ
98 (H := Hq) X ψ y) =
99 FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ y at hcomp
100 change
101 toGroupRing ψ
103 (H := Hq) X ψ y) = 0
104 exact hcomp.trans hboundary_y
105 letI := kernelAbelianizationModuleOfSurjective ψ hψ
106 obtain ⟨a, ha⟩ :=
107 (exact_kernelAbelianizationBoundaryLinearOfSurjective_toGroupRing
108 (H := Hq) ψ hψ Y).1 hYker
109 have htoDiff_map_nsmul_all :
110 ∀ m : ℕ,
111 FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap (H := Hq) X ψ (m • y) =
112 m • FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap (H := Hq) X ψ y := by
113 intro m
114 induction m with
115 | zero =>
116 simp only [zero_nsmul, map_zero]
117 | succ m ih =>
118 rw [succ_nsmul, map_add, ih, succ_nsmul]
119 have htoDiff_map_nsmul := htoDiff_map_nsmul_all n
120 have hd_nY : universalDifferential ψ w = n • Y := by
121 calc
122 universalDifferential ψ w =
124 (FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := Hq) X ψ w) := by
125 exact
127 (H := Hq) X ψ w).symm
128 _ = FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap (H := Hq) X ψ
129 (n • y) := by
130 rw [hder]
131 _ = n • Y := by
132 simpa [Y] using htoDiff_map_nsmul
133 let nw : ψ.ker := ⟨w, hwker⟩
134 have hboundary_class :
135 kernelAbelianizationBoundaryLinearOfSurjective ψ hψ
136 (Additive.ofMul (Abelianization.of nw)) =
137 n • kernelAbelianizationBoundaryLinearOfSurjective ψ hψ a := by
138 calc
139 kernelAbelianizationBoundaryLinearOfSurjective ψ hψ
140 (Additive.ofMul (Abelianization.of nw)) =
141 universalDifferential ψ w := by
142 rw [kernelAbelianizationBoundaryLinearOfSurjective_of]
143 _ = n • Y := hd_nY
144 _ = n • kernelAbelianizationBoundaryLinearOfSurjective ψ hψ a := by
145 simp only [ha]
146 have hclassAdd :
147 (Additive.ofMul (Abelianization.of nw) : KernelAbelianizationAdd ψ) = n • a := by
148 apply kernelAbelianizationBoundaryLinearOfSurjective_injective
149 (H := Hq) (ψ := ψ) hψ
150 simpa using hboundary_class
151 obtain ⟨a0, ha0⟩ := QuotientGroup.mk_surjective (Additive.toMul a)
152 have ha0' : Abelianization.of a0 = Additive.toMul a := by
153 change QuotientGroup.mk a0 = Additive.toMul a
154 exact ha0
155 have hclassMul :
156 Abelianization.of nw = (Abelianization.of a0) ^ n := by
157 have hmul := congrArg Additive.toMul hclassAdd
158 simpa [ha0'] using hmul
159 have hmemKer :
161 (F := FreeGroup X) ψ.ker n :=
163 (F := FreeGroup X) ψ.ker n hwker a0 hclassMul
164 have hker_eq : ψ.ker = N := by
165 ext g
166 change ψ g = 1 ↔ g ∈ N
167 exact QuotientGroup.eq_one_iff (N := N) g
168 simpa [hker_eq]
169 using hmemKer
171/--
172General finite-class discrete Magnus conclusion for a surjective finite target map, with the
173FoxDifferential finite-stage input supplied by the residue universal reverse inclusion.
174-/
175theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_of_surjective
178 (hForm : ProCGroups.FiniteGroupClass.Formation C)
179 [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H]
180 (hCH : C H)
181 {Q : Type} [Group Q]
182 (α : FreeGroup X →* Q) (hα : Function.Surjective α)
183 (β : Q →* H) (hβ : Function.Surjective β)
184 (hCker : C β.ker)
185 {w : FreeGroup X}
186 (hwker : w ∈ (β.comp α).ker)
187 (hzero :
188 FoxDifferential.zcUniversalDifferential C (β.comp α) w = 0) :
189 (⟨α w, by
190 change β (α w) = 1
191 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
192 commutator β.ker := by
193 exact
195 (C := C) (hC := hC) (X := X) (hForm := hForm) (hCH := hCH)
196 (α := α) (hα := hα) (β := β) (hβ := hβ) (hCker := hCker)
197 (fun j _ w hw hres =>
198 mem_foxCommutatorPowerSubgroup_of_residueUniversalDifferential_eq_zero
199 (X := X) (β.comp α).ker j.positive hw hres)
200 hwker hzero
202/--
203Finite-stage Magnus conclusion formulated with the finite Fox derivative vector. This is the
204form used after a continuous pro-\(C\) derivative is projected to one finite coefficient/target
205stage: the residue-universal reverse inclusion supplies the finite-stage Magnus input.
206-/
207theorem mem_commutator_ker_of_foxAlgebraicStageDerivativeVector_eq_zero
208 {Q H : Type} [Group Q] [Group H]
209 (α : FreeGroup X →* Q) (β : Q →* H) (n : ℕ) (hn : 0 < n)
210 (hpow : ∀ k : β.ker, k ^ n = 1)
211 {w : FreeGroup X}
212 (hwker : w ∈ (β.comp α).ker)
213 (hder :
215 (X := X) (β.comp α).ker n w = 0) :
216 (⟨α w, by
217 change β (α w) = 1
218 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
219 commutator β.ker := by
220 have hres :
222 (QuotientGroup.mk' (β.comp α).ker) w = 0 :=
223 (foxAlgebraicStageDerivativeVector_eq_zero_iff_residueUniversalDifferential_eq_zero
224 (X := X) (N := (β.comp α).ker) (n := n) (w := w)).1 hder
225 exact
227 (X := X) α β n hpow
228 (fun w hw hres =>
229 mem_foxCommutatorPowerSubgroup_of_residueUniversalDifferential_eq_zero
230 (X := X) (β.comp α).ker hn hw hres)
231 hwker hres
234universe u
236/--
237Universe-polymorphic finite-stage Magnus conclusion for finite source and target stages. This
238is only a transport of the Type 0 discrete Magnus theorem above: finite groups are lowered to
239an equivalent small model, and the finite-stage Fox derivative is reindexed along the
240free-basis equivalence.
241-/
242theorem mem_commutator_ker_of_finiteFoxStageDerivativeVector_eq_zero_finite
243 {X : Type u} [Fintype X] [DecidableEq X]
244 {Q H : Type u} [Group Q] [Group H] [Finite Q] [Finite H]
245 (α : FreeGroup X →* Q) (β : Q →* H) (n : ℕ) (hn : 0 < n)
246 (hpow : ∀ k : β.ker, k ^ n = 1)
247 {w : FreeGroup X}
248 (hwker : w ∈ (β.comp α).ker)
249 (hder :
251 (X := X) (β.comp α).ker n w = 0) :
252 (⟨α w, by
253 change β (α w) = 1
254 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
255 commutator β.ker := by
256 classical
257 letI : Finite X := inferInstance
258 rcases Finite.exists_equiv_fin X with ⟨m, ⟨eX⟩⟩
259 letI : DecidableEq (Fin m) := Classical.decEq (Fin m)
260 rcases Finite.exists_type_univ_nonempty_mulEquiv.{u, 0} Q with
261 ⟨Q0, instQ0Group, _instQ0Fintype, ⟨eQ⟩⟩
262 rcases Finite.exists_type_univ_nonempty_mulEquiv.{u, 0} H with
263 ⟨H0, instH0Group, _instH0Fintype, ⟨eH⟩⟩
264 letI : Group Q0 := instQ0Group
265 letI : Group H0 := instH0Group
266 let phi : FreeGroup X ≃* FreeGroup (Fin m) := FreeGroup.freeGroupCongr eX
267 let α0 : FreeGroup (Fin m) →* Q0 :=
268 eQ.toMonoidHom.comp (α.comp phi.symm.toMonoidHom)
269 let β0 : Q0 →* H0 :=
270 eH.toMonoidHom.comp (β.comp eQ.symm.toMonoidHom)
271 let w0 : FreeGroup (Fin m) := phi w
272 let M0 : Subgroup (FreeGroup (Fin m)) :=
273 (β0.comp α0).ker
274 haveI : M0.Normal := by
275 dsimp [M0]
276 infer_instance
277 have hM0 : (β.comp α).ker.map phi.toMonoidHom = M0 := by
278 ext z
279 constructor
280 · rintro ⟨x, hx, rfl⟩
281 change β0 (α0 (phi x)) = 1
282 change β (α x) = 1 at hx
283 have hphi : phi.symm (phi x) = x := phi.symm_apply_apply x
284 simpa [β0, α0, M0, hphi] using congrArg eH hx
285 · intro hz
286 refine ⟨phi.symm z, ?_, ?_⟩
287 · change β (α (phi.symm z)) = 1
288 have hz' : eH (β (α (phi.symm z))) = 1 := by
289 simpa [β0, α0, M0] using hz
290 exact eH.injective (by simpa using hz')
291 · exact phi.apply_symm_apply z
292 have hwker0 : w0 ∈ (β0.comp α0).ker := by
293 change β0 (α0 w0) = 1
294 change β (α w) = 1 at hwker
295 have hphi : phi.symm (phi w) = w := phi.symm_apply_apply w
296 simpa [β0, α0, w0, hphi] using congrArg eH hwker
297 have hderM0 :
299 (X := Fin m) M0 n w0 = 0 := by
300 simpa [M0, w0, phi] using
302 (X := X) (Y := Fin m) eX (β.comp α).ker M0 hM0 n hder
303 have hder0 :
305 (X := Fin m) (β0.comp α0).ker n w0 = 0 := by
306 simpa [M0] using hderM0
307 have hpow0 : ∀ k : β0.ker, k ^ n = 1 := by
308 intro k
309 have hkβ : β (eQ.symm k.1) = 1 := by
310 have hk0 : β0 k.1 = 1 := by
311 exact k.2
312 have hk : eH (β (eQ.symm k.1)) = 1 := by
313 simpa [β0] using hk0
314 exact eH.injective (by simpa using hk)
315 have hkpow := hpow ⟨eQ.symm k.1, hkβ⟩
316 have hkpow' : (eQ.symm k.1) ^ n = 1 :=
317 congrArg Subtype.val hkpow
318 have := congrArg eQ hkpow'
319 apply Subtype.ext
320 simpa using this
321 let q0 : β0.ker :=
322 ⟨α0 w0, by
323 change β0 (α0 w0) = 1
324 simpa [MonoidHom.mem_ker] using hwker0⟩
325 have hcomm0 : q0 ∈ commutator β0.ker := by
326 simpa [q0] using
327 mem_commutator_ker_of_foxAlgebraicStageDerivativeVector_eq_zero
328 (X := Fin m) α0 β0 n hn hpow0 hwker0 hder0
329 let κ : β0.ker →* β.ker :=
330 { toFun := fun k =>
331 ⟨eQ.symm k.1, by
332 change β (eQ.symm k.1) = 1
333 have hk0 : β0 k.1 = 1 := by
334 exact k.2
335 have hk : eH (β (eQ.symm k.1)) = 1 := by
336 simpa [β0] using hk0
337 exact eH.injective (by simpa using hk)⟩
338 map_one' := by
339 apply Subtype.ext
340 simp only [OneMemClass.coe_one, map_one]
341 map_mul' := by
342 intro a b
343 apply Subtype.ext
344 simp only [Subgroup.coe_mul, map_mul, MulMemClass.mk_mul_mk]}
345 have hcomm_map : (commutator β0.ker).map κ ≤ commutator β.ker := by
346 rw [_root_.map_commutator_eq]
347 exact Subgroup.commutator_mono (by intro x hx; trivial) (by intro x hx; trivial)
348 have hκq0 :
349 κ q0 =
350 (⟨α w, by
351 change β (α w) = 1
352 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) := by
353 apply Subtype.ext
354 have hphi : phi.symm (phi w) = w := phi.symm_apply_apply w
355 simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_comp, MonoidHom.coe_coe,
356 Function.comp_apply, hphi, MonoidHom.coe_mk, OneHom.coe_mk,
357 MulEquiv.symm_apply_apply, κ, q0, α0, w0]
358 have hκcomm : κ q0 ∈ commutator β.ker :=
359 hcomm_map ⟨q0, hcomm0, rfl⟩
360 simpa [hκq0] using hκcomm
363/--
364Discrete Magnus descent through a surjective finite source quotient, with the hypothesis
365expressed as ordinary relative Fox derivative zero for a representative word.
366-/
367theorem mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj_factor
368 {Q : Type} [Group Q]
369 (α : FreeGroup X →* Q) (hα : Function.Surjective α)
370 (β : Q →* H) (hβ : Function.Surjective β)
371 (q : β.ker) (w : FreeGroup X) (hw : α w = q.1)
372 (hn :
374 (H := H) X (β.comp α) w = 0) :
375 q ∈ commutator β.ker := by
376 let ψ : FreeGroup X →* H := β.comp α
377 have hψ : Function.Surjective ψ := by
378 intro h
379 rcases hβ h with ⟨q0, rfl⟩
380 rcases hα q0 with ⟨w0, rfl⟩
381 exact ⟨w0, rfl⟩
382 have hwker : w ∈ ψ.ker := by
383 change β (α w) = 1
384 rw [hw]
385 exact q.2
386 let n : ψ.ker := ⟨w, hwker⟩
387 have hncomm : n ∈ commutator ψ.ker :=
388 mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj
389 (X := X) (H := H) ψ hψ n (by simpa [ψ, n] using hn)
390 let κ : ψ.ker →* β.ker := {
391 toFun := fun n => ⟨α n.1, by
392 change β (α n.1) = 1
393 change ψ n.1 = 1
394 exact n.2⟩
395 map_one' := by
396 apply Subtype.ext
397 simp only [OneMemClass.coe_one, map_one]
398 map_mul' := by
399 intro n₁ n₂
400 apply Subtype.ext
401 simp only [Subgroup.coe_mul, map_mul, MulMemClass.mk_mul_mk]}
402 have hκn : κ n = q := by
403 apply Subtype.ext
404 exact hw
405 have hcomm_map :
406 (commutator ψ.ker).map κ ≤ commutator β.ker := by
407 rw [_root_.map_commutator_eq]
408 exact Subgroup.commutator_mono (by intro x hx; trivial) (by intro x hx; trivial)
409 simpa [hκn] using hcomm_map ⟨n, hncomm, rfl⟩
411/--
412Over the all-finite coefficient class, vanishing of the completed universal differential on a
413finite target quotient implies the ordinary discrete Magnus commutator conclusion.
414-/
415theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_allFinite
416 (N : Subgroup (FreeGroup X)) [N.Normal]
417 [TopologicalSpace (FoxDifferential.foxAlgebraicStageTargetQuotient (X := X) N)]
418 [DiscreteTopology (FoxDifferential.foxAlgebraicStageTargetQuotient (X := X) N)]
419 [IsTopologicalGroup (FoxDifferential.foxAlgebraicStageTargetQuotient (X := X) N)]
420 [Finite (FoxDifferential.foxAlgebraicStageTargetQuotient (X := X) N)]
421 (n : (QuotientGroup.mk' N).ker)
422 (hn :
425 (QuotientGroup.mk' N) n.1 = 0) :
426 n ∈ commutator (QuotientGroup.mk' N).ker := by
427 exact
428 mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj
429 (X := X)
430 (H := FoxDifferential.foxAlgebraicStageTargetQuotient (X := X) N)
431 (QuotientGroup.mk' N)
432 (QuotientGroup.mk'_surjective N)
433 n
435 (X := X) N n.1 hn)
437/--
438Over the all-finite coefficient class, vanishing of the completed universal differential for
439any surjective finite target map implies the ordinary discrete Magnus commutator conclusion.
440-/
441theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_allFinite_of_surjective
442 [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H] [Finite H]
443 (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
444 (n : ψ.ker)
445 (hn :
448 ψ n.1 = 0) :
449 n ∈ commutator ψ.ker := by
450 exact
451 mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj
452 (X := X) (H := H) ψ hψ n
454 (X := X) ψ hψ n.1 hn)
456/--
457All-finite discrete Magnus descent through a surjective finite source quotient, with the
458hypothesis expressed as zero of the completed Fox derivative vector for the representative
459word.
460-/
461theorem mem_commutator_ker_of_zcFreeFoxDerivVec_eq_zero_allFinite_of_surj_factor
462 {Q : Type} [Group Q]
463 [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H] [Finite H]
464 (α : FreeGroup X →* Q) (hα : Function.Surjective α)
465 (β : Q →* H) (hβ : Function.Surjective β)
466 (q : β.ker) (w : FreeGroup X) (hw : α w = q.1)
467 (hn :
470 (β.comp α) w = 0) :
471 q ∈ commutator β.ker := by
472 let ψ : FreeGroup X →* H := β.comp α
473 have hψ : Function.Surjective ψ := by
474 intro h
475 rcases hβ h with ⟨q0, rfl⟩
476 rcases hα q0 with ⟨w0, rfl⟩
477 exact ⟨w0, rfl⟩
478 exact
479 mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj_factor
480 (X := X) (H := H) α hα β hβ q w hw
482 (X := X) ψ hψ w (by simpa [ψ] using hn))
484/--
485All-finite discrete Magnus descent through a surjective finite source quotient. If a surjective
486free-group map \(\alpha: \mathrm{FreeGroup}(X) \to Q\) presents a finite-stage source and
487\(\beta: Q \to H\) is a surjective target map, vanishing of the completed universal
488differential on a representative word of \(q \in \ker \beta\) forces \(q\) into the commutator
489subgroup of \(\ker \beta\).
490-/
491theorem mem_commutator_ker_of_zcUnivDiff_eq_zero_allFinite_of_surj_factor
492 {Q : Type} [Group Q]
493 [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H] [Finite H]
494 (α : FreeGroup X →* Q) (hα : Function.Surjective α)
495 (β : Q →* H) (hβ : Function.Surjective β)
496 (q : β.ker) (w : FreeGroup X) (hw : α w = q.1)
497 (hn :
500 (β.comp α) w = 0) :
501 q ∈ commutator β.ker := by
502 exact
503 mem_commutator_ker_of_zcFreeFoxDerivVec_eq_zero_allFinite_of_surj_factor
504 (X := X) (H := H) α hα β hβ q w hw
507 (β.comp α) hn)
509/--
510Over the finite \(p\)-group coefficient class, vanishing of the completed universal
511differential on a finite \(p\)-group target quotient implies the ordinary discrete Magnus
512commutator conclusion.
513-/
514theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_pGroup
515 (p : ℕ) [Fact (Nat.Prime p)]
516 (N : Subgroup (FreeGroup X)) [N.Normal]
517 [TopologicalSpace (FoxDifferential.foxAlgebraicStageTargetQuotient (X := X) N)]
518 [DiscreteTopology (FoxDifferential.foxAlgebraicStageTargetQuotient (X := X) N)]
519 [IsTopologicalGroup (FoxDifferential.foxAlgebraicStageTargetQuotient (X := X) N)]
520 (hCtarget :
522 (FoxDifferential.foxAlgebraicStageTargetQuotient (X := X) N))
523 (n : (QuotientGroup.mk' N).ker)
524 (hn :
527 (QuotientGroup.mk' N) n.1 = 0) :
528 n ∈ commutator (QuotientGroup.mk' N).ker := by
529 exact
530 mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj
531 (X := X)
532 (H := FoxDifferential.foxAlgebraicStageTargetQuotient (X := X) N)
533 (QuotientGroup.mk' N)
534 (QuotientGroup.mk'_surjective N)
535 n
536 (relativeFreeGroupFoxDerivative_eq_zero_of_zcUniversalDifferential_eq_zero_pGroup
537 (X := X) (N := N) (p := p) (hCtarget := hCtarget) (w := n.1) hn)
539/--
540Over the finite \(p\)-group coefficient class, vanishing of the completed universal
541differential for any surjective finite \(p\)-group target map implies the ordinary discrete
542Magnus commutator conclusion.
543-/
544theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_pGroup_of_surjective
545 (p : ℕ) [Fact (Nat.Prime p)]
546 [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H]
547 (hCtarget : ProCGroups.FiniteGroupClass.pGroup p H)
548 (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
549 (n : ψ.ker)
550 (hn :
553 ψ n.1 = 0) :
554 n ∈ commutator ψ.ker := by
555 exact
556 mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj
557 (X := X) (H := H) ψ hψ n
559 (X := X) (H := H) (p := p) (hCtarget := hCtarget)
560 (ψ := ψ) (hψ := hψ) (w := n.1) hn)
562/--
563Finite-p discrete Magnus descent through a surjective finite source quotient, with the
564hypothesis expressed as zero of the completed Fox derivative vector for the representative
565word.
566-/
567theorem mem_commutator_ker_of_zcFreeFoxDerivVec_eq_zero_pGroup_of_surj_factor
568 (p : ℕ) [Fact (Nat.Prime p)]
569 {Q : Type} [Group Q]
570 [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H]
571 (hCtarget : ProCGroups.FiniteGroupClass.pGroup p H)
572 (α : FreeGroup X →* Q) (hα : Function.Surjective α)
573 (β : Q →* H) (hβ : Function.Surjective β)
574 (q : β.ker) (w : FreeGroup X) (hw : α w = q.1)
575 (hn :
578 (β.comp α) w = 0) :
579 q ∈ commutator β.ker := by
580 let ψ : FreeGroup X →* H := β.comp α
581 have hψ : Function.Surjective ψ := by
582 intro h
583 rcases hβ h with ⟨q0, rfl⟩
584 rcases hα q0 with ⟨w0, rfl⟩
585 exact ⟨w0, rfl⟩
586 exact
587 mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj_factor
588 (X := X) (H := H) α hα β hβ q w hw
590 (X := X) (H := H) (p := p) (hCtarget := hCtarget)
591 (ψ := ψ) (hψ := hψ) (w := w) (by simpa [ψ] using hn))
593/-- Finite-p discrete Magnus descent through a surjective finite source quotient. -/
594theorem mem_commutator_ker_of_zcUnivDiff_eq_zero_pGroup_of_surj_factor
595 (p : ℕ) [Fact (Nat.Prime p)]
596 {Q : Type} [Group Q]
597 [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H]
598 (hCtarget : ProCGroups.FiniteGroupClass.pGroup p H)
599 (α : FreeGroup X →* Q) (hα : Function.Surjective α)
600 (β : Q →* H) (hβ : Function.Surjective β)
601 (q : β.ker) (w : FreeGroup X) (hw : α w = q.1)
602 (hn :
605 (β.comp α) w = 0) :
606 q ∈ commutator β.ker := by
607 exact
608 mem_commutator_ker_of_zcFreeFoxDerivVec_eq_zero_pGroup_of_surj_factor
609 (X := X) (H := H) p hCtarget α hα β hβ q w hw
612 (β.comp α) hn)
614end
616end CrowellExactSequence