CrowellExactSequence/Discrete/MagnusComparison.lean

1import FoxDifferential.Discrete.KernelBoundary.MagnusKernel

2import FoxDifferential.Discrete.KernelBoundary.Quotient

3import FoxDifferential.Discrete.FoxCalculus.Boundary

4import FoxDifferential.Completed.Comparison.DiscreteCompletion

6/-

7PUBLIC_PAGE_SNAPSHOT

8generated_at: 2026-05-27T09:47:29+09:00

9lean_source: lean4/CrowellExactSequence/Discrete/MagnusComparison.lean

10translation_root: data/translation

11purpose: identifies the local data snapshot used to build pages/

12placement: after imports, never before imports

13-/

14/-!

15# Discrete Magnus input from the FoxDifferential library

17This file connects the `FoxDifferential` relative free Fox derivative with the discrete Crowell

18Magnus-kernel theorem. It reuses the kernel theorem rather than duplicating its proof.

19-/

21namespace CrowellExactSequence

23noncomputable section

25open FoxDifferential

27variable {X : Type} {H : Type}

28variable [Group H] [Fintype X] [DecidableEq X]

30/-- If the `FoxDifferential` relative free Fox derivative of a word vanishes, then the Crowell

31universal differential of the same word vanishes. -/

32theorem d_eq_zero_of_foxDifferential_relativeFreeGroupFoxDerivative_eq_zero

33 (ψ : FreeGroup X →* H) (w : FreeGroup X)

34 (hw :

35 FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative

36 (H := H) X ψ w = 0) :

37 universalDifferential ψ w = 0 := by

38 have hnew :

39 FoxDifferential.universalDifferential ψ w = 0 := by

40 have h :=

41 FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap_derivative

42 (H := H) X ψ w

43 rw [hw, map_zero] at h

44 exact h.symm

45 change FoxDifferential.universalDifferential ψ w = 0

46 exact hnew

48/-- Discrete Magnus-kernel theorem with the zero condition stated using the

49`FoxDifferential` relative free Fox derivative. -/

50theorem mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj

51 (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ) (n : ψ.ker)

52 (hn :

53 FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative

54 (H := H) X ψ n.1 = 0) :

55 n ∈ commutator ψ.ker :=

56 mem_commutator_ker_of_d_eq_zero_of_surjective (ψ := ψ) hψ n

57 (d_eq_zero_of_foxDifferential_relativeFreeGroupFoxDerivative_eq_zero

58 (X := X) (H := H) ψ n.1 hn)

60/-- Finite-stage Magnus reverse inclusion in residue-universal form.

62For the finite quotient `F/N`, zero of the residue universal Fox differential modulo `n`

63forces a kernel word into `[N,N]N^n`. -/

64theorem mem_finiteFoxCommutatorPowerSubgroup_of_residueUniversalDifferential_eq_zero

65 (N : Subgroup (FreeGroup X)) [N.Normal] {n : ℕ} (hn : 0 < n)

66 {w : FreeGroup X} (hwN : w ∈ N)

