CrowellExactSequence.Discrete.BlanchfieldLyndon
This module develops the Crowell--Blanchfield--Lyndon exact sequence and its completed coordinate forms.
import
Imported by
def freeGroupPresentationMiddleCoordinateEquiv
(r : Nat) (ψ : FreeGroup (Fin r) →* H) :
DifferentialModule ψ ≃ₗ[GroupRing H] (Fin r → GroupRing H) :=
(FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearEquivDifferential
(H := H) (Fin r) ψ).symmFor a finite free presentation \(\psi:F_r\to H\), the Crowell middle term is identified with the explicit module of relative Fox coordinates.
def freeGroupPresentationAugmentationGenerators
(r : Nat) (ψ : FreeGroup (Fin r) →* H) : Fin r → GroupRing H :=
fun i => augmentationGenerator H (ψ (FreeGroup.of i))The concrete BL tail generators \(\psi(x_i)-1\) for a finite free presentation.
def freeGroupPresentationBlanchfieldLyndonTailMap
(r : Nat) (ψ : FreeGroup (Fin r) →* H) :
(Fin r → GroupRing H) →ₗ[GroupRing H] GroupRing H :=
blanchfieldLyndonFiniteFamilyMap
(R := GroupRing H)
(freeGroupPresentationAugmentationGenerators (H := H) r ψ)The concrete Blanchfield--Lyndon tail map in relative Fox coordinates.
theorem freeGroupPresentationBlanchfieldLyndonTailMap_apply
(r : Nat) (ψ : FreeGroup (Fin r) →* H) (a : Fin r → GroupRing H) :
freeGroupPresentationBlanchfieldLyndonTailMap (H := H) r ψ a =
∑ i : Fin r, a i * augmentationGenerator H (ψ (FreeGroup.of i))The discrete Blanchfield--Lyndon tail map is evaluated on the canonical generators and then extended linearly to the coordinate module.
Show proof
by
rw [freeGroupPresentationBlanchfieldLyndonTailMap, blanchfieldLyndonFiniteFamilyMap_apply]
simp only [freeGroupPresentationAugmentationGenerators, augmentationGenerator_eq_groupRingBoundary,
smul_eq_mul]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. 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.
□def freeGroupPresentationRelativeDerivativeHeadMap
(r : Nat) (ψ : FreeGroup (Fin r) →* H) (hψ : Function.Surjective ψ) :
letI := kernelAbelianizationModuleOfSurjective ψ hψ
KernelAbelianizationAdd ψ →ₗ[GroupRing H] (Fin r → GroupRing H) := by
letI := kernelAbelianizationModuleOfSurjective ψ hψ
exact
(freeGroupPresentationMiddleCoordinateEquiv (H := H) r ψ).toLinearMap.comp
(kernelAbelianizationBoundaryLinearOfSurjective ψ hψ)The concrete BL head map: the Crowell head map written in relative Fox coordinates.
theorem freeGroupPresentationRelativeDerivativeHeadMap_of
(r : Nat) (ψ : FreeGroup (Fin r) →* H) (hψ : Function.Surjective ψ)
(n : ψ.ker) :
letIOn a kernel element, the concrete BL head map is the relative Fox derivative vector.
Show proof
kernelAbelianizationModuleOfSurjective ψ hψ
freeGroupPresentationRelativeDerivativeHeadMap (H := H) r ψ hψ
(Additive.ofMul (Abelianization.of n)) =
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := H) (Fin r) ψ n.1 := by
letI := kernelAbelianizationModuleOfSurjective ψ hψ
change
(freeGroupPresentationMiddleCoordinateEquiv (H := H) r ψ).toLinearMap
(kernelAbelianizationBoundaryLinearOfSurjective ψ hψ
(Additive.ofMul (Abelianization.of n))) =
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := H) (Fin r) ψ n.1
rw [kernelAbelianizationBoundaryLinearOfSurjective_of]
change
FoxDifferential.FoxCalculus.relativeDifferentialToFreeFoxCoordinates
(H := H) (Fin r) ψ (universalDifferential ψ n.1) =
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative (H := H) (Fin r) ψ n.1
exact FoxDifferential.FoxCalculus.relativeDifferentialToFreeFoxCoordinates_d
(H := H) (Fin r) ψ n.1Proof. 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 crowellExactSequence_of_surjective
{G : Type} [Group G]
(psi : MonoidHom G H) (hpsi : Function.Surjective psi) :
letIDiscrete Crowell exact sequence for a surjective group homomorphism.
Show proof
kernelAbelianizationModuleOfSurjective psi hpsi
Function.Injective
(kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi) ∧
Function.Exact
(kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi)
(toGroupRing psi) ∧
Function.Exact (toGroupRing psi) (augmentation H) ∧
Function.Surjective (augmentation H) := by
letI := kernelAbelianizationModuleOfSurjective psi hpsi
refine ⟨?_, ?_, exact_toGroupRing_augmentation (H := H) psi hpsi,
augmentation_surjective (H := H)⟩
· exact FoxDifferential.kernelAbelianizationBoundaryLinearOfSurjective_injective
(H := H) (ψ := psi) hpsi
· exact exact_kernelAbelianizationBoundaryLinearOfSurjective_toGroupRing (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 freeGroupPresentation_blanchfieldLyndonExactSequence
(r : Nat) (psi : MonoidHom (FreeGroup (Fin r)) H) (hpsi : Function.Surjective psi) :
letIThe discrete Blanchfield--Lyndon exact sequence for a surjective finite free presentation.
Show proof
kernelAbelianizationModuleOfSurjective psi hpsi
Function.Injective
(FoxCalculus.freeGroupPresentationRelativeDerivativeHeadMap (H := H) r psi hpsi) ∧
Function.Exact
(FoxCalculus.freeGroupPresentationRelativeDerivativeHeadMap (H := H) r psi hpsi)
(FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap (H := H) r psi) ∧
Function.Exact
(FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap (H := H) r psi)
(augmentation H) ∧
Function.Surjective (augmentation H) := by
letI := kernelAbelianizationModuleOfSurjective psi hpsi
let e : DifferentialModule psi ≃ₗ[GroupRing H] (Fin r → GroupRing H) :=
FoxCalculus.freeGroupPresentationMiddleCoordinateEquiv (H := H) r psi
let generators : Fin r → GroupRing H :=
FoxCalculus.freeGroupPresentationAugmentationGenerators (H := H) r psi
change
Function.Injective
(e.toLinearMap.comp
(kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi)) ∧
Function.Exact
(e.toLinearMap.comp
(kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi))
(blanchfieldLyndonFiniteFamilyMap (R := GroupRing H) generators) ∧
Function.Exact
(blanchfieldLyndonFiniteFamilyMap (R := GroupRing H) generators)
(augmentation H) ∧
Function.Surjective (augmentation H)
have hfox :
blanchfieldLyndonFiniteFamilyMap (R := GroupRing H) generators =
(toGroupRing psi).comp e.symm.toLinearMap := by
change
FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap (H := H) r psi =
(toGroupRing psi).comp
(FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap
(H := H) (Fin r) psi)
rw [FoxDifferential.FoxCalculus.toGroupRing_comp_relativeFreeFoxCoordinatesLinearMap]
apply LinearMap.ext
intro a
rw [FoxCalculus.freeGroupPresentationBlanchfieldLyndonTailMap_apply]
simp only [augmentationGenerator_eq_groupRingBoundary, FoxCalculus.relativeFreeGroupFoxBoundary,
LinearMap.coe_mk, AddHom.coe_mk]
have htoAug_exact :
Function.Exact
(e.toLinearMap.comp
(kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi))
((toAugmentationIdeal (H := H) psi).comp e.symm.toLinearMap) := by
exact
(LinearEquiv.conj_exact_iff_exact
(f := kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi)
(g := toAugmentationIdeal (H := H) psi) e).2
(exact_kernelAbelianizationBoundaryLinearOfSurjective_toAugmentationIdeal
(H := H) psi hpsi)
have hfree_inj :
Function.Injective
(e.toLinearMap.comp
(kernelAbelianizationBoundaryLinearOfSurjective (H := H) psi hpsi)) := by
intro x y hxy
apply FoxDifferential.kernelAbelianizationBoundaryLinearOfSurjective_injective
(H := H) (ψ := psi) hpsi
apply e.injective
simpa using hxy
refine ⟨hfree_inj, ?_, ?_, augmentation_surjective (H := H)⟩
· rw [hfox, ← subtype_comp_toAugmentationIdeal (H := H) psi]
exact
(Function.Injective.comp_exact_iff_exact
(R := GroupRing H) ((augmentationIdeal H).subtype_injective)).2
htoAug_exact
· rw [hfox]
intro z
constructor
· intro hz
rcases (exact_toGroupRing_augmentation (H := H) psi hpsi z).1 hz with ⟨x, hx⟩
rcases e.symm.surjective x with ⟨y, rfl⟩
exact ⟨y, hx⟩
· rintro ⟨y, rfl⟩
exact augmentation_toGroupRing_eq_zero (H := H) psi (e.symm y)Proof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. Surjectivity is proved by lifting the target coordinates at finite stages and checking that the boundary formula maps the lift to the prescribed target element. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. The augmentation module terms are generated by the chosen basis elements, so equality on those generators determines each coordinate map. The finite-stage exactness assertions are stable under the comparison isomorphisms used to move between separated and unseparated coordinates. Consequently the completed sequence inherits the same exactness calculation. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□