CrowellExactSequence.Profinite.KernelInjectivity
This module develops the Crowell--Blanchfield--Lyndon exact sequence and its completed coordinate forms.
def profiniteKernelAbelianizationBoundaryHomProCInteger
(C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
(hwell_dN :
CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi) :
ProfiniteKernelAbelianization psi →*
Multiplicative (FoxDifferential.ZCCompletedDifferentialModule C psi.toMonoidHom) :=
QuotientGroup.lift
(Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi)))
(completedKernelBoundaryProCInteger (G := G) (H := H) C psi)
hwell_dNBoundary from the topological kernel abelianization to \(A_{\psi}(C)\), assuming the displayed boundary kills \(\overline{[N,N]}\).
def profiniteKernelAbelianizationBoundaryAddProCInteger
(C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
(hwell_dN :
CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi) :
ProfiniteKernelAbelianizationAdd psi →+
FoxDifferential.ZCCompletedDifferentialModule C psi.toMonoidHom :=
(profiniteKernelAbelianizationBoundaryHomProCInteger
(G := G) (H := H) C psi hwell_dN).toAdditiveLeft
@[simp]Additive boundary from the topological kernel abelianization to \(A_{\psi}(C)\).
theorem profiniteKernelAbelianizationBoundaryAddProCInteger_of
(C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
(hwell_dN :
CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
(n : ProfiniteKernelSubgroup psi) :
profiniteKernelAbelianizationBoundaryAddProCInteger
(G := G) (H := H) C psi hwell_dN
(Additive.ofMul
(QuotientGroup.mk'
(Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n)) =
FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1The \(\mathbb{Z}_C\)-coefficient boundary map is obtained from the profinite kernel abelianization boundary construction.
Show proof
by
rflProof. 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.
□def profiniteKernelAbelianizationBoundaryHomProCIntegerSep
(C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
ProfiniteKernelAbelianization psi →*
Multiplicative
(FoxDifferential.ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom) :=
QuotientGroup.lift
(Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi)))
(separatedCompletedKernelBoundaryProCInteger (G := G) (H := H) C psi)
(separatedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)Separated boundary from the topological kernel abelianization to the finite-stage separated completed differential module. Unlike the algebraic target, this map is well-defined without a separate closedness or continuity hypothesis.
def profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
ProfiniteKernelAbelianizationAdd psi →+
FoxDifferential.ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom :=
(profiniteKernelAbelianizationBoundaryHomProCIntegerSep
(G := G) (H := H) C psi).toAdditiveLeftAdditive separated boundary from the topological kernel abelianization.
def proCKernelAbelianizationBoundaryAddProCIntegerSep
(ProC : ProCGroupPredicate.{u}) (psi : ContinuousMonoidHom G H) :
ProCKernelAbelianizationAdd ProC psi →+
FoxDifferential.ZCSeparatedCompletedDifferentialModule
ProC.finiteQuotientClass psi.toMonoidHom :=
profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := G) (H := H) ProC.finiteQuotientClass psi
@[simp]This declaration introduces the pro-\(C\) notation for the separated topological kernel boundary.
theorem profiniteKernelAbelianizationBoundaryAddProCIntegerSep_of
(C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
(n : ProfiniteKernelSubgroup psi) :
profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := G) (H := H) C psi
(Additive.ofMul
(QuotientGroup.mk'
(Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n)) =
FoxDifferential.zcSeparatedUniversalDifferential C psi.toMonoidHom n.1The separated \(\mathbb{Z}_C\)-coefficient boundary map is obtained from the profinite kernel abelianization boundary construction.
Show proof
by
rflProof. 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 zcDiffModuleToSep_profKerAbBoundaryAddZC
(C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
(hwell_dN :
CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
(x : ProfiniteKernelAbelianizationAdd psi) :
FoxDifferential.zcCompletedDifferentialModuleToSeparated C psi.toMonoidHom
(profiniteKernelAbelianizationBoundaryAddProCInteger
(G := G) (H := H) C psi hwell_dN x) =
profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := G) (H := H) C psi xThe map from the completed differential module to its separated quotient carries the kernel-abelianization boundary to its separated version.
Show proof
by
change
(fun y : ProfiniteKernelAbelianization psi =>
FoxDifferential.zcCompletedDifferentialModuleToSeparated C psi.toMonoidHom
(profiniteKernelAbelianizationBoundaryAddProCInteger
(G := G) (H := H) C psi hwell_dN (Additive.ofMul y)) =
profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := G) (H := H) C psi (Additive.ofMul y))
(Additive.toMul x)
refine QuotientGroup.induction_on (Additive.toMul x) ?_
intro n
change
FoxDifferential.zcCompletedDifferentialModuleToSeparated C psi.toMonoidHom
(profiniteKernelAbelianizationBoundaryAddProCInteger
(G := G) (H := H) C psi hwell_dN
(Additive.ofMul
(QuotientGroup.mk'
(Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n))) =
profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := G) (H := H) C psi
(Additive.ofMul
(QuotientGroup.mk'
(Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n))
rw [profiniteKernelAbelianizationBoundaryAddProCInteger_of,
profiniteKernelAbelianizationBoundaryAddProCIntegerSep_of,
FoxDifferential.zcCompletedDifferentialModuleToSeparated_universal]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. Injectivity follows by applying the separating family of finite-stage projections to the difference of two possible preimages. 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 presentedCompletedToZC_profiniteKernelAbelianizationBoundaryAdd
(C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
(hwell_dN :
CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
(x : ProfiniteKernelAbelianizationAdd psi) :
presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger (G := G) (H := H) C psi
(profiniteKernelAbelianizationBoundaryAddProCInteger
(G := G) (H := H) C psi hwell_dN x) =
0The Crowell--Blanchfield coordinate formula agrees with the quotient-level construction after passage to the separated or completed module.
Show proof
by
change
(fun y : ProfiniteKernelAbelianization psi =>
presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger (G := G) (H := H) C psi
(profiniteKernelAbelianizationBoundaryAddProCInteger
(G := G) (H := H) C psi hwell_dN (Additive.ofMul y)) = 0)
(Additive.toMul x)
refine QuotientGroup.induction_on (Additive.toMul x) ?_
intro n
change
presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger (G := G) (H := H) C psi
(profiniteKernelAbelianizationBoundaryAddProCInteger
(G := G) (H := H) C psi hwell_dN
(Additive.ofMul
(QuotientGroup.mk'
(Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n))) =
0
rw [profiniteKernelAbelianizationBoundaryAddProCInteger_of,
presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger_d_of_mem_ker]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. 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 profKerAbBoundaryAddZC_inj_of_kernel_le_closedCommutator
(C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
(hwell_dN :
CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
(hker :
∀ n : ProfiniteKernelSubgroup psi,
FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 = 0 →
n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) :
Function.Injective
(profiniteKernelAbelianizationBoundaryAddProCInteger
(G := G) (H := H) C psi hwell_dN)Magnus-kernel criterion form of injectivity for the genuine topological kernel boundary. In paper language this is the step \(ker(D|_N) = \overline{[N,N]} \mapsto d_N: N^{\mathrm{ab}}(C) \to A_{\psi}(C)\) is injective.
Show proof
by
intro x y hxy
suffices x - y = 0 by exact sub_eq_zero.mp this
let F :=
profiniteKernelAbelianizationBoundaryAddProCInteger
(G := G) (H := H) C psi hwell_dN
have hmap : F (x - y) = 0 := by
rw [map_sub, hxy, sub_self]
have hzero_of_map_zero :
∀ z : ProfiniteKernelAbelianizationAdd psi, F z = 0 → z = 0 := by
intro z hz
apply Additive.toMul.injective
change (Additive.toMul z : ProfiniteKernelAbelianization psi) = 1
revert hz
change
(fun q : ProfiniteKernelAbelianization psi =>
F (Additive.ofMul q) = 0 → q = 1) (Additive.toMul z)
refine QuotientGroup.induction_on (Additive.toMul z) ?_
intro n hn
change
QuotientGroup.mk'
(Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n = 1
exact (QuotientGroup.eq_one_iff
(N := Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n).2
(by
simpa [Subgroup.closedCommutator, F] using
hker n (by simpa [F] using hn))
exact hzero_of_map_zero (x - y) hmapProof. 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. Injectivity follows by applying the separating family of finite-stage projections to the difference of two possible preimages. 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 profKerAbBoundaryAddZCSep_inj_of_kernel_le_closedCommutator
(C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
(hker :
∀ n : ProfiniteKernelSubgroup psi,
FoxDifferential.zcSeparatedUniversalDifferential C psi.toMonoidHom n.1 = 0 →
n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) :
Function.Injective
(profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := G) (H := H) C psi)Magnus-kernel criterion form of injectivity for the separated topological kernel boundary.
Show proof
by
intro x y hxy
suffices x - y = 0 by exact sub_eq_zero.mp this
let F :=
profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := G) (H := H) C psi
have hmap : F (x - y) = 0 := by
rw [map_sub, hxy, sub_self]
have hzero_of_map_zero :
∀ z : ProfiniteKernelAbelianizationAdd psi, F z = 0 → z = 0 := by
intro z hz
apply Additive.toMul.injective
change (Additive.toMul z : ProfiniteKernelAbelianization psi) = 1
revert hz
change
(fun q : ProfiniteKernelAbelianization psi =>
F (Additive.ofMul q) = 0 → q = 1) (Additive.toMul z)
refine QuotientGroup.induction_on (Additive.toMul z) ?_
intro n hn
change
QuotientGroup.mk'
(Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n = 1
exact (QuotientGroup.eq_one_iff
(N := Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n).2
(by
simpa [Subgroup.closedCommutator, F] using
hker n (by simpa [F] using hn))
exact hzero_of_map_zero (x - y) hmapProof. 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. Injectivity follows by applying the separating family of finite-stage projections to the difference of two possible preimages. 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 kernel_le_closedCommutator_of_profKerAbBoundaryAddZC_inj
(C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
(hwell_dN :
CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi)
(hinj :
Function.Injective
(profiniteKernelAbelianizationBoundaryAddProCInteger
(G := G) (H := H) C psi hwell_dN)) :
∀ n : ProfiniteKernelSubgroup psi,
FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 = 0 →
n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)Injectivity of the genuine topological kernel boundary is exactly the Magnus-kernel criterion in the reverse direction. In paper language this says that once \(d_N: N^{\mathrm{ab}}(C) \to A_{\psi}(C)\) is known to be injective, an element of ker \(\psi\) whose completed Fox differential vanishes is already in \(\overline{[N,N]}\).
Show proof
by
intro n hn
let F :=
profiniteKernelAbelianizationBoundaryAddProCInteger
(G := G) (H := H) C psi hwell_dN
have hzero :
F
(Additive.ofMul
(QuotientGroup.mk'
(Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n)) =
F 0 := by
rw [profiniteKernelAbelianizationBoundaryAddProCInteger_of]
simpa [F] using hn
have hclass :
Additive.ofMul
(QuotientGroup.mk'
(Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n) =
0 :=
hinj hzero
have hmk :
QuotientGroup.mk'
(Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n = 1 := by
simpa using congrArg Additive.toMul hclass
exact (QuotientGroup.eq_one_iff
(N := Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n).1 hmkProof. 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. Injectivity follows by applying the separating family of finite-stage projections to the difference of two possible preimages. 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 profKerAbBoundaryAddZC_inj_iff_kernel_le_closedCommutator
(C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
(hwell_dN :
CompletedBoundaryKillsTopologicalCommutatorProCInteger (G := G) (H := H) C psi) :
Function.Injective
(profiniteKernelAbelianizationBoundaryAddProCInteger
(G := G) (H := H) C psi hwell_dN) ↔
∀ n : ProfiniteKernelSubgroup psi,
FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 = 0 →
n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)Injectivity of \(d_N: N^{\mathrm{ab}}(C) \to A_{\psi}(C)\) is equivalent to the continuous Magnus-kernel criterion.
Show proof
by
constructor
· exact
kernel_le_closedCommutator_of_profKerAbBoundaryAddZC_inj
(G := G) (H := H) C psi hwell_dN
· exact
profKerAbBoundaryAddZC_inj_of_kernel_le_closedCommutator
(G := G) (H := H) C psi hwell_dNProof. 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. Injectivity follows by applying the separating family of finite-stage projections to the difference of two possible preimages. Linear equivalences preserve exactness because composing with an isomorphism does not change kernels or images after transporting them along the equivalence. 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 profKerAbBoundaryAddZC_inj_of_continuous_zcUnivDiff_kernel_le_closedCommutator
(C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
[TopologicalSpace (FoxDifferential.ZCCompletedDifferentialModule C psi.toMonoidHom)]
[T1Space (FoxDifferential.ZCCompletedDifferentialModule C psi.toMonoidHom)]
(hD : Continuous
(fun g : G => FoxDifferential.zcUniversalDifferential C psi.toMonoidHom g))
(hker :
∀ n : ProfiniteKernelSubgroup psi,
FoxDifferential.zcUniversalDifferential C psi.toMonoidHom n.1 = 0 →
n ∈ Subgroup.closedCommutator (ProfiniteKernelSubgroup psi)) :
let hwell_dNContinuous-boundary version of the Magnus-kernel injectivity criterion. This packages the two paper steps that \(d_N\) is well-defined and that \(\ker D|_N \leq \overline{[N,N]}\): continuity of the completed universal differential supplies well-definedness, and the kernel criterion supplies injectivity of the resulting genuine boundary map.
Show proof
completedBoundaryKillsTopCommZC_of_continuous_zcUnivDiff
(G := G) (H := H) C psi hD
Function.Injective
(profiniteKernelAbelianizationBoundaryAddProCInteger
(G := G) (H := H) C psi hwell_dN) := by
let hwell_dN :=
completedBoundaryKillsTopCommZC_of_continuous_zcUnivDiff
(G := G) (H := H) C psi hD
exact
profKerAbBoundaryAddZC_inj_of_kernel_le_closedCommutator
(G := G) (H := H) C psi hwell_dN hkerProof. 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. Injectivity follows by applying the separating family of finite-stage projections to the difference of two possible preimages. 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.
□