CrowellExactSequence.Discrete.MagnusComparison
This module develops the Crowell--Blanchfield--Lyndon exact sequence and its completed coordinate forms.
import
theorem d_eq_zero_of_foxDifferential_relativeFreeGroupFoxDerivative_eq_zero
(ψ : FreeGroup X →* H) (w : FreeGroup X)
(hw :
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative
(H := H) X ψ w = 0) :
universalDifferential ψ w = 0If the FoxDifferential relative free Fox derivative of a word vanishes, then the Crowell universal differential of the same word vanishes.
Show proof
by
have hnew :
FoxDifferential.universalDifferential ψ w = 0 := by
have h :=
FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap_derivative
(H := H) X ψ w
rw [hw, map_zero] at h
exact h.symm
change FoxDifferential.universalDifferential ψ w = 0
exact hnewProof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. The augmentation module terms are generated by the chosen basis elements, so equality on those generators determines each coordinate map. The finite-stage exactness assertions are stable under the comparison isomorphisms used to move between separated and unseparated coordinates. Consequently the completed sequence inherits the same exactness calculation. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj
(ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ) (n : ψ.ker)
(hn :
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative
(H := H) X ψ n.1 = 0) :
n ∈ commutator ψ.kerDiscrete Magnus-kernel theorem with the zero condition formulated using the FoxDifferential relative free Fox derivative.
Show proof
mem_commutator_ker_of_d_eq_zero_of_surjective (ψ := ψ) hψ n
(d_eq_zero_of_foxDifferential_relativeFreeGroupFoxDerivative_eq_zero
(X := X) (H := H) ψ n.1 hn)Proof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. The augmentation module terms are generated by the chosen basis elements, so equality on those generators determines each coordinate map. The finite-stage exactness assertions are stable under the comparison isomorphisms used to move between separated and unseparated coordinates. Consequently the completed sequence inherits the same exactness calculation. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem mem_finiteFoxCommutatorPowerSubgroup_of_residueUniversalDifferential_eq_zero
(N : Subgroup (FreeGroup X)) [N.Normal] {n : ℕ} (hn : 0 < n)
{w : FreeGroup X} (hwN : w ∈ N)
(hres :
FoxDifferential.residueUniversalDifferential n (QuotientGroup.mk' N) w = 0) :
w ∈ FoxDifferential.finiteFoxCommutatorPowerSubgroup
(F := FreeGroup X) N nShow proof
by
let Hq := FoxDifferential.finiteFoxStageTargetQuotient (X := X) N
let ψ : FreeGroup X →* Hq := QuotientGroup.mk' N
have hψ : Function.Surjective ψ := by
simpa [ψ] using (QuotientGroup.mk'_surjective N)
obtain ⟨y, hy⟩ :=
FoxDifferential.exists_eq_nsmul_relFreeFoxDeriv_of_residueUnivDiff_eq_zero
(X := X) N hn w hres
have hder :
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := Hq) X ψ w = n • y :=
by simpa [Hq, ψ] using hy
have hwker : w ∈ ψ.ker := by
change ψ w = 1
exact (QuotientGroup.eq_one_iff (N := N) w).2 hwN
have hboundary_derivative :
FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ
(FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := Hq) X ψ w) = 0 := by
have hfund :=
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative_fundamental_formula
(H := Hq) X ψ w
have hgb : groupRingBoundary ψ w = 0 :=
groupRingBoundary_eq_zero_of_mem_ker (ψ := ψ) hwker
rw [hgb] at hfund
simpa [FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary] using hfund.symm
have hboundary_map_nsmul_all :
∀ m : ℕ,
FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ (m • y) =
m • FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ y := by
intro m
induction m with
| zero =>
simp only [zero_nsmul, map_zero]
| succ m ih =>
rw [succ_nsmul, map_add, ih, succ_nsmul]
have hboundary_map_nsmul := hboundary_map_nsmul_all n
have hboundary_nsmul :
n • FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ y = 0 := by
calc
n • FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ y =
FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ (n • y) := by
exact hboundary_map_nsmul.symm
_ = FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ
(FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := Hq) X ψ w) := by
rw [← hder]
_ = 0 := hboundary_derivative
have hboundary_y :
FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ y = 0 :=
FoxDifferential.groupRing_eq_zero_of_nsmul_eq_zero hn
(FoxDifferential.FoxCalculus.relativeFreeGroupFoxBoundary (H := Hq) X ψ y)
hboundary_nsmul
let Y : DifferentialModule ψ :=
FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap (H := Hq) X ψ y
have hYker : toGroupRing ψ Y = 0 := by
have hcomp :=
LinearMap.congr_fun
(FoxDifferential.FoxCalculus.toGroupRing_comp_relativeFreeFoxCoordinatesLinearMap
(H := Hq) X ψ) y
simpa [Y, hboundary_y] using hcomp
letI := kernelAbelianizationModuleOfSurjective ψ hψ
obtain ⟨a, ha⟩ :=
(exact_kernelAbelianizationBoundaryLinearOfSurjective_toGroupRing
(H := Hq) ψ hψ Y).1 hYker
have htoDiff_map_nsmul_all :
∀ m : ℕ,
FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap (H := Hq) X ψ (m • y) =
m • FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap (H := Hq) X ψ y := by
intro m
induction m with
| zero =>
simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, zero_nsmul, map_zero]
| succ m ih =>
rw [succ_nsmul, map_add, ih, succ_nsmul]
have htoDiff_map_nsmul := htoDiff_map_nsmul_all n
have hd_nY : universalDifferential ψ w = n • Y := by
calc
universalDifferential ψ w =
FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap (H := Hq) X ψ
(FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := Hq) X ψ w) := by
exact
(FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap_derivative
(H := Hq) X ψ w).symm
_ = FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap (H := Hq) X ψ
(n • y) := by
rw [hder]
_ = n • Y := by
simpa [Y] using htoDiff_map_nsmul
let nw : ψ.ker := ⟨w, hwker⟩
have hboundary_class :
kernelAbelianizationBoundaryLinearOfSurjective ψ hψ
(Additive.ofMul (Abelianization.of nw)) =
n • kernelAbelianizationBoundaryLinearOfSurjective ψ hψ a := by
calc
kernelAbelianizationBoundaryLinearOfSurjective ψ hψ
(Additive.ofMul (Abelianization.of nw)) =
universalDifferential ψ w := by
rw [kernelAbelianizationBoundaryLinearOfSurjective_of]
_ = n • Y := hd_nY
_ = n • kernelAbelianizationBoundaryLinearOfSurjective ψ hψ a := by
simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, ha]
have hclassAdd :
(Additive.ofMul (Abelianization.of nw) : KernelAbelianizationAdd ψ) = n • a := by
apply kernelAbelianizationBoundaryLinearOfSurjective_injective
(H := Hq) (ψ := ψ) hψ
simpa using hboundary_class
obtain ⟨a0, ha0⟩ := QuotientGroup.mk_surjective (Additive.toMul a)
have ha0' : Abelianization.of a0 = Additive.toMul a := by
simpa [Abelianization.of] using ha0
have hclassMul :
Abelianization.of nw = (Abelianization.of a0) ^ n := by
have hmul := congrArg Additive.toMul hclassAdd
simpa [ha0'] using hmul
have hmemKer :
w ∈ FoxDifferential.finiteFoxCommutatorPowerSubgroup
(F := FreeGroup X) ψ.ker n :=
FoxDifferential.mem_finiteFoxCommutatorPowerSubgroup_of_abelianization_eq_pow
(F := FreeGroup X) ψ.ker n hwker a0 hclassMul
have hker_eq : ψ.ker = N := by
ext g
change ψ g = 1 ↔ g ∈ N
exact QuotientGroup.eq_one_iff (N := N) g
simpa [hker_eq]
using hmemKerProof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. The augmentation module terms are generated by the chosen basis elements, so equality on those generators determines each coordinate map. The finite-stage exactness assertions are stable under the comparison isomorphisms used to move between separated and unseparated coordinates. Consequently the completed sequence inherits the same exactness calculation. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_of_surjective
{C : ProCGroups.FiniteGroupClass}
(hC : ProCGroups.FiniteGroupClass.Hereditary C)
(hForm : ProCGroups.FiniteGroupClass.Formation C)
[TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H]
(hCH : C H)
{Q : Type} [Group Q]
(α : FreeGroup X →* Q) (hα : Function.Surjective α)
(β : Q →* H) (hβ : Function.Surjective β)
(hCker : C β.ker)
{w : FreeGroup X}
(hwker : w ∈ (β.comp α).ker)
(hzero :
FoxDifferential.zcUniversalDifferential C (β.comp α) w = 0) :
(⟨α w, by
change β (α w) = 1
simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
commutator β.kerShow proof
by
exact
FoxDifferential.mem_commutator_ker_of_zcUnivDiff_eq_zero_of_finite_magnus_surj
(C := C) (hC := hC) (X := X) (hForm := hForm) (hCH := hCH)
(α := α) (hα := hα) (β := β) (hβ := hβ) (hCker := hCker)
(fun j _ w hw hres =>
mem_finiteFoxCommutatorPowerSubgroup_of_residueUniversalDifferential_eq_zero
(X := X) (β.comp α).ker j.positive hw hres)
hwker hzeroProof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem mem_commutator_ker_of_finiteFoxStageDerivativeVector_eq_zero
{Q H : Type} [Group Q] [Group H]
(α : FreeGroup X →* Q) (β : Q →* H) (n : ℕ) (hn : 0 < n)
(hpow : ∀ k : β.ker, k ^ n = 1)
{w : FreeGroup X}
(hwker : w ∈ (β.comp α).ker)
(hder :
FoxDifferential.finiteFoxStageDerivativeVector
(X := X) (β.comp α).ker n w = 0) :
(⟨α w, by
change β (α w) = 1
simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
commutator β.kerShow proof
by
have hres :
FoxDifferential.residueUniversalDifferential n
(QuotientGroup.mk' (β.comp α).ker) w = 0 :=
(FoxDifferential.finiteFoxStageDerivativeVector_eq_zero_iff_residueUniversalDifferential_eq_zero
(X := X) (β.comp α).ker n w).1 hder
exact
FoxDifferential.mem_commutator_ker_of_residueUniversalDifferential_eq_zero_of_kernel_le
(X := X) α β n hpow
(fun w hw hres =>
mem_finiteFoxCommutatorPowerSubgroup_of_residueUniversalDifferential_eq_zero
(X := X) (β.comp α).ker hn hw hres)
hwker hres
universe uProof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem mem_commutator_ker_of_finiteFoxStageDerivativeVector_eq_zero_finite
{X : Type u} [Fintype X] [DecidableEq X]
{Q H : Type u} [Group Q] [Group H] [Finite Q] [Finite H]
(α : FreeGroup X →* Q) (β : Q →* H) (n : ℕ) (hn : 0 < n)
(hpow : ∀ k : β.ker, k ^ n = 1)
{w : FreeGroup X}
(hwker : w ∈ (β.comp α).ker)
(hder :
FoxDifferential.finiteFoxStageDerivativeVector
(X := X) (β.comp α).ker n w = 0) :
(⟨α w, by
change β (α w) = 1
simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
commutator β.kerShow proof
by
classical
letI : Finite X := inferInstance
rcases Finite.exists_equiv_fin X with ⟨m, ⟨eX⟩⟩
rcases Finite.exists_type_univ_nonempty_mulEquiv.{u, 0} Q with
⟨Q0, instQ0Group, _instQ0Fintype, ⟨eQ⟩⟩
rcases Finite.exists_type_univ_nonempty_mulEquiv.{u, 0} H with
⟨H0, instH0Group, _instH0Fintype, ⟨eH⟩⟩
letI : Group Q0 := instQ0Group
letI : Group H0 := instH0Group
let phi : FreeGroup X ≃* FreeGroup (Fin m) := FreeGroup.freeGroupCongr eX
let α0 : FreeGroup (Fin m) →* Q0 :=
eQ.toMonoidHom.comp (α.comp phi.symm.toMonoidHom)
let β0 : Q0 →* H0 :=
eH.toMonoidHom.comp (β.comp eQ.symm.toMonoidHom)
let w0 : FreeGroup (Fin m) := phi w
let M0 : Subgroup (FreeGroup (Fin m)) :=
(β0.comp α0).ker
haveI : M0.Normal := by
dsimp [M0]
infer_instance
have hM0 : (β.comp α).ker.map phi.toMonoidHom = M0 := by
ext z
constructor
· rintro ⟨x, hx, rfl⟩
change β0 (α0 (phi x)) = 1
change β (α x) = 1 at hx
have hphi : phi.symm (phi x) = x := phi.symm_apply_apply x
simpa [β0, α0, M0, hphi] using congrArg eH hx
· intro hz
refine ⟨phi.symm z, ?_, ?_⟩
· change β (α (phi.symm z)) = 1
have hz' : eH (β (α (phi.symm z))) = 1 := by
simpa [β0, α0, M0] using hz
exact eH.injective (by simpa using hz')
· exact phi.apply_symm_apply z
have hwker0 : w0 ∈ (β0.comp α0).ker := by
change β0 (α0 w0) = 1
change β (α w) = 1 at hwker
have hphi : phi.symm (phi w) = w := phi.symm_apply_apply w
simpa [β0, α0, w0, hphi] using congrArg eH hwker
have hderM0 :
FoxDifferential.finiteFoxStageDerivativeVector
(X := Fin m) M0 n w0 = 0 := by
simpa [M0, w0, phi] using
FoxDifferential.finiteFoxStageDerivativeVector_eq_zero_reindex
(X := X) (Y := Fin m) eX (β.comp α).ker M0 hM0 n hder
have hder0 :
FoxDifferential.finiteFoxStageDerivativeVector
(X := Fin m) (β0.comp α0).ker n w0 = 0 := by
simpa [M0] using hderM0
have hpow0 : ∀ k : β0.ker, k ^ n = 1 := by
intro k
have hkβ : β (eQ.symm k.1) = 1 := by
have hk0 : β0 k.1 = 1 := by
change β0 k.1 = 1
exact k.2
have hk : eH (β (eQ.symm k.1)) = 1 := by
simpa [β0] using hk0
exact eH.injective (by simpa using hk)
have hkpow := hpow ⟨eQ.symm k.1, hkβ⟩
have hkpow' : (eQ.symm k.1) ^ n = 1 :=
congrArg Subtype.val hkpow
have := congrArg eQ hkpow'
apply Subtype.ext
simpa using this
let q0 : β0.ker :=
⟨α0 w0, by
change β0 (α0 w0) = 1
simpa [MonoidHom.mem_ker] using hwker0⟩
have hcomm0 : q0 ∈ commutator β0.ker := by
simpa [q0] using
mem_commutator_ker_of_finiteFoxStageDerivativeVector_eq_zero
(X := Fin m) α0 β0 n hn hpow0 hwker0 hder0
let κ : β0.ker →* β.ker :=
{ toFun := fun k =>
⟨eQ.symm k.1, by
change β (eQ.symm k.1) = 1
have hk0 : β0 k.1 = 1 := by
change β0 k.1 = 1
exact k.2
have hk : eH (β (eQ.symm k.1)) = 1 := by
simpa [β0] using hk0
exact eH.injective (by simpa using hk)⟩
map_one' := by
apply Subtype.ext
simp only [OneMemClass.coe_one, map_one]
map_mul' := by
intro a b
apply Subtype.ext
simp only [Subgroup.coe_mul, map_mul, MulMemClass.mk_mul_mk]}
have hcomm_map : (commutator β0.ker).map κ ≤ commutator β.ker := by
rw [_root_.map_commutator_eq]
exact Subgroup.commutator_mono (by intro x hx; trivial) (by intro x hx; trivial)
have hκq0 :
κ q0 =
(⟨α w, by
change β (α w) = 1
simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) := by
apply Subtype.ext
have hphi : phi.symm (phi w) = w := phi.symm_apply_apply w
simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply, hphi,
MonoidHom.coe_mk, OneHom.coe_mk, MulEquiv.symm_apply_apply, κ, q0, α0, w0]
have hκcomm : κ q0 ∈ commutator β.ker :=
hcomm_map ⟨q0, hcomm0, rfl⟩
simpa [hκq0] using hκcommProof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. Linear equivalences preserve exactness because composing with an isomorphism does not change kernels or images after transporting them along the equivalence. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. The augmentation module terms are generated by the chosen basis elements, so equality on those generators determines each coordinate map. The finite-stage exactness assertions are stable under the comparison isomorphisms used to move between separated and unseparated coordinates. Consequently the completed sequence inherits the same exactness calculation. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj_factor
{Q : Type} [Group Q]
(α : FreeGroup X →* Q) (hα : Function.Surjective α)
(β : Q →* H) (hβ : Function.Surjective β)
(q : β.ker) (w : FreeGroup X) (hw : α w = q.1)
(hn :
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative
(H := H) X (β.comp α) w = 0) :
q ∈ commutator β.kerDiscrete Magnus descent through a surjective finite source quotient, with the hypothesis expressed as ordinary relative Fox derivative zero for a representative word.
Show proof
by
let ψ : FreeGroup X →* H := β.comp α
have hψ : Function.Surjective ψ := by
intro h
rcases hβ h with ⟨q0, rfl⟩
rcases hα q0 with ⟨w0, rfl⟩
exact ⟨w0, rfl⟩
have hwker : w ∈ ψ.ker := by
change β (α w) = 1
rw [hw]
exact q.2
let n : ψ.ker := ⟨w, hwker⟩
have hncomm : n ∈ commutator ψ.ker :=
mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj
(X := X) (H := H) ψ hψ n (by simpa [ψ, n] using hn)
let κ : ψ.ker →* β.ker := {
toFun := fun n => ⟨α n.1, by
change β (α n.1) = 1
change ψ n.1 = 1
exact n.2⟩
map_one' := by
apply Subtype.ext
simp only [OneMemClass.coe_one, map_one]
map_mul' := by
intro n₁ n₂
apply Subtype.ext
simp only [Subgroup.coe_mul, map_mul, MulMemClass.mk_mul_mk]}
have hκn : κ n = q := by
apply Subtype.ext
exact hw
have hcomm_map :
(commutator ψ.ker).map κ ≤ commutator β.ker := by
rw [_root_.map_commutator_eq]
exact Subgroup.commutator_mono (by intro x hx; trivial) (by intro x hx; trivial)
simpa [hκn] using hcomm_map ⟨n, hncomm, rfl⟩Proof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. The augmentation module terms are generated by the chosen basis elements, so equality on those generators determines each coordinate map. The finite-stage exactness assertions are stable under the comparison isomorphisms used to move between separated and unseparated coordinates. Consequently the completed sequence inherits the same exactness calculation. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_allFinite
(N : Subgroup (FreeGroup X)) [N.Normal]
[TopologicalSpace (FoxDifferential.finiteFoxStageTargetQuotient (X := X) N)]
[DiscreteTopology (FoxDifferential.finiteFoxStageTargetQuotient (X := X) N)]
[IsTopologicalGroup (FoxDifferential.finiteFoxStageTargetQuotient (X := X) N)]
[Finite (FoxDifferential.finiteFoxStageTargetQuotient (X := X) N)]
(n : (QuotientGroup.mk' N).ker)
(hn :
FoxDifferential.zcUniversalDifferential
(ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass)
(QuotientGroup.mk' N) n.1 = 0) :
n ∈ commutator (QuotientGroup.mk' N).kerOver the all-finite coefficient class, vanishing of the completed universal differential on a finite target quotient implies the ordinary discrete Magnus commutator conclusion.
Show proof
by
exact
mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj
(X := X)
(H := FoxDifferential.finiteFoxStageTargetQuotient (X := X) N)
(QuotientGroup.mk' N)
(QuotientGroup.mk'_surjective N)
n
(FoxDifferential.relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_allFinite
(X := X) N n.1 hn)Proof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_allFinite_of_surjective
[TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H] [Finite H]
(ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
(n : ψ.ker)
(hn :
FoxDifferential.zcUniversalDifferential
(ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass)
ψ n.1 = 0) :
n ∈ commutator ψ.kerOver the all-finite coefficient class, vanishing of the completed universal differential for any surjective finite target map implies the ordinary discrete Magnus commutator conclusion.
Show proof
by
exact
mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj
(X := X) (H := H) ψ hψ n
(FoxDifferential.relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_allFinite_of_surj
(X := X) ψ hψ n.1 hn)Proof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem mem_commutator_ker_of_zcFreeFoxDerivVec_eq_zero_allFinite_of_surj_factor
{Q : Type} [Group Q]
[TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H] [Finite H]
(α : FreeGroup X →* Q) (hα : Function.Surjective α)
(β : Q →* H) (hβ : Function.Surjective β)
(q : β.ker) (w : FreeGroup X) (hw : α w = q.1)
(hn :
FoxDifferential.zcFreeGroupFoxDerivativeVector
(ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass)
(β.comp α) w = 0) :
q ∈ commutator β.kerAll-finite discrete Magnus descent through a surjective finite source quotient, with the hypothesis expressed as zero of the completed Fox derivative vector for the representative word.
Show proof
by
let ψ : FreeGroup X →* H := β.comp α
have hψ : Function.Surjective ψ := by
intro h
rcases hβ h with ⟨q0, rfl⟩
rcases hα q0 with ⟨w0, rfl⟩
exact ⟨w0, rfl⟩
exact
mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj_factor
(X := X) (H := H) α hα β hβ q w hw
(FoxDifferential.relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_allFinite_of_surj
(X := X) ψ hψ w (by simpa [ψ] using hn))Proof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem mem_commutator_ker_of_zcUnivDiff_eq_zero_allFinite_of_surj_factor
{Q : Type} [Group Q]
[TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H] [Finite H]
(α : FreeGroup X →* Q) (hα : Function.Surjective α)
(β : Q →* H) (hβ : Function.Surjective β)
(q : β.ker) (w : FreeGroup X) (hw : α w = q.1)
(hn :
FoxDifferential.zcUniversalDifferential
(ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass)
(β.comp α) w = 0) :
q ∈ commutator β.kerAll-finite discrete Magnus descent through a surjective finite source quotient. If a surjective free-group map \(\alpha: \mathrm{FreeGroup}(X) \to Q\) presents a finite-stage source and \(\beta: Q \to H\) is a surjective target map, vanishing of the completed universal differential on a representative word of \(q \in \ker \beta\) forces \(q\) into the commutator subgroup of \(\ker \beta\).
Show proof
by
exact
mem_commutator_ker_of_zcFreeFoxDerivVec_eq_zero_allFinite_of_surj_factor
(X := X) (H := H) α hα β hβ q w hw
(FoxDifferential.zcFreeGroupFoxDerivativeVector_eq_zero_of_zcUniversalDifferential_eq_zero
(C := (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass))
(β.comp α) hn)Proof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_pGroup
(p : ℕ) [Fact (Nat.Prime p)]
(N : Subgroup (FreeGroup X)) [N.Normal]
[TopologicalSpace (FoxDifferential.finiteFoxStageTargetQuotient (X := X) N)]
[DiscreteTopology (FoxDifferential.finiteFoxStageTargetQuotient (X := X) N)]
[IsTopologicalGroup (FoxDifferential.finiteFoxStageTargetQuotient (X := X) N)]
(hCtarget :
ProCGroups.FiniteGroupClass.pGroup p
(FoxDifferential.finiteFoxStageTargetQuotient (X := X) N))
(n : (QuotientGroup.mk' N).ker)
(hn :
FoxDifferential.zcUniversalDifferential
(ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass)
(QuotientGroup.mk' N) n.1 = 0) :
n ∈ commutator (QuotientGroup.mk' N).kerOver the finite \(p\)-group coefficient class, vanishing of the completed universal differential on a finite \(p\)-group target quotient implies the ordinary discrete Magnus commutator conclusion.
Show proof
by
exact
mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj
(X := X)
(H := FoxDifferential.finiteFoxStageTargetQuotient (X := X) N)
(QuotientGroup.mk' N)
(QuotientGroup.mk'_surjective N)
n
(FoxDifferential.relativeFreeGroupFoxDerivative_eq_zero_of_zcUniversalDifferential_eq_zero_pGroup
(X := X) (N := N) (p := p) (hCtarget := hCtarget) (w := n.1) hn)Proof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_pGroup_of_surjective
(p : ℕ) [Fact (Nat.Prime p)]
[TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H]
(hCtarget : ProCGroups.FiniteGroupClass.pGroup p H)
(ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
(n : ψ.ker)
(hn :
FoxDifferential.zcUniversalDifferential
(ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass)
ψ n.1 = 0) :
n ∈ commutator ψ.kerOver the finite \(p\)-group coefficient class, vanishing of the completed universal differential for any surjective finite \(p\)-group target map implies the ordinary discrete Magnus commutator conclusion.
Show proof
by
exact
mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj
(X := X) (H := H) ψ hψ n
(FoxDifferential.relFreeFoxDeriv_eq_zero_of_zcUnivDiff_eq_zero_pGroup_of_surj
(X := X) (H := H) (p := p) (hCtarget := hCtarget)
(ψ := ψ) (hψ := hψ) (w := n.1) hn)Proof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem mem_commutator_ker_of_zcFreeFoxDerivVec_eq_zero_pGroup_of_surj_factor
(p : ℕ) [Fact (Nat.Prime p)]
{Q : Type} [Group Q]
[TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H]
(hCtarget : ProCGroups.FiniteGroupClass.pGroup p H)
(α : FreeGroup X →* Q) (hα : Function.Surjective α)
(β : Q →* H) (hβ : Function.Surjective β)
(q : β.ker) (w : FreeGroup X) (hw : α w = q.1)
(hn :
FoxDifferential.zcFreeGroupFoxDerivativeVector
(ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass)
(β.comp α) w = 0) :
q ∈ commutator β.kerFinite-p discrete Magnus descent through a surjective finite source quotient, with the hypothesis expressed as zero of the completed Fox derivative vector for the representative word.
Show proof
by
let ψ : FreeGroup X →* H := β.comp α
have hψ : Function.Surjective ψ := by
intro h
rcases hβ h with ⟨q0, rfl⟩
rcases hα q0 with ⟨w0, rfl⟩
exact ⟨w0, rfl⟩
exact
mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj_factor
(X := X) (H := H) α hα β hβ q w hw
(FoxDifferential.relFreeFoxDeriv_eq_zero_of_zcFreeFoxDerivVec_eq_zero_pGroup_of_surj
(X := X) (H := H) (p := p) (hCtarget := hCtarget)
(ψ := ψ) (hψ := hψ) (w := w) (by simpa [ψ] using hn))Proof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem mem_commutator_ker_of_zcUnivDiff_eq_zero_pGroup_of_surj_factor
(p : ℕ) [Fact (Nat.Prime p)]
{Q : Type} [Group Q]
[TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H]
(hCtarget : ProCGroups.FiniteGroupClass.pGroup p H)
(α : FreeGroup X →* Q) (hα : Function.Surjective α)
(β : Q →* H) (hβ : Function.Surjective β)
(q : β.ker) (w : FreeGroup X) (hw : α w = q.1)
(hn :
FoxDifferential.zcUniversalDifferential
(ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass)
(β.comp α) w = 0) :
q ∈ commutator β.kerFinite-p discrete Magnus descent through a surjective finite source quotient.
Show proof
by
exact
mem_commutator_ker_of_zcFreeFoxDerivVec_eq_zero_pGroup_of_surj_factor
(X := X) (H := H) p hCtarget α hα β hβ q w hw
(FoxDifferential.zcFreeGroupFoxDerivativeVector_eq_zero_of_zcUniversalDifferential_eq_zero
(C := (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass))
(β.comp α) hn)Proof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□