67 (hres :

68 FoxDifferential.residueUniversalDifferential n (QuotientGroup.mk' N) w = 0) :

69 w ∈ FoxDifferential.finiteFoxCommutatorPowerSubgroup

70 (F := FreeGroup X) N n := by

71 let Hq := FoxDifferential.finiteFoxStageTargetQuotient (X := X) N

72 let ψ : FreeGroup X →* Hq := QuotientGroup.mk' N

73 have hψ : Function.Surjective ψ := by

74 simpa [ψ] using (QuotientGroup.mk'_surjective N)

75 obtain ⟨y, hy⟩ :=

76 FoxDifferential.exists_eq_nsmul_relFreeFoxDeriv_of_residueUnivDiff_eq_zero

77 (X := X) N hn w hres

78 have hder :

79 FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := Hq) X ψ w = n • y :=

80 by simpa [Hq, ψ] using hy

81 have hwker : w ∈ ψ.ker := by

82 change ψ w = 1

83 exact (QuotientGroup.eq_one_iff (N := N) w).2 hwN

84 have hboundary_derivative :

85 FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ

86 (FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := Hq) X ψ w) = 0 := by

87 have hfund :=

88 FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_fundamental_formula

89 (H := Hq) X ψ w

90 have hgb : groupRingBoundary ψ w = 0 :=

91 groupRingBoundary_eq_zero_of_mem_ker (ψ := ψ) hwker

92 rw [hgb] at hfund

93 simpa [FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary] using hfund.symm

94 have hboundary_map_nsmul_all :

95 ∀ m : ℕ,

96 FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ (m • y) =

97 m • FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ y := by

98 intro m

99 induction m with

100 | zero =>

101 simp only [zero_nsmul, map_zero]

102 | succ m ih =>

103 rw [succ_nsmul, map_add, ih, succ_nsmul]

104 have hboundary_map_nsmul := hboundary_map_nsmul_all n

105 have hboundary_nsmul :

106 n • FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ y = 0 := by

107 calc

108 n • FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ y =

109 FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ (n • y) := by

110 exact hboundary_map_nsmul.symm

111 _ = FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ

112 (FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := Hq) X ψ w) := by

113 rw [← hder]

114 _ = 0 := hboundary_derivative

115 have hboundary_y :

116 FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ y = 0 :=

117 FoxDifferential.groupRing_eq_zero_of_nsmul_eq_zero hn

118 (FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ y)

119 hboundary_nsmul

120 let Y : DifferentialModule ψ :=

121 FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap (H := Hq) X ψ y

122 have hYker : toGroupRing ψ Y = 0 := by

123 have hcomp :=

124 LinearMap.congr_fun

125 (FoxDifferential.FoxCalculus.toGroupRing_comp_relativeFreeFoxCoordinatesLinearMap

126 (H := Hq) X ψ) y

127 simpa [Y, hboundary_y] using hcomp

128 letI := kernelAbelianizationModuleOfSurjective ψ hψ

129 obtain ⟨a, ha⟩ :=

130 (exact_kernelAbelianizationBoundaryLinearOfSurjective_toGroupRing

131 (H := Hq) ψ hψ Y).1 hYker

132 have htoDiff_map_nsmul_all :

133 ∀ m : ℕ,

134 FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap (H := Hq) X ψ (m • y) =

135 m • FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap (H := Hq) X ψ y := by

136 intro m

137 induction m with

138 | zero =>

139 simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, zero_nsmul, map_zero]

140 | succ m ih =>

141 rw [succ_nsmul, map_add, ih, succ_nsmul]

142 have htoDiff_map_nsmul := htoDiff_map_nsmul_all n

143 have hd_nY : universalDifferential ψ w = n • Y := by

144 calc

145 universalDifferential ψ w =

146 FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap (H := Hq) X ψ

147 (FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := Hq) X ψ w) := by

148 exact

149 (FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap_derivative

150 (H := Hq) X ψ w).symm

151 _ = FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap (H := Hq) X ψ

152 (n • y) := by

153 rw [hder]

154 _ = n • Y := by

155 simpa [Y] using htoDiff_map_nsmul

156 let nw : ψ.ker := ⟨w, hwker⟩

157 have hboundary_class :

158 kernelAbelianizationBoundaryLinearOfSurjective ψ hψ

159 (Additive.ofMul (Abelianization.of nw)) =

160 n • kernelAbelianizationBoundaryLinearOfSurjective ψ hψ a := by

161 calc

162 kernelAbelianizationBoundaryLinearOfSurjective ψ hψ

163 (Additive.ofMul (Abelianization.of nw)) =

164 universalDifferential ψ w := by

165 rw [kernelAbelianizationBoundaryLinearOfSurjective_of]

166 _ = n • Y := hd_nY

167 _ = n • kernelAbelianizationBoundaryLinearOfSurjective ψ hψ a := by

