CrowellExactSequence.Profinite.FreeExactness
This module develops the Crowell--Blanchfield--Lyndon exact sequence and its completed coordinate forms.
import
theorem freeProC_presentedCrowellGroupAlgebraExactProCInteger_of_psi_surjective
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi) :
Function.Exact
(presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi)
(zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H)For surjective \(\psi\), the presented Crowell group-algebra sequence over the pro-\(C\) integers is exact.
Show proof
by
letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
⟨by
intro Q _ hQ
exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
let family : Fin r → sourceData.carrier :=
freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis
have htargetGen :
ProCGroups.Generation.TopologicallyGenerates
(G := H) (Set.range (fun i : Fin r => psi (family i))) := by
simpa [family] using
freeProCChosenFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsi
exact
exact_presentedCompletedToZC_of_boundary_family_topologicallyGenerates
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
(ProCGroupPredicate.finiteQuotientFormation ProC) psi family htargetGenProof. 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 freeProC_presentedSeparatedCrowellGroupAlgebraExactProCInteger_of_psi_surjective
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi) :
Function.Exact
(presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi)
(zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H)For surjective \(\psi\), the separated presented Crowell group-algebra sequence over the pro-\(C\) integers is exact.
Show proof
by
letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
⟨by
intro Q _ hQ
exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
let family : Fin r → sourceData.carrier :=
freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis
have htargetGen :
ProCGroups.Generation.TopologicallyGenerates
(G := H) (Set.range (fun i : Fin r => psi (family i))) := by
simpa [family] using
freeProCChosenFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsi
exact
exact_presentedSepToZC_of_boundary_family_topologicallyGenerates
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
(ProCGroupPredicate.finiteQuotientHereditary ProC)
(ProCGroupPredicate.finiteQuotientFormation ProC) psi family htargetGenProof. 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 freeProCClosedGeneratedTarget_proC_of_surjective
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.HasFiniteQuotientHereditary] [ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi) :
ProC
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)) : Subgroup
(ZCCompletedFoxSemidirect
ProC.finiteQuotientClass (ULift.{u} (Fin r)) H)))For a surjective map from a free pro-\(C\) group, the closed-generated target is again pro-\(C\).
Show proof
by
let family : ULift.{u} (Fin r) → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
letI : ProCGroup ProC H :=
ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi
letI : ProCGroup ProC
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass (ULift.{u} (Fin r)) H) :=
FoxDifferential.proCGroup_zcCompletedFoxSemidirect
(X := ULift.{u} (Fin r)) (H := H) ProC
simpa [family] using
FoxDifferential.freeProCZCCompletedFoxSemidirectClosedGeneratedTarget_proC
(ProC := ProC)
(fun i : ULift.{u} (Fin r) => psi (family i))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. 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 surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage.
□theorem freeProC_zcDiffModuleStageProjsSeparate_of_finiteRelationReductionsReflectRelations
(sourceData : FreeProCSourceData ProC)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hreflect :
zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations
ProC.finiteQuotientClass psi.toMonoidHom) :
zcCompletedDifferentialModuleStageProjectionsSeparate
ProC.finiteQuotientClass psi.toMonoidHomShow proof
zcDiffModuleStageProjsSeparate_of_preStageProjsSeparate
ProC.finiteQuotientClass psi.toMonoidHom
((zcDiffModulePreStageProjsSeparate_iff_finiteRelationReductionsReflectRelations
ProC.finiteQuotientClass psi.toMonoidHom).2 hreflect)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. 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. 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 freeProC_t2Space_zcDiffModuleNaturalTopology_of_finiteRelationReductionsReflectRelations
(sourceData : FreeProCSourceData ProC)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hreflect :
zcCompletedDifferentialModuleFiniteRelationReductionsReflectRelations
ProC.finiteQuotientClass psi.toMonoidHom) :
@T2Space
(ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
(zcCompletedDifferentialModuleNaturalTopology
ProC.finiteQuotientClass psi.toMonoidHom)Show proof
t2Space_zcCompletedDifferentialModuleNaturalTopology_of_separating
ProC.finiteQuotientClass psi.toMonoidHom
(freeProC_zcDiffModuleStageProjsSeparate_of_finiteRelationReductionsReflectRelations
(H := H) (ProC := ProC) sourceData psi hreflect)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 freeProC_zcDiffModuleStageProjsSeparate_of_relSubmoduleClosed
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientHereditary]
(sourceData : FreeProCSourceData ProC)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hclosed :
zcCompletedDifferentialModuleRelationSubmoduleClosed
ProC.finiteQuotientClass psi.toMonoidHom) :
zcCompletedDifferentialModuleStageProjectionsSeparate
ProC.finiteQuotientClass psi.toMonoidHomClosedness of the completed relation submodule implies that finite-stage projections separate points of the completed differential module.
Show proof
by
letI :
Nonempty
(ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :=
⟨zcCompletedDifferentialModuleComapIndex
(C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi
((ProCGroups.Completion.ProCIntegerIndex.terminal
(C := ProC.finiteQuotientClass) inferInstance),
zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩
have hdir :
Directed (· ≤ ·)
(id :
ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom →
ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :=
directed_zcCompletedDifferentialModuleIndex
(C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
(ProCGroupPredicate.finiteQuotientFormation ProC)
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi
exact
freeProC_zcDiffModuleStageProjsSeparate_of_finiteRelationReductionsReflectRelations
(H := H) (ProC := ProC) sourceData psi
(zcDiffModuleFiniteRelationReductionsReflectRelations_of_relSubmoduleClosed
ProC.finiteQuotientClass psi.toMonoidHom hdir hclosed)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 freeProC_t2Space_zcDiffModuleNaturalTopology_of_relSubmoduleClosed
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientHereditary]
(sourceData : FreeProCSourceData ProC)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hclosed :
zcCompletedDifferentialModuleRelationSubmoduleClosed
ProC.finiteQuotientClass psi.toMonoidHom) :
@T2Space
(ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
(zcCompletedDifferentialModuleNaturalTopology
ProC.finiteQuotientClass psi.toMonoidHom)Closedness of the completed relation submodule makes the natural topology on the completed differential module Hausdorff.
Show proof
t2Space_zcCompletedDifferentialModuleNaturalTopology_of_separating
ProC.finiteQuotientClass psi.toMonoidHom
(freeProC_zcDiffModuleStageProjsSeparate_of_relSubmoduleClosed
(H := H) (ProC := ProC) sourceData psi hclosed)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 freeProC_zcDiffModuleRelSubmoduleClosed_iff_stageProjsSeparate
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientHereditary]
(sourceData : FreeProCSourceData ProC)
(psi : ContinuousMonoidHom sourceData.carrier H) :
zcCompletedDifferentialModuleRelationSubmoduleClosed
ProC.finiteQuotientClass psi.toMonoidHom ↔
zcCompletedDifferentialModuleStageProjectionsSeparate
ProC.finiteQuotientClass psi.toMonoidHomClosedness of the completed relation submodule is equivalent to separation by all finite-stage projections.
Show proof
by
letI :
Nonempty
(ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :=
⟨zcCompletedDifferentialModuleComapIndex
(C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi
((ProCGroups.Completion.ProCIntegerIndex.terminal
(C := ProC.finiteQuotientClass) inferInstance),
zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩
have hdir :
Directed (· ≤ ·)
(id :
ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom →
ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :=
directed_zcCompletedDifferentialModuleIndex
(C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
(ProCGroupPredicate.finiteQuotientFormation ProC)
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi
exact
zcDiffModuleRelSubmoduleClosed_iff_stageProjsSeparate
ProC.finiteQuotientClass psi.toMonoidHom hdirProof. 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 freeProC_zcDiffModuleRelSubmoduleClosed_iff_t2_naturalTopology
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientHereditary]
(sourceData : FreeProCSourceData ProC)
(psi : ContinuousMonoidHom sourceData.carrier H) :
zcCompletedDifferentialModuleRelationSubmoduleClosed
ProC.finiteQuotientClass psi.toMonoidHom ↔
@T2Space
(ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
(zcCompletedDifferentialModuleNaturalTopology
ProC.finiteQuotientClass psi.toMonoidHom)Closedness of the completed relation submodule is equivalent to the natural topology being Hausdorff.
Show proof
by
letI :
Nonempty
(ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :=
⟨zcCompletedDifferentialModuleComapIndex
(C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi
((ProCGroups.Completion.ProCIntegerIndex.terminal
(C := ProC.finiteQuotientClass) inferInstance),
zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩
have hdir :
Directed (· ≤ ·)
(id :
ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom →
ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :=
directed_zcCompletedDifferentialModuleIndex
(C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
(ProCGroupPredicate.finiteQuotientFormation ProC)
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi
exact
zcCompletedDifferentialModuleRelationSubmoduleClosed_iff_t2_naturalTopology
ProC.finiteQuotientClass psi.toMonoidHom hdirProof. 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 freeProC_hmodule_continuous_naturalTopology
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi) :
@Continuous sourceData.carrier
(ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
inferInstance
(zcCompletedDifferentialModuleNaturalTopology
ProC.finiteQuotientClass psi.toMonoidHom)
(fun g : sourceData.carrier =>
presentedCompletedDifferentialFamilyMapProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
(freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC)
(freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i))
(freeProCClosedGeneratedTarget_proC_of_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi)
(freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)))
g))The Crowell--Blanchfield coordinate formula agrees with the quotient-level construction after passage to the separated or completed module.
Show proof
by
let family : ULift.{u} (Fin r) → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
let hfree :=
freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
let htarget :=
freeProCClosedGeneratedTarget_proC_of_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
let hφconv :=
freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
simpa [family, hfree, htarget, hφconv] using
continuous_closedGenerated_module_expansion_naturalTopology
(G := sourceData.carrier) (H := H) ProC psi family hfree htarget hφconvProof. 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 freeProCChosenULift_closedGeneratedCoordinateMap
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi) :
ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom →ₗ[
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
ZCFreeFoxCoordinates ProC.finiteQuotientClass
(X := ULift.{u} (Fin r)) (H := H) := by
letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
⟨by
intro Q _ hQ
exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
let family : ULift.{u} (Fin r) → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
let hfree :=
freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
let htarget :=
freeProCClosedGeneratedTarget_proC_of_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
let hφconv :=
freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
have hH : ProC (G := H) :=
(ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi).isProC
have hφHconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_convergesToOne
(ProC := ProC) sourceData hbasis psi.toMonoidHom
have hφHgen :
ProCGroups.Generation.TopologicallyGenerates
(G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsi
exact
closedGeneratedDerivativeCoordinatesLinearMapProCInteger
(G := sourceData.carrier) (H := H) ProC psi family hfree htarget hφconv
hH hφHconv hφHgenThe coordinate map determined by the chosen \(U\)-lifts has the specified closed generated image.
def freeProCChosenULift_sepFamilyMap
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H) :
ZCFreeFoxCoordinates ProC.finiteQuotientClass
(X := ULift.{u} (Fin r)) (H := H) →ₗ[
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
ZCSeparatedCompletedDifferentialModule
ProC.finiteQuotientClass psi.toMonoidHom :=
presentedSeparatedDifferentialFamilyMapProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)The separated finite-family map sends lifted chosen-basis coordinates to the separated completed differential module.
theorem freeProCChosenULift_sepFamilyMap_single
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(i : ULift.{u} (Fin r)) :
freeProCChosenULift_sepFamilyMap
(H := H) (ProC := ProC) sourceData hbasis psi
(Pi.single i (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) =
zcSeparatedUniversalDifferential
ProC.finiteQuotientClass psi.toMonoidHom
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i)The Crowell--Blanchfield coordinate formula agrees with the quotient-level construction after passage to the separated or completed module.
Show proof
by
exact
presentedSeparatedDifferentialFamilyMapProCInteger_single
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis) iProof. 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. 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 freeProCChosenULift_sepCoordinateMap
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
[T1Space
(ZCFreeFoxCoordinates ProC.finiteQuotientClass
(X := ULift.{u} (Fin r)) (H := H))] :
ZCSeparatedCompletedDifferentialModule
ProC.finiteQuotientClass psi.toMonoidHom →ₗ[
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
ZCFreeFoxCoordinates ProC.finiteQuotientClass
(X := ULift.{u} (Fin r)) (H := H) := by
letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
⟨by
intro Q _ hQ
exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
letI :
Nonempty
(ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :=
⟨zcCompletedDifferentialModuleComapIndex
(C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi
((ProCGroups.Completion.ProCIntegerIndex.terminal
(C := ProC.finiteQuotientClass) inferInstance),
zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩
have hdir :
Directed (· ≤ ·)
(id :
ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom →
ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :=
directed_zcCompletedDifferentialModuleIndex
(C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
(ProCGroupPredicate.finiteQuotientFormation ProC)
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi
let family : ULift.{u} (Fin r) → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
let hfree :=
freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
let htarget :=
freeProCClosedGeneratedTarget_proC_of_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
let hφconv :=
freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
have hH : ProC (G := H) :=
(ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi).isProC
have hφHconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_convergesToOne
(ProC := ProC) sourceData hbasis psi.toMonoidHom
have hφHgen :
ProCGroups.Generation.TopologicallyGenerates
(G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsi
exact
separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger
(G := sourceData.carrier) (H := H) ProC psi family hfree htarget hφconv
hdir sourceData.proCGroup.isProCGroup hH hφHconv hφHgenThe separated closed-generated coordinate map for the chosen finite free pro-\(C\) basis.
theorem freeProCChosenULift_sepCoordinateMap_universal
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
[T1Space
(ZCFreeFoxCoordinates ProC.finiteQuotientClass
(X := ULift.{u} (Fin r)) (H := H))]
(g : sourceData.carrier) :
freeProCChosenULift_sepCoordinateMap
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
(zcSeparatedUniversalDifferential
ProC.finiteQuotientClass psi.toMonoidHom g) =
freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC)
(freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i))
(freeProCClosedGeneratedTarget_proC_of_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi)
(freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i)))
gThe separated coordinate map sends the separated universal differential to the closed-generated Fox derivative vector.
Show proof
by
letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
⟨by
intro Q _ hQ
exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
letI :
Nonempty
(ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :=
⟨zcCompletedDifferentialModuleComapIndex
(C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi
((ProCGroups.Completion.ProCIntegerIndex.terminal
(C := ProC.finiteQuotientClass) inferInstance),
zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩
have hdir :
Directed (· ≤ ·)
(id :
ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom →
ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :=
directed_zcCompletedDifferentialModuleIndex
(C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
(ProCGroupPredicate.finiteQuotientFormation ProC)
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi
let family : ULift.{u} (Fin r) → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
let hfree :=
freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
let htarget :=
freeProCClosedGeneratedTarget_proC_of_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
let hφconv :=
freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
have hH : ProC (G := H) :=
(ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi).isProC
have hφHconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_convergesToOne
(ProC := ProC) sourceData hbasis psi.toMonoidHom
have hφHgen :
ProCGroups.Generation.TopologicallyGenerates
(G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsi
simpa [freeProCChosenULift_sepCoordinateMap, family, hfree, htarget, hφconv] using
separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger_universal
(G := sourceData.carrier) (H := H) ProC psi family hfree htarget hφconv
hdir sourceData.proCGroup.isProCGroup hH hφHconv hφHgen gProof. 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. 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.
□def freeProCChosenULift_sepCoordinateEquiv
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
[T1Space
(ZCFreeFoxCoordinates ProC.finiteQuotientClass
(X := ULift.{u} (Fin r)) (H := H))] :
ZCSeparatedCompletedDifferentialModule
ProC.finiteQuotientClass psi.toMonoidHom ≃ₗ[
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
ZCFreeFoxCoordinates ProC.finiteQuotientClass
(X := ULift.{u} (Fin r)) (H := H) := by
letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
⟨by
intro Q _ hQ
exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
letI :
Nonempty
(ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :=
⟨zcCompletedDifferentialModuleComapIndex
(C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi
((ProCGroups.Completion.ProCIntegerIndex.terminal
(C := ProC.finiteQuotientClass) inferInstance),
zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩
have hdir :
Directed (· ≤ ·)
(id :
ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom →
ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :=
directed_zcCompletedDifferentialModuleIndex
(C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
(ProCGroupPredicate.finiteQuotientFormation ProC)
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi
let family : ULift.{u} (Fin r) → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
let hfree :=
freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
let htarget :=
freeProCClosedGeneratedTarget_proC_of_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
let hφconv :=
freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
have hH : ProC (G := H) :=
(ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi).isProC
have hφHconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_convergesToOne
(ProC := ProC) sourceData hbasis psi.toMonoidHom
have hφHgen :
ProCGroups.Generation.TopologicallyGenerates
(G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsi
exact
separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger
(G := sourceData.carrier) (H := H) ProC psi family hfree htarget hφconv
hdir sourceData.proCGroup.isProCGroup hH hφHconv hφHgenThe separated coordinate equivalence for the chosen finite free pro-\(C\) basis.
theorem freeProC_profKerAbBoundaryAddZCSep_inj_of_continuousMagnus
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
[T1Space
(ZCFreeFoxCoordinates ProC.finiteQuotientClass
(X := ULift.{u} (Fin r)) (H := H))] :
Function.Injective
(profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi)The continuous Magnus hypothesis makes the separated pro-\(C\) kernel-abelianization boundary injective.
Show proof
by
apply
profKerAbBoundaryAddZCSep_inj_of_kernel_le_closedCommutator
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
intro n hnsep
let htarget :=
freeProCClosedGeneratedTarget_proC_of_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
apply
freeProC_closedGeneratedFoxVector_kernel_le_closedCommutator
(H := H) (ProC := ProC) sourceData hbasis psi hpsi htarget n
have hcoord_zero :
freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger
(H := H) (ProC := ProC) sourceData hbasis psi htarget n.1 = 0 := by
have happly :=
congrArg
(freeProCChosenULift_sepCoordinateMap
(H := H) (ProC := ProC) sourceData hbasis psi hpsi) hnsep
rw [freeProCChosenULift_sepCoordinateMap_universal] at happly
simpa [freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger, htarget] using happly
exact hcoord_zeroProof. 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 freeProCChosenULift_closedGenerated_fundamental_formula_stageProj
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
(i : ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom)
(g : sourceData.carrier) :
zcCompletedDifferentialModuleStageProjection
ProC.finiteQuotientClass psi.toMonoidHom i
(presentedCompletedDifferentialFamilyMapProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
(freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC)
(freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i))
(freeProCClosedGeneratedTarget_proC_of_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi)
(freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)))
g)) =
zcCompletedDifferentialModuleStageProjection
ProC.finiteQuotientClass psi.toMonoidHom i
(zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)At each finite stage, the chosen \(U\)-lift closed-generation map satisfies the fundamental formula after projection.
Show proof
by
letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
⟨by
intro Q _ hQ
exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
let family : ULift.{u} (Fin r) → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
let hfree :=
freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
let htarget :=
freeProCClosedGeneratedTarget_proC_of_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
let hφconv :=
freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
have hH : ProC (G := H) :=
(ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi).isProC
have hφHconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_convergesToOne
(ProC := ProC) sourceData hbasis psi.toMonoidHom
have hφHgen :
ProCGroups.Generation.TopologicallyGenerates
(G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsi
simpa [family, hfree, htarget, hφconv] using
closedGenerated_fundamental_formula_stageProj
(G := sourceData.carrier) (H := H) ProC psi family hfree htarget hφconv
hH hφHconv hφHgen i gProof. 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 freeProCChosenULift_closedGen_fundFormula_of_stageProjsSeparate
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
(hsep :
zcCompletedDifferentialModuleStageProjectionsSeparate
ProC.finiteQuotientClass psi.toMonoidHom) :
∀ g : sourceData.carrier,
presentedCompletedDifferentialFamilyMapProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
(freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC)
(freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i))
(freeProCClosedGeneratedTarget_proC_of_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi)
(freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)))
g) =
zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom gSeparation by finite-stage projections implies the closed-generation fundamental formula for the chosen \(U\)-lifts.
Show proof
by
let family : ULift.{u} (Fin r) → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
let hfree :=
freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
let htarget :=
freeProCClosedGeneratedTarget_proC_of_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
let hφconv :=
freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
have hH : ProC (G := H) :=
(ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi).isProC
have hφHconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_convergesToOne
(ProC := ProC) sourceData hbasis psi.toMonoidHom
have hφHgen :
ProCGroups.Generation.TopologicallyGenerates
(G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsi
simpa [family, hfree, htarget, hφconv] using
closedGenerated_fundamental_formula_naturalTopology_of_separating
(G := sourceData.carrier) (H := H) ProC psi family hfree htarget hφconv
hsep hH hφHconv hφHgenProof. 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 freeProCChosenULift_closedGen_fundFormula_of_relSubmoduleClosed
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
(hclosed :
zcCompletedDifferentialModuleRelationSubmoduleClosed
ProC.finiteQuotientClass psi.toMonoidHom) :
∀ g : sourceData.carrier,
presentedCompletedDifferentialFamilyMapProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
(freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC)
(freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i))
(freeProCClosedGeneratedTarget_proC_of_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi)
(freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)))
g) =
zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom gClosedness of the completed relation submodule implies the closed-generation fundamental formula for the chosen \(U\)-lifts.
Show proof
by
exact
freeProCChosenULift_closedGen_fundFormula_of_stageProjsSeparate
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
(freeProC_zcDiffModuleStageProjsSeparate_of_relSubmoduleClosed
(H := H) (ProC := ProC) sourceData psi hclosed)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 freeProC_zcDiffModuleRelSubmoduleClosed_of_closedGen_fundFormula
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
(hfundamental :
let htarget :=
freeProCClosedGeneratedTarget_proC_of_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
∀ g : sourceData.carrier,
presentedCompletedDifferentialFamilyMapProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
(freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC)
(freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i))
htarget
(freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)))
g) =
zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) :
zcCompletedDifferentialModuleRelationSubmoduleClosed
ProC.finiteQuotientClass psi.toMonoidHomThe closed-generation fundamental formula implies closedness of the completed differential-module relation submodule.
Show proof
by
letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
⟨by
intro Q _ hQ
exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
let family : ULift.{u} (Fin r) → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
let hfree :=
freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
let htarget :=
freeProCClosedGeneratedTarget_proC_of_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
let hφconv :=
freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
have hHProCGroup : ProCGroup ProC H :=
ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi
have hH : ProC (G := H) :=
hHProCGroup.isProC
have hφHconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_convergesToOne
(ProC := ProC) sourceData hbasis psi.toMonoidHom
have hφHgen :
ProCGroups.Generation.TopologicallyGenerates
(G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsi
exact
zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_isProCGroup_of_fundFormula
(G := sourceData.carrier) (H := H) ProC psi family hfree htarget hφconv
sourceData.proCGroup.isProCGroup hH hφHconv hφHgen
(by simpa [family, hfree, htarget, hφconv] using hfundamental)
/-- For the chosen finite free pro-`C` basis, relation-submodule closedness is exactly
injectivity of the closed-generated coordinate map.
This is the free-source form of Morishita's coordinate theorem before the final augmentation-ideal
or relation-reflection argument: after this point the only missing theorem is the unconditional
injectivity of this coordinate map. -/
-- Do not derive coordinate injectivity from the fundamental formula; both are downstream of closedness.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 freeProC_zcDiffModuleRelSubmoduleClosed_iff_closedGenCoord_inj
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi) :
zcCompletedDifferentialModuleRelationSubmoduleClosed
ProC.finiteQuotientClass psi.toMonoidHom ↔
Function.Injective
(freeProCChosenULift_closedGeneratedCoordinateMap
(H := H) (ProC := ProC) sourceData hbasis psi hpsi)For the chosen finite free pro-\(C\) basis, relation-submodule closedness is equivalent to injectivity of the closed-generated coordinate map.
Show proof
by
letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
⟨by
intro Q _ hQ
exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
letI :
Nonempty
(ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :=
⟨zcCompletedDifferentialModuleComapIndex
(C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi
((ProCGroups.Completion.ProCIntegerIndex.terminal
(C := ProC.finiteQuotientClass) inferInstance),
zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩
have hdir :
Directed (· ≤ ·)
(id :
ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom →
ZCCompletedDifferentialModuleIndex
ProC.finiteQuotientClass psi.toMonoidHom) :=
directed_zcCompletedDifferentialModuleIndex
(C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
(ProCGroupPredicate.finiteQuotientFormation ProC)
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi
let family : ULift.{u} (Fin r) → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
let hfree :=
freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
let htarget :=
freeProCClosedGeneratedTarget_proC_of_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
let hφconv :=
freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
have hH : ProC (G := H) :=
(ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi).isProC
have hφHconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_convergesToOne
(ProC := ProC) sourceData hbasis psi.toMonoidHom
have hφHgen :
ProCGroups.Generation.TopologicallyGenerates
(G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsi
have hiff :=
zcDiffModuleRelSubmoduleClosed_iff_closedGenCoord_inj_of_isProCGroup
(G := sourceData.carrier) (H := H) ProC psi family hfree htarget hφconv
hdir sourceData.proCGroup.isProCGroup hH hφHconv hφHgen
simpa [freeProCChosenULift_closedGeneratedCoordinateMap, family, hfree, htarget, hφconv,
hH, hφHconv, hφHgen] using hiffProof. 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 freeProC_zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_inj
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
(hcoord_inj :
Function.Injective
(freeProCChosenULift_closedGeneratedCoordinateMap
(H := H) (ProC := ProC) sourceData hbasis psi hpsi)) :
zcCompletedDifferentialModuleRelationSubmoduleClosed
ProC.finiteQuotientClass psi.toMonoidHomInjectivity of the closed-generated coordinate map implies closedness of the completed differential-module relation submodule.
Show proof
(freeProC_zcDiffModuleRelSubmoduleClosed_iff_closedGenCoord_inj
(H := H) (ProC := ProC) sourceData hbasis psi hpsi).2 hcoord_injProof. 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 freeProCChosenULift_closedGen_fundFormula_of_closedGenCoord_inj
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
(hcoord_inj :
Function.Injective
(freeProCChosenULift_closedGeneratedCoordinateMap
(H := H) (ProC := ProC) sourceData hbasis psi hpsi)) :
let htargetInjectivity of the closed-generated coordinate map implies the closed-generated fundamental formula for the chosen \(U\)-lifts.
Show proof
freeProCClosedGeneratedTarget_proC_of_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
∀ g : sourceData.carrier,
presentedCompletedDifferentialFamilyMapProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
(freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC)
(freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i))
htarget
(freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)))
g) =
zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g := by
exact
freeProCChosenULift_closedGen_fundFormula_of_relSubmoduleClosed
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
(freeProC_zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_inj
(H := H) (ProC := ProC) sourceData hbasis psi hpsi hcoord_inj)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. 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 freeProC_completedBoundaryKillsTopCommZC_of_closedGen_and_psi_surj
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
(htarget :
ProC
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)) : Subgroup
(ZCCompletedFoxSemidirect
ProC.finiteQuotientClass (ULift.{u} (Fin r)) H))))
(hbasis_A :
IsPresentedCompletedDifferentialFamilyBasisProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)) :
CompletedBoundaryKillsTopologicalCommutatorProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psiUnder closed generation and surjectivity of \(\psi\), the completed boundary kills the topological commutator subgroup.
Show proof
by
let family : ULift.{u} (Fin r) → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
let hfree :=
freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
let hφconv :=
freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
have hHProCGroup : ProCGroup ProC H :=
ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi
have hH : ProC (G := H) :=
hHProCGroup.isProC
have hφHconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_convergesToOne
(ProC := ProC) sourceData hbasis psi.toMonoidHom
have hφHgen :
ProCGroups.Generation.TopologicallyGenerates
(G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsi
have hleft_graph_eq :
∀ g : sourceData.carrier,
freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC) hfree (fun i : ULift.{u} (Fin r) => psi (family i))
htarget hφconv g =
presentedCompletedDifferentialFamilyCoordinatesProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi family hbasis_A
(zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) := by
exact
freeProCZCCompletedFoxDerivativeVectorViaClosedGen_eq_presentedCoordinates_zcUnivDiff
(G := sourceData.carrier) (H := H) ProC psi family hbasis_A hfree hH htarget hφconv
hφHconv hφHgen
exact
completedBoundaryKillsTopCommZC_of_closedGen_leftGraph
(G := sourceData.carrier) (H := H) ProC psi family hbasis_A hfree htarget hφconv
hleft_graph_eqProof. 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. 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 freeProC_exactAtSepA_of_continuousMagnus_zcBifilteredAllFiniteQuotientStages
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
[T1Space
(ZCFreeFoxCoordinates ProC.finiteQuotientClass
(X := ULift.{u} (Fin r)) (H := H))] :
Function.Exact
(profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi)
(presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi)The Crowell--Blanchfield coordinate formula agrees with the quotient-level construction after passage to the separated or completed module.
Show proof
by
letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
⟨by
intro Q _ hQ
exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
letI : CompactSpace sourceData.carrier :=
ProCGroup.compactSpace ProC sourceData.carrier
let family : ULift.{u} (Fin r) → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
let hfree :=
freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
let htarget :=
freeProCClosedGeneratedTarget_proC_of_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
let hφconv :=
freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
have hHProCGroup : ProCGroup ProC H :=
ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi
have hH : ProC (G := H) :=
hHProCGroup.isProC
have hH_isProC : IsProCGroup ProC.finiteQuotientClass H :=
hHProCGroup.isProCGroup
have hφHconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_convergesToOne
(ProC := ProC) sourceData hbasis psi.toMonoidHom
have hφHgen :
ProCGroups.Generation.TopologicallyGenerates
(G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsi
let φ : ULift.{u} (Fin r) → H := fun i => psi (family i)
let coords :=
freeProCChosenULift_sepCoordinateEquiv
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
let Dcoords : sourceData.carrier →
ZCFreeFoxCoordinates ProC.finiteQuotientClass
(X := ULift.{u} (Fin r)) (H := H) :=
fun g =>
freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC) hfree φ htarget hφconv g
have hright_graph_eq :
freeProCZCCompletedFoxRightHomViaClosedGenerated
(ProC := ProC) hfree φ htarget hφconv =
psi.toMonoidHom := by
exact
freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom
(ProC := ProC) (ULift.{u} (Fin r)) H hfree hH φ htarget hφconv
hφHconv hφHgen psi (by intro i; rfl)
have hcycle_closed :
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass
(ULift.{u} (Fin r)) H)) : Set
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass
(ULift.{u} (Fin r)) H)) := by
exact
freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_zcBiAllStages_coeffGraphRelDeriv
(ProC := ProC) (X := ULift.{u} (Fin r)) (H := H) φ hH_isProC hφHgen
refine
exact_boundaryAddZC_sep_of_coord_cycle_lift
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi family coords ?_ Dcoords ?_ ?_
· rfl
· intro n
simpa [coords, Dcoords, family, hfree, htarget, hφconv, φ] using
(freeProCChosenULift_sepCoordinateMap_universal
(H := H) (ProC := ProC) sourceData hbasis psi hpsi n.1).symm
· intro v hv
have hboundaryMap :
blanchfieldLyndonFiniteFamilyMap
(R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
(fun i : ULift.{u} (Fin r) =>
presentedCompletedDifferentialBoundaryProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi (family i)) =
zcFreeGroupFoxBoundary
ProC.finiteQuotientClass
(FreeGroup.lift φ) :=
finiteBLMap_boundaryZC_eq_zcFreeGroupFoxBoundary
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi family
have hvBoundary :
zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v = 0 := by
simpa [hboundaryMap, φ] using hv
have hy :
({ left := v, right := (1 : H) } :
ZCCompletedFoxSemidirect ProC.finiteQuotientClass
(ULift.{u} (Fin r)) H) ∈
freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ := by
constructor
· rfl
· exact hvBoundary
have hyTarget := hcycle_closed hy
rcases
freeProCZCFoxSemiLiftViaClosedGen_exists_preimage_of_mem_closedGenTarget
(ProC := ProC) hfree φ htarget hφconv hyTarget with
⟨g, hg⟩
have hleft : Dcoords g = v := by
have h := congrArg
(fun z : ZCCompletedFoxSemidirect ProC.finiteQuotientClass
(ULift.{u} (Fin r)) H => z.left) hg
simpa [Dcoords, freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated] using h
have hrightLift :
freeProCZCCompletedFoxRightHomViaClosedGenerated
(ProC := ProC) hfree φ htarget hφconv g = 1 := by
have h := congrArg
(fun z : ZCCompletedFoxSemidirect ProC.finiteQuotientClass
(ULift.{u} (Fin r)) H => z.right) hg
simpa [freeProCZCCompletedFoxRightHomViaClosedGenerated] using h
have hright : psi g = 1 := by
simpa [hright_graph_eq] using hrightLift
exact ⟨⟨g, hright⟩, hleft⟩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 chosenULift_hbasis_A_of_closedGen_fundFormula
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
(htarget :
ProC
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)) : Subgroup
(ZCCompletedFoxSemidirect
ProC.finiteQuotientClass (ULift.{u} (Fin r)) H))))
(hfundamental :
∀ g : sourceData.carrier,
presentedCompletedDifferentialFamilyMapProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
(freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC)
(freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i))
htarget
(freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)))
g) =
zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) :
IsPresentedCompletedDifferentialFamilyBasisProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)The closed-generation fundamental formula supplies the required chosen-\(U\)-lift basis data for \(A\).
Show proof
by
let family : ULift.{u} (Fin r) → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
let hfree :=
freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
let hφconv :=
freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
have hHProCGroup : ProCGroup ProC H :=
ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi
have hH : ProC (G := H) :=
hHProCGroup.isProC
have hφHconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_convergesToOne
(ProC := ProC) sourceData hbasis psi.toMonoidHom
have hφHgen :
ProCGroups.Generation.TopologicallyGenerates
(G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsi
exact
isPresentedCompletedDifferentialFamilyBasisZC_of_closedGen_fundFormula
(G := sourceData.carrier) (H := H) ProC psi family hfree
(by simpa [family] using htarget) hφconv hH hφHconv hφHgen
(by simpa [family, hfree, hφconv] using hfundamental)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 chosenULift_hbasis_A_of_closedGen_fundFormula_continuous
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
[TopologicalSpace (ZCCompletedDifferentialModule
ProC.finiteQuotientClass psi.toMonoidHom)]
[T2Space (ZCCompletedDifferentialModule
ProC.finiteQuotientClass psi.toMonoidHom)]
(htarget :
ProC
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)) : Subgroup
(ZCCompletedFoxSemidirect
ProC.finiteQuotientClass (ULift.{u} (Fin r)) H))))
(hmodule_continuous :
Continuous
(fun g : sourceData.carrier =>
presentedCompletedDifferentialFamilyMapProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
(freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC)
(freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i))
htarget
(freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)))
g)))
(huniv_continuous :
Continuous
(fun g : sourceData.carrier =>
zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)) :
IsPresentedCompletedDifferentialFamilyBasisProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)The Crowell--Blanchfield coordinate formula agrees with the quotient-level construction after passage to the separated or completed module.
Show proof
by
let family : ULift.{u} (Fin r) → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
let hfree :=
freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
let hφconv :=
freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
have hHProCGroup : ProCGroup ProC H :=
ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi
have hH : ProC (G := H) :=
hHProCGroup.isProC
have hφHconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_convergesToOne
(ProC := ProC) sourceData hbasis psi.toMonoidHom
have hφHgen :
ProCGroups.Generation.TopologicallyGenerates
(G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
simpa [family] using
freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
(ProC := ProC) sourceData hbasis psi hpsi
have hfundamental :
∀ g : sourceData.carrier,
presentedCompletedDifferentialFamilyMapProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi family
(freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC) hfree (fun i : ULift.{u} (Fin r) => psi (family i))
(by simpa [family] using htarget) hφconv g) =
zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g :=
closedGenerated_fundamental_formula_of_continuous
(G := sourceData.carrier) (H := H) ProC psi family hfree
(by simpa [family] using htarget) hφconv hH hφHconv hφHgen
(by simpa [family, hfree, hφconv] using hmodule_continuous)
(by simpa using huniv_continuous)
exact
chosenULift_hbasis_A_of_closedGen_fundFormula
(H := H) (ProC := ProC) sourceData hbasis psi hpsi htarget
(by simpa [family, hfree, hφconv] using hfundamental)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 freeProCChosenULiftFamilyOfBasisCard_hbasis_A_of_relationSubmoduleClosed
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
(hclosed :
zcCompletedDifferentialModuleRelationSubmoduleClosed
ProC.finiteQuotientClass psi.toMonoidHom) :
IsPresentedCompletedDifferentialFamilyBasisProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)Closedness of the completed relation submodule gives the required basis-indexed chosen-\(U\)-lift family in the Crowell module \(A\).
Show proof
by
let htarget :=
freeProCClosedGeneratedTarget_proC_of_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
have hfundamental :
∀ g : sourceData.carrier,
presentedCompletedDifferentialFamilyMapProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
(freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC)
(freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i))
htarget
(freeProCZCFoxSemiClosedGenGenerator_convergesToOne_of_finite
(ProC := ProC)
(fun i : ULift.{u} (Fin r) =>
psi (freeProCChosenULiftFamilyOfBasisCard
(ProC := ProC) sourceData hbasis i)))
g) =
zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g := by
simpa [htarget] using
freeProCChosenULift_closedGen_fundFormula_of_relSubmoduleClosed
(H := H) (ProC := ProC) sourceData hbasis psi hpsi hclosed
exact
chosenULift_hbasis_A_of_closedGen_fundFormula
(H := H) (ProC := ProC) sourceData hbasis psi hpsi htarget hfundamentalProof. 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 freeProCChosenULiftFamilyOfBasisCard_hbasis_A_of_closedGenCoord_inj
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi)
(hcoord_inj :
Function.Injective
(freeProCChosenULift_closedGeneratedCoordinateMap
(H := H) (ProC := ProC) sourceData hbasis psi hpsi)) :
IsPresentedCompletedDifferentialFamilyBasisProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)Injectivity of the closed-generated coordinate map gives the finite \(A_{\psi}(C)\)-basis theorem for the chosen lifted basis family.
Show proof
freeProCChosenULiftFamilyOfBasisCard_hbasis_A_of_relationSubmoduleClosed
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
(freeProC_zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_inj
(H := H) (ProC := ProC) sourceData hbasis psi hpsi hcoord_inj)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. 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 freeProC_presentedSepCrowellZC_of_continuousMagnus_zcBiAllStages_of_psi_surj
[T2Space H]
[ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
[ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
[ProC.DeterminedByFiniteQuotients]
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hpsi : Function.Surjective psi) :
Function.Injective
(profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi) ∧
Function.Exact
(profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi)
(presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi) ∧
Function.Exact
(presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi)
(zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H) ∧
Function.Surjective
(zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H)The all-stage continuous Magnus hypothesis and surjectivity of \(\psi\) give the separated Crowell exact sequence over \(\mathbb{Z}_C\).
Show proof
by
exact
⟨freeProC_profKerAbBoundaryAddZCSep_inj_of_continuousMagnus
(H := H) (ProC := ProC) sourceData hbasis psi hpsi,
freeProC_exactAtSepA_of_continuousMagnus_zcBifilteredAllFiniteQuotientStages
(H := H) (ProC := ProC) sourceData hbasis psi hpsi,
freeProC_presentedSeparatedCrowellGroupAlgebraExactProCInteger_of_psi_surjective
(H := H) (ProC := ProC) sourceData hbasis psi hpsi,
zcCompletedGroupAlgebraAugmentation_surjective
(C := ProC.finiteQuotientClass) (H := H)⟩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.
□