CrowellExactSequence.Discrete.MainTheorem
This module develops the Crowell--Blanchfield--Lyndon exact sequence and its completed coordinate forms.
theorem discreteCrowellExactSequence
{G : Type} [Group G]
(psi : MonoidHom G H) (hpsi : Function.Surjective psi) :
letIThe discrete Crowell exact sequence for a surjective group homomorphism, packaged as the full four-term exact sequence \((\ker \psi)^{\mathrm{ab}} \to A_{\psi} \to \mathbb{Z}[H] \to \mathbb{Z}\).
Show proof
kernelAbelianizationModuleOfSurjective psi hpsi
IsFourTermExactSequence
(kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi)
(toGroupRing psi)
(augmentation H) := by
letI := kernelAbelianizationModuleOfSurjective psi hpsi
exact Morishita2024.crowellExactSequence_of_surjective (H := H) 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. 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 discreteBlanchfieldLyndonExactSequence
(r : Nat) (psi : MonoidHom (FreeGroup (Fin r)) H) (hpsi : Function.Surjective psi) :
letIThe discrete Blanchfield--Lyndon coordinate exact sequence for a finite free presentation, packaged as the full four-term exact sequence.
Show proof
kernelAbelianizationModuleOfSurjective psi hpsi
IsFourTermExactSequence
(FoxCalculus.freeGroupPresentationRelativeDerivativeHeadMap (H := H) r psi hpsi)
(FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap (H := H) r psi)
(augmentation H) := by
letI := kernelAbelianizationModuleOfSurjective psi hpsi
exact Morishita2024.freeGroupPresentation_blanchfieldLyndonExactSequence (H := H) r 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. 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.
□