CrowellExactSequence.Profinite.BlanchfieldLyndon
This module develops the Crowell--Blanchfield--Lyndon exact sequence and its completed coordinate forms.
def freeProCBlanchfieldLyndonBoundaryProCInteger
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hbasis_A :
IsPresentedCompletedDifferentialFamilyBasisProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis))
(hwell_dN :
CompletedBoundaryKillsTopologicalCommutatorProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi) :
ProCKernelAbelianizationAdd ProC psi →
Fin r → ZCCompletedGroupAlgebra ProC.finiteQuotientClass H :=
fun x =>
presentedCompletedDifferentialFamilyCoordinatesProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis) hbasis_A
(profiniteKernelAbelianizationBoundaryAddProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi hwell_dN x)The first pro-\(C\) Blanchfield--Lyndon boundary map reads the kernel-abelianization boundary in the chosen \(A_{\psi}(C)\) coordinates.
theorem freeProC_exactAtA_iff_blanchfieldLyndonExactAtCoordinatesProCInteger
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hbasis_A :
IsPresentedCompletedDifferentialFamilyBasisProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis))
(hwell_dN :
CompletedBoundaryKillsTopologicalCommutatorProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi) :
Function.Exact
(profiniteKernelAbelianizationBoundaryAddProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi hwell_dN)
(presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi) ↔
Function.Exact
(freeProCBlanchfieldLyndonBoundaryProCInteger
(H := H) (ProC := ProC) sourceData hbasis psi hbasis_A hwell_dN)
(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)))Exactness at the \(A\)-term is equivalent to the coordinatewise Blanchfield--Lyndon exactness condition.
Show proof
by
let family : Fin r → sourceData.carrier :=
freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis
let dN :=
profiniteKernelAbelianizationBoundaryAddProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi hwell_dN
let coords :=
presentedCompletedDifferentialFamilyCoordinatesProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi family hbasis_A
let delta :=
presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
let blDelta :=
blanchfieldLyndonFiniteFamilyMap
(R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
(fun i : Fin r =>
presentedCompletedDifferentialBoundaryProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi (family i))
have hblDelta_comp : delta.comp coords.symm.toLinearMap = blDelta := by
rw [presentedCompletedDifferentialFamilyCoordinatesProCInteger_symm_toLinearMap]
exact
presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger_comp_familyMap
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi family
have hblDelta_apply (y) : blDelta y = delta (coords.symm y) := by
have h := congrArg (fun f => f y) hblDelta_comp
simpa [LinearMap.comp_apply] using h.symm
change
Function.Exact dN delta ↔
Function.Exact (fun x => coords (dN x)) blDelta
constructor
· intro hexact_A y
constructor
· intro hy
have hy_delta : delta (coords.symm y) = 0 := by
simpa [hblDelta_apply y] using hy
rcases (hexact_A (coords.symm y)).1 hy_delta with ⟨x, hx⟩
exact ⟨x, by simpa using congrArg coords hx⟩
· rintro ⟨x, rfl⟩
have hker : delta (dN x) = 0 :=
(hexact_A (dN x)).2 ⟨x, rfl⟩
calc
blDelta (coords (dN x)) = delta (coords.symm (coords (dN x))) :=
hblDelta_apply (coords (dN x))
_ = delta (dN x) := by rw [coords.symm_apply_apply]
_ = 0 := hker
· intro hexact_BL y
constructor
· intro hy
have hy_bl : blDelta (coords y) = 0 := by
calc
blDelta (coords y) = delta (coords.symm (coords y)) :=
hblDelta_apply (coords y)
_ = delta y := by rw [coords.symm_apply_apply]
_ = 0 := hy
rcases (hexact_BL (coords y)).1 hy_bl with ⟨x, hx⟩
refine ⟨x, ?_⟩
apply coords.injective
simpa using hx
· rintro ⟨x, rfl⟩
have hbl : blDelta (coords (dN x)) = 0 :=
(hexact_BL (coords (dN x))).2 ⟨x, rfl⟩
calc
delta (dN x) = delta (coords.symm (coords (dN x))) := by
rw [coords.symm_apply_apply]
_ = blDelta (coords (dN x)) := by
rw [hblDelta_apply]
_ = 0 := hblProof. 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. Linear equivalences preserve exactness because composing with an isomorphism does not change kernels or images after transporting them along the equivalence. 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 freeProCSeparatedBlanchfieldLyndonBoundaryProCInteger
[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) :
ProCKernelAbelianizationAdd ProC psi →
ZCFreeFoxCoordinates ProC.finiteQuotientClass
(X := ULift.{u} (Fin r)) (H := H) :=
fun x =>
freeProCChosenULift_sepCoordinateEquiv
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
(profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi x)The separated pro-\(C\) Blanchfield--Lyndon boundary map reads the separated kernel-abelianization boundary in the chosen coordinates.
theorem freeProC_exactAtSepA_iff_blanchfieldLyndonExactAtCoordinatesProCInteger
[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.Exact
(profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi)
(presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi) ↔
Function.Exact
(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)))Exactness at the separated Crowell module is equivalent to Blanchfield--Lyndon exactness in pro-\(C\)-integer coordinates.
Show proof
by
let family : ULift.{u} (Fin r) → sourceData.carrier :=
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
let dN :=
profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
let coords :=
freeProCChosenULift_sepCoordinateEquiv
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
let delta :=
presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi
let blDelta :=
blanchfieldLyndonFiniteFamilyMap
(R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
(fun i : ULift.{u} (Fin r) =>
presentedCompletedDifferentialBoundaryProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi (family i))
have hcoords_symm :
coords.symm.toLinearMap =
freeProCChosenULift_sepFamilyMap
(H := H) (ProC := ProC) sourceData hbasis psi := by
rfl
have hblDelta_comp : delta.comp coords.symm.toLinearMap = blDelta := by
rw [hcoords_symm]
exact
presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger_comp_familyMap
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi family
have hblDelta_apply (y) : blDelta y = delta (coords.symm y) := by
have h := congrArg (fun f => f y) hblDelta_comp
simpa [LinearMap.comp_apply] using h.symm
change
Function.Exact dN delta ↔
Function.Exact (fun x => coords (dN x)) blDelta
constructor
· intro hexact_A y
constructor
· intro hy
have hy_delta : delta (coords.symm y) = 0 := by
simpa [hblDelta_apply y] using hy
rcases (hexact_A (coords.symm y)).1 hy_delta with ⟨x, hx⟩
exact ⟨x, by simpa using congrArg coords hx⟩
· rintro ⟨x, rfl⟩
have hker : delta (dN x) = 0 :=
(hexact_A (dN x)).2 ⟨x, rfl⟩
calc
blDelta (coords (dN x)) = delta (coords.symm (coords (dN x))) :=
hblDelta_apply (coords (dN x))
_ = delta (dN x) := by rw [coords.symm_apply_apply]
_ = 0 := hker
· intro hexact_BL y
constructor
· intro hy
have hy_bl : blDelta (coords y) = 0 := by
calc
blDelta (coords y) = delta (coords.symm (coords y)) :=
hblDelta_apply (coords y)
_ = delta y := by rw [coords.symm_apply_apply]
_ = 0 := hy
rcases (hexact_BL (coords y)).1 hy_bl with ⟨x, hx⟩
refine ⟨x, ?_⟩
apply coords.injective
simpa using hx
· rintro ⟨x, rfl⟩
have hbl : blDelta (coords (dN x)) = 0 :=
(hexact_BL (coords (dN x))).2 ⟨x, rfl⟩
calc
delta (dN x) = delta (coords.symm (coords (dN x))) := by
rw [coords.symm_apply_apply]
_ = blDelta (coords (dN x)) := (hblDelta_apply (coords (dN x))).symm
_ = 0 := hblProof. 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.
□theorem freeProC_presentedBlanchfieldLyndonGAExactZC_of_psi_surj
[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
(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)For a surjective \(\psi\), the presented Blanchfield--Lyndon group-algebra sequence over \(\mathbb{Z}_C\) 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
simpa [family] using
exact_blanchfieldLyndonFiniteFamilyMap_boundary_family_of_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_presentedSepBlanchfieldLyndonGAExactZC_of_psi_surj
[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
(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)For a surjective \(\psi\), the separated presented Blanchfield--Lyndon group-algebra sequence over \(\mathbb{Z}_C\) is exact.
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
have htargetGen :
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] using
exact_blanchfieldLyndonFiniteFamilyMap_boundary_family_of_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_presentedSepBLZC_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) :
IsBlanchfieldLyndonExactSequence
(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 all-stage continuous Magnus hypothesis and surjectivity of \(\psi\) give the separated Blanchfield--Lyndon exact sequence over \(\mathbb{Z}_C\).
Show proof
by
let dN :=
profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
let coords :=
freeProCChosenULift_sepCoordinateEquiv
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
let blDelta :=
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))
have hinj_dN :
Function.Injective dN :=
freeProC_profKerAbBoundaryAddZCSep_inj_of_continuousMagnus
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
have hexact_A :
Function.Exact dN
(presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi) :=
freeProC_exactAtSepA_of_continuousMagnus_zcBifilteredAllFiniteQuotientStages
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
have hexact_BL_A :
Function.Exact
(fun x : ProCKernelAbelianizationAdd ProC psi => coords (dN x))
blDelta :=
(freeProC_exactAtSepA_iff_blanchfieldLyndonExactAtCoordinatesProCInteger
(H := H) (ProC := ProC) sourceData hbasis psi hpsi).1 hexact_A
change
IsBlanchfieldLyndonExactSequence
(fun x : ProCKernelAbelianizationAdd ProC psi => coords (dN x)) blDelta
(zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H)
refine ⟨?_, hexact_BL_A, ?_, ?_⟩
· intro x y hxy
exact hinj_dN (coords.injective hxy)
· exact
freeProC_presentedSepBlanchfieldLyndonGAExactZC_of_psi_surj
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
· exact
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.
□def finULiftEquiv (r : Nat) : Fin r ≃ ULift.{u} (Fin r) where
toFun i := ULift.up i
invFun i := i.down
left_inv := by
intro i
rfl
right_inv := by
intro i
cases i
rflThe finite-index lift comparison in the Crowell exact sequence is an equivalence, with inverse given by the reverse comparison map.
def freeProCSeparatedBlanchfieldLyndonBoundaryFinProCInteger
[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) :
ProCKernelAbelianizationAdd ProC psi →
Fin r → ZCCompletedGroupAlgebra ProC.finiteQuotientClass H :=
let e : Fin r ≃ ULift.{u} (Fin r) := finULiftEquiv r
fun x =>
(piReindexLinearEquiv
(R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) e).symm
(freeProCSeparatedBlanchfieldLyndonBoundaryProCInteger
(H := H) (ProC := ProC) sourceData hbasis psi hpsi x)The finite-index display reindexes the separated Blanchfield--Lyndon boundary map from \(\mathrm{ULift}(\mathrm{Fin}\, r)\) to \(\mathrm{Fin}\, r\).
theorem freeProC_exactAtSepA_iff_blanchfieldLyndonExactAtFinCoordinatesProCInteger
[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.Exact
(profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi)
(presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi) ↔
Function.Exact
(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)))Exactness at the separated Crowell module is equivalent to finite-coordinate Blanchfield--Lyndon exactness over the pro-\(C\) integers.
Show proof
by
let e : Fin r ≃ ULift.{u} (Fin r) := finULiftEquiv r
let L :
(Fin r → ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) ≃ₗ[
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
(ULift.{u} (Fin r) →
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) :=
piReindexLinearEquiv
(R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) e
let blULift :=
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))
let blFin :=
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))
have hblFin :
blFin = blULift.comp L.toLinearMap := by
simpa [blFin, blULift, L, e, finULiftEquiv, freeProCChosenULiftFamilyOfBasisCard] using
(finiteFamilyLinearMap_reindex
(R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
e
(fun i : ULift.{u} (Fin r) =>
presentedCompletedDifferentialBoundaryProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
((freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis) i)))
have hULiftIff :=
freeProC_exactAtSepA_iff_blanchfieldLyndonExactAtCoordinatesProCInteger
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
have htransport :
Function.Exact
(fun x : ProCKernelAbelianizationAdd ProC psi =>
L.symm
(freeProCSeparatedBlanchfieldLyndonBoundaryProCInteger
(H := H) (ProC := ProC) sourceData hbasis psi hpsi x))
(fun y : Fin r → ZCCompletedGroupAlgebra ProC.finiteQuotientClass H =>
blULift (L y)) ↔
Function.Exact
(freeProCSeparatedBlanchfieldLyndonBoundaryProCInteger
(H := H) (ProC := ProC) sourceData hbasis psi hpsi)
blULift :=
Function.Exact.linearEquiv_symm_comp_comp_iff
(R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) L
change
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
(fun x : ProCKernelAbelianizationAdd ProC psi =>
L.symm
(freeProCSeparatedBlanchfieldLyndonBoundaryProCInteger
(H := H) (ProC := ProC) sourceData hbasis psi hpsi x))
blFin
rw [hblFin]
exact hULiftIff.trans htransport.symmProof. 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.
□theorem freeProC_presentedSepBLFinZC_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) :
IsBlanchfieldLyndonExactSequence
(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 all-stage continuous Magnus hypothesis and surjectivity of \(\psi\) give the finite-coordinate separated Blanchfield--Lyndon exact sequence over \(\mathbb{Z}_C\).
Show proof
by
let e : Fin r ≃ ULift.{u} (Fin r) := finULiftEquiv r
let L :
(Fin r → ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) ≃ₗ[
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
(ULift.{u} (Fin r) →
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) :=
piReindexLinearEquiv
(R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) e
let dN :=
profiniteKernelAbelianizationBoundaryAddProCIntegerSep
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
let coords :=
freeProCChosenULift_sepCoordinateEquiv
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
have hinj_dN :
Function.Injective dN :=
freeProC_profKerAbBoundaryAddZCSep_inj_of_continuousMagnus
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
have hexact_A :
Function.Exact dN
(presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
(ProCGroupPredicate.finiteQuotientHereditary ProC) psi) :=
freeProC_exactAtSepA_of_continuousMagnus_zcBifilteredAllFiniteQuotientStages
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
refine ⟨?_, ?_, ?_, ?_⟩
· intro x y hxy
change L.symm (coords (dN x)) = L.symm (coords (dN y)) at hxy
exact hinj_dN (coords.injective (L.symm.injective hxy))
· exact
(freeProC_exactAtSepA_iff_blanchfieldLyndonExactAtFinCoordinatesProCInteger
(H := H) (ProC := ProC) sourceData hbasis psi hpsi).1 hexact_A
· exact
freeProC_presentedBlanchfieldLyndonGAExactZC_of_psi_surj
(H := H) (ProC := ProC) sourceData hbasis psi hpsi
· exact
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.
□theorem freeProCChosenULiftFamilyOfBasisCard_hbasis_A_of_chosenFamily_hbasis_A
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hbasis_A :
IsPresentedCompletedDifferentialFamilyBasisProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis)) :
IsPresentedCompletedDifferentialFamilyBasisProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)The universe-lifted chosen family inherits the \(A_{\psi}(C)\)-basis from the finite \(\mathrm{Fin}\, r\) display.
Show proof
by
let e : ULift.{u} (Fin r) ≃ Fin r :=
{ toFun := fun i => i.down
invFun := fun i => ULift.up i
left_inv := by
intro i
cases i
rfl
right_inv := by
intro i
rfl }
change
IsPresentedCompletedDifferentialFamilyBasisProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(fun i : ULift.{u} (Fin r) =>
freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis (e i))
exact
isPresentedCompletedDifferentialFamilyBasisProCInteger_reindex
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi e
(freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
hbasis_AProof. 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.
□theorem freeProCChosenFamilyOfBasisCard_hbasis_A_of_chosenULiftFamily_hbasis_A
(sourceData : FreeProCSourceData ProC)
{r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
(psi : ContinuousMonoidHom sourceData.carrier H)
(hbasis_A :
IsPresentedCompletedDifferentialFamilyBasisProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)) :
IsPresentedCompletedDifferentialFamilyBasisProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis)The finite \(\mathrm{Fin}\, r\) display inherits the \(A_{\psi}(C)\)-basis from the universe-lifted chosen family.
Show proof
by
let e : Fin r ≃ ULift.{u} (Fin r) :=
{ toFun := fun i => ULift.up i
invFun := fun i => i.down
left_inv := by
intro i
rfl
right_inv := by
intro i
cases i
rfl }
change
IsPresentedCompletedDifferentialFamilyBasisProCInteger
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
(fun i : Fin r =>
freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis (e i))
exact
isPresentedCompletedDifferentialFamilyBasisProCInteger_reindex
(G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi e
(freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
hbasis_AProof. 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.
□