CrowellExactSequence.Profinite.MainTheorem
This module develops the Crowell--Blanchfield--Lyndon exact sequence and its completed coordinate forms.
theorem profiniteSeparatedCrowellExactSequence
[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) :
IsFourTermExactSequence
(profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi)
(presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi)
(zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H)The separated completed Crowell exact sequence over pro-\(C\) integer coefficients, packaged as the full four-term exact sequence \(N^{\mathrm{ab}}(C)\) \(\to\) \(A_{\psi}(C)\) \(\to\) \(\mathbb{Z}_C\llbracket H\rrbracket\) \(\to\) \(\mathbb{Z}_C\).
Show proof
by
exact
freeProC_presentedSepCrowellZC_of_continuousMagnus_zcBiAllStages_of_psi_surj
(H := H) (ProC := ProC) sourceData hbasis psi hpsiProof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem profiniteSeparatedBlanchfieldLyndonExactSequence
[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) :
IsFourTermExactSequence
(freeProCSeparatedBlanchfieldLyndonBoundaryProCInteger
(H := H) (ProC := ProC) sourceData hbasis psi hpsi)
(blanchfieldLyndonFiniteFamilyMap
(R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
(fun i : ULift.{u} (Fin r) =>
presentedCompletedDifferentialBoundaryProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
((freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis) i)))
(zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H)The separated completed Blanchfield--Lyndon exact sequence in the universe-lifted finite coordinate basis, packaged as the full four-term exact sequence.
Show proof
by
exact
freeProC_presentedSepBLZC_of_continuousMagnus_zcBiAllStages_of_psi_surj
(H := H) (ProC := ProC) sourceData hbasis psi hpsiProof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem profiniteSeparatedBlanchfieldLyndonFinExactSequence
[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) :
IsFourTermExactSequence
(freeProCSeparatedBlanchfieldLyndonBoundaryFinProCInteger
(H := H) (ProC := ProC) sourceData hbasis psi hpsi)
(blanchfieldLyndonFiniteFamilyMap
(R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
(fun i : Fin r =>
presentedCompletedDifferentialBoundaryProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
((freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis) i)))
(zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H)The separated completed Blanchfield--Lyndon exact sequence in the concrete \(\operatorname{Fin} r\) coordinate basis, packaged as the full four-term exact sequence.
Show proof
by
exact
freeProC_presentedSepBLFinZC_of_continuousMagnus_zcBiAllStages_of_psi_surj
(H := H) (ProC := ProC) sourceData hbasis psi hpsiProof. 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.
□