168 simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, ha]

169 have hclassAdd :

170 (Additive.ofMul (Abelianization.of nw) : KernelAbelianizationAdd ψ) = n • a := by

171 apply kernelAbelianizationBoundaryLinearOfSurjective_injective

172 (H := Hq) (ψ := ψ) hψ

173 simpa using hboundary_class

174 obtain ⟨a0, ha0⟩ := QuotientGroup.mk_surjective (Additive.toMul a)

175 have ha0' : Abelianization.of a0 = Additive.toMul a := by

176 simpa [Abelianization.of] using ha0

177 have hclassMul :

178 Abelianization.of nw = (Abelianization.of a0) ^ n := by

179 have hmul := congrArg Additive.toMul hclassAdd

180 simpa [ha0'] using hmul

181 have hmemKer :

182 w ∈ FoxDifferential.finiteFoxCommutatorPowerSubgroup

183 (F := FreeGroup X) ψ.ker n :=

184 FoxDifferential.mem_finiteFoxCommutatorPowerSubgroup_of_abelianization_eq_pow

185 (F := FreeGroup X) ψ.ker n hwker a0 hclassMul

186 have hker_eq : ψ.ker = N := by

187 ext g

188 change ψ g = 1 ↔ g ∈ N

189 exact QuotientGroup.eq_one_iff (N := N) g

190 simpa [hker_eq]

191 using hmemKer

192

193/-- General finite-class discrete Magnus conclusion for a surjective finite target map.

194

195The pure finite-stage Magnus input required by `FoxDifferential` is discharged by the residue

196universal reverse inclusion proved above. -/

197theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_of_surjective

198 {C : ProCGroups.FiniteGroupClass}

199 (hC : ProCGroups.FiniteGroupClass.Hereditary C)

200 (hForm : ProCGroups.FiniteGroupClass.Formation C)

201 [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H]

202 (hCH : C H)

203 {Q : Type} [Group Q]

204 (α : FreeGroup X →* Q) (hα : Function.Surjective α)

205 (β : Q →* H) (hβ : Function.Surjective β)

206 (hCker : C β.ker)

207 {w : FreeGroup X}

208 (hwker : w ∈ (β.comp α).ker)

209 (hzero :

210 FoxDifferential.zcUniversalDifferential C (β.comp α) w = 0) :

211 (⟨α w, by

212 change β (α w) = 1

213 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈

214 commutator β.ker := by

215 exact

216 FoxDifferential.mem_commutator_ker_of_zcUnivDiff_eq_zero_of_finite_magnus_surj

217 (C := C) (hC := hC) (X := X) (hForm := hForm) (hCH := hCH)

218 (α := α) (hα := hα) (β := β) (hβ := hβ) (hCker := hCker)

219 (fun j _ w hw hres =>

220 mem_finiteFoxCommutatorPowerSubgroup_of_residueUniversalDifferential_eq_zero

221 (X := X) (β.comp α).ker j.positive hw hres)

222 hwker hzero

223

224/-- Finite-stage Magnus conclusion stated with the finite Fox derivative vector.

225

226This is the form used after a continuous pro-`C` derivative is projected to one finite

227coefficient/target stage: the residue-universal reverse inclusion supplies the finite-stage

228Magnus input. -/

229theorem mem_commutator_ker_of_finiteFoxStageDerivativeVector_eq_zero

230 {Q H : Type} [Group Q] [Group H]

231 (α : FreeGroup X →* Q) (β : Q →* H) (n : ℕ) (hn : 0 < n)

232 (hpow : ∀ k : β.ker, k ^ n = 1)

233 {w : FreeGroup X}

234 (hwker : w ∈ (β.comp α).ker)

235 (hder :

236 FoxDifferential.finiteFoxStageDerivativeVector

237 (X := X) (β.comp α).ker n w = 0) :

238 (⟨α w, by

239 change β (α w) = 1

240 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈

241 commutator β.ker := by

242 have hres :

243 FoxDifferential.residueUniversalDifferential n

244 (QuotientGroup.mk' (β.comp α).ker) w = 0 :=

245 (FoxDifferential.finiteFoxStageDerivativeVector_eq_zero_iff_residueUniversalDifferential_eq_zero

246 (X := X) (β.comp α).ker n w).1 hder

247 exact

248 FoxDifferential.mem_commutator_ker_of_residueUniversalDifferential_eq_zero_of_kernel_le

249 (X := X) α β n hpow

250 (fun w hw hres =>

251 mem_finiteFoxCommutatorPowerSubgroup_of_residueUniversalDifferential_eq_zero

252 (X := X) (β.comp α).ker hn hw hres)

253 hwker hres

254

255

256universe u

257

258/-- Universe-polymorphic finite-stage Magnus conclusion for finite source and target stages.

259

260This is only a transport of the `Type 0` discrete Magnus theorem above: finite groups are

261lowered to an equivalent small model, and the finite-stage Fox derivative is reindexed along the

262free-basis equivalence. -/

263theorem mem_commutator_ker_of_finiteFoxStageDerivativeVector_eq_zero_finite

264 {X : Type u} [Fintype X] [DecidableEq X]

265 {Q H : Type u} [Group Q] [Group H] [Finite Q] [Finite H]

266 (α : FreeGroup X →* Q) (β : Q →* H) (n : ℕ) (hn : 0 < n)

267 (hpow : ∀ k : β.ker, k ^ n = 1)

268 {w : FreeGroup X}

269 (hwker : w ∈ (β.comp α).ker)

270 (hder :

271 FoxDifferential.finiteFoxStageDerivativeVector

272 (X := X) (β.comp α).ker n w = 0) :

273 (⟨α w, by

274 change β (α w) = 1

275 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈

276 commutator β.ker := by

277 classical

278 letI : Finite X := inferInstance

279 rcases Finite.exists_equiv_fin X with ⟨m, ⟨eX⟩⟩

280 rcases Finite.exists_type_univ_nonempty_mulEquiv.{u, 0} Q with

281 ⟨Q0, instQ0Group, _instQ0Fintype, ⟨eQ⟩⟩

282 rcases Finite.exists_type_univ_nonempty_mulEquiv.{u, 0} H with

283 ⟨H0, instH0Group, _instH0Fintype, ⟨eH⟩⟩

284 letI : Group Q0 := instQ0Group

285 letI : Group H0 := instH0Group

286 let phi : FreeGroup X ≃* FreeGroup (Fin m) := FreeGroup.freeGroupCongr eX

287 let α0 : FreeGroup (Fin m) →* Q0 :=

288 eQ.toMonoidHom.comp (α.comp phi.symm.toMonoidHom)

289 let β0 : Q0 →* H0 :=

290 eH.toMonoidHom.comp (β.comp eQ.symm.toMonoidHom)

291 let w0 : FreeGroup (Fin m) := phi w

292 let M0 : Subgroup (FreeGroup (Fin m)) :=

293 (β0.comp α0).ker

294 haveI : M0.Normal := by

295 dsimp [M0]

296 infer_instance

297 have hM0 : (β.comp α).ker.map phi.toMonoidHom = M0 := by

298 ext z

299 constructor

300 · rintro ⟨x, hx, rfl⟩

301 change β0 (α0 (phi x)) = 1

302 change β (α x) = 1 at hx

303 have hphi : phi.symm (phi x) = x := phi.symm_apply_apply x

304 simpa [β0, α0, M0, hphi] using congrArg eH hx

305 · intro hz

306 refine ⟨phi.symm z, ?_, ?_⟩

307 · change β (α (phi.symm z)) = 1

308 have hz' : eH (β (α (phi.symm z))) = 1 := by

309 simpa [β0, α0, M0] using hz

310 exact eH.injective (by simpa using hz')

311 · exact phi.apply_symm_apply z

312 have hwker0 : w0 ∈ (β0.comp α0).ker := by

313 change β0 (α0 w0) = 1

314 change β (α w) = 1 at hwker

315 have hphi : phi.symm (phi w) = w := phi.symm_apply_apply w

316 simpa [β0, α0, w0, hphi] using congrArg eH hwker

317 have hderM0 :

318 FoxDifferential.finiteFoxStageDerivativeVector

319 (X := Fin m) M0 n w0 = 0 := by

320 simpa [M0, w0, phi] using

321 FoxDifferential.finiteFoxStageDerivativeVector_eq_zero_reindex

322 (X := X) (Y := Fin m) eX (β.comp α).ker M0 hM0 n hder

323 have hder0 :

324 FoxDifferential.finiteFoxStageDerivativeVector

325 (X := Fin m) (β0.comp α0).ker n w0 = 0 := by

326 simpa [M0] using hderM0

327 have hpow0 : ∀ k : β0.ker, k ^ n = 1 := by

328 intro k

329 have hkβ : β (eQ.symm k.1) = 1 := by

330 have hk0 : β0 k.1 = 1 := by

331 change β0 k.1 = 1

332 exact k.2

333 have hk : eH (β (eQ.symm k.1)) = 1 := by

334 simpa [β0] using hk0

335 exact eH.injective (by simpa using hk)

336 have hkpow := hpow ⟨eQ.symm k.1, hkβ⟩

337 have hkpow' : (eQ.symm k.1) ^ n = 1 :=

338 congrArg Subtype.val hkpow

339 have := congrArg eQ hkpow'

340 apply Subtype.ext

341 simpa using this

342 let q0 : β0.ker :=

343 ⟨α0 w0, by

344 change β0 (α0 w0) = 1

345 simpa [MonoidHom.mem_ker] using hwker0⟩

346 have hcomm0 : q0 ∈ commutator β0.ker := by

347 simpa [q0] using

348 mem_commutator_ker_of_finiteFoxStageDerivativeVector_eq_zero

349 (X := Fin m) α0 β0 n hn hpow0 hwker0 hder0

350 let κ : β0.ker →* β.ker :=

351 { toFun := fun k =>

352 ⟨eQ.symm k.1, by

353 change β (eQ.symm k.1) = 1

354 have hk0 : β0 k.1 = 1 := by

355 change β0 k.1 = 1

356 exact k.2

357 have hk : eH (β (eQ.symm k.1)) = 1 := by

358 simpa [β0] using hk0

359 exact eH.injective (by simpa using hk)⟩

360 map_one' := by

361 apply Subtype.ext

362 simp only [OneMemClass.coe_one, map_one]

363 map_mul' := by

364 intro a b

365 apply Subtype.ext

366 simp only [Subgroup.coe_mul, map_mul, MulMemClass.mk_mul_mk]}

367 have hcomm_map : (commutator β0.ker).map κ ≤ commutator β.ker := by

368 rw [_root_.map_commutator_eq]

369 exact Subgroup.commutator_mono (by intro x hx; trivial) (by intro x hx; trivial)

370 have hκq0 :

371 κ q0 =

372 (⟨α w, by

373 change β (α w) = 1

374 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) := by

375 apply Subtype.ext

376 have hphi : phi.symm (phi w) = w := phi.symm_apply_apply w

377 simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply, hphi,

378 MonoidHom.coe_mk, OneHom.coe_mk, MulEquiv.symm_apply_apply, κ, q0, α0, w0]

379 have hκcomm : κ q0 ∈ commutator β.ker :=

380 hcomm_map ⟨q0, hcomm0, rfl⟩

381 simpa [hκq0] using hκcomm

382

383

384/-- Discrete Magnus descent through a surjective finite source quotient, with the hypothesis

385stated as ordinary relative Fox derivative zero for a representative word. -/

386theorem mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj_factor

387 {Q : Type} [Group Q]

388 (α : FreeGroup X →* Q) (hα : Function.Surjective α)

389 (β : Q →* H) (hβ : Function.Surjective β)

390 (q : β.ker) (w : FreeGroup X) (hw : α w = q.1)

391 (hn :

392 FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative

393 (H := H) X (β.comp α) w = 0) :

394 q ∈ commutator β.ker := by

395 let ψ : FreeGroup X →* H := β.comp α

396 have hψ : Function.Surjective ψ := by

397 intro h

398 rcases hβ h with ⟨q0, rfl⟩

399 rcases hα q0 with ⟨w0, rfl⟩

400 exact ⟨w0, rfl⟩

401 have hwker : w ∈ ψ.ker := by

402 change β (α w) = 1

403 rw [hw]

404 exact q.2

405 let n : ψ.ker := ⟨w, hwker⟩

406 have hncomm : n ∈ commutator ψ.ker :=

407 mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj

408 (X := X) (H := H) ψ hψ n (by simpa [ψ, n] using hn)

409 let κ : ψ.ker →* β.ker := {

410 toFun := fun n => ⟨α n.1, by

411 change β (α n.1) = 1

412 change ψ n.1 = 1

413 exact n.2⟩

414 map_one' := by

415 apply Subtype.ext

416 simp only [OneMemClass.coe_one, map_one]

417 map_mul' := by

418 intro n₁ n₂

419 apply Subtype.ext

420 simp only [Subgroup.coe_mul, map_mul, MulMemClass.mk_mul_mk]}

421 have hκn : κ n = q := by

422 apply Subtype.ext

423 exact hw

424 have hcomm_map :

425 (commutator ψ.ker).map κ ≤ commutator β.ker := by

426 rw [_root_.map_commutator_eq]

427 exact Subgroup.commutator_mono (by intro x hx; trivial) (by intro x hx; trivial)

428 simpa [hκn] using hcomm_map ⟨n, hncomm, rfl⟩

429

430/-- Over the all-finite coefficient class, completed universal zero on a finite target quotient

431implies the ordinary discrete Magnus commutator conclusion. -/

432theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_allFinite

433 (N : Subgroup (FreeGroup X)) [N.Normal]

434 [TopologicalSpace (FoxDifferential.finiteFoxStageTargetQuotient (X := X) N)]

435 [DiscreteTopology (FoxDifferential.finiteFoxStageTargetQuotient (X := X) N)]

436 [IsTopologicalGroup (FoxDifferential.finiteFoxStageTargetQuotient (X := X) N)]

437 [Finite (FoxDifferential.finiteFoxStageTargetQuotient (X := X) N)]

438 (n : (QuotientGroup.mk' N).ker)

439 (hn :

440 FoxDifferential.zcUniversalDifferential

441 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass)

442 (QuotientGroup.mk' N) n.1 = 0) :

443 n ∈ commutator (QuotientGroup.mk' N).ker := by

444 exact

445 mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj

446 (X := X)

447 (H := FoxDifferential.finiteFoxStageTargetQuotient (X := X) N)

448 (QuotientGroup.mk' N)

449 (QuotientGroup.mk'_surjective N)

450 n

451 (FoxDifferential.relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_allFinite

452 (X := X) N n.1 hn)

453

454/-- Over the all-finite coefficient class, completed universal zero for any surjective finite

455target map implies the ordinary discrete Magnus commutator conclusion. -/

456theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_allFinite_of_surjective

457 [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H] [Finite H]

458 (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)

459 (n : ψ.ker)

460 (hn :

461 FoxDifferential.zcUniversalDifferential

462 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass)

463 ψ n.1 = 0) :

464 n ∈ commutator ψ.ker := by

465 exact

466 mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj

467 (X := X) (H := H) ψ hψ n

468 (FoxDifferential.relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_allFinite_of_surj

469 (X := X) ψ hψ n.1 hn)

470

471/-- All-finite discrete Magnus descent through a surjective finite source quotient, with the

472hypothesis stated as zero of the completed Fox derivative vector for the representative word. -/

473theorem mem_commutator_ker_of_zcFreeFoxDerivVec_eq_zero_allFinite_of_surj_factor

474 {Q : Type} [Group Q]

475 [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H] [Finite H]

476 (α : FreeGroup X →* Q) (hα : Function.Surjective α)

477 (β : Q →* H) (hβ : Function.Surjective β)

478 (q : β.ker) (w : FreeGroup X) (hw : α w = q.1)

479 (hn :

480 FoxDifferential.zcFreeGroupFoxDerivativeVector

481 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass)

482 (β.comp α) w = 0) :

483 q ∈ commutator β.ker := by

484 let ψ : FreeGroup X →* H := β.comp α

485 have hψ : Function.Surjective ψ := by

486 intro h

487 rcases hβ h with ⟨q0, rfl⟩

488 rcases hα q0 with ⟨w0, rfl⟩

489 exact ⟨w0, rfl⟩

490 exact

491 mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj_factor

492 (X := X) (H := H) α hα β hβ q w hw

493 (FoxDifferential.relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_allFinite_of_surj

494 (X := X) ψ hψ w (by simpa [ψ] using hn))

495

496/-- All-finite discrete Magnus descent through a surjective finite source quotient.

497

498If a surjective free-group map `α : FreeGroup X -> Q` presents a finite-stage source and

499`β : Q -> H` is a surjective target map, completed universal zero for a representative word of

500`q : ker β` forces `q` into the commutator subgroup of `ker β`. -/

501theorem mem_commutator_ker_of_zcUnivDiff_eq_zero_allFinite_of_surj_factor

502 {Q : Type} [Group Q]

503 [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H] [Finite H]

504 (α : FreeGroup X →* Q) (hα : Function.Surjective α)

505 (β : Q →* H) (hβ : Function.Surjective β)

506 (q : β.ker) (w : FreeGroup X) (hw : α w = q.1)

507 (hn :

508 FoxDifferential.zcUniversalDifferential

509 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass)

510 (β.comp α) w = 0) :

511 q ∈ commutator β.ker := by

512 exact

513 mem_commutator_ker_of_zcFreeFoxDerivVec_eq_zero_allFinite_of_surj_factor

514 (X := X) (H := H) α hα β hβ q w hw

515 (FoxDifferential.zcFreeGroupFoxDerivativeVector_eq_zero_of_zcUniversalDifferential_eq_zero

516 (C := (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass))

517 (β.comp α) hn)

518

519/-- Over the finite `p`-group coefficient class, completed universal zero on a finite

520`p`-group target quotient implies the ordinary discrete Magnus commutator conclusion. -/

521theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_pGroup

522 (p : ℕ) [Fact (Nat.Prime p)]

523 (N : Subgroup (FreeGroup X)) [N.Normal]

524 [TopologicalSpace (FoxDifferential.finiteFoxStageTargetQuotient (X := X) N)]

525 [DiscreteTopology (FoxDifferential.finiteFoxStageTargetQuotient (X := X) N)]

526 [IsTopologicalGroup (FoxDifferential.finiteFoxStageTargetQuotient (X := X) N)]

527 (hCtarget :

528 ProCGroups.FiniteGroupClass.pGroup p

529 (FoxDifferential.finiteFoxStageTargetQuotient (X := X) N))

530 (n : (QuotientGroup.mk' N).ker)

531 (hn :

532 FoxDifferential.zcUniversalDifferential

533 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass)

534 (QuotientGroup.mk' N) n.1 = 0) :

535 n ∈ commutator (QuotientGroup.mk' N).ker := by

536 exact

537 mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj

538 (X := X)

539 (H := FoxDifferential.finiteFoxStageTargetQuotient (X := X) N)

540 (QuotientGroup.mk' N)

541 (QuotientGroup.mk'_surjective N)

542 n

543 (FoxDifferential.relativeFreeGroupFoxDerivative_eq_zero_of_zcUniversalDifferential_eq_zero_pGroup

544 (X := X) (N := N) (p := p) (hCtarget := hCtarget) (w := n.1) hn)

545

546/-- Over the finite `p`-group coefficient class, completed universal zero for any surjective

547finite `p`-group target map implies the ordinary discrete Magnus commutator conclusion. -/

548theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_pGroup_of_surjective

549 (p : ℕ) [Fact (Nat.Prime p)]

550 [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H]

551 (hCtarget : ProCGroups.FiniteGroupClass.pGroup p H)

552 (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)

553 (n : ψ.ker)

554 (hn :

555 FoxDifferential.zcUniversalDifferential

556 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass)

557 ψ n.1 = 0) :

558 n ∈ commutator ψ.ker := by

559 exact

560 mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj

561 (X := X) (H := H) ψ hψ n

562 (FoxDifferential.relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_pGroup_of_surj

563 (X := X) (H := H) (p := p) (hCtarget := hCtarget)

564 (ψ := ψ) (hψ := hψ) (w := n.1) hn)

565

566/-- Finite-`p` discrete Magnus descent through a surjective finite source quotient, with the

567hypothesis stated as zero of the completed Fox derivative vector for the representative word. -/

568theorem mem_commutator_ker_of_zcFreeFoxDerivVec_eq_zero_pGroup_of_surj_factor

569 (p : ℕ) [Fact (Nat.Prime p)]

570 {Q : Type} [Group Q]

571 [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H]

572 (hCtarget : ProCGroups.FiniteGroupClass.pGroup p H)

573 (α : FreeGroup X →* Q) (hα : Function.Surjective α)

574 (β : Q →* H) (hβ : Function.Surjective β)

575 (q : β.ker) (w : FreeGroup X) (hw : α w = q.1)

576 (hn :

577 FoxDifferential.zcFreeGroupFoxDerivativeVector

578 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass)

579 (β.comp α) w = 0) :

580 q ∈ commutator β.ker := by

581 let ψ : FreeGroup X →* H := β.comp α

582 have hψ : Function.Surjective ψ := by

583 intro h

584 rcases hβ h with ⟨q0, rfl⟩

585 rcases hα q0 with ⟨w0, rfl⟩

586 exact ⟨w0, rfl⟩

587 exact

588 mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj_factor

589 (X := X) (H := H) α hα β hβ q w hw

590 (FoxDifferential.relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_pGroup_of_surj

591 (X := X) (H := H) (p := p) (hCtarget := hCtarget)

592 (ψ := ψ) (hψ := hψ) (w := w) (by simpa [ψ] using hn))

593

594/-- Finite-`p` discrete Magnus descent through a surjective finite source quotient. -/

595theorem mem_commutator_ker_of_zcUnivDiff_eq_zero_pGroup_of_surj_factor

596 (p : ℕ) [Fact (Nat.Prime p)]

597 {Q : Type} [Group Q]

598 [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H]

599 (hCtarget : ProCGroups.FiniteGroupClass.pGroup p H)

600 (α : FreeGroup X →* Q) (hα : Function.Surjective α)

601 (β : Q →* H) (hβ : Function.Surjective β)

602 (q : β.ker) (w : FreeGroup X) (hw : α w = q.1)

603 (hn :

604 FoxDifferential.zcUniversalDifferential

605 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass)

606 (β.comp α) w = 0) :

607 q ∈ commutator β.ker := by

608 exact

609 mem_commutator_ker_of_zcFreeFoxDerivVec_eq_zero_pGroup_of_surj_factor

610 (X := X) (H := H) p hCtarget α hα β hβ q w hw

611 (FoxDifferential.zcFreeGroupFoxDerivativeVector_eq_zero_of_zcUniversalDifferential_eq_zero

612 (C := (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass))

613 (β.comp α) hn)

614

615end

616

617end CrowellExactSequence