Yamaguchi Lean 4 Library
FoxDifferential/Completed/FiniteStage/MagnusQuotient.lean
FoxDifferential/Completed/FiniteStage/MagnusQuotient/Source

FoxDifferential/Completed/FiniteStage/MagnusQuotient.lean

1import FoxDifferential.Completed.FiniteStage.Stage.Derivative.Rules
2import FoxDifferential.Completed.FiniteStage.Stage.Derivative.Relators
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/FiniteStage/MagnusQuotient.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Finite-stage Magnus quotient bookkeeping
15This file contains the group-theoretic quotient step used after a finite-stage Magnus theorem:
16membership in `[N,N] N^m`, with `m` the cardinality of a finite target kernel, maps to the
17ordinary commutator subgroup of that finite kernel.
18-/
20namespace FoxDifferential
22noncomputable section
24universe u v
26variable {X : Type u}
28section Reindex
30variable {Y : Type v}
31variable [DecidableEq X] [DecidableEq Y]
33/-- Reindex the finite-stage Fox semidirect target along an equivalence of free bases. -/
35 (e : X ≃ Y)
36 (N : Subgroup (FreeGroup X)) [N.Normal]
37 (M : Subgroup (FreeGroup Y)) [M.Normal]
38 (hM : N.map (FreeGroup.freeGroupCongr e).toMonoidHom = M)
39 (n : ℕ) :
40 FiniteFoxStageSemidirect (X := X) N n →*
41 FiniteFoxStageSemidirect (X := Y) M n := by
42 let φ : FreeGroup X ≃* FreeGroup Y := FreeGroup.freeGroupCongr e
43 let qXY :
46 QuotientGroup.congr N M φ hM
47 exact
48 { toFun := fun a =>
49 { left := fun y =>
50 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n) qXY.toMonoidHom
51 (a.left (e.symm y))
52 right := qXY a.right }
53 map_one' := by
54 apply FiniteFoxStageSemidirect.ext
55 · funext y
56 simp only [MulEquiv.toMonoidHom_eq_coe, FiniteFoxStageSemidirect.one_left, Pi.zero_apply,
57 MonoidAlgebra.mapDomainRingHom_apply, MonoidHom.coe_coe, Finsupp.mapDomain_zero]
58 · simp only [FiniteFoxStageSemidirect.one_right, map_one]
59 map_mul' := by
60 intro a b
61 apply FiniteFoxStageSemidirect.ext
62 · funext y
63 have hright :
64 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n) qXY.toMonoidHom
65 (MonoidAlgebra.of (ModNCompletedCoeff n)
66 (finiteFoxStageTargetQuotient (X := X) N) a.right) =
67 MonoidAlgebra.of (ModNCompletedCoeff n)
68 (finiteFoxStageTargetQuotient (X := Y) M) (qXY a.right) := by
69 rcases QuotientGroup.mk'_surjective N a.right with ⟨w, hw⟩
70 rw [← hw]
71 simp only [MulEquiv.toMonoidHom_eq_coe, MonoidAlgebra.of, MonoidAlgebra.single, QuotientGroup.mk'_apply,
72 MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, MonoidHom.coe_coe, Finsupp.mapDomain_single]
73 simp only [MulEquiv.toMonoidHom_eq_coe, FiniteFoxStageSemidirect.mul_left, MonoidAlgebra.of_apply,
74 Pi.add_apply, Pi.smul_apply, smul_eq_mul, map_add, MonoidAlgebra.mapDomainRingHom_apply, MonoidHom.coe_coe,
75 add_right_inj]
76 change
77 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n) qXY.toMonoidHom
78 (MonoidAlgebra.of (ModNCompletedCoeff n)
79 (finiteFoxStageTargetQuotient (X := X) N) a.right *
80 b.left (e.symm y)) =
81 MonoidAlgebra.of (ModNCompletedCoeff n)
82 (finiteFoxStageTargetQuotient (X := Y) M) (qXY a.right) *
83 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n) qXY.toMonoidHom
84 (b.left (e.symm y))
85 rw [map_mul, hright]
86 · simp only [FiniteFoxStageSemidirect.mul_right, map_mul, MulEquiv.toMonoidHom_eq_coe,
87 MonoidAlgebra.mapDomainRingHom_apply, MonoidHom.coe_coe]}
89/-- The reindexing hom carries the finite-stage lift to the finite-stage lift. -/
91 (e : X ≃ Y)
92 (N : Subgroup (FreeGroup X)) [N.Normal]
93 (M : Subgroup (FreeGroup Y)) [M.Normal]
94 (hM : N.map (FreeGroup.freeGroupCongr e).toMonoidHom = M)
95 (n : ℕ) (w : FreeGroup X) :
96 finiteFoxStageSemidirectReindexHom (X := X) (Y := Y) e N M hM n
97 (finiteFoxStageLift (X := X) N n w) =
98 finiteFoxStageLift (X := Y) M n ((FreeGroup.freeGroupCongr e) w) := by
99 let φ : FreeGroup X ≃* FreeGroup Y := FreeGroup.freeGroupCongr e
100 let qXY :
103 QuotientGroup.congr N M φ hM
104 let f₁ : FreeGroup X →* FiniteFoxStageSemidirect (X := Y) M n :=
105 (finiteFoxStageSemidirectReindexHom (X := X) (Y := Y) e N M hM n).comp
106 (finiteFoxStageLift (X := X) N n)
107 let f₂ : FreeGroup X →* FiniteFoxStageSemidirect (X := Y) M n :=
108 (finiteFoxStageLift (X := Y) M n).comp φ.toMonoidHom
109 have hf : f₁ = f₂ := by
110 apply FreeGroup.ext_hom
111 intro x
112 apply FiniteFoxStageSemidirect.ext
113 · funext y
114 by_cases hy : y = e x
115 · subst hy
116 simp only [finiteFoxStageSemidirectReindexHom, MulEquiv.toMonoidHom_eq_coe,
117 MonoidAlgebra.mapDomainRingHom_apply, MonoidHom.coe_coe, finiteFoxStageLift, QuotientGroup.mk'_apply,
118 MonoidHom.coe_comp, MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply, FreeGroup.lift_apply_of,
119 QuotientGroup.congr_mk, FreeGroup.freeGroupCongr_apply, FreeGroup.map.of, Pi.single_eq_same, f₁, f₂, φ]
120 rw [e.symm_apply_apply, Pi.single_eq_same]
121 simp only [MonoidAlgebra.mapDomain_one]
122 · have hne : e.symm y ≠ x := by
123 intro h
124 exact hy ((e.apply_symm_apply y).symm.trans (by simp only [h]))
125 simp only [finiteFoxStageSemidirectReindexHom, MulEquiv.toMonoidHom_eq_coe,
126 MonoidAlgebra.mapDomainRingHom_apply, MonoidHom.coe_coe, finiteFoxStageLift, QuotientGroup.mk'_apply,
127 MonoidHom.coe_comp, MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply, FreeGroup.lift_apply_of,
128 QuotientGroup.congr_mk, FreeGroup.freeGroupCongr_apply, FreeGroup.map.of, Pi.single_eq_of_ne hne,
129 Finsupp.mapDomain_zero, Pi.single_eq_of_ne hy, f₁, f₂, φ]
130 · simp only [finiteFoxStageSemidirectReindexHom, MulEquiv.toMonoidHom_eq_coe,
131 MonoidAlgebra.mapDomainRingHom_apply, MonoidHom.coe_coe, finiteFoxStageLift, QuotientGroup.mk'_apply,
132 MonoidHom.coe_comp, MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply, FreeGroup.lift_apply_of,
133 QuotientGroup.congr_mk, FreeGroup.freeGroupCongr_apply, FreeGroup.map.of, f₁, f₂, φ]
134 exact congrArg (fun f : FreeGroup X →* FiniteFoxStageSemidirect (X := Y) M n => f w) hf
136/-- Finite-stage Fox derivative vectors reindex along an equivalence of free bases. -/
138 (e : X ≃ Y)
139 (N : Subgroup (FreeGroup X)) [N.Normal]
140 (M : Subgroup (FreeGroup Y)) [M.Normal]
141 (hM : N.map (FreeGroup.freeGroupCongr e).toMonoidHom = M)
142 (n : ℕ) (w : FreeGroup X) :
143 finiteFoxStageDerivativeVector (X := Y) M n ((FreeGroup.freeGroupCongr e) w) =
144 fun y =>
145 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
146 (QuotientGroup.congr N M (FreeGroup.freeGroupCongr e) hM).toMonoidHom
147 (finiteFoxStageDerivativeVector (X := X) N n w (e.symm y)) := by
148 have h :=
149 congrArg FiniteFoxStageSemidirect.left
151 (X := X) (Y := Y) e N M hM n w)
154/-- Zero of a finite-stage Fox derivative vector is invariant under reindexing the free basis. -/
156 (e : X ≃ Y)
157 (N : Subgroup (FreeGroup X)) [N.Normal]
158 (M : Subgroup (FreeGroup Y)) [M.Normal]
159 (hM : N.map (FreeGroup.freeGroupCongr e).toMonoidHom = M)
160 (n : ℕ) {w : FreeGroup X}
161 (hw : finiteFoxStageDerivativeVector (X := X) N n w = 0) :
162 finiteFoxStageDerivativeVector (X := Y) M n ((FreeGroup.freeGroupCongr e) w) = 0 := by
163 rw [finiteFoxStageDerivativeVector_reindex (X := X) (Y := Y) e N M hM n w]
164 funext y
165 simp only [MulEquiv.toMonoidHom_eq_coe, hw, Pi.zero_apply, MonoidAlgebra.mapDomainRingHom_apply,
166 MonoidHom.coe_coe, Finsupp.mapDomain_zero]
168end Reindex
170variable {Q H : Type u}
171variable [Group Q] [Group H]
173section CommutatorPowerSubgroup
175variable {F : Type u} [Group F]
177/-- The ordinary commutator subgroup of `N`, mapped back to the ambient group, is contained in
178the finite Fox commutator-power subgroup. -/
180 (N : Subgroup F) (n : ℕ) :
181 (commutator N).map N.subtype ≤ finiteFoxCommutatorPowerSubgroup (F := F) N n := by
182 rw [Subgroup.map_subtype_commutator]
183 refine Subgroup.commutator_le.mpr ?_
184 intro a ha b hb
185 exact Subgroup.subset_normalClosure
186 (Or.inl ⟨a, ha, b, hb, rfl⟩)
188/-- `n`th powers from `N` are defining relators for the finite Fox commutator-power subgroup. -/
190 (N : Subgroup F) (n : ℕ) {a : F} (ha : a ∈ N) :
191 a ^ n ∈ finiteFoxCommutatorPowerSubgroup (F := F) N n :=
192 Subgroup.subset_normalClosure (Or.inr ⟨a, ha, rfl⟩)
194/-- If the abelianization class of a kernel element is an `n`th power, then the element lies in
195`[N,N]N^n`. -/
197 (N : Subgroup F) (n : ℕ) {w : F} (hw : w ∈ N) (a : N)
198 (hclass :
199 Abelianization.of ⟨w, hw⟩ = (Abelianization.of a) ^ n) :
200 w ∈ finiteFoxCommutatorPowerSubgroup (F := F) N n := by
201 have hclass' :
202 Abelianization.of (a ^ n) = Abelianization.of ⟨w, hw⟩ := by
203 simpa using hclass.symm
204 have hcommN : (a ^ n)⁻¹ * ⟨w, hw⟩ ∈ commutator N :=
205 QuotientGroup.eq.mp hclass'
206 have hcommF :
207 ((a : F) ^ n)⁻¹ * w ∈
209 have hmap :
210 (((a ^ n)⁻¹ * ⟨w, hw⟩ : N) : F) ∈ (commutator N).map N.subtype :=
211 ⟨(a ^ n)⁻¹ * ⟨w, hw⟩, hcommN, rfl⟩
212 exact
214 (by simpa using hmap)
215 have hpowF :
216 (a : F) ^ n ∈ finiteFoxCommutatorPowerSubgroup (F := F) N n :=
218 have hmul :
219 (a : F) ^ n * (((a : F) ^ n)⁻¹ * w) ∈
221 (finiteFoxCommutatorPowerSubgroup (F := F) N n).mul_mem hpowF hcommF
222 simpa [mul_assoc] using hmul
224end CommutatorPowerSubgroup
226/-- Residue-Fox form of the finite-stage Magnus reverse inclusion.
228The finite-stage derivative is not a separate Fox theory: it is the residue free Fox derivative
229for `FreeGroup X -> F/N`. This is the concise form in which the remaining finite Magnus theorem
230should be stated. -/
232 [DecidableEq X]
233 (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ) :
234 (finiteFoxStageLift (X := X) N n).ker ≤
235 finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n ↔
236 ∀ w : FreeGroup X,
237 w ∈ N →
238 residueFreeGroupFoxDerivativeVector n (QuotientGroup.mk' N) w = 0 →
239 w ∈ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n := by
241 constructor
242 · intro h w hwN hder
243 exact h w hwN (by
245 using hder)
246 · intro h w hwN hder
247 exact h w hwN (by
249 using hder)
251/-- Residue-universal form of the finite-stage Magnus reverse inclusion.
253With a finite free basis, the finite-stage coordinate vector is equivalent to the residue
254universal differential, so the remaining theorem is a kernel statement in the residue universal
255module. -/
257 [DecidableEq X] [Fintype X]
258 (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ) :
259 (finiteFoxStageLift (X := X) N n).ker ≤
260 finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n ↔
261 ∀ w : FreeGroup X,
262 w ∈ N →
263 residueUniversalDifferential n (QuotientGroup.mk' N) w = 0 →
264 w ∈ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n := by
266 constructor
267 · intro h w hwN hres
268 exact h w hwN
270 (X := X) N n w).2 hres)
271 · intro h w hwN hder
272 exact h w hwN
274 (X := X) N n w).1 hder)
276/-- The finite commutator-power subgroup maps into the ordinary commutator subgroup of a target
277kernel whenever the chosen exponent kills that kernel.
279This is the formal quotient bookkeeping needed after the finite-stage Magnus kernel theorem:
280the commutator relators map to commutators in `ker β`, while the power relators map to `1` by the
281given exponent-killing hypothesis. -/
283 (α : FreeGroup X →* Q) (β : Q →* H) (n : ℕ)
284 (hpow : ∀ k : β.ker, k ^ n = 1)
285 {w : FreeGroup X}
286 (hwker : w ∈ (β.comp α).ker)
287 (hw :
289 (F := FreeGroup X) (β.comp α).ker n) :
290 (⟨α w, by
291 change β (α w) = 1
292 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
293 commutator β.ker := by
294 let K : Subgroup Q := β.ker
295 let S : Subgroup (FreeGroup X) := (⁅K, K⁆).comap α
296 have hSnormal : S.Normal := by
297 dsimp [S, K]
298 infer_instance
299 have hrel_le :
300 finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) (β.comp α).ker n ≤ S := by
301 refine Subgroup.normalClosure_le_normal ?_
302 intro g hg
303 rcases hg with ⟨a, ha, b, hb, rfl⟩ | ⟨a, ha, rfl⟩
304 · change α ⁅a, b⁆ ∈ ⁅K, K⁆
305 rw [map_commutatorElement]
306 have haK : α a ∈ K := by
307 change β (α a) = 1
308 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using ha
309 have hbK : α b ∈ K := by
310 change β (α b) = 1
311 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hb
312 exact Subgroup.commutator_mem_commutator haK hbK
313 · change α (a ^ n) ∈ ⁅K, K⁆
314 rw [map_pow]
315 have haK : α a ∈ β.ker := by
316 change β (α a) = 1
317 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using ha
318 have hpowQ : (α a) ^ n = 1 := by
319 simpa using congrArg Subtype.val (hpow ⟨α a, haK⟩)
320 rw [hpowQ]
321 exact (⁅K, K⁆).one_mem
322 have hQ : α w ∈ ⁅K, K⁆ := hrel_le hw
323 have hQmap : α w ∈ (commutator β.ker).map β.ker.subtype := by
324 simpa [K, Subgroup.map_subtype_commutator] using hQ
325 rcases hQmap with ⟨c, hc, hcval⟩
326 have hc_eq :
327 c =
328 (⟨α w, by
329 change β (α w) = 1
330 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) := by
331 apply Subtype.ext
332 exact hcval
333 simpa [hc_eq] using hc
335/-- The finite-kernel cardinality version of the quotient bookkeeping lemma. -/
337 (α : FreeGroup X →* Q) (β : Q →* H) [Finite β.ker]
338 {w : FreeGroup X}
339 (hwker : w ∈ (β.comp α).ker)
340 (hw :
342 (F := FreeGroup X) (β.comp α).ker (Nat.card β.ker)) :
343 (⟨α w, by
344 change β (α w) = 1
345 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
346 commutator β.ker := by
347 exact
349 (X := X) α β (Nat.card β.ker) (fun _ => pow_card_eq_one') hwker hw
351/-- Finite quotient commutator conclusion from the finite-stage Magnus reverse inclusion.
353Once the kernel of the finite-stage lift has been identified with `[N,N]N^m`, a zero
354finite-stage derivative for a representative word gives the ordinary commutator conclusion in
355`ker β`. -/
357 [DecidableEq X]
358 (α : FreeGroup X →* Q) (β : Q →* H) (n : ℕ)
359 (hpow : ∀ k : β.ker, k ^ n = 1)
360 (hmag :
361 (finiteFoxStageLift (X := X) (β.comp α).ker n).ker ≤
362 finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) (β.comp α).ker n)
363 {w : FreeGroup X}
364 (hwker : w ∈ (β.comp α).ker)
365 (hder :
366 finiteFoxStageDerivativeVector (X := X) (β.comp α).ker n w = 0) :
367 (⟨α w, by
368 change β (α w) = 1
369 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
370 commutator β.ker := by
371 have hwrel :
372 w ∈ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) (β.comp α).ker n :=
373 hmag
374 ((mem_ker_finiteFoxStageLift_iff (X := X) (β.comp α).ker n).2
375 ⟨hwker, hder⟩)
376 exact
378 (X := X) α β n hpow hwker hwrel
380/-- Finite quotient commutator conclusion from the residue-universal finite Magnus kernel
381statement. -/
383 [DecidableEq X] [Fintype X]
384 (α : FreeGroup X →* Q) (β : Q →* H) (n : ℕ)
385 (hpow : ∀ k : β.ker, k ^ n = 1)
386 (hmag :
387 ∀ w : FreeGroup X,
388 w ∈ (β.comp α).ker →
389 residueUniversalDifferential n (QuotientGroup.mk' (β.comp α).ker) w = 0 →
391 (F := FreeGroup X) (β.comp α).ker n)
392 {w : FreeGroup X}
393 (hwker : w ∈ (β.comp α).ker)
394 (hder :
395 residueUniversalDifferential n (QuotientGroup.mk' (β.comp α).ker) w = 0) :
396 (⟨α w, by
397 change β (α w) = 1
398 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
399 commutator β.ker := by
400 exact
402 (X := X) α β n hpow hwker (hmag w hwker hder)
404/-- Cardinality-specialized finite quotient commutator conclusion from the finite-stage Magnus
405reverse inclusion. -/
407 [DecidableEq X]
408 (α : FreeGroup X →* Q) (β : Q →* H) [Finite β.ker]
409 (hmag :
410 (finiteFoxStageLift (X := X) (β.comp α).ker (Nat.card β.ker)).ker ≤
412 (F := FreeGroup X) (β.comp α).ker (Nat.card β.ker))
413 {w : FreeGroup X}
414 (hwker : w ∈ (β.comp α).ker)
415 (hder :
416 finiteFoxStageDerivativeVector (X := X) (β.comp α).ker (Nat.card β.ker) w = 0) :
417 (⟨α w, by
418 change β (α w) = 1
419 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
420 commutator β.ker := by
421 exact
423 (X := X) α β (Nat.card β.ker) (fun _ => pow_card_eq_one') hmag hwker hder
425/-- Cardinality-specialized finite quotient commutator conclusion from the residue-universal
426finite Magnus kernel statement. -/
428 [DecidableEq X] [Fintype X]
429 (α : FreeGroup X →* Q) (β : Q →* H) [Finite β.ker]
430 (hmag :
431 ∀ w : FreeGroup X,
432 w ∈ (β.comp α).ker →
434 (QuotientGroup.mk' (β.comp α).ker) w = 0 →
436 (F := FreeGroup X) (β.comp α).ker (Nat.card β.ker))
437 {w : FreeGroup X}
438 (hwker : w ∈ (β.comp α).ker)
439 (hder :
441 (QuotientGroup.mk' (β.comp α).ker) w = 0) :
442 (⟨α w, by
443 change β (α w) = 1
444 simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
445 commutator β.ker := by
446 exact
448 (X := X) α β (Nat.card β.ker) (fun _ => pow_card_eq_one') hmag hwker hder
450end
452end FoxDifferential