import
def finiteFoxStageSemidirectReindexHom
(e : X ≃ Y)
(N : Subgroup (FreeGroup X)) [N.Normal]
(M : Subgroup (FreeGroup Y)) [M.Normal]
(hM : N.map (FreeGroup.freeGroupCongr e).toMonoidHom = M)
(n : ℕ) :
FiniteFoxStageSemidirect (X := X) N n →*
FiniteFoxStageSemidirect (X := Y) M n := by
let φ : FreeGroup X ≃* FreeGroup Y := FreeGroup.freeGroupCongr e
let qXY :
finiteFoxStageTargetQuotient (X := X) N ≃*
finiteFoxStageTargetQuotient (X := Y) M :=
QuotientGroup.congr N M φ hM
exact
{ toFun := fun a =>
{ left := fun y =>
MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n) qXY.toMonoidHom
(a.left (e.symm y))
right := qXY a.right }
map_one' := by
apply FiniteFoxStageSemidirect.ext
· funext y
simp only [MulEquiv.toMonoidHom_eq_coe, FiniteFoxStageSemidirect.one_left, Pi.zero_apply,
MonoidAlgebra.mapDomainRingHom_apply, MonoidHom.coe_coe, Finsupp.mapDomain_zero]
· simp only [FiniteFoxStageSemidirect.one_right, map_one]
map_mul' := by
intro a b
apply FiniteFoxStageSemidirect.ext
· funext y
have hright :
MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n) qXY.toMonoidHom
(MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) a.right) =
MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := Y) M) (qXY a.right) := by
rcases QuotientGroup.mk'_surjective N a.right with ⟨w, hw⟩
rw [← hw]
simp only [MulEquiv.toMonoidHom_eq_coe, MonoidAlgebra.of, MonoidAlgebra.single, QuotientGroup.mk'_apply,
MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, MonoidHom.coe_coe, Finsupp.mapDomain_single]
simp only [MulEquiv.toMonoidHom_eq_coe, FiniteFoxStageSemidirect.mul_left, MonoidAlgebra.of_apply,
Pi.add_apply, Pi.smul_apply, smul_eq_mul, map_add, MonoidAlgebra.mapDomainRingHom_apply, MonoidHom.coe_coe,
add_right_inj]
change
MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n) qXY.toMonoidHom
(MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) a.right *
b.left (e.symm y)) =
MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := Y) M) (qXY a.right) *
MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n) qXY.toMonoidHom
(b.left (e.symm y))
rw [map_mul, hright]
· simp only [FiniteFoxStageSemidirect.mul_right, map_mul, MulEquiv.toMonoidHom_eq_coe,
MonoidAlgebra.mapDomainRingHom_apply, MonoidHom.coe_coe]}Reindex the finite-stage Fox semidirect target along an equivalence of free bases.
theorem finiteFoxStageSemidirectReindexHom_lift
(e : X ≃ Y)
(N : Subgroup (FreeGroup X)) [N.Normal]
(M : Subgroup (FreeGroup Y)) [M.Normal]
(hM : N.map (FreeGroup.freeGroupCongr e).toMonoidHom = M)
(n : ℕ) (w : FreeGroup X) :
finiteFoxStageSemidirectReindexHom (X := X) (Y := Y) e N M hM n
(finiteFoxStageLift (X := X) N n w) =
finiteFoxStageLift (X := Y) M n ((FreeGroup.freeGroupCongr e) w)Show proof
by
let φ : FreeGroup X ≃* FreeGroup Y := FreeGroup.freeGroupCongr e
let qXY :
finiteFoxStageTargetQuotient (X := X) N ≃*
finiteFoxStageTargetQuotient (X := Y) M :=
QuotientGroup.congr N M φ hM
let f₁ : FreeGroup X →* FiniteFoxStageSemidirect (X := Y) M n :=
(finiteFoxStageSemidirectReindexHom (X := X) (Y := Y) e N M hM n).comp
(finiteFoxStageLift (X := X) N n)
let f₂ : FreeGroup X →* FiniteFoxStageSemidirect (X := Y) M n :=
(finiteFoxStageLift (X := Y) M n).comp φ.toMonoidHom
have hf : f₁ = f₂ := by
apply FreeGroup.ext_hom
intro x
apply FiniteFoxStageSemidirect.ext
· funext y
by_cases hy : y = e x
· subst hy
simp only [finiteFoxStageSemidirectReindexHom, MulEquiv.toMonoidHom_eq_coe,
MonoidAlgebra.mapDomainRingHom_apply, MonoidHom.coe_coe, finiteFoxStageLift, QuotientGroup.mk'_apply,
MonoidHom.coe_comp, MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply, FreeGroup.lift_apply_of,
QuotientGroup.congr_mk, FreeGroup.freeGroupCongr_apply, FreeGroup.map.of, Pi.single_eq_same, f₁, f₂, φ]
rw [e.symm_apply_apply, Pi.single_eq_same]
simp only [MonoidAlgebra.mapDomain_one]
· have hne : e.symm y ≠ x := by
intro h
exact hy ((e.apply_symm_apply y).symm.trans (by simp only [h]))
simp only [finiteFoxStageSemidirectReindexHom, MulEquiv.toMonoidHom_eq_coe,
MonoidAlgebra.mapDomainRingHom_apply, MonoidHom.coe_coe, finiteFoxStageLift, QuotientGroup.mk'_apply,
MonoidHom.coe_comp, MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply, FreeGroup.lift_apply_of,
QuotientGroup.congr_mk, FreeGroup.freeGroupCongr_apply, FreeGroup.map.of, Pi.single_eq_of_ne hne,
Finsupp.mapDomain_zero, Pi.single_eq_of_ne hy, f₁, f₂, φ]
· simp only [finiteFoxStageSemidirectReindexHom, MulEquiv.toMonoidHom_eq_coe,
MonoidAlgebra.mapDomainRingHom_apply, MonoidHom.coe_coe, finiteFoxStageLift, QuotientGroup.mk'_apply,
MonoidHom.coe_comp, MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply, FreeGroup.lift_apply_of,
QuotientGroup.congr_mk, FreeGroup.freeGroupCongr_apply, FreeGroup.map.of, f₁, f₂, φ]
exact congrArg (fun f : FreeGroup X →* FiniteFoxStageSemidirect (X := Y) M n => f w) hfProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem finiteFoxStageDerivativeVector_reindex
(e : X ≃ Y)
(N : Subgroup (FreeGroup X)) [N.Normal]
(M : Subgroup (FreeGroup Y)) [M.Normal]
(hM : N.map (FreeGroup.freeGroupCongr e).toMonoidHom = M)
(n : ℕ) (w : FreeGroup X) :
finiteFoxStageDerivativeVector (X := Y) M n ((FreeGroup.freeGroupCongr e) w) =
fun y =>
MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff n)
(QuotientGroup.congr N M (FreeGroup.freeGroupCongr e) hM).toMonoidHom
(finiteFoxStageDerivativeVector (X := X) N n w (e.symm y))Finite-stage Fox derivative vectors reindex along an equivalence of free bases.
Show proof
by
have h :=
congrArg FiniteFoxStageSemidirect.left
(finiteFoxStageSemidirectReindexHom_lift
(X := X) (Y := Y) e N M hM n w)
simpa [finiteFoxStageDerivativeVector, finiteFoxStageSemidirectReindexHom] using h.symmProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem finiteFoxStageDerivativeVector_eq_zero_reindex
(e : X ≃ Y)
(N : Subgroup (FreeGroup X)) [N.Normal]
(M : Subgroup (FreeGroup Y)) [M.Normal]
(hM : N.map (FreeGroup.freeGroupCongr e).toMonoidHom = M)
(n : ℕ) {w : FreeGroup X}
(hw : finiteFoxStageDerivativeVector (X := X) N n w = 0) :
finiteFoxStageDerivativeVector (X := Y) M n ((FreeGroup.freeGroupCongr e) w) = 0Zero of a finite-stage Fox derivative vector is invariant under reindexing the free basis.
Show proof
by
rw [finiteFoxStageDerivativeVector_reindex (X := X) (Y := Y) e N M hM n w]
funext y
simp only [MulEquiv.toMonoidHom_eq_coe, hw, Pi.zero_apply, MonoidAlgebra.mapDomainRingHom_apply,
MonoidHom.coe_coe, Finsupp.mapDomain_zero]Proof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem commutator_subtype_le_finiteFoxCommutatorPowerSubgroup
(N : Subgroup F) (n : ℕ) :
(commutator N).map N.subtype ≤ finiteFoxCommutatorPowerSubgroup (F := F) N nThe ordinary commutator subgroup of \(N\), mapped back to the ambient group, is contained in the finite Fox commutator-power subgroup.
Show proof
by
rw [Subgroup.map_subtype_commutator]
refine Subgroup.commutator_le.mpr ?_
intro a ha b hb
exact Subgroup.subset_normalClosure
(Or.inl ⟨a, ha, b, hb, rfl⟩)Proof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem pow_mem_finiteFoxCommutatorPowerSubgroup
(N : Subgroup F) (n : ℕ) {a : F} (ha : a ∈ N) :
a ^ n ∈ finiteFoxCommutatorPowerSubgroup (F := F) N nNth powers from N are defining relators for the finite Fox commutator-power subgroup.
Show proof
Subgroup.subset_normalClosure (Or.inr ⟨a, ha, rfl⟩)Proof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem mem_finiteFoxCommutatorPowerSubgroup_of_abelianization_eq_pow
(N : Subgroup F) (n : ℕ) {w : F} (hw : w ∈ N) (a : N)
(hclass :
Abelianization.of ⟨w, hw⟩ = (Abelianization.of a) ^ n) :
w ∈ finiteFoxCommutatorPowerSubgroup (F := F) N nIf the abelianization class of a kernel element is an \(n\)-th power, then the element lies in \([N,N]N^n\).
Show proof
by
have hclass' :
Abelianization.of (a ^ n) = Abelianization.of ⟨w, hw⟩ := by
simpa using hclass.symm
have hcommN : (a ^ n)⁻¹ * ⟨w, hw⟩ ∈ commutator N :=
QuotientGroup.eq.mp hclass'
have hcommF :
((a : F) ^ n)⁻¹ * w ∈
finiteFoxCommutatorPowerSubgroup (F := F) N n := by
have hmap :
(((a ^ n)⁻¹ * ⟨w, hw⟩ : N) : F) ∈ (commutator N).map N.subtype :=
⟨(a ^ n)⁻¹ * ⟨w, hw⟩, hcommN, rfl⟩
exact
commutator_subtype_le_finiteFoxCommutatorPowerSubgroup (F := F) N n
(by simpa using hmap)
have hpowF :
(a : F) ^ n ∈ finiteFoxCommutatorPowerSubgroup (F := F) N n :=
pow_mem_finiteFoxCommutatorPowerSubgroup (F := F) N n a.2
have hmul :
(a : F) ^ n * (((a : F) ^ n)⁻¹ * w) ∈
finiteFoxCommutatorPowerSubgroup (F := F) N n :=
(finiteFoxCommutatorPowerSubgroup (F := F) N n).mul_mem hpowF hcommF
simpa [mul_assoc] using hmulProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem ker_finiteFoxStageLift_le_finiteFoxCommutatorPowerSubgroup_iff_residue
[DecidableEq X]
(N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ) :
(finiteFoxStageLift (X := X) N n).ker ≤
finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n ↔
∀ w : FreeGroup X,
w ∈ N →
residueFreeGroupFoxDerivativeVector n (QuotientGroup.mk' N) w = 0 →
w ∈ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N nResidue-Fox form of the finite-stage Magnus reverse inclusion. The finite-stage derivative is not a separate Fox theory: it is the residue free Fox derivative for the quotient map \(\mathrm{FreeGroup}(X) \to F/N\). This is the residue form of the finite Magnus reverse inclusion, expressed through the finite-stage derivative.
Show proof
by
rw [ker_finiteFoxStageLift_le_finiteFoxCommutatorPowerSubgroup_iff]
constructor
· intro h w hwN hder
exact h w hwN (by
simpa [finiteFoxStageDerivativeVector_eq_residueFreeGroupFoxDerivativeVector (X := X) N n]
using hder)
· intro h w hwN hder
exact h w hwN (by
simpa [finiteFoxStageDerivativeVector_eq_residueFreeGroupFoxDerivativeVector (X := X) N n]
using hder)Proof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem ker_finiteFoxStageLift_le_finiteFoxCommutatorPowerSubgroup_iff_residueUniversal
[DecidableEq X] [Fintype X]
(N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ) :
(finiteFoxStageLift (X := X) N n).ker ≤
finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n ↔
∀ w : FreeGroup X,
w ∈ N →
residueUniversalDifferential n (QuotientGroup.mk' N) w = 0 →
w ∈ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N nShow proof
by
rw [ker_finiteFoxStageLift_le_finiteFoxCommutatorPowerSubgroup_iff]
constructor
· intro h w hwN hres
exact h w hwN
((finiteFoxStageDerivativeVector_eq_zero_iff_residueUniversalDifferential_eq_zero
(X := X) N n w).2 hres)
· intro h w hwN hder
exact h w hwN
((finiteFoxStageDerivativeVector_eq_zero_iff_residueUniversalDifferential_eq_zero
(X := X) N n w).1 hder)Proof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem mem_commutator_ker_of_mem_finiteFoxCommutatorPowerSubgroup_of_pow_eq_one
(α : FreeGroup X →* Q) (β : Q →* H) (n : ℕ)
(hpow : ∀ k : β.ker, k ^ n = 1)
{w : FreeGroup X}
(hwker : w ∈ (β.comp α).ker)
(hw :
w ∈ finiteFoxCommutatorPowerSubgroup
(F := FreeGroup X) (β.comp α).ker n) :
(⟨α w, by
change β (α w) = 1
simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
commutator β.kerThe finite commutator-power subgroup maps into the ordinary commutator subgroup of a target kernel whenever the chosen exponent kills that kernel. This is the mathematical quotient bookkeeping needed after the finite-stage Magnus kernel theorem: the commutator relators map to commutators in kernel \(\beta\), while the power relators map to \(1\) by the given exponent-killing hypothesis.
Show proof
by
let K : Subgroup Q := β.ker
let S : Subgroup (FreeGroup X) := (⁅K, K⁆).comap α
have hSnormal : S.Normal := by
dsimp [S, K]
infer_instance
have hrel_le :
finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) (β.comp α).ker n ≤ S := by
refine Subgroup.normalClosure_le_normal ?_
intro g hg
rcases hg with ⟨a, ha, b, hb, rfl⟩ | ⟨a, ha, rfl⟩
· change α ⁅a, b⁆ ∈ ⁅K, K⁆
rw [map_commutatorElement]
have haK : α a ∈ K := by
change β (α a) = 1
simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using ha
have hbK : α b ∈ K := by
change β (α b) = 1
simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hb
exact Subgroup.commutator_mem_commutator haK hbK
· change α (a ^ n) ∈ ⁅K, K⁆
rw [map_pow]
have haK : α a ∈ β.ker := by
change β (α a) = 1
simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using ha
have hpowQ : (α a) ^ n = 1 := by
simpa using congrArg Subtype.val (hpow ⟨α a, haK⟩)
rw [hpowQ]
exact (⁅K, K⁆).one_mem
have hQ : α w ∈ ⁅K, K⁆ := hrel_le hw
have hQmap : α w ∈ (commutator β.ker).map β.ker.subtype := by
simpa [K, Subgroup.map_subtype_commutator] using hQ
rcases hQmap with ⟨c, hc, hcval⟩
have hc_eq :
c =
(⟨α w, by
change β (α w) = 1
simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) := by
apply Subtype.ext
exact hcval
simpa [hc_eq] using hcProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem mem_commutator_ker_of_mem_finiteFoxCommutatorPowerSubgroup_card
(α : FreeGroup X →* Q) (β : Q →* H) [Finite β.ker]
{w : FreeGroup X}
(hwker : w ∈ (β.comp α).ker)
(hw :
w ∈ finiteFoxCommutatorPowerSubgroup
(F := FreeGroup X) (β.comp α).ker (Nat.card β.ker)) :
(⟨α w, by
change β (α w) = 1
simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
commutator β.kerThe finite-kernel cardinality version of the quotient bookkeeping lemma.
Show proof
by
exact
mem_commutator_ker_of_mem_finiteFoxCommutatorPowerSubgroup_of_pow_eq_one
(X := X) α β (Nat.card β.ker) (fun _ => pow_card_eq_one') hwker hwProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem mem_commutator_ker_of_finiteFoxStageDerivativeVector_eq_zero_of_ker_le
[DecidableEq X]
(α : FreeGroup X →* Q) (β : Q →* H) (n : ℕ)
(hpow : ∀ k : β.ker, k ^ n = 1)
(hmag :
(finiteFoxStageLift (X := X) (β.comp α).ker n).ker ≤
finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) (β.comp α).ker n)
{w : FreeGroup X}
(hwker : w ∈ (β.comp α).ker)
(hder :
finiteFoxStageDerivativeVector (X := X) (β.comp α).ker n w = 0) :
(⟨α w, by
change β (α w) = 1
simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
commutator β.kerFinite quotient commutator conclusion from the finite-stage Magnus reverse inclusion. Once the kernel of the finite-stage lift has been identified with \([N,N]N^m\), a zero finite-stage derivative for a representative word gives the ordinary commutator conclusion in kernel \beta.
Show proof
by
have hwrel :
w ∈ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) (β.comp α).ker n :=
hmag
((mem_ker_finiteFoxStageLift_iff (X := X) (β.comp α).ker n).2
⟨hwker, hder⟩)
exact
mem_commutator_ker_of_mem_finiteFoxCommutatorPowerSubgroup_of_pow_eq_one
(X := X) α β n hpow hwker hwrelProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem mem_commutator_ker_of_residueUniversalDifferential_eq_zero_of_kernel_le
[DecidableEq X] [Fintype X]
(α : FreeGroup X →* Q) (β : Q →* H) (n : ℕ)
(hpow : ∀ k : β.ker, k ^ n = 1)
(hmag :
∀ w : FreeGroup X,
w ∈ (β.comp α).ker →
residueUniversalDifferential n (QuotientGroup.mk' (β.comp α).ker) w = 0 →
w ∈ finiteFoxCommutatorPowerSubgroup
(F := FreeGroup X) (β.comp α).ker n)
{w : FreeGroup X}
(hwker : w ∈ (β.comp α).ker)
(hder :
residueUniversalDifferential n (QuotientGroup.mk' (β.comp α).ker) w = 0) :
(⟨α w, by
change β (α w) = 1
simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
commutator β.kerFinite quotient commutator conclusion from the residue-universal finite Magnus kernel statement.
Show proof
by
exact
mem_commutator_ker_of_mem_finiteFoxCommutatorPowerSubgroup_of_pow_eq_one
(X := X) α β n hpow hwker (hmag w hwker hder)Proof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem mem_commutator_ker_of_finiteFoxStageDerivativeVector_eq_zero_of_ker_le_card
[DecidableEq X]
(α : FreeGroup X →* Q) (β : Q →* H) [Finite β.ker]
(hmag :
(finiteFoxStageLift (X := X) (β.comp α).ker (Nat.card β.ker)).ker ≤
finiteFoxCommutatorPowerSubgroup
(F := FreeGroup X) (β.comp α).ker (Nat.card β.ker))
{w : FreeGroup X}
(hwker : w ∈ (β.comp α).ker)
(hder :
finiteFoxStageDerivativeVector (X := X) (β.comp α).ker (Nat.card β.ker) w = 0) :
(⟨α w, by
change β (α w) = 1
simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
commutator β.kerThe cardinality-specialized finite quotient commutator conclusion from the finite-stage Magnus reverse inclusion.
Show proof
by
exact
mem_commutator_ker_of_finiteFoxStageDerivativeVector_eq_zero_of_ker_le
(X := X) α β (Nat.card β.ker) (fun _ => pow_card_eq_one') hmag hwker hderProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□theorem mem_commutator_ker_of_residueUniversalDifferential_eq_zero_of_kernel_le_card
[DecidableEq X] [Fintype X]
(α : FreeGroup X →* Q) (β : Q →* H) [Finite β.ker]
(hmag :
∀ w : FreeGroup X,
w ∈ (β.comp α).ker →
residueUniversalDifferential (Nat.card β.ker)
(QuotientGroup.mk' (β.comp α).ker) w = 0 →
w ∈ finiteFoxCommutatorPowerSubgroup
(F := FreeGroup X) (β.comp α).ker (Nat.card β.ker))
{w : FreeGroup X}
(hwker : w ∈ (β.comp α).ker)
(hder :
residueUniversalDifferential (Nat.card β.ker)
(QuotientGroup.mk' (β.comp α).ker) w = 0) :
(⟨α w, by
change β (α w) = 1
simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
commutator β.kerThe cardinality-specialized finite quotient commutator conclusion from the residue-universal finite Magnus kernel statement.
Show proof
by
exact
mem_commutator_ker_of_residueUniversalDifferential_eq_zero_of_kernel_le
(X := X) α β (Nat.card β.ker) (fun _ => pow_card_eq_one') hmag hwker hderProof. Work at the specified finite Fox stage. The quotient group and coefficient ring are finite, so all group-algebra expressions have finite support and the formulas are checked on group-like basis elements. The crossed-differential rule gives the product, inverse, derivative, and boundary identities; coefficient maps, quotient maps, source/target refinements, relation submodules, and semidirect constructions are then verified coordinatewise and extended by linearity. For stage systems or limit-comparison statements, compatibility under refinement and projection extensionality assemble the coordinate calculations.
□